diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 38 | ||||
| -rw-r--r-- | src/sail_lib.ml | 4 | ||||
| -rw-r--r-- | src/smtlib.ml | 8 | ||||
| -rw-r--r-- | src/value.ml | 5 |
4 files changed, 55 insertions, 0 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index d73d1a02..45837513 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1022,6 +1022,19 @@ let smt_builtin ctx name args ret_ctyp = | _ -> failwith ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp) + +let writes = ref (-1) + +let builtin_write_mem ctx wk addr_size addr data_size data = + [Write_mem (smt_cval ctx wk, smt_cval ctx addr, smt_cval ctx data)] + +let reads = ref (-1) + +let builtin_read_mem ctx rk addr_size addr data_size = + incr reads; + let name = "R" ^ string_of_int !reads in + [Read_mem (name, smt_cval ctx rk, smt_cval ctx addr)] + let rec smt_conversion ctx from_ctyp to_ctyp x = match from_ctyp, to_ctyp with | _, _ when ctyp_equal from_ctyp to_ctyp -> x @@ -1384,6 +1397,21 @@ let smt_instr ctx = | _ -> Reporting.unreachable l __POS__ "Bad arguments for sqrt_real" end + (* See lib/regfp.sail *) + else if name = "platform_write_mem" then + begin match args with + | [wk; addr_size; addr; data_size; data] -> + builtin_write_mem ctx wk addr_size addr data_size data + | _ -> + Reporting.unreachable l __POS__ "Bad arguments for __write_mem" + end + else if name = "platform_read_mem" then + begin match args with + | [rk; addr_size; addr; data_size] -> + builtin_read_mem ctx rk addr_size addr data_size + | _ -> + Reporting.unreachable l __POS__ "Bad arguments for __read_mem" + end else let value = smt_builtin ctx name args ret_ctyp in [define_const ctx id ret_ctyp value] @@ -1521,6 +1549,12 @@ let optimize_smt stack = end | (Declare_datatypes _ | Declare_tuple _) as def -> Stack.push def stack' + | Write_mem (wk, addr, data) as def -> + uses_in_exp wk; uses_in_exp addr; uses_in_exp data; + Stack.push def stack' + | Read_mem (name, rk, addr) as def -> + uses_in_exp rk; uses_in_exp addr; + Stack.push def stack' | Assert exp as def -> uses_in_exp exp; Stack.push def stack' @@ -1542,6 +1576,10 @@ let optimize_smt stack = Queue.add (Define_const (var, typ, simp_smt_exp vars exp)) queue | None -> assert false end + | Write_mem (wk, addr, data) -> + Queue.add (Write_mem (simp_smt_exp vars wk, simp_smt_exp vars addr, simp_smt_exp vars data)) queue + | Read_mem (name, rk, addr) -> + Queue.add (Read_mem (name, simp_smt_exp vars rk, simp_smt_exp vars addr)) queue | Assert exp -> Queue.add (Assert (simp_smt_exp vars exp)) queue | (Declare_datatypes _ | Declare_tuple _) as def -> diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 39485769..61e62d76 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -186,6 +186,10 @@ let sint = function let add_int (x, y) = Big_int.add x y let sub_int (x, y) = Big_int.sub x y +let sub_nat (x, y) = + let z = Big_int.sub x y in + if Big_int.less z Big_int.zero then Big_int.zero else z + let mult (x, y) = Big_int.mul x y (* This is euclidian division from lem *) diff --git a/src/smtlib.ml b/src/smtlib.ml index 1665419c..a252ea4a 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -182,6 +182,8 @@ type smt_def = | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp | Declare_const of string * smt_typ | Define_const of string * smt_typ * smt_exp + | Write_mem of smt_exp * smt_exp * smt_exp + | Read_mem of string * smt_exp * smt_exp | Declare_datatypes of string * (string * (string * smt_typ) list) list | Declare_tuple of int | Assert of smt_exp @@ -242,6 +244,12 @@ let pp_smt_def = | Define_const (name, ty, exp) -> pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp] + | Write_mem (wk, addr, data) -> + pp_sfun "write-mem" [pp_smt_exp wk; pp_smt_exp addr; pp_smt_exp data] + + | Read_mem (name, rk, addr) -> + pp_sfun "read-mem" [string name; pp_smt_exp rk; pp_smt_exp addr] + | Declare_datatypes (name, ctors) -> let pp_ctor (ctor_name, fields) = match fields with diff --git a/src/value.ml b/src/value.ml index 958a1919..6ccecac0 100644 --- a/src/value.ml +++ b/src/value.ml @@ -341,6 +341,10 @@ let value_sub_int = function | [v1; v2] -> V_int (Sail_lib.sub_int (coerce_int v1, coerce_int v2)) | _ -> failwith "value sub" +let value_sub_nat = function + | [v1; v2] -> V_int (Sail_lib.sub_nat (coerce_int v1, coerce_int v2)) + | _ -> failwith "value sub_nat" + let value_negate = function | [v1] -> V_int (Sail_lib.negate (coerce_int v1)) | _ -> failwith "value negate" @@ -663,6 +667,7 @@ let primops = ("shift_bits_right", value_shift_bits_right); ("add_int", value_add_int); ("sub_int", value_sub_int); + ("sub_nat", value_sub_nat); ("div_int", value_quotient); ("mult_int", value_mult); ("mult", value_mult); |