Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Evaluating nested operators might use wrong registers #1560

Open
bugarela opened this issue Dec 10, 2024 · 0 comments
Open

Evaluating nested operators might use wrong registers #1560

bugarela opened this issue Dec 10, 2024 · 0 comments
Assignees
Labels
bug Something isn't working simulator Quint simulator

Comments

@bugarela
Copy link
Collaborator

Found this nasty problem:

module test {
  type Option[a] = Some(a) | None

  pure def findFirst(l, f) = l.foldl(None, (a, i) => if (a == None and f(i)) Some(i) else a)

  pure val foo = [1, 2, 3].findFirst(i => {
    [9, i].findFirst(j => j > 0) == None
  })
}

calling foo in the REPL yields the wrong result:

$ quint -r local/test.qnt::test
Quint REPL 0.22.4
Type ".exit" to exit, or ".help" for more information
>>> foo
Some(9)

it should be impossible for this to result in 9 as it is not part of [1, 2, 3].

The problem happens because the new evaluator's lambda registries has a single registry per parameter, for optimization reasons. However, in this particular case, we need to have two separate instances of these registers, as some of them need to keep the accumulator and element of the outter call and others for the accumulator and element of the inner call.

I can't think of a way to reproduce this without using nested user-defined operators that use folds, so I hope this is not affecting too much. I'll look for a solution ASAP.

@bugarela bugarela self-assigned this Dec 10, 2024
@bugarela bugarela added bug Something isn't working simulator Quint simulator labels Dec 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working simulator Quint simulator
Projects
None yet
Development

No branches or pull requests

1 participant