SMT: Make path conditionals more precise

Previously path conditionals for a node were defined as the path
conditional of the immediate dominator (+ a guard for explicit guard
nodes after conditional branches), whereas now they are the path
conditional of the immediate dominator plus an expression
encapsulating all the guards between the immediate dominator and the
node. This is needed as the previous method was incorrect for certain
control flow graphs.

This slows down the generated SMT massively, because it causes the
path conditionals to become huge when the immediate dominator is far
away from the node in question. It also changes computing path
conditionals from O(n) to O(n^2) which is not ideal as our inlined
graphs can become massive. Need to figure out a better way to generate
minimal path conditionals between the immediate dominator and the
node.

I upped the timeout for the SMT tests from 20s to 300s each but this
may still cause a failure in Jenkins because that machine is slow.

5 files changed, 60 insertions, 8 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 086d4d11..350f50d9 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -67,6 +67,8 @@ let opt_ignore_overflow = ref false
 
 let opt_auto = ref false
 
+let opt_debug_graphs = ref false
+
 module EventMap = Map.Make(Event)
 
 (* Note that we have to use x : ty ref rather than mutable x : ty, to
@@ -278,6 +280,10 @@ let rec smt_cval ctx cval =
      Fn ("=", [smt_cval ctx cval; Bin "1"])
   | V_call (Bnot, [cval]) ->
      Fn ("not", [smt_cval ctx cval])
+  | V_call (Band, cvals) ->
+     Fn ("and", List.map (smt_cval ctx) cvals)
+  | V_call (Bor, cvals) ->
+     Fn ("or", List.map (smt_cval ctx) cvals)
   | V_ctor_kind (union, ctor_id, unifiers, _) ->
      Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)])
   | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
@@ -322,6 +328,9 @@ let add_event ctx ev smt =
   let stack = event_stack ctx ev in
   Stack.push (Fn ("=>", [ctx.pathcond; smt])) stack
 
+let add_pathcond_event ctx ev =
+  Stack.push ctx.pathcond (event_stack ctx ev)
+
 let overflow_check ctx smt =
   if not !opt_ignore_overflow then (
     Util.warn "Adding overflow check in generated SMT";
@@ -903,6 +912,16 @@ let builtin_compare_bits fn ctx v1 v2 ret_ctyp =
 
   | _ -> builtin_type_error ctx fn [v1; v2] (Some ret_ctyp)
 
+(* ***** String operations: lib/real.sail ***** *)
+
+let builtin_decimal_string_of_bits ctx v =
+  begin match cval_ctyp v with
+  | CT_fbits (n, _) ->
+     Fn ("int.to.str", [Fn ("bv2nat", [smt_cval ctx v])])
+
+  | _ -> builtin_type_error ctx "decimal_string_of_bits" [v] None
+  end
+
 (* ***** Real number operations: lib/real.sail ***** *)
 
 let builtin_sqrt_real ctx root v =
@@ -986,6 +1005,7 @@ let smt_builtin ctx name args ret_ctyp =
   (* string builtins *)
   | "concat_str", [v1; v2], CT_string -> ctx.use_string := true; Fn ("str.++", [smt_cval ctx v1; smt_cval ctx v2])
   | "eq_string", [v1; v2], CT_bool -> ctx.use_string := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+  | "decimal_string_of_bits", [v], CT_string -> ctx.use_string := true; builtin_decimal_string_of_bits ctx v
 
   (* lib/real.sail *)
   (* Note that sqrt_real is special and is handled by smt_instr. *)
@@ -1408,7 +1428,7 @@ let smt_instr ctx =
   | I_aux (I_clear _, _) -> []
 
   | I_aux (I_match_failure, _) ->
-     add_event ctx Match (Bool_lit false);
+     add_pathcond_event ctx Match;
      []
 
   | I_aux (I_undefined ctyp, _) -> []
@@ -1606,6 +1626,12 @@ let rec smt_query ctx = function
   | Q_or qs ->
      Fn ("or", List.map (smt_query ctx) qs)
 
+let dump_graph function_id cfg =
+  let gv_file = string_of_id function_id ^ ".gv" in
+  let out_chan = open_out gv_file in
+  Jib_ssa.make_dot out_chan cfg;
+  close_out out_chan
+
 let smt_cdef props lets name_file ctx all_cdefs = function
   | CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
      begin match find_function [] function_id all_cdefs with
@@ -1641,14 +1667,13 @@ let smt_cdef props lets name_file ctx all_cdefs = function
         let visit_order =
           try topsort cfg with
           | Not_a_DAG n ->
-             let gv_file = string_of_id function_id ^ ".gv" in
-             let out_chan = open_out gv_file in
-             make_dot out_chan cfg;
-             close_out out_chan;
+             dump_graph function_id cfg;
              raise (Reporting.err_general pragma_l
-                      (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s"
-                         prop_type (string_of_id function_id) n gv_file))
+                      (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s.gv"
+                         prop_type (string_of_id function_id) n (string_of_id function_id)))
         in
