From 7280e7bcdcb56521482846af3282f6adbd277ce0 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 9 May 2019 18:39:48 +0100
Subject: 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.
---
 src/jib/jib_smt.ml  | 39 ++++++++++++++++++++++++++++++++-------
 src/jib/jib_ssa.ml  | 20 +++++++++++++++++++-
 src/jib/jib_util.ml |  4 ++++
 src/property.mli    |  2 ++
 src/sail.ml         |  3 +++
 5 files changed, 60 insertions(+), 8 deletions(-)

(limited to 'src')

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");
-- 
cgit v1.2.3


From 5fe14d1d13e4d6a3bc9a2a0390d645b383e56349 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 9 May 2019 19:37:56 +0100
Subject: SMT: Add explicit terminators to SSA graph

Makes the graph slightly cleaner, and means we can represent
conditionals in a way that shoud allow computing path conditions much
easier.

Essentially rather than a basic block being a list of instructions
where the last instruction is a jump (or other terminator) it is now a
list of instructions combined with an explict terminator, i.e.

CF_block (instrs @ I_jump (cval, label) ==> CF_block (instrs, T_jump (n, label))

Rather than storing the cval in the T_jump it just has a number that
links to a mapping from numbers to cvals, and we represent the
negation of any cval in that table by negating its number. Therefore
at any join point in the CFG, we can efficiently check when the
joining path conditionals contain both n and minus n and remove both.
---
 src/jib/jib_smt.ml  |  35 +++++++++-------
 src/jib/jib_ssa.ml  | 118 ++++++++++++++++++++++++++++++++++++----------------
 src/jib/jib_ssa.mli |  13 +++++-
 3 files changed, 112 insertions(+), 54 deletions(-)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 350f50d9..de5feca1 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1343,6 +1343,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,
@@ -1421,21 +1434,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_pathcond_event ctx Match;
-     []
-
-  | 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))
@@ -1451,9 +1454,11 @@ 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 ->
+  | CF_block (instrs, terminator) ->
      let ctx = { ctx with pathcond = get_pathcond ctx ssanodes } in
-     List.concat (List.map (smt_instr ctx) instrs)
+     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 *)
   | _ -> []
 
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index a4a77f9d..dfacf90a 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,12 +61,16 @@ 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_vertex graph n = graph.nodes.(n)
@@ -77,6 +82,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 +198,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 +240,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 +449,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 +569,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,13 +650,19 @@ 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 =
     List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)
   in
 
+  (*
   let rec between_dom p n =
     if n = p then
       []
@@ -634,13 +678,13 @@ let place_pi_functions graph start idom children =
          | _, pred -> pred
          end
       | None -> assert false
-  in
+  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
+       let bd = [] (* between_dom p n *) in
        if p <> -1 then
          begin match graph.nodes.(p) with
          | Some ((dom_ssa, _), _, _) ->
@@ -699,9 +743,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..72cf1a1e 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -77,10 +77,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
-- 
cgit v1.2.3


From 999c20c525ac8d268b7c6c4c643e6d5b35c53665 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Fri, 10 May 2019 00:31:29 +0100
Subject: 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.
---
 src/jib/jib_smt.ml  | 56 +++++++++++++++++++++++++++--------------------------
 src/jib/jib_ssa.ml  | 27 +++++++-------------------
 src/jib/jib_ssa.mli |  2 ++
 src/smtlib.ml       | 10 ++++++++++
 4 files changed, 48 insertions(+), 47 deletions(-)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index de5feca1..3b42e749 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -93,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
@@ -118,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;
   }
@@ -281,9 +281,9 @@ let rec smt_cval ctx cval =
   | V_call (Bnot, [cval]) ->
      Fn ("not", [smt_cval ctx cval])
   | V_call (Band, cvals) ->
-     Fn ("and", List.map (smt_cval ctx) cvals)
+     smt_conj (List.map (smt_cval ctx) cvals)
   | V_call (Bor, cvals) ->
-     Fn ("or", List.map (smt_cval ctx) 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, _) ->
@@ -326,10 +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 ctx.pathcond (event_stack ctx ev)
+  Stack.push (Lazy.force ctx.pathcond) (event_stack ctx ev)
 
 let overflow_check ctx smt =
   if not !opt_ignore_overflow then (
@@ -1269,11 +1269,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))
@@ -1286,12 +1282,28 @@ let smt_ssanode ctx cfg preds =
      | Some mux ->
         [Define_const (zencode_name id, smt_ctyp ctx ctyp, mux)]
 
-let rec get_pathcond ctx fns =
+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
+  match get_vertex cfg n with
+  | Some ((_, CF_guard cond), _, _) ->
+     smt_cval ctx (get_cond cfg cond)
+  | 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 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 "Predecessor node does not exist"
+       in
+       let pis = List.map get_pi (IntSet.elements preds) in
+       prerr_endline (string_of_int n ^ string_of_cval (V_call (Bor, pis)));
+       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
@@ -1455,7 +1467,6 @@ let smt_cfnode all_cdefs ctx ssanodes =
      in
      smt_reg_decs @ List.map smt_start (NameMap.bindings inits)
   | CF_block (instrs, terminator) ->
