Merge branch 'smt_experiments' into sail2

15 files changed, 308 insertions, 98 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index ad52751b..522faab7 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -425,7 +425,8 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
          E_internal_return(to_ast_exp ctx exp)
        else
          raise (Reporting.err_general l "Internal return construct found without -dmagic_hash")
-    | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
+    | P.E_deref exp ->
+       E_app (Id_aux (Id "__deref", l), [to_ast_exp ctx exp])
     ), (l,()))
 
 and to_ast_measure ctx (P.Measure_aux(m,l)) : unit internal_loop_measure =
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 086d4d11..7f622f85 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
@@ -91,7 +93,7 @@ type ctx = {
     (* When generating SMT for an instruction pathcond will contain
        the global path conditional of the containing block in the
        control flow graph *)
-    pathcond : smt_exp;
+    pathcond : smt_exp Lazy.t;
     (* Set if we need to use strings *)
     use_string : bool ref;
     use_real : bool ref
@@ -116,7 +118,7 @@ let initial_ctx () = {
     arg_stack = Stack.create ();
     ast = Defs [];
     events = ref EventMap.empty;
-    pathcond = Bool_lit true;
+    pathcond = lazy (Bool_lit true);
     use_string = ref false;
     use_real = ref false;
   }
@@ -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) ->
+     smt_conj (List.map (smt_cval ctx) cvals)
+  | V_call (Bor, cvals) ->
+     smt_disj (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, _) ->
@@ -320,7 +326,10 @@ let rec smt_cval ctx cval =
 
 let add_event ctx ev smt =
   let stack = event_stack ctx ev in
-  Stack.push (Fn ("=>", [ctx.pathcond; smt])) stack
+  Stack.push (Fn ("=>", [Lazy.force ctx.pathcond; smt])) stack
+
+let add_pathcond_event ctx ev =
+  Stack.push (Lazy.force ctx.pathcond) (event_stack ctx ev)
 
 let overflow_check ctx smt =
   if not !opt_ignore_overflow then (
@@ -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. *)
@@ -1002,6 +1022,23 @@ let smt_builtin ctx name args ret_ctyp =
 
   | _ -> failwith ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp)
 
+(* Memory reads and writes as defined in lib/regfp.sail *)
+let writes = ref (-1)
+
+let builtin_write_mem ctx wk addr_size addr data_size data =
+  incr writes;
+  let name = "W" ^ string_of_int !writes in
+  [Write_mem (name, smt_cval ctx wk, smt_cval ctx addr, smt_cval ctx data)],
+  Var name
+
+let reads = ref (-1)
+
+let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
+  incr reads;
+  let name = "R" ^ string_of_int !reads in
+  [Read_mem (name, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr)],
+  Var name
+
 let rec smt_conversion ctx from_ctyp to_ctyp x =
   match from_ctyp, to_ctyp with
   | _, _ when ctyp_equal from_ctyp to_ctyp -> x
