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

Issue in kontrol merge-nodes when a simplification only applies in one branch #194

Open
lucasmt opened this issue Nov 20, 2023 · 0 comments

Comments

@lucasmt
Copy link
Contributor

lucasmt commented Nov 20, 2023

kontrol merge-nodes can run into an issue where one branch simplifies an expression and the other doesn't, which causes problems when the two branches are merged. For example, the following happens when trying to use it for the test in PR #162:

  1. One of the side conditions C in our configuration contains the subexpression X modInt 2 ==Int 0.
  2. We branch on the condition X /Int 2 ==Int 0.
  3. In the branch where X /Int 2 ==Int 0, X modInt 2 ==Int 0 can be simplified to X ==Int 0. This turns C into a different side condition C'.
  4. In the branch where X /Int 2 =/=Int 0, the simplification doesn't apply, so it remains as C.
  5. As a result, when we merge the two nodes, instead of getting C #And ( ( X /Int 2 =/=Int 0 andBool B ) orBool ( X /Int 2 ==Int 0 andBool B' ) ) (where B and B' are the constraints that are different between the two branches) we instead get ( ( X /Int 2 =/=Int 0 andBool B andBool C ) orBool ( X /Int 2 ==Int 0 andBool B' andBool C' ) ).

Because this can happen when C is alread a merged expression like (P andBool Q) orBool (notBool P andBool Q'), this can quickly compound over multiple applications of merge-nodes and grow into a large unreadable expression with multiple nested andBool and orBool operators.

What can we do about this?

  • While we can write a lemma to turn ( ( X /Int 2 =/=Int 0 andBool B andBool C ) orBool ( X /Int 2 ==Int 0 andBool B' andBool C' ) ) back into C #And ( ( X /Int 2 =/=Int 0 andBool B ) orBool ( X /Int 2 ==Int 0 andBool B' ) ), this lemma is both very complex and very non-generalizable (we would need to write a different lemma for every case). So this approach doesn't seem ideal.
  • If we were able to specify what we want our merged node to look like, Kontrol should be able to determine that it subsumes both of the individual nodes being merged. This is similar to a loop invariant, and if we implement a way to specify loop invariants as annotations in the Solidity code, that functionality can probably also be used for this.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant