SMT: Add control flow node numbers to memory events to track program order

Add path conditions to memory events

Allow simplication of generated SMT based on constructor kinds

3 files changed, 62 insertions, 43 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 897c685a..7420707c 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -88,6 +88,7 @@ type ctx = {
     arg_stack : (int * string) Stack.t;
     ast : Type_check.tannot defs;
     events : smt_exp Stack.t EventMap.t ref;
+    node : int;
     pathcond : smt_exp Lazy.t;
     use_string : bool ref;
     use_real : bool ref
@@ -112,6 +113,7 @@ let initial_ctx () = {
     arg_stack = Stack.create ();
     ast = Defs [];
     events = ref EventMap.empty;
+    node = -1;
     pathcond = lazy (Bool_lit true);
     use_string = ref false;
     use_real = ref false;
@@ -1022,7 +1024,8 @@ 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_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))],
+  [Write_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk,
+              smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))],
   Var (name ^ "_ret")
 
 let ea_writes = ref (-1)
@@ -1030,7 +1033,8 @@ let ea_writes = ref (-1)
 let builtin_write_mem_ea ctx wk addr_size addr data_size =
   incr ea_writes;
   let name = "A" ^ string_of_int !ea_writes in
-  [Write_mem_ea (name, smt_cval ctx wk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))],
+  [Write_mem_ea (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk,
+                 smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))],
   Enum "unit"
 
 let reads = ref (-1)
@@ -1038,7 +1042,8 @@ 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, smt_ctyp ctx (cval_ctyp addr))],
+  [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk,
+             smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))],
   Var (name ^ "_ret")
 
 let excl_results = ref (-1)
@@ -1046,7 +1051,7 @@ let excl_results = ref (-1)
 let builtin_excl_res ctx =
   incr excl_results;
   let name = "E" ^ string_of_int !excl_results in
-  [Excl_res name],
+  [Excl_res (name, ctx.node, Lazy.force ctx.pathcond)],
   Var (name ^ "_ret")
 
 let barriers = ref (-1)
@@ -1054,7 +1059,7 @@ let barriers = ref (-1)
 let builtin_barrier ctx bk =
   incr barriers;
   let name = "B" ^ string_of_int !barriers in
-  [Barrier (name, smt_cval ctx bk)],
+  [Barrier (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx bk)],
   Enum "unit"
 
 let rec smt_conversion ctx from_ctyp to_ctyp x =
@@ -1297,8 +1302,8 @@ let smt_ssanode ctx cfg preds =
   | Phi (id, ctyp, ids) ->
      let get_pi n =
        match get_vertex cfg n with
-       | Some ((ssanodes, _), _, _) ->
-          List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)
+       | Some ((ssa_elems, _), _, _) ->
+          List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems)
        | None -> failwith "Predecessor node does not exist"
      in
      let pis = List.map get_pi (IntSet.elements preds) in
@@ -1362,8 +1367,8 @@ 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))
+    | Some ((ssa_elems, _), _, _) ->
+       V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems))
     | None -> failwith "Node does not exist"
   in
   match get_vertex cfg n with
@@ -1535,7 +1540,7 @@ let smt_instr ctx =
        end
      else if not extern then
        let smt_args = List.map (smt_cval ctx) args in
-       [define_const ctx id ret_ctyp (Fn (zencode_id function_id, smt_args))]
+       [define_const ctx id ret_ctyp (Ctor (zencode_id function_id, smt_args))]
      else
        failwith ("Unrecognised function " ^ string_of_id function_id)
 
@@ -1571,7 +1576,7 @@ let smt_instr ctx =
   | instr ->
      failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr))
 
-let smt_cfnode all_cdefs ctx ssanodes =
+let smt_cfnode all_cdefs ctx ssa_elems =
   let open Jib_ssa in
   function
   | CF_start inits ->
@@ -1622,7 +1627,7 @@ module Make_optimizer(S : Sequence) = struct
          | None -> Hashtbl.add uses var 1
          end
       | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
-      | Fn (f, exps) ->
+      | Fn (_, exps) | Ctor (_, exps) ->
          List.iter uses_in_exp exps
       | Ite (cond, t, e) ->
          uses_in_exp cond; uses_in_exp t; uses_in_exp e
@@ -1646,19 +1651,20 @@ module Make_optimizer(S : Sequence) = struct
          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;
+      | Write_mem (_, _, active, wk, addr, _, data, _) as def ->
+         uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data;
          Stack.push def stack'
-      | Write_mem_ea (_, wk, addr, _, data_size, _) as def ->
-         uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size;
+      | Write_mem_ea (_, _, active, wk, addr, _, data_size, _) as def ->
+         uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size;
          Stack.push def stack'
-      | Read_mem (_, _, rk, addr, _) as def ->
-         uses_in_exp rk; uses_in_exp addr;
+      | Read_mem (_, _, active, _, rk, addr, _) as def ->
+         uses_in_exp active; uses_in_exp rk; uses_in_exp addr;
          Stack.push def stack'
-      | Barrier (_, bk) as def ->
-         uses_in_exp bk;
+      | Barrier (_, _, active, bk) as def ->
+         uses_in_exp active; uses_in_exp bk;
          Stack.push def stack'
-      | Excl_res _ as def ->
+      | Excl_res (_, _, active) as def ->
+         uses_in_exp active;
          Stack.push def stack'
       | Assert exp as def ->
          uses_in_exp exp;
@@ -1668,35 +1674,46 @@ module Make_optimizer(S : Sequence) = struct
     Stack.fold remove_unused () stack;
 
     let vars = Hashtbl.create (Stack.length stack') in
+    let kinds = Hashtbl.create (Stack.length stack') in
     let seq = S.create () in
 
     let constant_propagate = function
       | Declare_const _ as def ->
          S.add def seq
       | Define_const (var, typ, exp) ->
-         begin match Hashtbl.find_opt uses var, simp_smt_exp vars exp with
+         let exp = simp_smt_exp vars kinds exp in
+         begin match Hashtbl.find_opt uses var, simp_smt_exp vars kinds exp with
          | _, (Bin _ | Bool_lit _) ->
             Hashtbl.add vars var exp
          | _, Var _ when !opt_propagate_vars ->
             Hashtbl.add vars var exp
+         | _, (Ctor (str, _)) ->
+            Hashtbl.add kinds var str;
+            S.add (Define_const (var, typ, exp)) seq
          | Some 1, _ ->
             Hashtbl.add vars var exp
          | Some _, exp ->
             S.add (Define_const (var, typ, exp)) seq
          | None, _ -> assert false
          end
-      | Write_mem (name, wk, addr, addr_ty, data, data_ty) ->
-         S.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data, data_ty)) seq
-      | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) ->
-         S.add (Write_mem_ea (name, simp_smt_exp vars wk, simp_smt_exp vars addr, addr_ty, simp_smt_exp vars data_size, data_size_ty)) seq
-      | Read_mem (name, typ, rk, addr, addr_typ) ->
-         S.add (Read_mem (name, typ, simp_smt_exp vars rk, simp_smt_exp vars addr, addr_typ)) seq
-      | Barrier (name, bk) ->
-         S.add (Barrier (name, simp_smt_exp vars bk)) seq
-      | Excl_res name ->
-         S.add (Excl_res name) seq
+      | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) ->
+         S.add (Write_mem (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk,
+                           simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data, data_ty))
+               seq
+      | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) ->
+         S.add (Write_mem_ea (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk,
+                              simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data_size, data_size_ty))
+               seq
+      | Read_mem (name, node, active, typ, rk, addr, addr_typ) ->
+         S.add (Read_mem (name, node, simp_smt_exp vars kinds active, typ, simp_smt_exp vars kinds rk,
+                          simp_smt_exp vars kinds addr, addr_typ))
+               seq
+      | Barrier (name, node, active, bk) ->
+         S.add (Barrier (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds bk)) seq
+      | Excl_res (name, node, active) ->
+         S.add (Excl_res (name, node, simp_smt_exp vars kinds active)) seq
       | Assert exp ->
-         S.add (Assert (simp_smt_exp vars exp)) seq
+         S.add (Assert (simp_smt_exp vars kinds exp)) seq
       | (Declare_datatypes _ | Declare_tuple _) as def ->
          S.add def seq
       | Define_fun _ -> assert false
@@ -1817,18 +1834,18 @@ let smt_instr_list name ctx all_cdefs instrs =
   List.iter (fun n ->
       begin match get_vertex cfg n with
       | None -> ()
-      | Some ((ssanodes, cfnode), preds, succs) ->
+      | Some ((ssa_elems, cfnode), preds, succs) ->
          let muxers =
-           ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat
+           ssa_elems |> 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
+         let ctx = { ctx with node = n; pathcond = lazy (get_pathcond n cfg ctx) } in
+         let basic_block = smt_cfnode all_cdefs ctx ssa_elems cfnode in
          push_smt_defs stack muxers;
-         push_smt_defs stack basic_block;
+         push_smt_defs stack basic_block
       end
     ) visit_order;
 
-  stack
+  stack, cfg
 
 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 ->
@@ -1855,7 +1872,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
           |> remove_pointless_goto
         in
 
-        let stack = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in
+        let stack, _ = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in
 
         let query = smt_query ctx pragma.query in
         push_smt_defs stack [Assert (Fn ("not", [query]))];
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index f6198a37..910388b6 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -52,6 +52,7 @@ open Ast
 open Ast_util
 open Jib
 open Jib_util
+open Jib_ssa
 open Smtlib
 
 val opt_ignore_overflow : bool ref
@@ -95,8 +96,9 @@ type ctx = {
        src/property.ml for the event types *)
     events : smt_exp Stack.t EventMap.t ref;
     (** When generating SMT for an instruction pathcond will contain
-       the global path conditional of the containing block in the
+       the global path conditional of the containing block/node in the
        control flow graph *)
+    node : int;
     pathcond : smt_exp Lazy.t;
     (** Set if we need to use strings or real numbers in the generated
        SMT, which then requires set-logic ALL or similar depending on
@@ -116,7 +118,7 @@ val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * ctx
 
 val smt_header : ctx -> cdef list -> smt_def list
 
-val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t
+val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * (ssa_elem list * cf_node) Jib_ssa.array_graph
 
 module type Sequence = sig
   type 'a t
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index dadb20fd..3357bc11 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -61,7 +61,7 @@ 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