@@ -1214,7 +1251,7 @@ let push_smt_defs stack smt_defs =
 (* When generating SMT when we encounter joins between two or more
    blocks such as in the example below, we have to generate a muxer
    that chooses the correct value of v_n or v_m to assign to v_o. We
-   use the pi nodes that contain the global path condition for each
+   use the pi nodes that contain the path condition for each
    block to generate an if-then-else for each phi function. The order
    of the arguments to each phi function is based on the graph node
    index for the predecessor nodes.
@@ -1249,11 +1286,7 @@ let smt_ssanode ctx cfg preds =
      let pis = List.map get_pi (IntSet.elements preds) in
      let mux =
        List.fold_right2 (fun pi id chain ->
-           let pathcond =
-             match pi with
-             | [cval] -> smt_cval ctx cval
-             | _ -> Fn ("and", List.map (smt_cval ctx) pi)
-           in
+           let pathcond = smt_conj (List.map (smt_cval ctx) pi) in
            match chain with
            | Some smt ->
               Some (Ite (pathcond, Var (zencode_name id), smt))
@@ -1266,12 +1299,68 @@ let smt_ssanode ctx cfg preds =
      | Some mux ->
         [Define_const (zencode_name id, smt_ctyp ctx ctyp, mux)]
 
-let rec get_pathcond ctx fns =
+(* The pi condition are computed by traversing the dominator tree,
+   with 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.
+
+   This should work 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 are
+   sufficient to choose outcomes of phi functions above.
+
+   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.
+*)
+let rec get_pathcond n cfg ctx =
   let open Jib_ssa in
-  match fns with
-  | [] | Pi [] :: _ -> Bool_lit true
-  | Pi cvals :: _ -> Fn ("and", List.map (smt_cval ctx) cvals)
-  | Phi _ :: fns -> get_pathcond ctx fns
+  let get_pi m =
+    match get_vertex cfg m with
+    | Some ((ssanodes, _), _, _) ->
+       V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes))
+    | None -> failwith "Node does not exist"
+  in
+  match get_vertex cfg n with
+  | Some ((_, CF_guard cond), _, _) ->
+     smt_cval ctx (get_pi n)
+  | Some (_, preds, succs) ->
+     if IntSet.cardinal preds = 0 then
+       Bool_lit true
+     else if IntSet.cardinal preds = 1 then
+       get_pathcond (IntSet.min_elt preds) cfg ctx
+     else
+       let pis = List.map get_pi (IntSet.elements preds) in
+       smt_cval ctx (V_call (Bor, pis))
+
+  | None -> assert false (* Should never be called for a non-existent node *)
 
 (* For any complex l-expression we need to turn it into a
    read-modify-write in the SMT solver. The SSA transform turns CL_id
@@ -1323,6 +1412,19 @@ let rmw_modify smt = function
      end
   | _ -> assert false
 
+let smt_terminator ctx =
+  let open Jib_ssa in
+  function
+  | T_end id ->
+     add_event ctx Return (Var (zencode_name id));
+     []
+
+  | T_match_failure ->
+     add_pathcond_event ctx Match;
+     []
+
+  | T_undefined _ | T_goto _ | T_jump _ | T_label _ | T_none -> []
+
 (* For a basic block (contained in a control-flow node / cfnode), we
    turn the instructions into a sequence of define-const and
    declare-const expressions. Because we are working with a SSA graph,
@@ -1340,6 +1442,24 @@ let smt_instr ctx =
          | _ ->
             Reporting.unreachable l __POS__ "Bad arguments for sqrt_real"
          end
+       (* See lib/regfp.sail *)
+       else if name = "platform_write_mem" then
+         begin match args with
+         | [wk; addr_size; addr; data_size; data] ->
+            let mem_event, var = builtin_write_mem ctx wk addr_size addr data_size data in
+            mem_event @ [define_const ctx id ret_ctyp var]
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __write_mem"
+         end
+       else if name = "platform_read_mem" then
+         begin match args with
+         | [rk; addr_size; addr; data_size] ->
+            let mem_event, var = builtin_read_mem ctx rk addr_size addr data_size ret_ctyp in
+            mem_event @ [define_const ctx id ret_ctyp var]
+                                                   
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __read_mem"
+         end
        else
          let value = smt_builtin ctx name args ret_ctyp in
          [define_const ctx id ret_ctyp value]
@@ -1401,21 +1521,11 @@ let smt_instr ctx =
      end;
      [declare_const ctx id ctyp]
 
-  | I_aux (I_end id, _) ->
-     add_event ctx Return (Var (zencode_name id));
-     []
-
   | I_aux (I_clear _, _) -> []
 
-  | I_aux (I_match_failure, _) ->
-     add_event ctx Match (Bool_lit false);
-     []
-
-  | I_aux (I_undefined ctyp, _) -> []
-
-  (* I_jump and I_goto will only appear as terminators for basic blocks. *)
-  | I_aux ((I_jump _ | I_goto _), _) -> []
-
+  (* Should only appear as terminators for basic blocks. *)
+  | I_aux ((I_jump _ | I_goto _ | I_end _ | I_match_failure | I_undefined _), (_, l)) ->
+     Reporting.unreachable l __POS__ "SMT: Instruction should only appear as block terminator"
 
   | instr ->
      failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr))
@@ -1431,9 +1541,10 @@ let smt_cfnode all_cdefs ctx ssanodes =
        | _ -> declare_const ctx id ctyp
      in
      smt_reg_decs @ List.map smt_start (NameMap.bindings inits)
-  | CF_block instrs ->
-     let ctx = { ctx with pathcond = get_pathcond ctx ssanodes } in
-     List.concat (List.map (smt_instr ctx) instrs)
+  | CF_block (instrs, terminator) ->
+     let smt_instrs = List.map (smt_instr ctx) instrs in
+     let smt_term = smt_terminator ctx terminator in
+     List.concat (smt_instrs @ [smt_term])
   (* We can ignore any non basic-block/start control-flow nodes *)
   | _ -> []
 
