Backport fixes to SMT generation from poly_mapping branch

1 files changed, 248 insertions, 95 deletions

diff --git a/src/smtlib.ml b/src/smtlib.ml
index 06386f61..e12657c3 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -60,6 +60,30 @@ type smt_typ =
   | Tuple of smt_typ list
   | Array of smt_typ * smt_typ
 
+let rec smt_typ_compare t1 t2 =
+  match t1, t2 with
+  | Bitvec n, Bitvec m -> compare n m
+  | Bool, Bool -> 0
+  | String, String -> 0
+  | Real, Real -> 0
+  | Datatype (name1, _), Datatype (name2, _) -> String.compare name1 name2
+  | Tuple ts1, Tuple ts2 -> Util.lex_ord_list smt_typ_compare ts1 ts2
+  | Array (t11, t12), Array (t21, t22) ->
+     let c = smt_typ_compare t11 t21 in
+     if c = 0 then smt_typ_compare t12 t22 else c
+  | Bitvec _, _ -> 1
+  | _, Bitvec _ -> -1
+  | Bool, _ -> 1
+  | _, Bool -> -1
+  | String, _ -> 1
+  | _, String -> -1
+  | Real, _ -> 1
+  | _, Real -> -1
+  | Datatype _, _ -> 1
+  | _, Datatype _ -> -1
+  | Tuple _, _ -> 1
+  | _, Tuple _ -> -1
+
 let rec smt_typ_equal t1 t2 =
   match t1, t2 with
   | Bitvec n, Bitvec m -> n = m
@@ -89,11 +113,11 @@ let mk_variant name ctors =
 
 type smt_exp =
   | Bool_lit of bool
-  | Hex of string
-  | Bin of string
+  | Bitvec_lit of Sail2_values.bitU list
   | Real_lit of string
   | String_lit of string
   | Var of string
+  | Shared of string
   | Read_res of string
   | Enum of string
   | Fn of string * smt_exp list
@@ -102,6 +126,11 @@ type smt_exp =
   | SignExtend of int * smt_exp
   | Extract of int * int * smt_exp
   | Tester of string * smt_exp
+  | Syntactic of smt_exp * smt_exp list
+  | Struct of string * (string * smt_exp) list
+  | Field of string * smt_exp
+  (* Used by sail-axiomatic, should never be generated by sail -smt! *)
+  | Forall of (string * smt_typ) list * smt_exp
 
 let rec fold_smt_exp f = function
   | Fn (name, args) -> f (Fn (name, List.map (fold_smt_exp f) args))
@@ -110,7 +139,11 @@ let rec fold_smt_exp f = function
   | SignExtend (n, exp) -> f (SignExtend (n, fold_smt_exp f exp))
   | Extract (n, m, exp) -> f (Extract (n, m, fold_smt_exp f exp))
   | Tester (ctor, exp) -> f (Tester (ctor, fold_smt_exp f exp))
-  | (Bool_lit _ | Hex _ | Bin _ | Real_lit _ | String_lit _ | Var _ | Read_res _ | Enum _ as exp) -> f exp
+  | Forall (binders, exp) -> f (Forall (binders, fold_smt_exp f exp))
+  | Syntactic (exp, exps) -> f (Syntactic (fold_smt_exp f exp, List.map (fold_smt_exp f) exps))
+  | Field (name, exp) -> f (Field (name, fold_smt_exp f exp))
+  | Struct (name, fields) -> f (Struct (name, List.map (fun (field, exp) -> field, fold_smt_exp f exp) fields))
+  | (Bool_lit _ | Bitvec_lit  _ | Real_lit _ | String_lit _ | Var _ | Shared _ | Read_res _ | Enum _ as exp) -> f exp
 
 let smt_conj = function
   | [] -> Bool_lit true
@@ -136,21 +169,13 @@ let bvshl x y  = Fn ("bvshl", [x; y])
 let bvlshr x y = Fn ("bvlshr", [x; y])
 let bvult x y  = Fn ("bvult", [x; y])
 
-let bvzero n =
-  if n mod 4 = 0 then
-    Hex (String.concat "" (Util.list_init (n / 4) (fun _ -> "0")))
-  else
-    Bin (String.concat "" (Util.list_init n (fun _ -> "0")))
+let bvzero n = Bitvec_lit (Sail2_operators_bitlists.zeros (Big_int.of_int n))
 
