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.

12 files changed, 216 insertions, 12 deletions

diff --git a/language/jib.ott b/language/jib.ott
index 447b25e3..dfda3bbc 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -58,6 +58,8 @@ name :: '' ::=
 
 op :: '' ::=
   | not               :: :: bnot
+  | or                :: :: bor
+  | and               :: :: band
   | hd                :: :: list_hd
   | tl                :: :: list_tl
   | bit_to_bool       :: :: bit_to_bool
diff --git a/lib/mapping.sail b/lib/mapping.sail
new file mode 100644
index 00000000..6cbb7585
--- /dev/null
+++ b/lib/mapping.sail
@@ -0,0 +1,84 @@
+$ifndef _MAPPING
+$define _MAPPING
+
+$include <arith.sail>
+$include <option.sail>
+
+val string_take = "string_take" : (string, nat) -> string
+val string_drop = "string_drop" : (string, nat) -> string
+val string_length = "string_length" : string -> nat
+val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
+val string_startswith = "string_startswith" : (string, string) -> bool
+
+val n_leading_spaces : string -> nat
+function n_leading_spaces s =
+  match s {
+    "" => 0,
+    _ => match string_take(s, 1) {
+      " " => 1 + n_leading_spaces(string_drop(s, 1)),
+      _ => 0
+    }
+  }
+
+val spc     : unit <-> string
+val opt_spc : unit <-> string
+val def_spc : unit <-> string
+
+val spc_forwards : unit -> string
+function spc_forwards () = " "
+val spc_backwards : string -> unit
+function spc_backwards s = ()
+val spc_matches_prefix : string -> option((unit, nat))
+function spc_matches_prefix s = {
+  let n = n_leading_spaces(s);
+  match n {
+    0 => None(),
+    _ => Some((), n)
+  }
+}
+
+val opt_spc_forwards : unit -> string
+function opt_spc_forwards () = ""
+val opt_spc_backwards : string -> unit
+function opt_spc_backwards s = ()
+val opt_spc_matches_prefix : string -> option((unit, nat))
+function opt_spc_matches_prefix s =
+  Some((), n_leading_spaces(s))
+
+val def_spc_forwards : unit -> string
+function def_spc_forwards () = " "
+val def_spc_backwards : string -> unit
+function def_spc_backwards s = ()
+val def_spc_matches_prefix : string -> option((unit, nat))
+function def_spc_matches_prefix s = opt_spc_matches_prefix(s)
+
+val sep : unit <-> string
+mapping sep : unit <-> string = {
+  ()     <-> opt_spc() ^ "," ^ def_spc()
+}
+
+$ifdef _DEFAULT_DEC
+$include <vector_dec.sail>
+
+val hex_bits_20 : bits(20) <-> string
+val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string
+val hex_bits_20_forwards_matches : bits(20) -> bool
+function hex_bits_20_forwards_matches bv = true
+val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat))
+val hex_bits_20_backwards_matches : string -> bool
+function hex_bits_20_backwards_matches s = match s {
+  s if match hex_bits_20_matches_prefix(s) {
+    Some (_, n) if n == string_length(s) => true,
+    _ => false
+  } => true,
+  _ => false
+}
+val hex_bits_20_backwards : string -> bits(20)
+function hex_bits_20_backwards s =
+  match hex_bits_20_matches_prefix(s) {
+      Some (bv, n) if n == string_length(s) => bv
+  }
+
+$endif
+
+$endif
diff --git a/lib/real.sail b/lib/real.sail
index 47d3f9bd..cd63a622 100644
--- a/lib/real.sail
+++ b/lib/real.sail
@@ -1,5 +1,5 @@
-$ifndef __REAL
-$define __REAL
+$ifndef _REAL
+$define _REAL
 
 val "neg_real" : real -> real
 
diff --git a/lib/string.sail b/lib/string.sail
index 3fe74eb5..87e4da57 100644
--- a/lib/string.sail
+++ b/lib/string.sail
@@ -5,6 +5,8 @@ $include <arith.sail>
 
 val eq_string = {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string) -> bool
 
+overload operator == = {eq_string}
+
 infixl 9 ^-^
 
 val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string
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");
diff --git a/test/smt/encdec.sat.sail b/test/smt/encdec.sat.sail
new file mode 100644
index 00000000..d34f3629
--- /dev/null
+++ b/test/smt/encdec.sat.sail
@@ -0,0 +1,64 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+type regbits  = bits(5)
+
+val reg_name : bits(5) <-> string
+mapping reg_name = {
+  0b00000 <-> "zero",
+  0b00001 <-> "ra",
+  0b00010 <-> "sp",
+  0b00011 <-> "gp",
+  0b00100 <-> "tp",
+  0b00101 <-> "t0",
+  0b00110 <-> "t1",
+  0b00111 <-> "t2",
+  0b01000 <-> "fp",
+  0b01001 <-> "s1",
+  0b01010 <-> "a0",
+  0b01011 <-> "a1",
+  0b01100 <-> "a2",
+  0b01101 <-> "a3",
+  0b01110 <-> "a4",
+  0b01111 <-> "a5",
+  0b10000 <-> "a6",
+  0b10001 <-> "a7",
+  0b10010 <-> "s2",
+  0b10011 <-> "s3",
+  0b10100 <-> "s4",
+  0b10101 <-> "s5",
+  0b10110 <-> "s6",
+  0b10111 <-> "s7",
+  0b11000 <-> "s8",
+  0b11001 <-> "s9",
+  0b11010 <-> "s10",
+  0b11011 <-> "s11",
+  0b11100 <-> "t3",
+  0b11101 <-> "t4",
+  0b11110 <-> "t5",
+  0b11111 <-> "t6"
+}
+
+enum uop = RISCV_LUI | RISCV_AUIPC
+
+mapping utype_mnemonic : uop <-> string = {
+  RISCV_LUI   <-> "lui",
+  RISCV_AUIPC <-> "auipc"
+}
+
+val assembly : ast <-> string
+
+scattered union ast
+
+union clause ast = UTYPE : (bits(20), regbits, uop)
+
+mapping clause assembly = UTYPE(imm, rd, op)
+  <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
+
+$counterexample
+function prop(x: string) -> bool = {
+  not_bool(utype_mnemonic(RISCV_LUI) == x)
+}
diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py
index c9cadec3..f59bdba9 100755
--- a/test/smt/run_tests.py
+++ b/test/smt/run_tests.py
@@ -23,7 +23,7 @@ def test_smt(name, solver, sail_opts):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
-                step('timeout 20s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
+                step('timeout 300s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
                 if re.match('.+\.sat\.sail$', filename):
                     step('grep -q ^sat$ {}.out'.format(basename))
                 else:
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
index 87c55487..ed45112e 100644
--- a/test/smt/rv_add_0.unsat.sail
+++ b/test/smt/rv_add_0.unsat.sail
@@ -145,7 +145,7 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-$counterexample
+$property
 function prop(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
   X(rs1) = v;
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {