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. #4541 merge node all in one with out-of-date MergedEdge; failed for anti-unification. complex implementation.
2. #4521 merge node all in one
3. #4618
4. #4621
5. #4612

MERGED:

1. #4599 update dev
2. #4607 refactor minimize.
3. #4603 Introduce MergedEdge
4. #4617
5. #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. #4642
2. #4645

[Stevengre]

More PRs for this issue:

1. #4499
2. #4647