SMT: Lazily compute efficient path conditionals

Effectively reverts 7280e7b with a different method that isn't slow,
although it's not totally clear that this is correct - it could just
be more subtly wrong than before commit 7280e7b.

Following is mostly so I can remember what I did to document & write
up properly at some point:

What we do is compute 'pi' conditions as before by traversing the
dominator tree, we each node having a pi condition defined as the
conjunction of all guards between it and the start node in the
dominator tree. This is imprecise because we have situations like

  1
 / \
2   3
|   |
|   4
|   |\
5   6 9
 \ /  |
  7   10
  |
  8

where 8 = match_failure, 1 = start and 10 = return.

2, 3, 6 and 9 are guards as they come directly after a control flow
split, which always follows a conditional jump.

Here the path through the dominator tree for the match_failure is
1->7->8 which contains no guards so the pi condition would be empty.
What we do now is walk backwards (CFG must be acyclic at this point)
until we hit the join point prior to where we require a path
condition. We then take the disjunction of the pi conditions for the
join point's predecessors, so 5 and 6 in this case. Which gives us a
path condition of 2 | (3 & 6) as the dominator chains are 1->2->5 and
1->3->4->6.

I think this works as any split in the control flow must have been
caused by a conditional jump followed by distinct guards, so each of
the nodes immediately prior to a join point must be dominated by at
least one unique guard. It also explains why the pi conditions seem
sufficient to choose outcomes of phi functions.

If we hit a guard before a join (such as 9 for return's path
conditional) we just return the pi condition for that guard, i.e.
(3 & 9) for 10. If we reach start then the path condition is simply
true.

1 files changed, 2 insertions, 0 deletions

diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 72cf1a1e..dadb20fd 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -60,6 +60,8 @@ val make : initial_size:int -> unit -> 'a array_graph
 
 module IntSet : Set.S with type elt = int
 
+val get_cond : 'a array_graph -> int -> Jib.cval
+     
 val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option
 
 val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit