SMT: Add struct value literals

Generates much better SMT that assigning each field one-by-one
starting with an undefined struct.

7 files changed, 52 insertions, 8 deletions

diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index b4837637..bc3314ec 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -153,7 +153,8 @@ type ctx =
     convert_typ : ctx -> typ -> ctyp;
     optimize_anf : ctx -> typ aexp -> typ aexp;
     specialize_calls : bool;
-    ignore_64 : bool
+    ignore_64 : bool;
+    struct_value : bool
   }
 
 let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env =
@@ -168,7 +169,8 @@ let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env =
     convert_typ = convert_typ;
     optimize_anf = optimize_anf;
     specialize_calls = false;
-    ignore_64 = false
+    ignore_64 = false;
+    struct_value = false
   }
 
 let ctyp_of_typ ctx typ = ctx.convert_typ ctx typ
@@ -248,6 +250,23 @@ let rec compile_aval l ctx = function
      [iclear tup_ctyp gs]
      @ cleanup
 
+  | AV_record (fields, typ) when ctx.struct_value ->
+     let ctyp = ctyp_of_typ ctx typ in
+     let gs = ngensym () in
+     let compile_fields (id, aval) =
+       let field_setup, cval, field_cleanup = compile_aval l ctx aval in
+       field_setup,
+       (id, cval),
+       field_cleanup
+     in
+     let field_triples = List.map compile_fields (Bindings.bindings fields) in
+     let setup = List.concat (List.map (fun (s, _, _) -> s) field_triples) in
+     let fields = List.map (fun (_, f, _) -> f) field_triples in
+     let cleanup = List.concat (List.map (fun (_, _, c) -> c) field_triples) in
+     [idecl ctyp gs],
+     V_struct (fields, ctyp),
+     [iclear ctyp gs]
+     
   | AV_record (fields, typ) ->
      let ctyp = ctyp_of_typ ctx typ in
      let gs = ngensym () in
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 12cd4a63..b9970733 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -84,7 +84,8 @@ type ctx =
     convert_typ : ctx -> typ -> ctyp;
     optimize_anf : ctx -> typ aexp -> typ aexp;
     specialize_calls : bool;
-    ignore_64 : bool
+    ignore_64 : bool;
+    struct_value : bool
   }
 
 val initial_ctx :
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index e0d7167f..eb7f5695 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -163,6 +163,7 @@ let rec cval_subst id subst = function
   | V_tuple_member (cval, len, n) -> V_tuple_member (cval_subst id subst cval, len, n)
   | V_ctor_kind (cval, ctor, unifiers, ctyp) -> V_ctor_kind (cval_subst id subst cval, ctor, unifiers, ctyp)
   | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> V_ctor_unwrap (ctor, cval_subst id subst cval, unifiers, ctyp)
+  | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> field, cval_subst id subst cval) fields, ctyp)
   | V_poly (cval, ctyp) -> V_poly (cval_subst id subst cval, ctyp)
 
 let rec instrs_subst id subst =
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 27a1a467..78de9069 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -191,6 +191,19 @@ let rec smt_cval env cval =
         Fn (zencode_upper_id struct_id ^ "_" ^ field, [smt_cval env union])
      | _ -> failwith "Field for non-struct type"
      end
+  | V_struct (fields, ctyp) ->
+     begin match ctyp with
+     | CT_struct (struct_id, field_ctyps) ->
+        let set_field (field, cval) =
+          match Util.assoc_compare_opt Id.compare field field_ctyps with
+          | None -> failwith "Field type not found"
+          | Some ctyp when ctyp_equal (cval_ctyp cval) ctyp ->
+             smt_cval env cval
+          | _ -> failwith "Type mismatch when generating struct for SMT"
+        in
+        Fn (zencode_upper_id struct_id, List.map set_field fields)
+     | _ -> failwith "Struct does not have struct type"
+     end 
   | V_tuple_member (frag, len, n) ->
      Fn (Printf.sprintf "tup_%d_%d" len n, [smt_cval env frag])
   | cval -> failwith ("Unrecognised cval " ^ string_of_cval ~zencode:false cval)
@@ -440,9 +453,6 @@ let builtin_shift shiftop env vbits vshift ret_ctyp =
 
 let builtin_not_bits env v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
-  | CT_fbits _, CT_fbits _ ->
-     Fn ("bvnot", [smt_cval env v])
-
   | CT_lbits _, CT_fbits (n, _) ->
      bvnot (Extract (n - 1, 0, Fn ("contents", [smt_cval env v])))
 
