SMT: Finish adding all memory builtins from lib/regfp.sail

4 files changed, 98 insertions, 2 deletions

diff --git a/lib/regfp.sail b/lib/regfp.sail
index ebbf1655..da9c11d6 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -120,10 +120,12 @@ val __read_mem
   (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n) effect {rmem}
 val __write_mem_ea
   = { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" }
-  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem}
+  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
+  (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem}
 val __write_mem
   = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
-  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv}
+  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
+  (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv}
 val __excl_res
   = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" }
   : unit -> bool effect {exmem}
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index db97eb6a..897c685a 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1025,6 +1025,14 @@ let builtin_write_mem ctx wk addr_size addr data_size data =
   [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))],
   Var (name ^ "_ret")
 
+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))],
+  Enum "unit"
+
 let reads = ref (-1)
 
 let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
@@ -1033,6 +1041,22 @@ let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
   [Read_mem (name, 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)
+
+let builtin_excl_res ctx =
+  incr excl_results;
+  let name = "E" ^ string_of_int !excl_results in
+  [Excl_res name],
+  Var (name ^ "_ret")
+
+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)],
+  Enum "unit"
+
 let rec smt_conversion ctx from_ctyp to_ctyp x =
   match from_ctyp, to_ctyp with
   | _, _ when ctyp_equal from_ctyp to_ctyp -> x
@@ -1445,6 +1469,14 @@ let smt_instr ctx =
          | _ ->
             Reporting.unreachable l __POS__ "Bad arguments for __write_mem"
          end
+       else if name = "platform_write_mem_ea" then
+         begin match args with
+         | [wk; addr_size; addr; data_size] ->
+            let mem_event, var = builtin_write_mem_ea ctx wk addr_size addr data_size in
+            mem_event @ [define_const ctx id ret_ctyp var]
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __write_mem_ea"
+         end
        else if name = "platform_read_mem" then
          begin match args with
          | [rk; addr_size; addr; data_size] ->
@@ -1453,6 +1485,22 @@ let smt_instr ctx =
          | _ ->
             Reporting.unreachable l __POS__ "Bad arguments for __read_mem"
          end
+       else if name = "platform_barrier" then
+         begin match args with
+         | [bk] ->
+            let mem_event, var = builtin_barrier ctx bk in
+            mem_event @ [define_const ctx id ret_ctyp var]
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __barrier"
+         end
+       else if name = "platform_excl_res" then
+         begin match args with
+         | [_] ->
+            let mem_event, var = builtin_excl_res ctx in
+            mem_event @ [define_const ctx id ret_ctyp var]
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __excl_res"
+         end
        else
          let value = smt_builtin ctx name args ret_ctyp in
          [define_const ctx id ret_ctyp value]
@@ -1601,9 +1649,17 @@ module Make_optimizer(S : Sequence) = struct
       | Write_mem (_, wk, addr, _, data, _) as def ->
          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;
+         Stack.push def stack'
       | Read_mem (_, _, rk, addr, _) as def ->
          uses_in_exp rk; uses_in_exp addr;
          Stack.push def stack'
+      | Barrier (_, bk) as def ->
+         uses_in_exp bk;
+         Stack.push def stack'
+      | Excl_res _ as def ->
+         Stack.push def stack'
       | Assert exp as def ->
          uses_in_exp exp;
          Stack.push def stack'
@@ -1631,8 +1687,14 @@ module Make_optimizer(S : Sequence) = struct
          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
       | Assert exp ->
          S.add (Assert (simp_smt_exp vars exp)) seq
       | (Declare_datatypes _ | Declare_tuple _) as def ->
diff --git a/src/smtlib.ml b/src/smtlib.ml
index c6b86fcb..5a2fcd44 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -230,7 +230,10 @@ type smt_def =
   | Declare_const of string * smt_typ
   | Define_const of string * smt_typ * smt_exp
   | Write_mem of string * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
+  | Write_mem_ea of string * smt_exp * smt_exp * smt_typ * smt_exp * smt_typ
   | Read_mem of string * smt_typ * smt_exp * smt_exp * smt_typ
+  | Barrier of string * smt_exp
+  | Excl_res of string
   | Declare_datatypes of string * (string * (string * smt_typ) list) list
   | Declare_tuple of int
   | Assert of smt_exp
@@ -251,8 +254,14 @@ let suffix_variables_def sfx = function
      Define_const (name ^ sfx, ty, suffix_variables_exp sfx exp)
   | Write_mem (name, wk, addr, addr_ty, data, data_ty) ->
      Write_mem (name ^ sfx, suffix_variables_exp sfx wk, suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data, data_ty)
+  | Write_mem_ea (name, wk, addr, addr_ty, data_size, data_size_ty) ->
+     Write_mem (name ^ sfx, suffix_variables_exp sfx wk, suffix_variables_exp sfx addr, addr_ty, suffix_variables_exp sfx data_size, data_size_ty)
   | Read_mem (name, ty, rk, addr, addr_ty) ->
      Read_mem (name ^ sfx, ty, suffix_variables_exp sfx rk, suffix_variables_exp sfx addr, addr_ty)
+  | Barrier (name, bk) ->
+     Barrier (name ^ sfx, bk)
+  | Excl_res name ->
+     Excl_res (name ^ sfx)
   | Declare_datatypes (name, ctors) ->
      Declare_datatypes (name, ctors)
   | Declare_tuple n ->
@@ -351,11 +360,22 @@ let pp_smt_def =
      ^^ 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_ea (name, wk, addr, addr_ty, data_size, data_size_ty) ->
+     pp_sfun "define-const" [string (name ^ "_kind"); string "Zwrite_kind"; pp_smt_exp wk] ^^ hardline
+     ^^ 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, 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 ^ "_addr"); pp_smt_typ addr_ty; pp_smt_exp addr] ^^ hardline
      ^^ pp_sfun "declare-const" [string (name ^ "_ret"); pp_smt_typ ty]
 
+  | Barrier (name, bk) ->
+     pp_sfun "define-const" [string (name ^ "_kind"); string "Zbarrier_kind"; pp_smt_exp bk]
+
+  | Excl_res name ->
+     pp_sfun "declare-const" [string (name ^ "_res"); pp_smt_typ Bool]
+
   | Declare_datatypes (name, ctors) ->
      let pp_ctor (ctor_name, fields) =
        match fields with
diff --git a/test/smt/mem_builtins.unsat.sail b/test/smt/mem_builtins.unsat.sail
new file mode 100644
index 00000000..28e44658
--- /dev/null
+++ b/test/smt/mem_builtins.unsat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+$include <regfp.sail>
+
+$property
+function prop() -> bool = {
+  __barrier(Barrier_DSB);
+  let _ = __excl_res();
+  __write_mem_ea(Write_exclusive_release, 32, 0xFFFF_FFFF, 8);
+  true
+}