-let bvones n =
-  if n mod 4 = 0 then
-    Hex (String.concat "" (Util.list_init (n / 4) (fun _ -> "F")))
-  else
-    Bin (String.concat "" (Util.list_init n (fun _ -> "1")))
+let bvones n = Bitvec_lit (Sail2_operators_bitlists.ones (Big_int.of_int n))
 
 let simp_equal x y =
   match x, y with
-  | Bin str1, Bin str2 -> Some (str1 = str2)
+  | Bitvec_lit bv1, Bitvec_lit bv2 -> Some (Sail2_operators_bitlists.eq_vec bv1 bv2)
   | _, _ -> None
 
 let simp_and xs =
@@ -175,6 +200,16 @@ let simp_or xs =
      else
        Fn ("or", xs)
 
+let rec all_bitvec_lit = function
+  | Bitvec_lit _ :: rest -> all_bitvec_lit rest
+  | [] -> true
+  | _ :: _ -> false
+
+let rec merge_bitvec_lit = function
+  | Bitvec_lit b :: rest -> b @ merge_bitvec_lit rest
+  | [] -> []
+  | _ :: _ -> assert false
+
 let simp_fn = function
   | Fn ("not", [Fn ("not", [exp])]) -> exp
   | Fn ("not", [Bool_lit b]) -> Bool_lit (not b)
@@ -184,6 +219,9 @@ let simp_fn = function
   | Fn ("and", xs) -> simp_and xs
   | Fn ("=>", [Bool_lit true; y]) -> y
   | Fn ("=>", [Bool_lit false; y]) -> Bool_lit true
+  | Fn ("bvsub", [Bitvec_lit bv1; Bitvec_lit bv2]) -> Bitvec_lit (Sail2_operators_bitlists.sub_vec bv1 bv2)
+  | Fn ("bvadd", [Bitvec_lit bv1; Bitvec_lit bv2]) -> Bitvec_lit (Sail2_operators_bitlists.add_vec bv1 bv2)
+  | Fn ("concat", xs) when all_bitvec_lit xs -> Bitvec_lit (merge_bitvec_lit xs)
   | Fn ("=", [x; y]) as exp ->
      begin match simp_equal x y with
      | Some b -> Bool_lit b
@@ -205,7 +243,16 @@ let rec simp_smt_exp vars kinds = function
      | Some exp -> simp_smt_exp vars kinds exp
      | None -> Var v
      end