@@ -1486,6 +1597,12 @@ let optimize_smt stack =
        end
     | (Declare_datatypes _ | Declare_tuple _) as def ->
        Stack.push def stack'
+    | Write_mem (_, wk, addr, data) as def ->
+       uses_in_exp wk; uses_in_exp addr; uses_in_exp data;
+       Stack.push def stack'
+    | Read_mem (_, _, rk, addr) as def ->
+       uses_in_exp rk; uses_in_exp addr;
+       Stack.push def stack'
     | Assert exp as def ->
        uses_in_exp exp;
        Stack.push def stack'
@@ -1507,6 +1624,10 @@ let optimize_smt stack =
           Queue.add (Define_const (var, typ, simp_smt_exp vars exp)) queue
        | None -> assert false
        end
+    | Write_mem (name, wk, addr, data) ->
+       Queue.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, simp_smt_exp vars data)) queue
+    | Read_mem (name, typ, rk, addr) ->
+       Queue.add (Read_mem (name, typ, simp_smt_exp vars rk, simp_smt_exp vars addr)) queue
     | Assert exp ->
        Queue.add (Assert (simp_smt_exp vars exp)) queue
     | (Declare_datatypes _ | Declare_tuple _) as def ->
@@ -1582,16 +1703,6 @@ let expand_reg_deref ctx = function
      end
   | instr -> instr
 
-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 rec smt_query ctx = function
   | Q_all ev ->
      let stack = event_stack ctx ev in
@@ -1606,6 +1717,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 +1758,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
@@ -1657,6 +1773,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
                let muxers =
                  ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat
                in
+               let ctx = { ctx with pathcond = lazy (get_pathcond n cfg ctx) } in
                let basic_block = smt_cfnode all_cdefs ctx ssanodes cfnode in
                push_smt_defs stack muxers;
                push_smt_defs stack basic_block;
@@ -1671,12 +1788,14 @@ let smt_cdef props lets name_file ctx all_cdefs = function
         if prop_type = "counterexample" then
           output_string out_chan "(set-option :produce-models true)\n";
 
+        let header = smt_header ctx all_cdefs in
+        
         if !(ctx.use_string) || !(ctx.use_real) then
           output_string out_chan "(set-logic ALL)\n"
         else
           output_string out_chan "(set-logic QF_AUFBVDT)\n";
 
-        List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") (smt_header ctx all_cdefs);
+        List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") header;
 
         let queue = optimize_smt stack in
         Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 9a9a3361..0f0f582e 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -53,6 +53,7 @@ open Jib
 open Jib_util
 
 module IntSet = Set.Make(struct type t = int let compare = compare end)
+module IntMap = Map.Make(struct type t = int let compare = compare end)
 
 (**************************************************************************)
 (* 1. Mutable graph type                                                  *)
@@ -60,14 +61,24 @@ module IntSet = Set.Make(struct type t = int let compare = compare end)
 
 type 'a array_graph = {
     mutable next : int;
