Make branch extraction more intelligent #652
Conversation
| @@ -377,14 +377,24 @@ def extend( | |||
| if self._check_abstract(node, kcfg): | |||
| return | |||
|
|
|||
| if not kcfg.splits(target_id=node.id): | |||
There was a problem hiding this comment.
This check is no longer relevant?
There was a problem hiding this comment.
Yes, as I understand, it was the check preventing us from branching over and over again. But by simplifying before branching when it tries to branch a second time without having made an execution step, one of the branches will now simplify to bottom and it won't branch.
There was a problem hiding this comment.
What do you mean by 'over and over again', when can that happen? As part of looping code?
src/pyk/kcfg/explore.py
Outdated
|
|
||
| for constraint in branches: | ||
| cterm = node.cterm.add_constraint(constraint) | ||
| cterm, _ = self.cterm_simplify(cterm) |
There was a problem hiding this comment.
...and here use kast_simplify?
There was a problem hiding this comment.
and maybe put the constraint back into the cterm if that's what's easier for branch later on...
There was a problem hiding this comment.
Using kast_simplify. I removed for now the adding of the already simplified term as the new branch nodes.
There was a problem hiding this comment.
Why kast_simplify instead of cterm_simplify?
There was a problem hiding this comment.
I guess the argument is performance. Have we checked on KEVM that it solves the problems we had there?
There was a problem hiding this comment.
I don't myself know if it makes an appreciable difference to performance, but if it doesn't make any difference to have the configuration in there, it's just simpler.
I have checked and it does solve my issue with repeated branching. I'm not sure if there was a specific problem that prompted #632 or just a general observation. @PetarMax, do you have a KEVM example where this was causing problems that I could test this against?
…everification/pyk into noah/extract-branches-fix
| if len(branches) > 1: | ||
| kcfg.split_on_constraints(node.id, branches) | ||
| _LOGGER.info( | ||
| f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' | ||
| ) | ||
| return |
There was a problem hiding this comment.
In this case, will the unsimplified constraint be added to the configuration or will the Haskell backend simplify it? The problem that we had was that the booster was not able to simplify a given constraint. Perhaps just checking for #Bottom will be enough.
I will try to run this on an appropriate test from the engagement in question.
There was a problem hiding this comment.
The unsimplified contsraint will be added, but that should be enough to make it only take the one branch on subsequent execute call.
There was a problem hiding this comment.
If the backend can't simplify a constraint, then it needs more lemmas to do so, or is a bug in the backend.
Closes #632. Before introducing a branch, simplify each of the would-be new nodes and see if they simplify to bottom If there are more than 1 non-bottom node, add all these simplified nodes to the CFG, creating a split/branch. If not, simply continue straight-line execution. This should reduce eliminate some infeasible branching by simplifying earlier in the process. Also should eliminate repeated branching encountered in runtimeverification/evm-semantics#2065 when creating new proofs from branches. --------- Co-authored-by: devops <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
Closes #632. Before introducing a branch, simplify each of the would-be new nodes and see if they simplify to bottom If there are more than 1 non-bottom node, add all these simplified nodes to the CFG, creating a split/branch. If not, simply continue straight-line execution. This should reduce eliminate some infeasible branching by simplifying earlier in the process. Also should eliminate repeated branching encountered in runtimeverification/evm-semantics#2065 when creating new proofs from branches. --------- Co-authored-by: devops <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
Closes #632. Before introducing a branch, simplify each of the would-be new nodes and see if they simplify to bottom If there are more than 1 non-bottom node, add all these simplified nodes to the CFG, creating a split/branch. If not, simply continue straight-line execution. This should reduce eliminate some infeasible branching by simplifying earlier in the process. Also should eliminate repeated branching encountered in runtimeverification/evm-semantics#2065 when creating new proofs from branches. --------- Co-authored-by: devops <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
Closes #632. Before introducing a branch, simplify each of the would-be new nodes and see if they simplify to bottom If there are more than 1 non-bottom node, add all these simplified nodes to the CFG, creating a split/branch. If not, simply continue straight-line execution. This should reduce eliminate some infeasible branching by simplifying earlier in the process. Also should eliminate repeated branching encountered in runtimeverification/evm-semantics#2065 when creating new proofs from branches. --------- Co-authored-by: devops <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
Closes #632.
Before introducing a branch, simplify each of the would-be new nodes and see if they simplify to bottom
If there are more than 1 non-bottom node, add all these simplified nodes to the CFG, creating a split/branch. If not, simply continue straight-line execution.
This should reduce eliminate some infeasible branching by simplifying earlier in the process.
Also should eliminate repeated branching encountered in runtimeverification/evm-semantics#2065 when creating new proofs from branches.