-  | (Read_res _ | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
+  | (Read_res _ | Shared _ | Enum _ | Bitvec_lit _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp
+  | Field (field, exp) ->
+     let exp = simp_smt_exp vars kinds exp in
+     begin match exp with
+     | Struct (_, fields) ->
+        List.assoc field fields
+     | _ -> Field (field, exp)
+     end
+  | Struct (name, fields) ->
+     Struct (name, List.map (fun (field, exp) -> field, simp_smt_exp vars kinds exp) fields)
   | Fn (f, exps) ->
      let exps = List.map (simp_smt_exp vars kinds) exps in
      simp_fn (Fn (f, exps))
@@ -220,8 +267,8 @@ let rec simp_smt_exp vars kinds = function
   | Extract (i, j, exp) ->
      let exp = simp_smt_exp vars kinds exp in
      begin match exp with
-     | Bin str ->
-        Bin (String.sub str ((String.length str - 1) - i) ((i + 1) - j))
+     | Bitvec_lit bv ->
+        Bitvec_lit (Sail2_operators_bitlists.subrange_vec_dec bv (Big_int.of_int i) (Big_int.of_int j))
      | _ -> Extract (i, j, exp)
      end
   | Tester (str, exp) ->
@@ -235,48 +282,167 @@ let rec simp_smt_exp vars kinds = function
         end
      | _ -> Tester (str, exp)
      end
+  | Syntactic (exp, _) -> exp
   | SignExtend (i, exp) ->
      let exp = simp_smt_exp vars kinds exp in
-     SignExtend (i, exp)
+     begin match exp with
+     | Bitvec_lit bv ->
+        Bitvec_lit (Sail2_operators_bitlists.sign_extend bv (Big_int.of_int (i + List.length bv)))
+     | _ -> SignExtend (i, exp)
+     end
+  | Forall (binders, exp) -> Forall (binders, exp)
+
+type read_info = {
+    name : string;
+    node : int;
+    active : smt_exp;
+    kind : smt_exp;
+    addr_type : smt_typ;
+    addr : smt_exp;
+    ret_type : smt_typ;
+    doc : string
+  }
+
+type write_info = {
+    name : string;
+    node : int;
+    active  : smt_exp;
+    kind : smt_exp;
+    addr_type : smt_typ;
+    addr : smt_exp;
+    data_type : smt_typ;
+    data : smt_exp;
+    doc : string
+  }
+
+type barrier_info = {
+    name : string;
+    node : int;
+    active : smt_exp;
+    kind : smt_exp;
+    doc : string
+  }
+
+type branch_info = {
+    name : string;
+    node : int;
+    active : smt_exp;
+    addr_type : smt_typ;
+    addr : smt_exp;
+    doc : string
+  }
+
+type cache_op_info = {
+    name : string;
+    node : int;
+    active : smt_exp;
+    kind : smt_exp;
+    addr_type : smt_typ;
+    addr : smt_exp;
+    doc : string
+  }
 
 type smt_def =
   | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
+  | Declare_fun of string * smt_typ list * smt_typ
   | Declare_const of string * smt_typ
   | Define_const of string * smt_typ * smt_exp
-  | Write_mem of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
+  (* Same as Define_const, but it'll never be removed by simplification *)
+  | Preserve_const of string * smt_typ * smt_exp
+  | Write_mem of write_info
   | Write_mem_ea of string * int * smt_exp * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
-  | Read_mem of string * int * smt_exp * smt_typ * smt_exp * smt_exp * smt_typ
-  | Barrier of string * int * smt_exp * smt_exp
+  | Read_mem of read_info
+  | Barrier of barrier_info
+  | Branch_announce of branch_info
+  | Cache_maintenance of cache_op_info
   | Excl_res of string * int * smt_exp
   | Declare_datatypes of string * (string * (string * smt_typ) list) list
   | Declare_tuple of int
   | Assert of smt_exp
 
+let smt_def_map_exp f = function
+  | Define_fun (name, args, ty, exp) -> Define_fun (name, args, ty, f exp)
+  | Declare_fun (name, args, ty) -> Declare_fun (name, args, ty)
+  | Declare_const (name, ty) -> Declare_const (name, ty)
+  | Define_const (name, ty, exp) -> Define_const (name, ty, f exp)
+  | Preserve_const (name, ty, exp) -> Preserve_const (name, ty, f exp)
+  | Write_mem w -> Write_mem { w with active = f w.active; kind = f w.kind; addr = f w.addr; data = f w.data }
+  | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) ->
+     Write_mem_ea (name, node, f active, f wk, f addr, addr_ty, f data_size, data_size_ty)
+  | Read_mem r -> Read_mem { r with active = f r.active; kind = f r.kind; addr = f r.addr }
+  | Barrier b -> Barrier { b with active = f b.active; kind = f b.kind }
+  | Cache_maintenance m -> Cache_maintenance { m with active = f m.active; kind = f m.kind ; addr = f m.addr }
+  | Branch_announce c -> Branch_announce { c with active = f c.active; addr = f c.addr }
+  | Excl_res (name, node, active) -> Excl_res (name, node, f active)
+  | Declare_datatypes (name, ctors) -> Declare_datatypes (name, ctors)
+  | Declare_tuple n -> Declare_tuple n
+  | Assert exp -> Assert (f exp)
+
+let smt_def_iter_exp f = function
+  | Define_fun (name, args, ty, exp) -> f exp
+  | Define_const (name, ty, exp) -> f exp
+  | Preserve_const (name, ty, exp) -> f exp
+  | Write_mem w -> f w.active; f w.kind; f w.addr; f w.data
+  | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) ->
+     f active; f wk; f addr; f data_size
+  | Read_mem r -> f r.active; f r.kind; f r.addr
+  | Barrier b -> f b.active; f b.kind
+  | Cache_maintenance m -> f m.active; f m.kind; f m.addr
+  | Branch_announce c -> f c.active; f c.addr
+  | Excl_res (name, node, active) -> f active
+  | Assert exp -> f exp
+  | Declare_fun _ | Declare_const _ | Declare_tuple _ | Declare_datatypes _ -> ()
+
 let declare_datatypes = function
   | Datatype (name, ctors) -> Declare_datatypes (name, ctors)
   | _ -> assert false
 
+(** For generating SMT with multiple threads (i.e. for litmus tests),
+   we suffix all the variables in the generated SMT with a thread
+   identifier to avoid any name clashes between the two threads. *)
+
 let suffix_variables_exp sfx =
-  fold_smt_exp (function Var v -> Var (v ^ sfx) | exp -> exp)
+  fold_smt_exp (function Var v -> Var (v ^ sfx) | Read_res v -> Read_res (v ^ sfx) | exp -> exp)
+
+let suffix_variables_read_info sfx (r : read_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { r with name = r.name ^ sfx; active = suffix r.active; kind = suffix r.kind; addr = suffix r.addr }
+
+let suffix_variables_write_info sfx (w : write_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { w with name = w.name ^ sfx; active = suffix w.active; kind = suffix w.kind; addr = suffix w.addr; data = suffix w.data }
+
+let suffix_variables_barrier_info sfx (b : barrier_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { b with name = b.name ^ sfx; active = suffix b.active; kind = suffix b.kind }
+
+let suffix_variables_branch_info sfx (c : branch_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { c with name = c.name ^ sfx; active = suffix c.active; addr = suffix c.addr }
+
+let suffix_variables_cache_op_info sfx (m : cache_op_info) =
+  let suffix exp = suffix_variables_exp sfx exp in
+  { m with name = m.name ^ sfx; kind = suffix m.kind; active = suffix m.active; addr = suffix m.addr }
 
 let suffix_variables_def sfx = function
   | Define_fun (name, args, ty, exp) ->
      Define_fun (name ^ sfx, List.map (fun (arg, ty) -> sfx ^ arg, ty) args, ty, suffix_variables_exp sfx exp)
+  | Declare_fun (name, tys, ty) ->
+     Declare_fun (name ^ sfx, tys, ty)
   | Declare_const (name, ty) ->
      Declare_const (name ^ sfx, ty)
   | Define_const (name, ty, exp) ->
      Define_const (name ^ sfx, ty, suffix_variables_exp sfx exp)
-  | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) ->
-     Write_mem (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk,
-                suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data, data_ty)
+  | Preserve_const (name, ty, exp) ->
+     Preserve_const (name, ty, suffix_variables_exp sfx exp)
+  | Write_mem w -> Write_mem (suffix_variables_write_info sfx w)
   | Write_mem_ea (name, node, active , wk, addr, addr_ty, data_size, data_size_ty) ->
-     Write_mem (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk,
-                suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_ty)
-  | Read_mem (name, node, active, ty, rk, addr, addr_ty) ->
-     Read_mem (name ^ sfx, node, suffix_variables_exp sfx active, ty, suffix_variables_exp sfx rk,
-               suffix_variables_exp sfx addr, addr_ty)
-  | Barrier (name, node, active, bk) ->
-     Barrier (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx bk)
+     Write_mem_ea (name ^ sfx, node, suffix_variables_exp sfx active, suffix_variables_exp sfx wk,
+                   suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_ty)
+  | Read_mem r -> Read_mem (suffix_variables_read_info sfx r)
+  | Barrier b -> Barrier (suffix_variables_barrier_info sfx b)
+  | Cache_maintenance m -> Cache_maintenance (suffix_variables_cache_op_info sfx m)
+  | Branch_announce c -> Branch_announce (suffix_variables_branch_info sfx c)
   | Excl_res (name, node, active) ->
      Excl_res (name ^ sfx, node, suffix_variables_exp sfx active)
   | Declare_datatypes (name, ctors) ->
@@ -286,54 +452,37 @@ let suffix_variables_def sfx = function
   | Assert exp ->
      Assert (suffix_variables_exp sfx exp)
 
-let merge_datatypes defs1 defs2 =
-  let module StringSet = Set.Make(String) in
-  let datatype_name = function
-    | Declare_datatypes (name, _) -> name
-    | _ -> assert false
-  in
-  let names = List.fold_left (fun set def -> StringSet.add (datatype_name def) set) StringSet.empty defs1 in
-  defs1 @ List.filter (fun def -> not (StringSet.mem (datatype_name def) names)) defs2
-
-let merge_tuples defs1 defs2 =
-  let tuple_size = function
-    | Declare_tuple size -> size
-    | _ -> assert false
-  in
-  let names = List.fold_left (fun set def -> Util.IntSet.add (tuple_size def) set) Util.IntSet.empty defs1 in
-  defs1 @ List.filter (fun def -> not (Util.IntSet.mem (tuple_size def) names)) defs2
-
-let merge_smt_defs defs1 defs2 =
-  let is_tuple = function
-    | Declare_datatypes _ | Declare_tuple _ -> true
-    | _ -> false
-  in
-  let is_datatype = function
-    | Declare_datatypes _ | Declare_tuple _ -> true
-    | _ -> false
-  in
-  let datatypes1, body1 = List.partition is_datatype defs1 in
-  let datatypes2, body2 = List.partition is_datatype defs2 in
-  let tuples1, datatypes1 = List.partition is_tuple datatypes1 in
-  let tuples2, datatypes2 = List.partition is_tuple datatypes2 in
-  merge_tuples tuples1 tuples2 @ merge_datatypes datatypes1 datatypes2 @ body1 @ body2
-
 let pp_sfun str docs =
   let open PPrint in
   parens (separate space (string str :: docs))
 
+let rec pp_smt_typ =
+  let open PPrint in
+  function
+  | Bool -> string "Bool"
+  | String -> string "String"
+  | Real -> string "Real"
+  | Bitvec n -> string (Printf.sprintf "(_ BitVec %d)" n)
+  | Datatype (name, _) -> string name
+  | Tuple tys -> pp_sfun ("Tup" ^ string_of_int (List.length tys)) (List.map pp_smt_typ tys)
+  | Array (ty1, ty2) -> pp_sfun "Array" [pp_smt_typ ty1; pp_smt_typ ty2]
+
+let pp_str_smt_typ (str, ty) = let open PPrint in parens (string str ^^ space ^^ pp_smt_typ ty)
+
 let rec pp_smt_exp =
   let open PPrint in
   function
   | Bool_lit b -> string (string_of_bool b)
   | Real_lit str -> string str
   | String_lit str -> string ("\"" ^ str ^ "\"")
-  | Hex str -> string ("#x" ^ str)
-  | Bin str -> string ("#b" ^ str)
+  | Bitvec_lit bv -> string (Sail2_values.show_bitlist_prefix '#' bv)
   | Var str -> string str
+  | Shared str -> string str
   | Read_res str -> string (str ^ "_ret")
   | Enum str -> string str
   | Fn (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
+  | Field (str, exp) -> parens (string str ^^ space ^^ pp_smt_exp exp)
+  | Struct (str, fields) -> parens (string str ^^ space ^^ separate_map space (fun (_, exp) -> pp_smt_exp exp) fields)
   | Ctor (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps)
   | 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])
@@ -343,19 +492,9 @@ let rec pp_smt_exp =
      parens (string (Printf.sprintf "(_ is %s)" kind) ^^ space ^^ pp_smt_exp exp)
   | SignExtend (i, exp) ->
      parens (string (Printf.sprintf "(_ sign_extend %d)" i) ^^ space ^^ pp_smt_exp exp)
-
-let rec pp_smt_typ =
-  let open PPrint in
-  function
-  | Bool -> string "Bool"
-  | String -> string "String"
-  | Real -> string "Real"
-  | Bitvec n -> string (Printf.sprintf "(_ BitVec %d)" n)
-  | Datatype (name, _) -> string name
-  | Tuple tys -> pp_sfun ("Tup" ^ string_of_int (List.length tys)) (List.map pp_smt_typ tys)
-  | Array (ty1, ty2) -> pp_sfun "Array" [pp_smt_typ ty1; pp_smt_typ ty2]
-
-let pp_str_smt_typ (str, ty) = let open PPrint in string str ^^ space ^^ pp_smt_typ ty
+  | Syntactic (exp, _) -> pp_smt_exp exp
+  | Forall (binders, exp) ->
+     parens (string "forall" ^^ space ^^ parens (separate_map space pp_str_smt_typ binders) ^^ space ^^ pp_smt_exp exp)
 
 let pp_smt_def =
   let open PPrint in
@@ -367,18 +506,23 @@ let pp_smt_def =
              ^^ space ^^ pp_smt_typ ty
              ^//^ pp_smt_exp exp)
 
+  | Declare_fun (name, args, ty) ->
+     parens (string "declare-fun" ^^ space ^^ string name
+             ^^ space ^^ parens (separate_map space pp_smt_typ args)
+             ^^ space ^^ pp_smt_typ ty)
+
   | Declare_const (name, ty) ->
      pp_sfun "declare-const" [string name; pp_smt_typ ty]
 
-  | Define_const (name, ty, exp) ->
+  | Define_const (name, ty, exp) | Preserve_const (name, ty, exp) ->
      pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp]
 
-  | Write_mem (name, _, active, wk, addr, addr_ty, data, data_ty) ->
-     pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_data"); pp_smt_typ data_ty; pp_smt_exp data] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
-     ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ Bool]
+  | Write_mem w ->
+     pp_sfun "define-const" [string (w.name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp w.kind] ^^ hardline
+     ^^ pp_sfun "define-const" [string (w.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp w.active] ^^ hardline
+     ^^ pp_sfun "define-const" [string (w.name ^ "_data"); pp_smt_typ w.data_type; pp_smt_exp w.data] ^^ hardline
+     ^^ pp_sfun "define-const" [string (w.name ^ "_addr"); pp_smt_typ w.addr_type; pp_smt_exp w.addr] ^^ hardline
+     ^^ pp_sfun "declare-const" [string (w.name ^ "_ret"); pp_smt_typ Bool]
 
   | Write_mem_ea (name, _, active, wk, addr, addr_ty, data_size, data_size_ty) ->
      pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline
@@ -386,15 +530,24 @@ let pp_smt_def =
      ^^ pp_sfun "define-const" [string (name ^ "_size"); pp_smt_typ data_size_ty; pp_smt_exp data_size] ^^ hardline
      ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr]
 
-  | Read_mem (name, _, active, ty, rk, addr, addr_ty) ->
-     pp_sfun "define-const" [string (name ^ "_kind"); string "Zread_kind"; pp_smt_exp rk] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
-     ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ ty]
+  | Read_mem r ->
+     pp_sfun "define-const" [string (r.name ^ "_kind"); string "Zread_kind"; pp_smt_exp r.kind] ^^ hardline
+     ^^ pp_sfun "define-const" [string (r.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp r.active] ^^ hardline
+     ^^ pp_sfun "define-const" [string (r.name ^ "_addr"); pp_smt_typ r.addr_type; pp_smt_exp r.addr] ^^ hardline
+     ^^ pp_sfun "declare-const" [string (r.name ^ "_ret"); pp_smt_typ r.ret_type]
 
-  | Barrier (name, _, active, bk) ->
-     pp_sfun "define-const" [string (name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp bk] ^^ hardline
-     ^^ pp_sfun "define-const" [string (name ^ "_active"); pp_smt_typ Bool; pp_smt_exp active]
+  | Barrier b ->
+     pp_sfun "define-const" [string (b.name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp b.kind] ^^ hardline
+     ^^ pp_sfun "define-const" [string (b.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp b.active]
+
+  | Cache_maintenance m ->
+     pp_sfun "define-const" [string (m.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp m.active] ^^ hardline
+     ^^ pp_sfun "define-const" [string (m.name ^ "_kind"); string "Zcache_op_kind"; pp_smt_exp m.kind] ^^ hardline
+     ^^ pp_sfun "define-const" [string (m.name ^ "_addr"); pp_smt_typ m.addr_type; pp_smt_exp m.addr]
+
+  | Branch_announce c ->
+     pp_sfun "define-const" [string (c.name ^ "_active"); pp_smt_typ Bool; pp_smt_exp c.active] ^^ hardline
+     ^^ pp_sfun "define-const" [string (c.name ^ "_addr"); pp_smt_typ c.addr_type; pp_smt_exp c.addr]
 
   | Excl_res (name, _, active) ->
      pp_sfun "declare-const" [string (name ^ "_res"); pp_smt_typ Bool] ^^ hardline
@@ -404,7 +557,7 @@ let pp_smt_def =
      let pp_ctor (ctor_name, fields) =
        match fields with
        | [] -> parens (string ctor_name)
-       | _ -> pp_sfun ctor_name (List.map (fun field -> parens (pp_str_smt_typ field)) fields)
+       | _ -> pp_sfun ctor_name (List.map pp_str_smt_typ fields)
      in
      pp_sfun "declare-datatypes"
        [Printf.ksprintf string "((%s 0))" name;