-    mutable nodes : ('a * IntSet.t * IntSet.t) option array
+    mutable nodes : ('a * IntSet.t * IntSet.t) option array;
+    mutable next_cond : int;
+    mutable conds : cval IntMap.t
   }
 
 let make ~initial_size () = {
     next = 0;
-    nodes = Array.make initial_size None
+    nodes = Array.make initial_size None;
+    next_cond = 1;
+    conds = IntMap.empty
   }
 
+let get_cond graph n =
+  if n >= 0 then
+    IntMap.find n graph.conds
+  else
+    V_call (Bnot, [IntMap.find (abs n) graph.conds])
+     
 let get_vertex graph n = graph.nodes.(n)
 
 let iter_graph f graph =
@@ -77,6 +88,12 @@ let iter_graph f graph =
     | None -> ()
   done
 
+let add_cond cval graph =
+  let n = graph.next_cond in
+  graph.conds <- IntMap.add n cval graph.conds;
+  graph.next_cond <- n + 1;
+  n
+
 (** Add a vertex to a graph, returning the node index *)
 let add_vertex data graph =
   let n = graph.next in
@@ -187,12 +204,32 @@ let prune visited graph =
 (* 2. Mutable control flow graph                                          *)
 (**************************************************************************)
 
+type terminator =
+  | T_undefined of ctyp
+  | T_match_failure
+  | T_end of name
+  | T_goto of string
+  | T_jump of int * string
+  | T_label of string
+  | T_none
+
 type cf_node =
   | CF_label of string
-  | CF_block of instr list
-  | CF_guard of cval
+  | CF_block of instr list * terminator
+  | CF_guard of int
   | CF_start of ctyp NameMap.t
 
+let to_terminator graph = function
+  | I_label label -> T_label label
+  | I_goto label -> T_goto label
+  | I_jump (cval, label) ->
+     let n = add_cond cval graph in
+     T_jump (n, label)
+  | I_end name -> T_end name
+  | I_match_failure -> T_match_failure
+  | I_undefined ctyp -> T_undefined ctyp
+  | _ -> assert false
+
 (* For now we only generate CFGs for flat lists of instructions *)
 let control_flow_graph instrs =
   let module StringMap = Map.Make(String) in
@@ -209,46 +246,42 @@ let control_flow_graph instrs =
 
   let cf_split (I_aux (aux, _)) =
     match aux with
-    | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end _ | I_match_failure | I_undefined _ -> true
+    | I_label _ | I_goto _ | I_jump _ | I_end _ | I_match_failure | I_undefined _ -> true
     | _ -> false
   in
 
   let rec cfg preds instrs =
     let before, after = instr_split_at cf_split instrs in
-    let last = match after with
-      | I_aux (I_label _, _) :: _ -> []
-      | instr :: _ -> [instr]
-      | _ -> []
+    let terminator, after = match after with
+      | I_aux (instr, _) :: after -> to_terminator graph instr, after
+      | [] -> T_none, []
     in
-    let preds = match before @ last with
-      | [] -> preds
-      | instrs ->
-         let n = add_vertex ([], CF_block instrs) graph in
+    let preds = match before, terminator with
+      | [], (T_none | T_label _) -> preds
+      | instrs, _ ->
+         let n = add_vertex ([], CF_block (instrs, terminator)) graph in
          List.iter (fun p -> add_edge p n graph) preds;
          [n]
     in
-    match after with
-    | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after ->
+    match terminator with
+    | T_end _ | T_match_failure | T_undefined _ ->
        cfg [] after
 
-    | I_aux (I_goto label, _) :: after ->
+    | T_goto label ->
        List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds;
        cfg [] after
 
-    | I_aux (I_jump (cval, label), _) :: after ->
-       let t = add_vertex ([], CF_guard cval) graph in
-       let f = add_vertex ([], CF_guard (V_call (Bnot, [cval]))) graph in
+    | T_jump (cond, label) ->
+       let t = add_vertex ([], CF_guard cond) graph in
+       let f = add_vertex ([], CF_guard (- cond)) graph in
        List.iter (fun p -> add_edge p t graph; add_edge p f graph) preds;
        add_edge t (StringMap.find label !labels) graph;
        cfg [f] after
 
-    | I_aux (I_label label, _) :: after ->
+    | T_label label ->
        cfg (StringMap.find label !labels :: preds) after
 
-    | I_aux (_, (_, l)) :: after ->
-       Reporting.unreachable l __POS__ "Could not add instruction to control-flow graph"
-
-    | [] -> preds
+    | T_none -> preds
   in
 
   let start = add_vertex ([], CF_start NameMap.empty) graph in
@@ -422,7 +455,7 @@ let place_phi_functions graph df =
 
   let orig_A n =
     match graph.nodes.(n) with
-    | Some ((_, CF_block instrs), _, _) ->
+    | Some ((_, CF_block (instrs, _)), _, _) ->
        let vars = List.fold_left NameCTSet.union NameCTSet.empty (List.map instr_typed_writes instrs) in
        let vars = NameCTSet.diff vars (all_decls instrs) in
        all_vars := NameCTSet.union vars !all_vars;
@@ -542,21 +575,32 @@ let rename_variables graph root children =
          counts := NameMap.add id i !counts;
          push_stack id i;
          I_init (ctyp, ssa_name i id, cval)
-      | I_jump (cval, label) ->
-         I_jump (fold_cval cval, label)
-      | I_end id ->
-         let i = top_stack id in
-         I_end (ssa_name i id)
       | instr -> instr
     in
     I_aux (aux, annot)
   in
 
+  let ssa_terminator = function
+    | T_jump (cond, label) ->
+       begin match IntMap.find_opt cond graph.conds with
+       | Some cval ->
+          graph.conds <- IntMap.add cond (fold_cval cval) graph.conds;
+          T_jump (cond, label)
+       | None -> assert false
+       end
+    | T_end id ->
+       let i = top_stack id in
+       T_end (ssa_name i id)
+    | terminator -> terminator
+  in
+
   let ssa_cfnode = function
     | CF_start inits -> CF_start inits
-    | CF_block instrs -> CF_block (List.map ssa_instr instrs)
+    | CF_block (instrs, terminator) ->
+       let instrs = List.map ssa_instr instrs in
+       CF_block (instrs, ssa_terminator terminator)
     | CF_label label -> CF_label label
-    | CF_guard cval -> CF_guard (fold_cval cval)
+    | CF_guard cond -> CF_guard cond
   in
 
   let ssa_ssanode = function
@@ -612,7 +656,12 @@ let rename_variables graph root children =
 
 let place_pi_functions graph start idom children =
   let get_guard = function
-    | CF_guard guard -> [guard]
+    | CF_guard cond ->
+       begin match IntMap.find_opt (abs cond) graph.conds with
+       | Some guard when cond > 0 -> [guard]
+       | Some guard -> [V_call (Bnot, [guard])]
+       | None -> assert false
+       end
     | _ -> []
   in
   let get_pi_contents ssanodes =
@@ -681,9 +730,9 @@ let string_of_phis = function
 
 let string_of_node = function
   | (phis, CF_label label) -> string_of_phis phis ^ label
-  | (phis, CF_block instrs) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs
+  | (phis, CF_block (instrs, terminator)) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs
   | (phis, CF_start inits) -> string_of_phis phis ^ "START"
-  | (phis, CF_guard cval) -> string_of_phis phis ^ (String.escaped (Pretty_print_sail.to_string (pp_cval cval)))
+  | (phis, CF_guard cval) -> string_of_phis phis ^ string_of_int cval
 
 let vertex_color = function
   | (_, CF_start _) -> "peachpuff"
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 759e1ccb..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
@@ -77,10 +79,19 @@ exception Not_a_DAG of int
 
 val topsort : 'a array_graph -> int list
 
+type terminator =
+  | T_undefined of Jib.ctyp
+  | T_match_failure
+  | T_end of Jib.name
+  | T_goto of string
+  | T_jump of int * string
+  | T_label of string
+  | T_none
+
 type cf_node =
   | CF_label of string
-  | CF_block of Jib.instr list
-  | CF_guard of Jib.cval
+  | CF_block of Jib.instr list * terminator
+  | CF_guard of int
   | CF_start of Jib.ctyp NameMap.t
 
 val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph
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/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 55928e06..37e99662 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -920,8 +920,7 @@ let doc_lit (L_aux(lit,l)) =
       let denom = Big_int.pow_int_positive 10 (String.length f) in
       (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
     | _ ->
-      raise (Reporting.Fatal_error
-        (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in
+      raise (Reporting.err_syntax_loc l "could not parse real literal") in
     parens (separate space (List.map string [
       "realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
 
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index ae86a0fd..89830d38 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -423,8 +423,7 @@ let doc_lit_lem (L_aux(lit,l)) =
       let denom = Big_int.pow_int_positive 10 (String.length f) in
       (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
     | _ ->
-      raise (Reporting.Fatal_error
-        (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in
+      raise (Reporting.err_syntax_loc l "could not parse real literal") in
     parens (separate space (List.map string [
       "realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
 
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/reporting.ml b/src/reporting.ml
index c85f20ff..9387ee6b 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -133,7 +133,7 @@ type error =
   | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
   | Err_todo of Parse_ast.l * string
   | Err_syntax of Lexing.position * string
-  | Err_syntax_locn of Parse_ast.l * string
+  | Err_syntax_loc of Parse_ast.l * string
   | Err_lex of Lexing.position * string
   | Err_type of Parse_ast.l * string
 
@@ -145,7 +145,7 @@ let dest_err = function
      (Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line, Loc l, m ^ issues)
   | Err_todo (l, m) -> ("Todo" ^ m, Loc l, "")
   | Err_syntax (p, m) -> ("Syntax error", Pos p, m)
-  | Err_syntax_locn (l, m) -> ("Syntax error", Loc l, m)
+  | Err_syntax_loc (l, m) -> ("Syntax error", Loc l, m)
   | Err_lex (p, s) -> ("Lexical error", Pos p, s)
   | Err_type (l, m) -> ("Type error", Loc l, m)
 
@@ -156,6 +156,7 @@ let err_todo l m = Fatal_error (Err_todo (l, m))
 let err_unreachable l ocaml_pos m = Fatal_error (Err_unreachable (l, ocaml_pos, m))
 let err_general l m = Fatal_error (Err_general (l, m))
 let err_typ l m = Fatal_error (Err_type (l,m))
+let err_syntax_loc l m = Fatal_error (Err_syntax_loc (l, m))
 
 let unreachable l pos msg =
   raise (err_unreachable l pos msg)
diff --git a/src/reporting.mli b/src/reporting.mli
index 86399e84..28f2a799 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -93,7 +93,7 @@ type error =
   | Err_todo of Parse_ast.l * string
 
   | Err_syntax of Lexing.position * string
-  | Err_syntax_locn of Parse_ast.l * string
+  | Err_syntax_loc of Parse_ast.l * string
   | Err_lex of Lexing.position * string
   | Err_type of Parse_ast.l * string
 
@@ -111,6 +111,9 @@ val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
 (** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
 val err_typ : Parse_ast.l -> string -> exn
 
+(** [err_syntax_loc] is an abbreviation for [Fatal_error (Err_syntax_loc (l, m))] *)
+val err_syntax_loc : Parse_ast.l -> string -> exn
+  
 val unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'a
 
 val print_error : error -> unit
diff --git a/src/sail.ml b/src/sail.ml
index 13fea6f2..eff90fa3 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -321,6 +321,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/src/sail_lib.ml b/src/sail_lib.ml
index 83d58178..13ed491b 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -193,6 +193,10 @@ let sint = function
 
 let add_int (x, y) = Big_int.add x y
 let sub_int (x, y) = Big_int.sub x y
+let sub_nat (x, y) =
+  let z = Big_int.sub x y in
+  if Big_int.less z Big_int.zero then Big_int.zero else z
+
 let mult (x, y) = Big_int.mul x y
 
 (* This is euclidian division from lem *)
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 7f485447..ab6ebf55 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])
@@ -172,6 +182,8 @@ type smt_def =
   | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
   | Declare_const of string * smt_typ
   | Define_const of string * smt_typ * smt_exp
+  | Write_mem of string * smt_exp * smt_exp * smt_exp
+  | Read_mem of string * smt_typ * smt_exp * smt_exp
   | Declare_datatypes of string * (string * (string * smt_typ) list) list
   | Declare_tuple of int
   | Assert of smt_exp
@@ -232,6 +244,12 @@ let pp_smt_def =
   | Define_const (name, ty, exp) ->
      pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp]
 
+  | Write_mem (name, wk, addr, data) ->
+     pp_sfun "declare-const" [string name; pp_smt_typ Bool]
+
+  | Read_mem (name, ty, rk, addr) ->
+     pp_sfun "declare-const" [string name; pp_smt_typ ty]
+
   | Declare_datatypes (name, ctors) ->
      let pp_ctor (ctor_name, fields) =
        match fields with
diff --git a/src/type_check.ml b/src/type_check.ml
index 2ce6ea94..2be68ade 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -903,7 +903,7 @@ end = struct
     try
       Bindings.find id env.top_val_specs
     with
-    | Not_found -> typ_error env (id_loc id) ("No val spec found for " ^ string_of_id id)
+    | Not_found -> typ_error env (id_loc id) ("No type signature found for " ^ string_of_id id)
 
   let get_val_spec id env =
     try
diff --git a/src/value.ml b/src/value.ml
index 2760b220..6c2e0839 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -350,11 +350,8 @@ let value_sub_int = function
   | _ -> failwith "value sub"
 
 let value_sub_nat = function
-  | [v1; v2] -> V_int (
-                    let n = Sail_lib.sub_int (coerce_int v1, coerce_int v2) in
-                    if Big_int.less_equal n Big_int.zero then Big_int.zero else n
-                  )
-  | _ -> failwith "value sub_int"
+  | [v1; v2] -> V_int (Sail_lib.sub_nat (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value sub_nat"
 
 let value_negate = function
   | [v1] -> V_int (Sail_lib.negate (coerce_int v1))