SMT: Support generic vectors and handle lets between specs and functions

If we have e.g.

$property
val prop : ...

let X = 0

function prop(...) = X == ...

then we need to ensure that let X is included when we generate the
property.

7 files changed, 108 insertions, 12 deletions

diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 3edd2cd7..77f220dd 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -167,6 +167,20 @@ let aexp_typ (AE_aux (aux, _, _)) =
   match aux with
   | AE_val aval -> aval_typ aval
   | AE_app (_, _, typ) -> typ
+  | AE_cast (_, typ) -> typ
+  | AE_assign _ -> unit_typ
+  | AE_let (_, _, _, _, _, typ) -> typ
+  | AE_block (_, _, typ) -> typ
+  | AE_return (_, typ) -> typ
+  | AE_throw (_, typ) -> typ
+  | AE_if (_, _, _, typ) -> typ
+  | AE_field (_, _, typ) -> typ
+  | AE_case (_, _, typ) -> typ
+  | AE_try (_, _, typ) -> typ
+  | AE_record_update (_, _, typ) -> typ
+  | AE_for _ -> unit_typ
+  | AE_loop _ -> unit_typ
+  | AE_short_circuit _ -> bool_typ
 
 let rec aval_rename from_id to_id = function
   | AV_lit (lit, typ) -> AV_lit (lit, typ)
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 0fe986e4..41684b73 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -198,6 +198,7 @@ let rec is_stack_ctyp ctyp = match ctyp with
   | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
   | CT_ref ctyp -> true
   | CT_poly -> true
+  | CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64)
 
 let is_stack_typ ctx typ = is_stack_ctyp (ctyp_of_typ ctx typ)
 
@@ -1116,6 +1117,7 @@ let rec sgen_ctyp = function
   | CT_real -> "real"
   | CT_ref ctyp -> sgen_ctyp ctyp ^ "*"
   | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *)
+  | CT_constant _ -> "CONSTANT"
 
 let rec sgen_ctyp_name = function
   | CT_unit -> "unit"
@@ -1136,6 +1138,7 @@ let rec sgen_ctyp_name = function
   | CT_real -> "real"
   | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp
   | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *)
+  | CT_constant _ -> "CONSTANT"
 
 let sgen_cval cval = string_of_cval cval
 
@@ -1159,6 +1162,7 @@ let rec sgen_clexp = function
   | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")"
   | CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))"
   | CL_void -> assert false
+  | CL_rmw _ -> assert false
 
 let rec sgen_clexp_pure = function
   | CL_id (Have_exception _, _) -> "have_exception"
@@ -1169,6 +1173,7 @@ let rec sgen_clexp_pure = function
   | CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n
   | CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))"
   | CL_void -> assert false
