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, 10 insertions, 0 deletions

diff --git a/src/smtlib.ml b/src/smtlib.ml
index 7f485447..1665419c 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -100,6 +100,16 @@ type smt_exp =
   | Extract of int * int * smt_exp
   | Tester of string * smt_exp
 
+let smt_conj = function
+  | [] -> Bool_lit true
+  | [x] -> x
+  | xs -> Fn ("and", xs)
+
+let smt_disj = function
+  | [] -> Bool_lit false
+  | [x] -> x
+  | xs -> Fn ("or", xs)
+
 let extract i j x = Extract (i, j, x)
 
 let bvnot x    = Fn ("bvnot", [x])