From df7101474911964e7d8dbf5b6fd3de3ed66b7fc8 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 10 May 2019 21:10:19 +0100 Subject: SMT: Implement memory events for read_mem and write_mem Generate SMT where the memory reads and writes are totally unconstrained, allowing additional constraints to be added that restrict the possible reads and writes based on some memory model. --- src/jib/jib_smt.ml | 35 ++++++++++++------- src/smtlib.ml | 12 +++---- test/smt/litmus.sail | 82 -------------------------------------------- test/smt/store_load.sat.sail | 55 +++++++++++++++++++++++++++++ 4 files changed, 83 insertions(+), 101 deletions(-) delete mode 100644 test/smt/litmus.sail create mode 100644 test/smt/store_load.sat.sail diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 45837513..4afd1fa9 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1022,18 +1022,22 @@ 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) - +(* Memory reads and writes as defined in lib/regfp.sail *) 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)] + incr writes; + let name = "W" ^ string_of_int !writes in + [Write_mem (name, smt_cval ctx wk, smt_cval ctx addr, smt_cval ctx data)], + Var name let reads = ref (-1) -let builtin_read_mem ctx rk addr_size addr data_size = +let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp = incr reads; let name = "R" ^ string_of_int !reads in - [Read_mem (name, smt_cval ctx rk, smt_cval ctx addr)] + [Read_mem (name, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr)], + Var name let rec smt_conversion ctx from_ctyp to_ctyp x = match from_ctyp, to_ctyp with @@ -1401,14 +1405,17 @@ let smt_instr ctx = 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 + let mem_event, var = builtin_write_mem ctx wk addr_size addr data_size data in + mem_event @ [define_const ctx id ret_ctyp var] | _ -> 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 + let mem_event, var = builtin_read_mem ctx rk addr_size addr data_size ret_ctyp in + mem_event @ [define_const ctx id ret_ctyp var] + | _ -> Reporting.unreachable l __POS__ "Bad arguments for __read_mem" end @@ -1549,10 +1556,10 @@ let optimize_smt stack = end | (Declare_datatypes _ | Declare_tuple _) as def -> Stack.push def stack' - | Write_mem (wk, addr, data) as def -> + | 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 -> + | Read_mem (_, _, rk, addr) as def -> uses_in_exp rk; uses_in_exp addr; Stack.push def stack' | Assert exp as def -> @@ -1576,10 +1583,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 + | Write_mem (name, wk, addr, data) -> + Queue.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, simp_smt_exp vars data)) queue + | Read_mem (name, typ, rk, addr) -> + Queue.add (Read_mem (name, typ, 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 -> @@ -1740,12 +1747,14 @@ let smt_cdef props lets name_file ctx all_cdefs = function if prop_type = "counterexample" then output_string out_chan "(set-option :produce-models true)\n"; + let header = smt_header ctx all_cdefs in + if !(ctx.use_string) || !(ctx.use_real) then output_string out_chan "(set-logic ALL)\n" else output_string out_chan "(set-logic QF_AUFBVDT)\n"; - List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") (smt_header ctx all_cdefs); + List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") header; let queue = optimize_smt stack in Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue; diff --git a/src/smtlib.ml b/src/smtlib.ml index a252ea4a..ab6ebf55 100644 --- a/src/smtlib.ml +++ b/src/smtlib.ml @@ -182,8 +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 + | Write_mem of string * smt_exp * smt_exp * smt_exp + | Read_mem of string * smt_typ * smt_exp * smt_exp | Declare_datatypes of string * (string * (string * smt_typ) list) list | Declare_tuple of int | Assert of smt_exp @@ -244,11 +244,11 @@ 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] + | Write_mem (name, wk, addr, data) -> + pp_sfun "declare-const" [string name; pp_smt_typ Bool] - | Read_mem (name, rk, addr) -> - pp_sfun "read-mem" [string name; pp_smt_exp rk; pp_smt_exp addr] + | Read_mem (name, ty, rk, addr) -> + pp_sfun "declare-const" [string name; pp_smt_typ ty] | Declare_datatypes (name, ctors) -> let pp_ctor (ctor_name, fields) = diff --git a/test/smt/litmus.sail b/test/smt/litmus.sail deleted file mode 100644 index 68e38269..00000000 --- a/test/smt/litmus.sail +++ /dev/null @@ -1,82 +0,0 @@ -default Order dec - -$include -$include - -register x0 : bits(32) -register x1 : bits(32) -register x2 : bits(32) -register x3 : bits(32) - -function wX(r: bits(2), v: bits(32)) -> unit = { - match r { - 0b00 => x0 = v, - 0b01 => x1 = v, - 0b10 => x2 = v, - 0b11 => x3 = v - } -} - -function rX(r: bits(2)) -> bits(32) = { - match r { - 0b00 => x0, - 0b01 => x1, - 0b10 => x2, - 0b11 => x3 - } -} - -overload X = {rX, wX} - -scattered union ast - -val execute : ast -> bool - -union clause ast = LOAD : (bits(2), bits(2)) - -function clause execute(LOAD(rd, rs)) = { - X(rd) = __read_mem(Read_plain, 32, X(rs), 4); - true -} - -union clause ast = STORE : (bits(2), bits(2)) - -function clause execute(STORE(rd, rs)) = { - let addr = X(rd); - __write_mem(Write_plain, 32, addr, 4, X(rs)) -} - -/* -RISCV LB -"PodRW Rfe PodRW Rfe" -Cycle=Rfe PodRW Rfe PodRW -Relax=PodRW -Safe=Rfe -Generator=diy7 (version 7.51+4(dev)) -Prefetch=0:x=F,0:y=W,1:y=F,1:x=W -Com=Rf Rf -Orig=PodRW Rfe PodRW Rfe -{ -0:x6=x; 0:x7=1; 0:x8=y; -1:x6=y; 1:x7=1; 1:x8=x; -} - P0 | P1 ; - lw x5,0(x6) | lw x5,0(x6) ; - sw x7,0(x8) | sw x7,0(x8) ; -exists -(0:x5=1 /\ 1:x5=1) -*/ - -$property -function P0() -> bool = { - let i1 = execute(LOAD(0b00, 0b01)); - let i2 = execute(STORE(0b10, 0b11)); - i1 & i2 -} - -$property -function P1() -> bool = { - let i1 = execute(LOAD(0b00, 0b01)); - let i2 = execute(STORE(0b10, 0b11)); - i1 & i2 -} diff --git a/test/smt/store_load.sat.sail b/test/smt/store_load.sat.sail new file mode 100644 index 00000000..810bbfbb --- /dev/null +++ b/test/smt/store_load.sat.sail @@ -0,0 +1,55 @@ +default Order dec + +$include +$include + +register x0 : bits(32) +register x1 : bits(32) +register x2 : bits(32) +register x3 : bits(32) + +function wX(r: bits(2), v: bits(32)) -> unit = { + match r { + 0b00 => x0 = v, + 0b01 => x1 = v, + 0b10 => x2 = v, + 0b11 => x3 = v + } +} + +function rX(r: bits(2)) -> bits(32) = { + match r { + 0b00 => x0, + 0b01 => x1, + 0b10 => x2, + 0b11 => x3 + } +} + +overload X = {rX, wX} + +scattered union ast + +val execute : ast -> bool + +union clause ast = LOAD : (bits(2), bits(2)) + +function clause execute(LOAD(rd, rs)) = { + X(rd) = __read_mem(Read_plain, 32, X(rs), 4); + true +} + +union clause ast = STORE : (bits(2), bits(2)) + +function clause execute(STORE(rd, rs)) = { + let addr = X(rd); + __write_mem(Write_plain, 32, addr, 4, X(rs)) +} + +/* Default memory model is as weak as possible, so this is not true */ +$counterexample +function prop() -> bool = { + let _ = execute(STORE(0b01, 0b10)); + let _ = execute(LOAD(0b00, 0b01)); + X(0b00) == X(0b10) +} -- cgit v1.2.3