diff options
| author | Alasdair Armstrong | 2019-05-17 16:34:00 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-17 16:34:00 +0100 |
| commit | f0b547154b3d2ce9e4bac74b0c56f20d6db76cd2 (patch) | |
| tree | b6d1053bea33a115879fe24b4c5e6add0bae566e /src/smtlib.ml | |
| parent | 4a95bb1c25fe84be62f6eada024f964472736e69 (diff) | |
SMT: Finish adding all memory builtins from lib/regfp.sail
Diffstat (limited to 'src/smtlib.ml')
| -rw-r--r-- | src/smtlib.ml | 20 |
1 files changed, 20 insertions, 0 deletions
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 |