+  | CL_rmw _ -> assert false
 
 (** Generate instructions to copy from a cval to a clexp. This will
    insert any needed type conversions from big integers to small
@@ -1947,7 +1952,7 @@ let rec ctyp_dependencies = function
   | CT_ref ctyp -> ctyp_dependencies ctyp
   | CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
   | CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
-  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly -> []
+  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly | CT_constant _ -> []
 
 let codegen_ctg ctx = function
   | CTG_vector (direction, ctyp) -> codegen_vector ctx (direction, ctyp)
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 76239b35..14f9cc18 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -67,6 +67,8 @@ let lbits_size () = Util.power 2 !lbits_index
 
 let lint_size = ref 128
 
+let vector_index = ref 5
+
 let smt_unit = mk_enum "Unit" ["Unit"]
 let smt_lbits = mk_record "Bits" [("size", Bitvec !lbits_index); ("bits", Bitvec (lbits_size ()))]
 
@@ -96,7 +98,7 @@ let rec smt_ctyp = function
   | CT_variant (id, ctors) ->
      mk_variant (zencode_upper_id id) (List.map (fun (id, ctyp) -> (zencode_id id, smt_ctyp ctyp)) ctors)
   | CT_tup ctyps -> Tuple (List.map smt_ctyp ctyps)
-  | CT_vector (_, ctyp) -> Array (Bitvec 8, smt_ctyp ctyp)
+  | CT_vector (_, ctyp) -> Array (Bitvec !vector_index, smt_ctyp ctyp)
   | CT_string -> Bitvec 64
   | ctyp -> failwith ("Unhandled ctyp: " ^ string_of_ctyp ctyp)
 
@@ -557,7 +559,12 @@ let builtin_vector_access env vec i ret_ctyp =
   | CT_fbits (n, _), CT_constant i, CT_bit ->
      Extract (Big_int.to_int i, Big_int.to_int i, smt_cval env vec)
 
-  | _ -> failwith "Cannot compile vector subrange"
+  | CT_vector _, CT_constant i, _ ->
+     Fn ("select", [smt_cval env vec; bvint !vector_index i])
+  | CT_vector _, index_ctyp, _ ->
+     Fn ("select", [smt_cval env vec; force_size !vector_index (int_size index_ctyp) (smt_cval env i)])
+
+  | _ -> builtin_type_error "vector_access" [vec; i] (Some ret_ctyp)
 
 let builtin_vector_update env vec i x ret_ctyp =
   match cval_ctyp vec, cval_ctyp i, cval_ctyp x, ret_ctyp with
@@ -575,7 +582,12 @@ let builtin_vector_update env vec i x ret_ctyp =
      let top = Extract (n - 1, 1, smt_cval env vec) in
      Fn ("concat", [top; smt_cval env x])
 
-  | _ -> failwith "Cannot compile vector update"
+  | CT_vector _, CT_constant i, ctyp, CT_vector _ ->
+     Fn ("store", [smt_cval env vec; bvint !vector_index i; smt_cval env x])
+  | CT_vector _, index_ctyp, _, CT_vector _ ->
+     Fn ("store", [smt_cval env vec; force_size !vector_index (int_size index_ctyp) (smt_cval env i); smt_cval env x])
+
+  | _ -> builtin_type_error "vector_update" [vec; i; x] (Some ret_ctyp)
 
 let builtin_unsigned env v ret_ctyp =
   match cval_ctyp v, ret_ctyp with
@@ -1223,12 +1235,19 @@ let smt_cfnode all_cdefs env =
   (* We can ignore any non basic-block/start control-flow nodes *)
   | _ -> []
 
-let rec find_function id = function
+(** When we generate a property for a CDEF_spec, we find it's
+   associated function body in a CDEF_fundef node. However, we must
+   keep track of any global letbindings between the spec and the
+   fundef, so they can appear in the generated SMT. *)
+let rec find_function lets id = function
   | CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 ->
-     Some (heap_return, args, body)
+     lets, Some (heap_return, args, body)
+  | CDEF_let (_, vars, setup) :: cdefs ->
+     let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in
+     find_function (lets @ vars @ setup) id cdefs;
   | _ :: cdefs ->
-     find_function id cdefs
-  | [] -> None
+     find_function lets id cdefs
+  | [] -> lets, None
 
 let optimize_smt stack =
   let stack' = Stack.create () in
@@ -1313,8 +1332,8 @@ let smt_header stack cdefs =
 
 let smt_cdef props lets name_file env 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
-     | Some (None, args, instrs) ->
+     begin match find_function [] function_id all_cdefs with
+     | intervening_lets, Some (None, args, instrs) ->
         let prop_type, prop_args, pragma_l, vs = Bindings.find function_id props in
 
         let stack = Stack.create () in
@@ -1327,7 +1346,7 @@ let smt_cdef props lets name_file env all_cdefs = function
 
         let instrs =
           let open Jib_optimize in
-          (lets @ instrs)
+          (lets @ intervening_lets @ instrs)
           |> inline all_cdefs (fun _ -> true)
           |> flatten_instrs
           |> remove_unused_labels
@@ -1379,7 +1398,6 @@ let rec smt_cdefs props lets name_file env ast =
   function
   | CDEF_let (_, vars, setup) :: cdefs ->
      let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in
-     print_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr (vars @ setup)));
      smt_cdefs props (lets @ vars @ setup) name_file env ast cdefs;
   | cdef :: cdefs ->
      smt_cdef props lets name_file env ast cdef;
diff --git a/test/smt/foreach_simple_2.unsat.sail b/test/smt/foreach_simple_2.unsat.sail
new file mode 100644
index 00000000..ce466044
--- /dev/null
+++ b/test/smt/foreach_simple_2.unsat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+let C = 0
+
+$property
+function prop() -> bool = {
+  let n = 3;
+  bv = 0x0;
+  foreach (i from C to n) {
+    bv[i] = bitone
+  };
+  bv == 0xF
+}
diff --git a/test/smt/gvector.unsat.sail b/test/smt/gvector.unsat.sail
new file mode 100644
index 00000000..23054765
--- /dev/null
+++ b/test/smt/gvector.unsat.sail
@@ -0,0 +1,15 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : vector(32, dec, vector(32, dec, bit))
+
+type is_reg('n: Int) -> Bool = 0 <= 'n <= 31
+
+$property
+function prop forall 'n, is_reg('n). (n: int('n)) -> bool = {
+  foreach (i from 0 to 31) {
+    R[i] = 0xDEAD_BEEF;
+  };
+  R[n] == 0xDEAD_BEEF
+}
\ No newline at end of file
diff --git a/test/smt/gvector_trivial.unsat.sail b/test/smt/gvector_trivial.unsat.sail
new file mode 100644
index 00000000..37a4fbed
--- /dev/null
+++ b/test/smt/gvector_trivial.unsat.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : vector(32, dec, vector(32, dec, bit))
+
+$property
+function prop() -> bool = {
+  R[0] = 0xDEAD_BEEF;
+  R[0] == 0xDEAD_BEEF
+}
\ No newline at end of file
diff --git a/test/smt/let_intervene.unsat.sail b/test/smt/let_intervene.unsat.sail
new file mode 100644
index 00000000..5494848b
--- /dev/null
+++ b/test/smt/let_intervene.unsat.sail
@@ -0,0 +1,18 @@
+default Order dec
+
+$include <prelude.sail>
+
+$property
+val prop : unit -> bool
+
+let C = 0
+let x = bitone
+
+function prop() = {
+  let n = 3;
+  bv = 0x0;
+  foreach (i from C to n) {
+    bv[i] = x
+  };
+  bv == 0xF
+}