Fix Sail->SMT generation for struct values

src/lib/smt_exp.ml

@@ -106,6 +106,7 @@ type smt_exp =
  | Tester of string * smt_exp
  | Unwrap of Ast.id * bool * smt_exp
  | Field of Ast.id * Ast.id * smt_exp
+ | Struct of Ast.id * (Ast.id * smt_exp) list
  | Store of smt_array_info * string * smt_exp * smt_exp * smt_exp
  | Empty_list
  | Hd of string * smt_exp
@@ -126,6 +127,8 @@ let rec fold_smt_exp f = function
  f (Store (info, store_fn, fold_smt_exp f arr, fold_smt_exp f index, fold_smt_exp f x))
  | Hd (hd_op, xs) -> f (Hd (hd_op, fold_smt_exp f xs))
  | Tl (tl_op, xs) -> f (Tl (tl_op, fold_smt_exp f xs))
+ | Struct (struct_id, fields) ->
+ f (Struct (struct_id, List.map (fun (field_id, exp) -> (field_id, fold_smt_exp f exp)) fields))
  | (Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Var _ | Unit | Member _ | Empty_list) as exp -> f exp
 
 let extract i j x = Extract (i, j, x)
@@ -725,6 +728,8 @@ and simp simpset exp =
  | Tester (ctor, exp) -> Tester (ctor, simp simpset exp)
  | Unwrap (ctor, b, exp) -> Unwrap (ctor, b, simp simpset exp)
  | Field (struct_id, field_id, exp) -> Field (struct_id, field_id, simp simpset exp)
+ | Struct (struct_id, fields) ->
+ Struct (struct_id, List.map (fun (field_id, exp) -> (field_id, simp simpset exp)) fields)
  | Empty_list | Bool_lit _ | Bitvec_lit _ | Real_lit _ | String_lit _ | Unit | Member _ | Hd _ | Tl _ -> exp
 
 type smt_def =
@@ -768,6 +773,8 @@ let rec pp_smt_exp =
  | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
  | Field (struct_id, field_id, exp) ->
  parens (string (zencode_upper_id struct_id ^ "_" ^ zencode_id field_id) ^^ space ^^ pp_smt_exp exp)
+ | Struct (struct_id, fields) ->
+ parens (string (zencode_upper_id struct_id) ^^ space ^^ separate_map space (fun (_, exp) -> pp_smt_exp exp) fields)
  | Unwrap (ctor, _, exp) -> parens (string ("un" ^ zencode_id ctor) ^^ space ^^ pp_smt_exp exp)
  | Ite (cond, then_exp, else_exp) ->
  parens (separate space [string "ite"; pp_smt_exp cond; pp_smt_exp then_exp; pp_smt_exp else_exp])

src/lib/smt_gen.ml

@@ -383,14 +383,34 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct
  let union_ctyp = cval_ctyp union in
  let* union = smt_cval union in
  return (Unwrap (ctor, Config.union_ctyp_classify union_ctyp, union))
- | V_field (record, field) -> begin
+ | V_field (record, field) -> (
  match cval_ctyp record with
  | CT_struct (struct_id, _) ->
  let* record = smt_cval record in
  return (Field (struct_id, field, record))
- | _ -> failwith "Field for non-struct type"
- end
- | cval -> return (Var (Name (mk_id "UNKNOWN", -1))) (* failwith ("Unrecognised cval " ^ string_of_cval cval) *)
+ | _ ->
+ let* l = current_location in
+ Reporting.unreachable l __POS__ "Field for non-struct type found"
+ )
+ | V_struct (fields, ctyp) -> (
+ match ctyp with
+ | CT_struct (struct_id, _) ->
+ let* fields =
+ mapM
+ (fun (field_id, field) ->
+ let* field = smt_cval field in
+ return (field_id, field)
+ )
+ fields
+ in
+ return (Struct (struct_id, fields))
+ | _ ->
+ let* l = current_location in
+ Reporting.unreachable l __POS__ "Struct literal with non-struct type found"
+ )
+ | V_tuple _ | V_tuple_member _ ->
+ let* l = current_location in
+ Reporting.unreachable l __POS__ "Found tuple value, which should have been removed before SMT generation"
  )
 
  (* [bvzeint esz cval] (BitVector Zero Extend INTeger), takes a cval

src/sail_smt_backend/jib_smt.ml

@@ -144,6 +144,7 @@ module Make_optimizer (S : Sequence) = struct
  uses_in_exp arr;
  uses_in_exp index;
  uses_in_exp x
+ | Struct (_, fields) -> List.iter (fun (_, field) -> uses_in_exp field) fields
  in
 
  let remove_unused () = function

src/sail_sv_backend/sv_ir.ml

@@ -206,6 +206,9 @@ let rec visit_smt_exp (vis : svir_visitor) outer_smt_exp =
  | Field (struct_id, field_id, exp) ->
  let exp' = visit_smt_exp vis exp in
  if exp == exp' then no_change else Field (struct_id, field_id, exp')
+ | Struct (struct_id, fields) ->
+ let fields' = map_no_copy (fun (field_id, exp) -> (field_id, visit_smt_exp vis exp)) fields in
+ if fields == fields' then no_change else Struct (struct_id, fields)
  | Fn (f, args) ->
  let args' = map_no_copy (visit_smt_exp vis) args in
  if args == args' then no_change else Fn (f, args')

test/smt/struct_prop.unsat.sail

@@ -0,0 +1,6 @@
+struct MyStruct = { f : bool }
+
+let my_struct : MyStruct = struct { f = true }
+
+$property
+function prop() -> bool = my_struct.f