diff options
-rw-r--r-- | handwritten_support/riscv_extras.v | 47 | ||||
-rw-r--r-- | model/prelude_mem.sail | 24 |
2 files changed, 39 insertions, 32 deletions
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index cc68a54..33bc9ec 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -36,31 +36,38 @@ Definition MEMea_conditional_release {rv a e} (addr : mword a) size : monad rv u Definition MEMea_conditional_strong_release {rv a e} (addr : mword a) size : monad rv unit e := write_mem_ea Write_RISCV_conditional_strong_release addr size. - -(* Some wrappers copied from aarch64_extras *) -(* TODO: Harmonise into a common library *) (* -Definition get_slice_int_bl len n lo := - (* TODO: Is this the intended behaviour? *) - let hi := lo + len - 1 in - let bs := bools_of_int (hi + 1) n in - subrange_list false bs hi lo - -val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -Definition get_slice_int len n lo := of_bools (get_slice_int_bl len n lo) +val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e *) -Definition write_ram {rv e} m size (hexRAM : mword m) (addr : mword m) (data : mword (8 * size)) : monad rv bool e := - write_mem_val data. -Definition read_ram {rv e} m size `{ArithFact (size >= 0)} (_ : mword m) (addr : mword m) : monad rv (mword (8 * size)) e := - read_mem Read_plain addr size. -(* -Definition string_of_bits bs := string_of_bv (bits_of bs). -Definition string_of_int := show +Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_plain addr size. +Definition MEMr_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_acquire addr size. +Definition MEMr_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_strong_acquire addr size. +Definition MEMr_reserved {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved addr size. +Definition MEMr_reserved_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_acquire addr size. +Definition MEMr_reserved_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >= 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_strong_acquire addr size. -Definition _sign_extend bits len := maybe_failwith (of_bits (exts_bv len bits)) -Definition _zero_extend bits len := maybe_failwith (of_bits (extz_bv len bits)) +(* +val MEMw : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_conditional : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_conditional_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e +val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e *) + +Definition MEMw {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_plain addr size v. +Definition MEMw_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_release addr size v. +Definition MEMw_strong_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_strong_release addr size v. +Definition MEMw_conditional {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional addr size v. +Definition MEMw_conditional_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional_release addr size v. +Definition MEMw_conditional_strong_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional_strong_release addr size v. + Definition shift_bits_left {a b} (v : mword a) (n : mword b) : mword a := shiftl v (int_of_mword false n). diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 8e483f8..b6fa0bc 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -2,22 +2,22 @@ * They depend on the XLEN of the architecture. */ -val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm. +val __WriteRAM = {lem: "MEMw", coq: "MEMw", _: "write_ram"} : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} -val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm. +val __WriteRAM_release = {lem: "MEMw_release", coq: "MEMw_release", _: "write_ram"} : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} -val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm. +val __WriteRAM_strong_release = {lem: "MEMw_strong_release", coq: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} -val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm. +val __WriteRAM_conditional = {lem: "MEMw_conditional", coq: "MEMw_conditional", _: "write_ram"} : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} -val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm. +val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", coq: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} -val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm. +val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", coq: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} val __RISCV_write : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv} @@ -36,22 +36,22 @@ function __RISCV_write (addr, width, data, aq, rl, con) = val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit -val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0. +val __ReadRAM = { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. +val __ReadRAM_acquire = { lem: "MEMr_acquire", coq: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. +val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", coq: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0. +val __ReadRAM_reserved = { lem: "MEMr_reserved", coq: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. +val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", coq: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. +val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", coq: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} val __RISCV_read : forall 'n, 'n >= 0. (xlenbits, atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} |