-     let ctx = { ctx with pathcond = get_pathcond ctx ssanodes } in
      let smt_instrs = List.map (smt_instr ctx) instrs in
      let smt_term = smt_terminator ctx terminator in
      List.concat (smt_instrs @ [smt_term])
@@ -1607,16 +1618,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
@@ -1687,6 +1688,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;
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index dfacf90a..0f0f582e 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -73,6 +73,12 @@ let make ~initial_size () = {
     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 =
@@ -662,34 +668,15 @@ 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 (bd @ args) :: ssa, cfnode), preds, succs)
+            graph.nodes.(n) <- Some ((Pi args :: ssa, cfnode), preds, succs)
          | None -> assert false
          end
     | None -> assert false
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
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])
-- 
cgit v1.2.3


From 1110dcc2ad0979614987b40422b33b9ecb9c40f0 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 10 May 2019 16:24:11 +0100
Subject: SMT: Fix error in get_pathcond

---
 src/jib/jib_smt.ml | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 3b42e749..d73d1a02 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1284,25 +1284,24 @@ let smt_ssanode ctx cfg preds =
 
 let rec get_pathcond n cfg ctx =
   let open Jib_ssa in
+  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_cond cfg 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 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 "Predecessor node does not exist"
-       in
        let pis = List.map get_pi (IntSet.elements preds) in
-       prerr_endline (string_of_int n ^ string_of_cval (V_call (Bor, pis)));
        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
-- 
cgit v1.2.3


From 0ade72d50d578753332fb78753bbd43c09122d08 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 10 May 2019 19:25:18 +0100
Subject: SMT: Experiment with symbolic memory reads and writes

---
 src/jib/jib_smt.ml | 38 ++++++++++++++++++++++++++++++++++++++
 src/sail_lib.ml    |  4 ++++
 src/smtlib.ml      |  8 ++++++++
 src/value.ml       |  5 +++++
 4 files changed, 55 insertions(+)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index d73d1a02..45837513 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1022,6 +1022,19 @@ 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)
 
+
+let writes = ref (-1)
+
+let builtin_write_mem ctx wk addr_size addr data_size data =
+  [Write_mem (smt_cval ctx wk, smt_cval ctx addr, smt_cval ctx data)]
+
+let reads = ref (-1)
+
+let builtin_read_mem ctx rk addr_size addr data_size =
+  incr reads;
+  let name = "R" ^ string_of_int !reads in
+  [Read_mem (name, smt_cval ctx rk, smt_cval ctx addr)]
+
 let rec smt_conversion ctx from_ctyp to_ctyp x =
   match from_ctyp, to_ctyp with
   | _, _ when ctyp_equal from_ctyp to_ctyp -> x
