diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/Makefile | 9 | ||||
| -rw-r--r-- | riscv/prelude.sail | 56 | ||||
| -rw-r--r-- | riscv/riscv_extras.v | 162 | ||||
| -rw-r--r-- | riscv/riscv_mem.sail | 4 |
4 files changed, 201 insertions, 30 deletions
diff --git a/riscv/Makefile b/riscv/Makefile index 4805c8b2..5093c41e 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -77,6 +77,14 @@ riscvScript.sml : riscv.lem riscv_extras.lem riscvTheory.uo riscvTheory.ui: riscvScript.sml Holmake riscvTheory.uo +COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail + +riscv.v riscv_types.v: $(SAIL_SRCS) + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_SRCS) +%.vo: %.v + coqc $(COQ_LIBS) $< +riscv.vo: riscv_types.vo riscv_extras.vo + # we exclude prelude.sail here, most code there should move to sail lib LOC_FILES:=$(SAIL_SRCS) main.sail include ../etc/loc.mk @@ -89,5 +97,6 @@ clean: -rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem -rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml -rm -f platform_main.native platform coverage.native + -rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v -Holmake cleanAll ocamlbuild -clean diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 6eeda601..131162ec 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -134,7 +134,7 @@ val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) (' overload append = {bitvector_concat, vector_concat} -val not_bool = "not" : bool -> bool +val not_bool = {coq: "negb", _: "not"} : bool -> bool val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) @@ -158,7 +158,7 @@ function neq_anything (x, y) = not_bool(x == y) overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} -val and_bool = "and_bool" : (bool, bool) -> bool +val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -168,7 +168,7 @@ function and_vec (xs, ys) = builtin_and_vec(xs, ys) overload operator & = {and_bool, and_vec} -val or_bool = "or_bool" : (bool, bool) -> bool +val or_bool = {coq: "orb", _:"or_bool"} : (bool, bool) -> bool val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -182,7 +182,7 @@ val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) -val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) +val hex_slice = "hex_slice" : forall 'n 'm, 'n >= 'm. (string, atom('n), atom('m)) -> bits('n - 'm) val __SetSlice_bits = "set_slice" : forall 'n 'm. (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n) @@ -191,16 +191,16 @@ val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int -val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) +val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w) -val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n) +val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n) function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o) val __raw_SetSlice_bits : forall 'n 'w. (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n) -val __raw_GetSlice_bits : forall 'n 'w. +val __raw_GetSlice_bits : forall 'n 'w, 'w >= 0. (atom('n), atom('w), bits('n), int) -> bits('w) val "shiftl" : forall 'm. (bits('m), int) -> bits('m) @@ -239,10 +239,10 @@ val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> r overload operator ^ = {xor_vec, int_power, real_power, concat_str} -val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p. +val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int +val add_int = {ocaml: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -252,10 +252,10 @@ val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} -val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p. +val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) -val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int +val sub_int = {ocaml: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", lem: "integerMinus"} : (nat, nat) -> nat @@ -266,9 +266,9 @@ val "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n) val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real -val negate_range = {ocaml: "minus_big_int", lem: "integerNegate"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) +val negate_range = {ocaml: "minus_big_int", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) -val negate_int = {ocaml: "minus_big_int", lem: "integerNegate"} : int -> int +val negate_int = {ocaml: "minus_big_int", lem: "integerNegate", coq: "Z.opp"} : int -> int val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real @@ -279,7 +279,7 @@ overload negate = {negate_range, negate_int, negate_real} val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) -val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int +val mult_int = {ocaml: "mult", lem: "integerMult", coq: "Z.mul"} : (int, int) -> int val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real @@ -287,25 +287,25 @@ overload operator * = {mult_range, mult_int, mult_real} val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real -val gteq_int = "gteq" : (int, int) -> bool +val gteq_int = {coq: "Z.geb", _: "gteq"} : (int, int) -> bool val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool overload operator >= = {gteq_atom, gteq_int, gteq_real} -val lteq_int = "lteq" : (int, int) -> bool +val lteq_int = {coq: "Z.leb", _: "lteq"} : (int, int) -> bool val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool overload operator <= = {lteq_atom, lteq_int, lteq_real} -val gt_int = "gt" : (int, int) -> bool +val gt_int = {coq: "Z.gtb", _: "gt"} : (int, int) -> bool val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool overload operator > = {gt_atom, gt_int, gt_real} -val lt_int = "lt" : (int, int) -> bool +val lt_int = {coq: "Z.ltb", _: "lt"} : (int, int) -> bool val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool @@ -315,7 +315,7 @@ val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int val RoundUp = {ocaml: "round_up", lem: "realCeiling"} : real -> int -val abs_int = {ocaml: "abs_int", lem: "abs"} : int -> int +val abs_int = {ocaml: "abs_int", lem: "abs", coq: "Z.abs"} : int -> int val abs_real = {ocaml: "abs_real", lem: "abs"} : real -> real @@ -365,25 +365,25 @@ function __RISCV_write (addr, width, data) = { val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit -val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm. +val __ReadRAM = { lem: "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. +val __ReadRAM_acquire = { lem: "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. +val __ReadRAM_strong_acquire = { lem: "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. +val __ReadRAM_reserved = { lem: "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. +val __ReadRAM_reserved_acquire = { lem: "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. +val __ReadRAM_reserved_strong_acquire = { lem: "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. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} +val __RISCV_read : forall 'n, 'n >= 0. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} function __RISCV_read (addr, width, aq, rl, res) = match (aq, rl, res) { (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)), @@ -398,7 +398,7 @@ function __RISCV_read (addr, width, aq, rl, res) = val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit -val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) +val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm) val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} @@ -476,7 +476,7 @@ val vector64 : int -> bits(64) function vector64 n = __raw_GetSlice_int(64, n, 0) -val to_bits : forall 'l.(atom('l), int) -> bits('l) +val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) function to_bits (l, n) = __raw_GetSlice_int(l, n, 0) val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o. diff --git a/riscv/riscv_extras.v b/riscv/riscv_extras.v new file mode 100644 index 00000000..a3cb3fb9 --- /dev/null +++ b/riscv/riscv_extras.v @@ -0,0 +1,162 @@ +Require Import Sail2_instr_kinds. +Require Import Sail2_values. +Require Import Sail2_operators_mwords. +Require Import Sail2_prompt_monad. +Require Import Sail2_prompt. +Require Import String. +Require Import List. +Import List.ListNotations. + +Axiom real : Type. + +(* +val MEMr : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e +val MEMr_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e +val MEMr_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e +val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e +*) +Definition MEMr {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (mword b) e := read_mem Read_plain addr size. +Definition MEMr_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (mword b) e := read_mem Read_reserve addr size. + +(*val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e*) +Definition read_tag_bool {regval a e} (addr : mword a) : monad regval bool e := + read_tag addr >>= fun t => + maybe_fail "read_tag_bool" (bool_of_bitU t). + +(*val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e*) +Definition write_tag_bool {regval a e} (addr : mword a) t : monad regval unit e := + write_tag addr (bitU_of_bool t) >>= fun _ => returnm tt. + +Definition MEMr_tag {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e := + read_mem Read_plain addr size >>= fun v => + read_tag_bool addr >>= fun t => + returnm (t, v). + +Definition MEMr_tag_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e := + read_mem Read_plain addr size >>= fun v => + read_tag_bool addr >>= fun t => + returnm (t, v). + +(* +val MEMea : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_tag : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +*) +Definition MEMea {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_plain addr size. +Definition MEMea_conditional {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_conditional addr size. + +Definition MEMea_tag {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_plain addr size. +Definition MEMea_tag_conditional {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_conditional addr size. + +(* +val MEMval : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e +val MEMval_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e +val MEMval_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e +val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e +*) +Definition MEMval {regval a b e} (_ : mword a) (size : Z) (v : mword b) : monad regval unit e := write_mem_val v >>= fun _ => returnm tt. +Definition MEMval_conditional {regval a b e} (_ : mword a) (size : Z) (v : mword b) : monad regval bool e := write_mem_val v >>= fun b => returnm (if b then true else false). +Definition MEMval_tag {regval a b e} (addr : mword a) (size : Z) t (v : mword b) : monad regval unit e := write_mem_val v >>= fun _ => write_tag_bool addr t >>= fun _ => returnm tt. +Definition MEMval_tag_conditional {regval a b e} (addr : mword a) (size : Z) t (v : mword b) : monad regval bool e := write_mem_val v >>= fun b => write_tag_bool addr t >>= fun _ => returnm (if b then true else false). + +(*val MEM_sync : forall 'regval 'e. unit -> monad 'regval unit 'e*) + +Definition MEM_sync {regval e} (_:unit) : monad regval unit e := barrier Barrier_MIPS_SYNC. + +(* 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) +*) +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 _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)) +*) +Definition shift_bits_left {a b} (v : mword a) (n : mword b) : mword a := + shiftl v (int_of_mword false n). + +Definition shift_bits_right {a b} (v : mword a) (n : mword b) : mword a := + shiftr v (int_of_mword false n). + +Definition shift_bits_right_arith {a b} (v : mword a) (n : mword b) : mword a := + arith_shiftr v (int_of_mword false n). + +(* Use constants for undefined values for now *) +Definition internal_pick {rv a e} (vs : list a) : monad rv a e := +match vs with +| (h::_) => returnm h +| _ => Fail "empty list in internal_pick" +end. +Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%string. +Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. +Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii). +(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*) +Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >= 0)} : monad rv (vec a len) e := returnm (vec_init u len). +(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) +Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0). +(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) +Definition undefined_bits {rv e} := @undefined_bitvector rv e. +Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU. +(*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*) +Definition undefined_range {rv e} i j `{ArithFact (i <= j)} : monad rv {z : Z & ArithFact (i <= z /\ z <= j)} e := returnm (build_ex i). +Definition undefined_atom {rv e} i : monad rv Z e := returnm i. +Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii). + +Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. + +(*val elf_entry : unit -> integer*) +Definition elf_entry (_:unit) : Z := 0. +(*declare ocaml target_rep function elf_entry := `Elf_loader.elf_entry`*) + +(*Definition print_bits msg bs := prerr_endline (msg ^ (string_of_bits bs)) + +val get_time_ns : unit -> integer*) +Definition get_time_ns (_:unit) : Z := 0. +(*declare ocaml target_rep function get_time_ns := `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`*) + +Definition eq_bit (x : bitU) (y : bitU) : bool := + match x, y with + | B0, B0 => true + | B1, B1 => true + | BU, BU => true + | _,_ => false + end. + +Require Import Zeuclid. +Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}. +apply existT with (x := ZEuclid.modulo m n). +constructor. +destruct H. +assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. } +rewrite <- H at 3. +lapply (ZEuclid.mod_always_pos m n); omega. +Qed. + +(* Override the more general version *) + +Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r. +Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r. + + +Definition print_endline (_:string) : unit := tt. +Definition prerr_endline (_:string) : unit := tt. +Definition prerr_string (_:string) : unit := tt. +Definition putchar {T} (_:T) : unit := tt. +Require DecimalString. +Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 72b7e8da..9425c0ff 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -8,7 +8,7 @@ function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool unsigned(addr) % width == 0 // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n. MemoryOpResult(bits(8 * 'n)) = +function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) = match (t, __RISCV_read(addr, width, aq, rl, res)) { (Instruction, None()) => MemException(E_Fetch_Access_Fault), (Data, None()) => MemException(E_Load_Access_Fault), @@ -16,7 +16,7 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo MemValue(v) } } -function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) = +function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) = /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */ if t == Data & within_mmio_readable(addr, width) then mmio_read(addr, width) |