diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 86793f5b4..943f0fc4e 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -59,7 +59,7 @@ enum { OPT_ENABLE_ZICBOM, OPT_ENABLE_ZICBOZ, OPT_CACHE_BLOCK_SIZE, - OPT_ENABLE_ZJPM, + OPT_ENABLE_ZPM, }; static bool do_dump_dts = false; @@ -135,7 +135,7 @@ static struct option options[] = { {"pmp-count", required_argument, 0, OPT_PMP_COUNT }, {"pmp-grain", required_argument, 0, OPT_PMP_GRAIN }, {"enable-next", no_argument, 0, 'N' }, - {"ram-size", required_argument, 0, 'z' }, + {"ram-size", required_argument, 0, 'z' }, {"disable-compressed", no_argument, 0, 'C' }, {"disable-writable-misa", no_argument, 0, 'I' }, {"disable-fdext", no_argument, 0, 'F' }, @@ -146,7 +146,7 @@ static struct option options[] = { {"report-arch", no_argument, 0, 'a' }, {"test-signature", required_argument, 0, 'T' }, {"signature-granularity", required_argument, 0, 'g' }, - {"enable-zpm", no_argument, 0, OPT_ENABLE_ZJPM }, + {"enable-zpm", no_argument, 0, OPT_ENABLE_ZPM }, #ifdef RVFI_DII {"rvfi-dii", required_argument, 0, 'r' }, #endif @@ -290,7 +290,7 @@ static int process_args(int argc, char **argv) "t:" "T:" "g:" - "h" + "h" #ifdef RVFI_DII "r:" #endif @@ -346,10 +346,10 @@ static int process_args(int argc, char **argv) fprintf(stderr, "enabling N extension.\n"); rv_enable_next = true; break; - case OPT_ENABLE_ZJPM: + case OPT_ENABLE_ZPM: fprintf(stderr, "enabling pointer masking support.\n"); rv_enable_zpm = true; - break; + break; case 'I': fprintf(stderr, "disabling writable misa CSR.\n"); rv_enable_writable_misa = false; diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 115c7fc69..cf89b753c 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -259,4 +259,4 @@ val print_bits : string -> bitvector -> unit let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs))) val print_dbg : string -> unit -let print_dbg msg = () \ No newline at end of file +let print_dbg msg = () diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 813f00d88..820c48b47 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -113,7 +113,7 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let width_bytes = size_bytes(width); // This is checked during decoding. @@ -134,7 +134,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let vaddr_ = transform_effective_address(vaddr, pmm); + let vaddr_ = transform_effective_address(vaddr, pmm); if not(is_aligned(vaddr_, width)) then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } else { @@ -195,7 +195,7 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let 'width_bytes = size_bytes(width); // This is checked during decoding. @@ -207,7 +207,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let vaddr_ = transform_effective_address(vaddr, pmm); + let vaddr_ = transform_effective_address(vaddr, pmm); if not(is_aligned(vaddr_, width)) then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddr_, ReadWrite(Data, Data)) { @@ -261,4 +261,4 @@ mapping amo_mnemonic : amoop <-> string = { } mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd) - <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" \ No newline at end of file + <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 73ec50af7..72f57ca4c 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -320,57 +320,26 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool = function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = not(plat_enable_misaligned_access()) & not(is_aligned(vaddr, width)) -function transform_VA (effective_address : xlenbits,pmlen : {7, 16}) -> xlenbits = { - let XLEN = sizeof(xlen); - let i = XLEN -(pmlen +1); - let effective_bit = effective_address[i..i]; - let masked_bits = replicate_bits(effective_bit, pmlen); - let unmasked_bits = effective_address[i..0]; - masked_bits @ unmasked_bits +function transform_VA (effective_address : xlenbits, pmlen : {7, 16}) -> xlenbits = { + sign_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0]) } -function transform_PA (effective_address : xlenbits,pmlen : {7, 16}) -> xlenbits = { - let XLEN = sizeof(xlen); - let i = XLEN -(pmlen +1); - let masked_bits = replicate_bits(0b0, pmlen); - let unmasked_bits = effective_address[i..0]; - masked_bits @ unmasked_bits +function transform_PA (effective_address : xlenbits, pmlen : {7, 16}) -> xlenbits = { + zero_extend(effective_address[sizeof(xlen) - pmlen - 1 .. 0]) } function transform_effective_address(vaddr : xlenbits, pmm : bool) -> xlenbits = { if pmm then { let pmm_bits = get_pmm(); let mode = translationMode(cur_privilege); - match (mode) { - (Sbare) => { - match (pmm_bits){ - (0b10) => transform_PA (vaddr,7), - (0b11) => transform_PA (vaddr,16), - } - }, - (Sv39) => { - match (pmm_bits){ - (0b10) => transform_VA (vaddr,7), - (0b11) => transform_VA (vaddr,16), - } - }, - (Sv48) => { - match (pmm_bits){ - (0b10) => transform_VA (vaddr,7), - (0b11) => transform_VA (vaddr,16), - } - }, - (Sv57) => { - match (pmm_bits){ - (0b10) => transform_VA (vaddr,7), - (0b11) => transform_VA (vaddr,16), - } - }, + match pmm_bits { + pmm_mode(Enabled7) => if mode == Sbare then transform_PA(vaddr, 7) else transform_VA(vaddr, 7), + pmm_mode(Enabled16) => if mode == Sbare then transform_PA(vaddr, 16) else transform_VA(vaddr, 16), } - } - else { - vaddr //PMM is not active - } + } + else { + vaddr + } } function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { @@ -790,4 +759,4 @@ function clause execute SFENCE_VMA(rs1, rs2) = { } mapping clause assembly = SFENCE_VMA(rs1, rs2) - <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) \ No newline at end of file + <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 47cca08cf..f71810c09 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -137,7 +137,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled( val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -162,7 +162,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } }, Ext_DataAddr_OK(vaddr) => { - let vaddr_ = transform_effective_address(vaddr, pmm) in + let vaddr_ = transform_effective_address(vaddr, pmm) in if check_misaligned(vaddr_, width_type) then { if i == 0 then { handle_mem_exception(vaddr_, E_Load_Addr_Align()); return RETIRE_FAIL } else { @@ -244,7 +244,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(E val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); @@ -457,7 +457,7 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEna val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let pmm = is_pmm_active(); - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); @@ -551,7 +551,7 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEn val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let pmm = is_pmm_active(); - let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ (EMUL_pow); + let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ (EMUL_data_pow); let width_type : word_width = size_bytes(EEW_data_bytes); let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); @@ -567,7 +567,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - let vaddr_ = transform_effective_address(vaddr, pmm) in + let vaddr_ = transform_effective_address(vaddr, pmm) in if check_misaligned(vaddr_, width_type) then { handle_mem_exception(vaddr_, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr_, Write(Data)) { @@ -840,7 +840,7 @@ mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if extensionEnabled(Ext_V) val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { - let pmm = is_pmm_active(); + let pmm = is_pmm_active(); let width_type : word_width = BYTE; let start_element = get_start_element(); let vd_or_vs3_val : vector('n, dec, bits(8)) = read_vreg(num_elem, 8, 0, vd_or_vs3); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 2b6b25818..2f12c5cbd 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -96,7 +96,7 @@ val sys_enable_next = pure {c: "sys_enable_next", ocaml: "Platform.enable_next", supervisor mode is implemented and non-bare addressing modes are supported. */ val sys_enable_writable_fiom = pure {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool /* whether the PME extension was enabled at boot */ -val sys_enable_pmm = pure {c: "sys_enable_pmm", ocaml: "Platform.enable_pmm", _: "sys_enable_pmm"} : unit -> bool +val sys_enable_zpm = pure {c: "sys_enable_zpm", ocaml: "Platform.enable_zpm", _: "sys_enable_zpm"} : unit -> bool /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */ val sys_pmp_count = pure {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) /* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g. @@ -756,6 +756,21 @@ function read_seed_csr() -> xlenbits = { /* Writes to the seed CSR are ignored */ function write_seed_csr () -> option(xlenbits) = None() +/* Pointer Masking Different modes */ +enum PointerMaskingMode = { + Disabled, // Pointer Masking Disabled + Reserved, // Reserved Encoding for Pointer Masking + Enabled7, // Pointer Masking Enabled with PMM = 7 + Enabled16, // Pointer Masking Enabled with PMM = 16 +} + +mapping pmm_mode : PointerMaskingMode <-> bits(2) = { + Disabled <-> 0b00, + Reserved <-> 0b01, + Enabled7 <-> 0b10, + Enabled16 <-> 0b11, +} + /* mseccfg is a XLEN-bit read/write register that controls */ /* security features */ bitfield MSeccfg : bits(64) = { @@ -824,7 +839,7 @@ register senvcfg : SEnvcfg function legalize_mseccfg(o : MSeccfg, v : bits(64)) -> MSeccfg = { let v = Mk_MSeccfg(v); // Update PMM field only if Pointer Masking is enabled and Written value is legal - let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != 0b01)) then v[PMM] else o[PMM]]; + let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -833,7 +848,7 @@ function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = { let v = Mk_MEnvcfg(v); let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Update PMM field only if Pointer Masking is enabled and Written value is legal - let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != 0b01)) then v[PMM] else o[PMM]]; + let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -842,7 +857,7 @@ function legalize_senvcfg(o : SEnvcfg, v : bits(64)) -> SEnvcfg = { let v = Mk_SEnvcfg(v); let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Update PMM field only if Pointer Masking is enabled and Written value is legal - let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != 0b01)) then v[PMM] else o[PMM]]; + let o = [o with PMM = if (sys_enable_zpm() & (sizeof(xlen) != 32) & (v[PMM] != pmm_mode(Reserved))) then v[PMM] else o[PMM]]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -858,16 +873,6 @@ function is_fiom_active() -> bool = { } } -// Return whether or not PMM is currently active, based on the current -// privilege and the menvcfg,senvcfg and mseccfg settings. -function is_pmm_active() -> bool = { - match cur_privilege { - Machine => (mseccfg[PMM] == 0b11 | mseccfg[PMM] == 0b10), - Supervisor => (menvcfg[PMM] == 0b11 | menvcfg[PMM] == 0b10), - User => ((menvcfg[PMM] == 0b11 | menvcfg[PMM] == 0b10) | (senvcfg[PMM] == 0b11 | senvcfg[PMM] == 0b10)), - } -} - /* vector csrs */ register vstart : bits(16) /* use the largest possible length of vstart */ register vxsat : bits(1) @@ -886,13 +891,16 @@ bitfield Vtype : xlenbits = { register vtype : Vtype //Returns the PMM bits value depends on the Privilege mode -function get_pmm() -> bits(2) = { +function get_pmm() -> bits(2) = match cur_privilege { Machine => mseccfg[PMM], Supervisor => menvcfg[PMM], - User => if extensionEnabled(Ext_S) then senvcfg[PMM] else menvcfg[PMM], + User => if extensionEnabled(Ext_S) then senvcfg[PMM] else menvcfg[PMM], } -} + +// Return whether or not PMM is currently active, based on the current +// privilege and the menvcfg,senvcfg and mseccfg settings. +function is_pmm_active() -> bool = get_pmm() != zeros(2) /* the dynamic selected element width (SEW) */ /* this returns the power of 2 for SEW */