@@ -1384,6 +1397,21 @@ 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] ->
+            builtin_write_mem ctx wk addr_size addr data_size data
+         | _ ->
+            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] ->
+            builtin_read_mem ctx rk addr_size addr data_size
+         | _ ->
+            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]
@@ -1521,6 +1549,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 (name, 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'
@@ -1542,6 +1576,10 @@ let optimize_smt stack =
           Queue.add (Define_const (var, typ, simp_smt_exp vars exp)) queue
        | None -> assert false
        end
+    | Write_mem (wk, addr, data) ->
+       Queue.add (Write_mem (simp_smt_exp vars wk, simp_smt_exp vars addr, simp_smt_exp vars data)) queue
+    | Read_mem (name, rk, addr) ->
+       Queue.add (Read_mem (name, 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 ->
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 39485769..61e62d76 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -186,6 +186,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 1665419c..a252ea4a 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -182,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 smt_exp * smt_exp * smt_exp
+  | Read_mem of string * smt_exp * smt_exp
   | Declare_datatypes of string * (string * (string * smt_typ) list) list
   | Declare_tuple of int
   | Assert of smt_exp
@@ -242,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 (wk, addr, data) ->
+     pp_sfun "write-mem" [pp_smt_exp wk; pp_smt_exp addr; pp_smt_exp data]
+
+  | Read_mem (name, rk, addr) ->
+     pp_sfun "read-mem" [string name; pp_smt_exp rk; pp_smt_exp addr]
+
   | Declare_datatypes (name, ctors) ->
      let pp_ctor (ctor_name, fields) =
        match fields with
diff --git a/src/value.ml b/src/value.ml
index 958a1919..6ccecac0 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -341,6 +341,10 @@ let value_sub_int = function
   | [v1; v2] -> V_int (Sail_lib.sub_int (coerce_int v1, coerce_int v2))
   | _ -> failwith "value sub"
 
+let value_sub_nat = function
+  | [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))
   | _ -> failwith "value negate"
@@ -663,6 +667,7 @@ let primops =
       ("shift_bits_right", value_shift_bits_right);
       ("add_int", value_add_int);
       ("sub_int", value_sub_int);
+      ("sub_nat", value_sub_nat);
       ("div_int", value_quotient);
       ("mult_int", value_mult);
       ("mult", value_mult);
-- 
cgit v1.2.3


From df7101474911964e7d8dbf5b6fd3de3ed66b7fc8 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Fri, 10 May 2019 21:10:19 +0100
Subject: SMT: Implement memory events for read_mem and write_mem

Generate SMT where the memory reads and writes are totally
unconstrained, allowing additional constraints to be added that
restrict the possible reads and writes based on some memory model.
---
 src/jib/jib_smt.ml | 35 ++++++++++++++++++++++-------------
 src/smtlib.ml      | 12 ++++++------
 2 files changed, 28 insertions(+), 19 deletions(-)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 45837513..4afd1fa9 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1022,18 +1022,22 @@ 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 =
-  [Write_mem (smt_cval ctx wk, smt_cval ctx addr, smt_cval ctx 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 =
+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_cval ctx rk, smt_cval ctx addr)]
+  [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
@@ -1401,14 +1405,17 @@ let smt_instr ctx =
        else if name = "platform_write_mem" then
          begin match args with
          | [wk; addr_size; addr; data_size; data] ->
-            builtin_write_mem ctx 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] ->
-            builtin_read_mem ctx 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
@@ -1549,10 +1556,10 @@ let optimize_smt stack =
        end
     | (Declare_datatypes _ | Declare_tuple _) as def ->
        Stack.push def stack'
-    | Write_mem (wk, addr, data) as def ->
+    | 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 (name, rk, addr) as def ->
+    | Read_mem (_, _, rk, addr) as def ->
        uses_in_exp rk; uses_in_exp addr;
        Stack.push def stack'
     | Assert exp as def ->
@@ -1576,10 +1583,10 @@ let optimize_smt stack =
           Queue.add (Define_const (var, typ, simp_smt_exp vars exp)) queue
        | None -> assert false
        end
-    | Write_mem (wk, addr, data) ->
-       Queue.add (Write_mem (simp_smt_exp vars wk, simp_smt_exp vars addr, simp_smt_exp vars data)) queue
-    | Read_mem (name, rk, addr) ->
-       Queue.add (Read_mem (name, simp_smt_exp vars rk, simp_smt_exp vars addr)) queue
+    | 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 ->
@@ -1740,12 +1747,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/smtlib.ml b/src/smtlib.ml
index a252ea4a..ab6ebf55 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -182,8 +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 smt_exp * smt_exp * smt_exp
-  | Read_mem of string * smt_exp * 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
@@ -244,11 +244,11 @@ 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 (wk, addr, data) ->
-     pp_sfun "write-mem" [pp_smt_exp wk; pp_smt_exp addr; pp_smt_exp data]
+  | Write_mem (name, wk, addr, data) ->
+     pp_sfun "declare-const" [string name; pp_smt_typ Bool]
 
-  | Read_mem (name, rk, addr) ->
-     pp_sfun "read-mem" [string name; pp_smt_exp rk; pp_smt_exp addr]
+  | 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) =
-- 
cgit v1.2.3


From 3677cfc13e19efe650488a3a25917324bd6ccef7 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Mon, 13 May 2019 23:29:15 +0100
Subject: Parse dereferences in orderinary expressions

---
 src/initial_check.ml    | 3 ++-
 src/pretty_print_coq.ml | 3 +--
 src/pretty_print_lem.ml | 3 +--
 src/reporting.ml        | 5 +++--
 src/reporting.mli       | 5 ++++-
 src/type_check.ml       | 2 +-
 6 files changed, 12 insertions(+), 9 deletions(-)

(limited to 'src')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 790a6624..70252a1a 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -411,7 +411,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/pretty_print_coq.ml b/src/pretty_print_coq.ml
index f26c74d7..afa63cb9 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 10441ed5..708749cc 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/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/type_check.ml b/src/type_check.ml
index 0365e2e5..eeb6773b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -902,7 +902,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
-- 
cgit v1.2.3


From f6cc45f2788dc777d1fa35aa9a216de994992288 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 13 May 2019 16:20:35 +0100
Subject: SMT: Add comment explaining path conditionals

---
 src/jib/jib_smt.ml | 43 ++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 42 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 4afd1fa9..7f622f85 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1251,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.
@@ -1299,6 +1299,47 @@ let smt_ssanode ctx cfg preds =
      | Some mux ->
         [Define_const (zencode_name id, smt_ctyp ctx ctyp, mux)]
 
+(* 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
   let get_pi m =
-- 
cgit v1.2.3