diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 63 | ||||
| -rw-r--r-- | riscv/riscv_mem.sail | 18 | ||||
| -rw-r--r-- | riscv/riscv_step.sail | 4 |
3 files changed, 51 insertions, 34 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 1be06536..24913719 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -13,6 +13,7 @@ val hex_bits : forall 'n . (atom('n), bits('n)) <-> string val string_startswith = "string_startswith" : (string, string) -> bool val string_drop = "string_drop" : (string, nat) -> string +val string_take = "string_take" : (string, nat) -> string val string_length = "string_length" : string -> nat val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat)) @@ -710,29 +711,6 @@ function hex_bits_64_backwards s = } - -val spc_forwards : unit -> string -function spc_forwards () = " " -val spc_backwards : string -> unit -function spc_backwards s = () - -val spc_matches_prefix = "spc_matches_prefix" : string -> option((unit, nat)) - -val opt_spc_forwards : unit -> string -function opt_spc_forwards () = "" -val opt_spc_backwards : string -> unit -function opt_spc_backwards s = () - -val opt_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat)) - -val def_spc_forwards : unit -> string -function def_spc_forwards () = " " -val def_spc_backwards : string -> unit -function def_spc_backwards s = () - -val def_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat)) - - val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool @@ -1153,3 +1131,42 @@ function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = /* Special version of zero_extend that the Lem back-end knows will be at a case split on 'm and uses a more generic type for. (Temporary hack, honest) */ val zero_extend_type_hack = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) + + +val n_leading_spaces : string -> nat +function n_leading_spaces s = + match s { + "" => 0, + _ => match string_take(s, 1) { + " " => 1 + n_leading_spaces(string_drop(s, 1)), + _ => 0 + } + } + +val spc_forwards : unit -> string +function spc_forwards () = " " +val spc_backwards : string -> unit +function spc_backwards s = () +val spc_matches_prefix : string -> option((unit, nat)) +function spc_matches_prefix s = { + let n = n_leading_spaces(s); + match n { + 0 => None(), + _ => Some((), n) + } +} + +val opt_spc_forwards : unit -> string +function opt_spc_forwards () = "" +val opt_spc_backwards : string -> unit +function opt_spc_backwards s = () +val opt_spc_matches_prefix : string -> option((unit, nat)) +function opt_spc_matches_prefix s = + Some((), n_leading_spaces(s)) + +val def_spc_forwards : unit -> string +function def_spc_forwards () = " " +val def_spc_backwards : string -> unit +function def_spc_backwards s = () +val def_spc_matches_prefix : string -> option((unit, nat)) +function def_spc_matches_prefix s = opt_spc_matches_prefix(s) diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 2d59a891..2bcc9797 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -16,12 +16,12 @@ 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, 'n > 0. MemoryOpResult(bits(8 * 'n)) = +function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> 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) else if within_phys_mem(addr, width) - then phys_mem_read(t, addr, width, false, false, false) + then phys_mem_read(t, addr, width, aq, rl, res) else MemException(E_Load_Access_Fault) /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ @@ -33,12 +33,12 @@ val MEMr_reserved : forall 'n, 'n > 0. (xlenbits, atom('n)) -> Me val MEMr_reserved_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} val MEMr_reserved_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} -function MEMr (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_acquire (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_strong_acquire (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_reserved (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_reserved_acquire (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width) +function MEMr (addr, width) = checked_mem_read(Data, addr, width, false, false, false) +function MEMr_acquire (addr, width) = checked_mem_read(Data, addr, width, true, false, false) +function MEMr_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, false) +function MEMr_reserved (addr, width) = checked_mem_read(Data, addr, width, false, false, true) +function MEMr_reserved_acquire (addr, width) = checked_mem_read(Data, addr, width, true, false, true) +function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, true) /* NOTE: The rreg effect is due to MMIO. */ val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape} @@ -47,7 +47,7 @@ function mem_read (addr, width, aq, rl, res) = { if (aq | res) & (~ (is_aligned_addr(addr, width))) then MemException(E_Load_Addr_Align) else match (aq, rl, res) { - (false, false, false) => checked_mem_read(Data, addr, width), + (false, false, false) => checked_mem_read(Data, addr, width, false, false, false), (true, false, false) => MEMr_acquire(addr, width), (false, false, true) => MEMr_reserved(addr, width), (true, false, true) => MEMr_reserved_acquire(addr, width), diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail index 8e5a0090..f9675115 100644 --- a/riscv/riscv_step.sail +++ b/riscv/riscv_step.sail @@ -21,7 +21,7 @@ function fetch() -> FetchResult = * well as to generate precise fault addresses in any fetch * exceptions. */ - match checked_mem_read(Instruction, ppclo, 2) { + match checked_mem_read(Instruction, ppclo, 2, false, false, false) { MemException(e) => F_Error(E_Fetch_Access_Fault, PC), MemValue(ilo) => { if isRVC(ilo) then F_RVC(ilo) @@ -30,7 +30,7 @@ function fetch() -> FetchResult = match translateAddr(PChi, Execute, Instruction) { TR_Failure(e) => F_Error(e, PChi), TR_Address(ppchi) => { - match checked_mem_read(Instruction, ppchi, 2) { + match checked_mem_read(Instruction, ppchi, 2, false, false, false) { MemException(e) => F_Error(E_Fetch_Access_Fault, PChi), MemValue(ihi) => F_Base(append(ihi, ilo)) } |