+        if !opt_debug_graphs then
+          dump_graph function_id cfg;
 
         List.iter (fun n ->
             begin match get_vertex cfg n with
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 9a9a3361..a4a77f9d 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -619,15 +619,33 @@ let place_pi_functions graph start idom children =
     List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)
   in
 
+  let rec between_dom p n =
+    if n = p then
+      []
+    else
+      match graph.nodes.(n) with
+      | Some ((_, cfnode), preds, _) ->
+         let preds = List.concat (List.map (between_dom p) (IntSet.elements preds)) in
+         begin match get_guard cfnode, preds with
+         | [guard], [pred] -> [V_call (Band, [guard; pred])]
+         | [guard], [] -> [guard]
+         | [guard], _ -> [V_call (Band, [guard; V_call (Bor, preds)])]
+         | _, (_ :: _ :: _ as preds) -> [V_call (Bor, preds)]
+         | _, pred -> pred
+         end
+      | None -> assert false
+  in
+
   let rec go n =
     begin match graph.nodes.(n) with
     | Some ((ssa, cfnode), preds, succs) ->
        let p = idom.(n) in
+       let bd = between_dom p n in
        if p <> -1 then
          begin match graph.nodes.(p) with
          | Some ((dom_ssa, _), _, _) ->
             let args = get_guard cfnode @ get_pi_contents dom_ssa in
-            graph.nodes.(n) <- Some ((Pi args :: ssa, cfnode), preds, succs)
+            graph.nodes.(n) <- Some ((Pi (bd @ args) :: ssa, cfnode), preds, succs)
          | None -> assert false
          end
     | None -> assert false
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 378f5fae..3326d4ad 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -278,6 +278,8 @@ let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
 
 let string_of_op = function
   | Bnot -> "@not"
+  | Band -> "@and"
+  | Bor -> "@or"
   | List_hd -> "@hd"
   | List_tl -> "@tl"
   | Bit_to_bool -> "@bit_to_bool"
@@ -896,6 +898,8 @@ let rec infer_call op vs =
   match op, vs with
   | Bit_to_bool, _ -> CT_bool
   | Bnot, _ -> CT_bool
+  | Band, _ -> CT_bool
+  | Bor, _ -> CT_bool
   | List_hd, [v] ->
      begin match cval_ctyp v with
      | CT_list ctyp -> ctyp
diff --git a/src/property.mli b/src/property.mli
index 3789fa63..f84a85e3 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -90,6 +90,8 @@ val rewrite : tannot defs -> tannot defs
 
 type event = Overflow | Assertion | Assumption | Match | Return
 
+val string_of_event : event -> string
+
 module Event : sig
   type t = event
   val compare : event -> event -> int
diff --git a/src/sail.ml b/src/sail.ml
index c2b2ed65..daec1fdb 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -315,6 +315,9 @@ let options = Arg.align ([
   ( "-ddump_flow_graphs",
     Arg.Set Jib_compile.opt_debug_flow_graphs,
     " (debug) dump flow analysis for Sail functions when compiling to C");
+  ( "-ddump_smt_graphs",
+    Arg.Set Jib_smt.opt_debug_graphs,
+    " (debug) dump flow analysis for properties when generating SMT");
   ( "-dtc_verbose",
     Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
     "<verbosity> (debug) verbose typechecker output: 0 is silent");