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.
Currently we have the
minimize_kcfgroutine, 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 "fromsourcenode, givencondition, you will reachtargetnode usingrulesatdepth". Current edges in the KCFG just store a singledepth, rules, withconditionalways being#Top.merge_nodes(CTerm, CTerm) -> boolon the nodes following the edges. In the case of the diagram, we pairwise run it on all ofB,C,D(or do it iteratively for each pair and do smaller mergings). If two nodes (such asBandC) havemerge_nodesreturnTrue, we do the following: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, ifErepresents the more abstract configuration, we would computeE #And { PC1 #Implies SUBST1 } #And { PC2 #Implies SUBST2 }, whereSUBST1instantiatesEtoB, andSUBST2instantiatesEtoC.A1andA2from the graph, and insert new nodeB \/ C, and insert an edge fromAtoB \/ Cwith edge data[(d1, PC1), (d2, PC2)], and insert a split fromB \/ CtoBandCwith conditionsPC1,PC2.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.