diff options
| -rw-r--r-- | src/jib/jib_smt.ml | 4 | ||||
| -rw-r--r-- | src/smtlib.ml | 6 | ||||
| -rw-r--r-- | test/smt/load_store_dep.sat.sail | 12 |
3 files changed, 18 insertions, 4 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 7420707c..0d6f42fe 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1044,7 +1044,7 @@ let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp = let name = "R" ^ string_of_int !reads in [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))], - Var (name ^ "_ret") + Read_res name let excl_results = ref (-1) @@ -1626,7 +1626,7 @@ module Make_optimizer(S : Sequence) = struct | Some n -> Hashtbl.replace uses var (n + 1) | None -> Hashtbl.add uses var 1 end - | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> () + | Enum _ | Read_res _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> () | Fn (_, exps) | Ctor (_, exps) -> List.iter uses_in_exp exps | Ite (cond, t, e) -> diff --git a/src/smtlib.ml b/src/smtlib.ml index 5de13bdb..b90f33a7 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -94,6 +94,7 @@ type smt_exp = | Real_lit of string | String_lit of string | Var of string + | Read_res of string | Enum of string | Fn of string * smt_exp list | Ctor of string * smt_exp list @@ -109,7 +110,7 @@ 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 _ | Enum _ as exp) -> f exp + | (Bool_lit _ | Hex _ | Bin _ | Real_lit _ | String_lit _ | Var _ | Read_res _ | Enum _ as exp) -> f exp let smt_conj = function | [] -> Bool_lit true @@ -204,7 +205,7 @@ let rec simp_smt_exp vars kinds = function | Some exp -> simp_smt_exp vars kinds exp | None -> Var v end - | (Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp + | (Read_res _ | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ as exp) -> exp | Fn (f, exps) -> let exps = List.map (simp_smt_exp vars kinds) exps in simp_fn (Fn (f, exps)) @@ -330,6 +331,7 @@ let rec pp_smt_exp = | Hex str -> string ("#x" ^ str) | Bin str -> string ("#b" ^ str) | Var 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) | Ctor (str, exps) -> parens (string str ^^ space ^^ separate_map space pp_smt_exp exps) diff --git a/test/smt/load_store_dep.sat.sail b/test/smt/load_store_dep.sat.sail new file mode 100644 index 00000000..bb35c6f7 --- /dev/null +++ b/test/smt/load_store_dep.sat.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <prelude.sail> +$include "test/arch.sail" + +/* Default memory model is as weak as possible, so this is not true */ +$counterexample +function prop() -> bool = { + let _ = arch_load(0b00, 0b01); + let _ = arch_store(0b10, 0b00); + X(0b01) == X(0b10) +} |