Node merging to reduce branching for CSE

[ehildenb]

Currently we have the minimize_kcfg routine, which pulls branches up to the top of a the KCFG, and unions edges together. That can improve performance of a transition system by reducing the amount of rules that are injected into the definition, but does not reduce overall branching factor of the function. Here is a link to a diagram for references: https://docs.google.com/drawings/d/1l8i_aUMcL8E7WyxHmk2cqRIY74fQ-yvMdhhdDNcOUp0/edit.

In this diagram, on the left, we've already run the existing KCFG minimization routine which lifts splits to the top and collapses subsequent edges into a single edge. We want to transform it into the diagram on the right, which has pushed the split forward through the edges that come after it. In order to make this transformation preserve information, we make the following adjustments:

• Edges now store a list of tuples (depth, rules, condition), which means that "from source node, given condition, you will reach target node using rules at depth". Current edges in the KCFG just store a single depth, rules, with condition always being #Top.
• When we see a split with edges following, we run a semantics-specific heuristic called merge_nodes(CTerm, CTerm) -> bool on the nodes following the edges. In the case of the diagram, we pairwise run it on all of B, C, D (or do it iteratively for each pair and do smaller mergings). If two nodes (such as B and C) have merge_nodes return True, we do the following:
  • Compute the node B \/ C, which has fresh variables in places where the configurations differ, and the specific assignments to the fresh variables conditioned on the path-condition from teh split node leading to each node. So for example, if E represents the more abstract configuration, we would compute E #And { PC1 #Implies SUBST1 } #And { PC2 #Implies SUBST2 }, where SUBST1 instantiates E to B, and SUBST2 instantiates E to C.
  • Remove nodes A1 and A2 from the graph, and insert new node B \/ C, and insert an edge from A to B \/ C with edge data [(d1, PC1), (d2, PC2)], and insert a split from B \/ C to B and C with conditions PC1, PC2.
  • Repeat procedure with other splits followed by edges, where the user-supplied heuristic fires on the edge targets.

This effectively "pushes splits down", allowing us to reduce the overall branching factor of the proof if we can push them all the way down to the target node of the proof.

[Baltoli]

@palinatolmach can you assign the correct people to this, please?

[palinatolmach]

Will assign to @Stevengre once he's added to the org, thanks @Baltoli!

[Stevengre]

Hi @palinatolmach! Thank you for reminding me about joining the org. I just realized that I had only enabled 2FA on my account a few days ago, but I didn't actually join the organization. Sorry for the delay, and I'll make sure to join the org now.

[Stevengre]

MERGING:

BLOCKED:

1. Merge node #4541 merge node all in one with out-of-date MergedEdge; failed for anti-unification. complex implementation.
2. 4425 node merging to reduce branching for cse #4521 merge node all in one
3. Create split by nodes alternative #4618
4. Merge CTerm #4621
5. Mergeable heuristic in KCFGSemantics for merging node #4612

MERGED:

1. Update .gitignore for MacOS and Pycharm #4599 update dev
2. Move kcfg.minimize into a separate file and class #4607 refactor minimize.
3. MergedEdge class for merging node functionality #4603 Introduce MergedEdge
4. Create Split without CSubst #4617
5. Feature merge node #4628

[Stevengre]

I want to optimize cterms_anti_unify, but I've decided to give up because implementing it for multiple variables is challenging. Keeping it simple helps ensure correctness. If this simple formula would reduce the verification time significantly, I will attempt to optimize it with a correct algorithm.

Thought:

1. construct a tree from top vars (V_0) to bottom vars/tokens (X).
2. given V_n ==K X, replace V_n by V_0
3. lift the constraints
   I'm uncertain whether this algorithm is correct for multiple variables; it needs to be tested on more complex cases.

References:

1. Optimize cterms_anti_unify #4642
2. Optimize cterms_anti_unify #4645

[Stevengre]

More PRs for this issue:

1. Fix match_with_constraint #4499
2. Avoid using merge_nodes by default #4647