@@ -1341,7 +1351,7 @@ let generate_smt props name_file env ast =
         env
     in
     let t = Profile.start () in
-    let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true } ast in
+    let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true; struct_value = true } ast in
     Profile.finish "Compiling to Jib IR" t;
 
     smt_cdefs props name_file env cdefs cdefs
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 79c5910e..92cfe03b 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -509,6 +509,7 @@ let rename_variables graph root children =
     | V_tuple_member (f, len, n) -> V_tuple_member (fold_cval f, len, n)
     | V_ctor_kind (f, ctor, unifiers, ctyp) -> V_ctor_kind (fold_cval f, ctor, unifiers, ctyp)
     | V_ctor_unwrap (ctor, f, unifiers, ctyp) -> V_ctor_unwrap (ctor, fold_cval f, unifiers, ctyp)
+    | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> field, fold_cval cval) fields, ctyp)
     | V_poly (f, ctyp) -> V_poly (fold_cval f, ctyp)
   in
 
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index c04564a5..d9edd9c4 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -169,6 +169,8 @@ let rec cval_rename from_id to_id = function
   | V_ctor_unwrap (ctor, f, unifiers, ctyp) -> V_ctor_unwrap (ctor, cval_rename from_id to_id f, unifiers, ctyp)
   | V_hd cval -> V_hd (cval_rename from_id to_id cval)
   | V_tl cval -> V_tl (cval_rename from_id to_id cval)
+  | V_struct (fields, ctyp) ->
+     V_struct (List.map (fun (field, cval) -> field, cval_rename from_id to_id cval) fields, ctyp)
   | V_poly (f, ctyp) -> V_poly (cval_rename from_id to_id f, ctyp)
 
 let rec clexp_rename from_id to_id = function
@@ -305,6 +307,9 @@ let rec string_of_cval ?zencode:(zencode=true) = function
      Printf.sprintf "%s.%s"
        (string_of_cval' ~zencode:zencode f)
        (Util.zencode_string (string_of_id ctor))
+  | V_struct (fields, _) ->
+     Printf.sprintf "{%s}"
+       (Util.string_of_list ", " (fun (field, cval) -> string_of_id field ^ " = " ^ string_of_cval' ~zencode:zencode cval) fields)
   | V_ctor_unwrap (ctor, f, unifiers, _) ->
      Printf.sprintf "%s.%s"
        (string_of_cval' ~zencode:zencode f)
@@ -755,6 +760,7 @@ let rec map_cval_ctyp f = function
      V_field (map_cval_ctyp f cval, field)
   | V_hd cval -> V_hd (map_cval_ctyp f cval)
   | V_tl cval -> V_tl (map_cval_ctyp f cval)
+  | V_struct (fields, ctyp) -> V_struct (List.map (fun (id, cval) -> id, map_cval_ctyp f cval) fields, f ctyp)
   | V_poly (cval, ctyp) -> V_poly (map_cval_ctyp f cval, f ctyp)
 
 
@@ -933,6 +939,7 @@ and cval_ctyp = function
         end
      | ctyp -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Inavlid type for V_field " ^ full_string_of_ctyp ctyp)
      end
+  | V_struct (fields, ctyp) -> ctyp
   | V_call (op, vs) -> infer_call vs op
 
 let rec clexp_ctyp = function
diff --git a/src/smtlib.ml b/src/smtlib.ml
index aa7a4e19..abac05f2 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -123,6 +123,11 @@ let rec simp_fn = function
   | Fn ("not", [Fn ("not", [exp])]) -> exp
   | exp -> exp
 
+let rec simp_ite = function
+  | Ite (cond, Bool_lit true, Bool_lit false) -> cond
+  | Ite (_, Var v, Var v') when v = v' -> Var v
+  | exp -> exp
+         
 let rec simp_smt_exp vars = function
   | Var v -> 
      begin match Hashtbl.find_opt vars v with
@@ -137,7 +142,7 @@ let rec simp_smt_exp vars = function
      let cond = simp_smt_exp vars cond in
      let t = simp_smt_exp vars t in
      let e = simp_smt_exp vars e in
-     Ite (cond, t, e)
+     simp_ite (Ite (cond, t, e))
   | Extract (i, j, exp) ->
      let exp = simp_smt_exp vars exp in
      Extract (i, j, exp)