From 04b917a1e9ba20e811a79341ea996f3467b5fd47 Mon Sep 17 00:00:00 2001 From: Nathaniel Filardo Date: Thu, 27 Jul 2023 16:08:52 +0000 Subject: [PATCH 1/9] Update sail-cheri-mcu build to Ubuntu 22.04 --- azure-pipelines.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 8fc5879..81b7a29 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -15,7 +15,7 @@ jobs: - job: displayName: Build Sail Simulator pool: - vmImage: ubuntu-20.04 + vmImage: ubuntu-22.04 timeoutInMinutes: 30 steps: - checkout: self From 8efbb268da976bdbe8eb47e1eb676d0e647092a9 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Mon, 22 Jan 2024 17:28:31 +0000 Subject: [PATCH 2/9] Update sail-riscv submodule --- sail-riscv | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sail-riscv b/sail-riscv index 6d0cc0f..4b55553 160000 --- a/sail-riscv +++ b/sail-riscv @@ -1 +1 @@ -Subproject commit 6d0cc0fac7ad743651e295594c274e9b89ca23f7 +Subproject commit 4b555538e3fdf552799b5eae2f422c0aeb6a699f From 1d5fc5ab5fb2c7028257ba9bbbf172595d415fc5 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Fri, 12 Jan 2024 04:27:16 +0000 Subject: [PATCH 3/9] Catch up to upstream EXTZ/EXTS chages Adapt Alex's 182dc52ef468884f31c0e002118a8c75df0a69fb --- src/cheri_addr_checks.sail | 2 +- src/cheri_cap_common.sail | 6 +++--- src/cheri_decode_ext.sail | 12 ++++++------ src/cheri_insts.sail | 34 +++++++++++++++++----------------- src/cheri_mem_metadata.sail | 6 +++--- 5 files changed, 30 insertions(+), 30 deletions(-) diff --git a/src/cheri_addr_checks.sail b/src/cheri_addr_checks.sail index df90483..8688e84 100644 --- a/src/cheri_addr_checks.sail +++ b/src/cheri_addr_checks.sail @@ -76,7 +76,7 @@ function handle_cheri_cap_exception(capEx, regnum) = then print_string("CHERI ", string_of_capex(capEx) ^ " Reg=" ^ string_of_capreg_idx(regnum) ^ " PC=" ^ BitStr(PC)); let t : sync_exception = struct { trap = E_Extension(EXC_CHERI), - excinfo = Some(EXTZ(regnum @ CapExCode(capEx)) : xlenbits), + excinfo = Some(zero_extend(regnum @ CapExCode(capEx)) : xlenbits), ext = None() }; set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC)) diff --git a/src/cheri_cap_common.sail b/src/cheri_cap_common.sail index e150e12..cc82dcc 100644 --- a/src/cheri_cap_common.sail +++ b/src/cheri_cap_common.sail @@ -303,7 +303,7 @@ function encCapabilityToCapability(t,c) : (bool, EncCapability) -> Capability = let otype = (if isExe | c.cotype == 0b000 then 0b0 else 0b1) @ c.cotype; /* The 4-bit exponent is expanded to 5 bits, using 0xf to encode a cap_max_E value that enables representing the entire address space. */ - let E = if c.cE == 0xf then cap_max_E_bits else EXTZ(c.cE); + let E = if c.cE == 0xf then cap_max_E_bits else zero_extend(c.cE); return struct { tag = t, perm_user0 = perm_user0 , @@ -454,7 +454,7 @@ function setCapBounds(cap, base, length) : (Capability, CapAddrBits, CapAddrBits var B = truncate(base >> e_sat, cap_mantissa_width + 1); var T = truncate(top >> e_sat, cap_mantissa_width + 1); /* Work out whether we have lost significant bits in top */ - var maskLo : CapLenBits = EXTZ(ones(e_sat)); + var maskLo : CapLenBits = zero_extend(ones(e_sat)); lostSignificantTop = unsigned(top & maskLo) != 0; if lostSignificantTop then { /* we must increment T to make sure it is still above top even with lost bits */ @@ -474,7 +474,7 @@ function setCapBounds(cap, base, length) : (Capability, CapAddrBits, CapAddrBits /* Recompute B, T, mask etc for new e_sat */ B = truncate(base >> e_sat, cap_mantissa_width + 1); T = truncate(top >> e_sat, cap_mantissa_width + 1); - maskLo = EXTZ(ones(e_sat)); + maskLo = zero_extend(ones(e_sat)); lostSignificantTop = unsigned(top & maskLo) != 0; if lostSignificantTop then { T = T + 1; diff --git a/src/cheri_decode_ext.sail b/src/cheri_decode_ext.sail index 2f15ccd..35c58c2 100644 --- a/src/cheri_decode_ext.sail +++ b/src/cheri_decode_ext.sail @@ -66,13 +66,13 @@ function ext_post_decode_hook(x) : ast -> ast = { UTYPE(imm, 0b0 @ cd : bits(4), RISCV_AUIPC) => AUIPCC(imm, 0b0 @ cd), RISCV_JAL(imm, cd) => CJAL(imm, cd), RISCV_JALR(imm, cs1, cd) => CJALR(imm, cs1, cd), - C_JAL(imm) => CJAL(EXTS(imm @ 0b0), ra), - C_JALR(rs1) => CJALR(EXTZ(0b0), rs1, ra), - C_J(imm) => CJAL(EXTS(imm @ 0b0), zreg), - C_JR(rs1) => CJALR(EXTZ(0b0), rs1, zreg), + C_JAL(imm) => CJAL(sign_extend(imm @ 0b0), ra), + C_JALR(rs1) => CJALR(zero_extend(0b0), rs1, ra), + C_J(imm) => CJAL(sign_extend(imm @ 0b0), zreg), + C_JR(rs1) => CJALR(zero_extend(0b0), rs1, zreg), C_MV(rd, 0b1 @ rs2 : bits(4)) => CMove(rd, 0b0 @ rs2), - C_ADDI4SPN(rdc, nzimm) => CIncAddrImmediate(creg2reg_idx(rdc), sp, EXTZ(nzimm @ 0b00)), - C_ADDI16SP(imm) => CIncAddrImmediate(sp, sp, EXTS(imm @ 0x0)), + C_ADDI4SPN(rdc, nzimm) => CIncAddrImmediate(creg2reg_idx(rdc), sp, zero_extend(nzimm @ 0b00)), + C_ADDI16SP(imm) => CIncAddrImmediate(sp, sp, sign_extend(imm @ 0x0)), OTHERS => OTHERS } } diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index b2b4dea..380a6a9 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -68,7 +68,7 @@ union clause ast = AUIPCC : (bits(20), regidx) * **address** replaced with **PCC**.**address** $+$ *imm* $\times$ 2048. */ function clause execute AUIPCC(imm, cd) = { - let off : xlenbits = EXTS(imm) << 11; + let off : xlenbits = sign_extend(imm) << 11; let (representable, newCap) = setCapAddr(PCC, PC + off); C(cd) = clearTagIf(newCap, not(representable)); RETIRE_SUCCESS @@ -80,7 +80,7 @@ union clause ast = AUICGP : (bits(20), regidx) * **address** replaced with **CGP**.**address** $+$ *imm* $\times$ 2048. */ function clause execute AUICGP(imm, cd) = { - let off : xlenbits = EXTS(imm) << 11; + let off : xlenbits = sign_extend(imm) << 11; let cgp_val = C(CGP_IDX); /* $c3 */ let (representable, newCap) = incCapAddr(cgp_val, off); C(cd) = clearTagIf(newCap, isCapSealed(cgp_val) | not(representable)); @@ -100,7 +100,7 @@ union clause ast = CJAL : (bits(21), regidx) * - **PCC**.**address** $+$ *imm* is unaligned, ignoring bit 0. */ function clause execute(CJAL(imm, cd)) = { - let off : xlenbits = EXTS(imm); + let off : xlenbits = sign_extend(imm); let newPC = PC + off; if not(inCapBounds(PCC, newPC, min_instruction_bytes())) then { handle_cheri_cap_exception(CapEx_BoundsViolation, PCC_IDX); @@ -140,7 +140,7 @@ union clause ast = CJALR : (bits(12), regidx, regidx) */ function clause execute(CJALR(imm, cs1, cd)) = { let cs1_val = C(cs1); - let off : xlenbits = EXTS(imm); + let off : xlenbits = sign_extend(imm); let newPC = [cs1_val.address + off with 0 = bitzero]; /* clear bit zero as for RISCV JALR */ if not (cs1_val.tag) then { handle_cheri_reg_exception(CapEx_TagViolation, cs1); @@ -191,7 +191,7 @@ union clause ast = CGetTop : (regidx, regidx) */ function clause execute (CGetPerm(rd, cs1)) = { let capVal = C(cs1); - X(rd) = EXTZ(getCapPerms(capVal)); + X(rd) = zero_extend(getCapPerms(capVal)); RETIRE_SUCCESS } @@ -201,7 +201,7 @@ function clause execute (CGetPerm(rd, cs1)) = { */ function clause execute (CGetType(rd, cs1)) = { let capVal = C(cs1); - X(rd) = EXTZ(capVal.otype); + X(rd) = zero_extend(capVal.otype); RETIRE_SUCCESS } @@ -297,7 +297,7 @@ function clause execute (CGetLen(rd, cs1)) = { */ function clause execute (CGetTag(rd, cs1)) = { let capVal = C(cs1); - X(rd) = EXTZ(bool_to_bits(capVal.tag)); + X(rd) = zero_extend(bool_to_bits(capVal.tag)); RETIRE_SUCCESS } @@ -434,7 +434,7 @@ union clause ast = CIncAddrImmediate : (regidx, regidx, bits(12)) */ function clause execute (CIncAddrImmediate(cd, cs1, imm)) = { let cs1_val = C(cs1); - let immBits : xlenbits = EXTS(imm); + let immBits : xlenbits = sign_extend(imm); let inCap = clearTagIfSealed(cs1_val); let (success, newCap) = incCapAddr(inCap, immBits); @@ -520,7 +520,7 @@ function clause execute (CSetBoundsImmediate(cd, cs1, uimm)) = { let cs1_val = C(cs1); let newBase = cs1_val.address; - let newLen : CapAddrBits = EXTZ(uimm); + let newLen : CapAddrBits = zero_extend(uimm); let inBounds = inCapBounds(cs1_val, newBase, unsigned(newLen)); let inCap = clearTagIfSealed(cs1_val); @@ -641,7 +641,7 @@ function clause execute (CTestSubset(rd, cs1, cs2)) = { else 0b1; - X(rd) = EXTZ(result); + X(rd) = zero_extend(result); RETIRE_SUCCESS } @@ -654,7 +654,7 @@ union clause ast = CSEQX : (regidx, regidx, regidx) function clause execute (CSEQX(rd, cs1, cs2)) = { let cs1_val = C(cs1); let cs2_val = C(cs2); - X(rd) = EXTZ(bool_to_bits(cs1_val == cs2_val)); + X(rd) = zero_extend(bool_to_bits(cs1_val == cs2_val)); RETIRE_SUCCESS } @@ -746,7 +746,7 @@ union clause ast = LoadCapImm : (regidx, regidx, bits(12)) * implementation supports unaligned data accesses. */ function clause execute LoadCapImm(cd, cs1, imm) = { - let offset : xlenbits = EXTS(imm); + let offset : xlenbits = sign_extend(imm); let auth_val = C(cs1); let vaddrBits = auth_val.address + offset; if not(auth_val.tag) then { @@ -819,7 +819,7 @@ union clause ast = StoreCapImm : (regidx, regidx, bits(12)) * - *cs1*.**address** $+$ *imm* $+$ **CLEN** $/$ 8 $\gt$ *cs1*.**top**. */ function clause execute StoreCapImm(cs2, cs1, imm) = { - let offset : xlenbits = EXTS(imm); + let offset : xlenbits = sign_extend(imm); let auth_val = C(cs1); let vaddrBits = auth_val.address + offset; let cs2_val = C(cs2); @@ -971,7 +971,7 @@ mapping clause encdec_compressed = C_CLCSP(ui86 @ ui5 @ ui43, rd) if rd != zreg function clause execute (C_CLCSP(uimm, rd)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); execute(LoadCapImm(rd, sp, imm)) } @@ -989,7 +989,7 @@ mapping clause encdec_compressed = C_CSCSP(ui86 @ ui53, rs2) <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10 function clause execute (C_CSCSP(uimm, rs2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); execute(StoreCapImm(rs2, sp, imm)) } @@ -1005,7 +1005,7 @@ mapping clause encdec_compressed = C_CLC(ui76 @ ui53, rs1, rd) <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00 function clause execute (C_CLC(uimm, rsc, rdc)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); let rd = creg2reg_idx(rdc); let rs = creg2reg_idx(rsc); execute(LoadCapImm(rd, rs, imm)) @@ -1023,7 +1023,7 @@ mapping clause encdec_compressed = C_CSC(ui76 @ ui53, rs1, rs2) <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00 function clause execute (C_CSC(uimm, rsc1, rsc2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); let rs1 = creg2reg_idx(rsc1); let rs2 = creg2reg_idx(rsc2); execute(StoreCapImm(rs2, rs1, imm)) diff --git a/src/cheri_mem_metadata.sail b/src/cheri_mem_metadata.sail index eb422d0..2092a3f 100644 --- a/src/cheri_mem_metadata.sail +++ b/src/cheri_mem_metadata.sail @@ -79,7 +79,7 @@ function __WriteRAM_Meta(addr, width, tag) = { let tag_addr = addr_to_tag_addr(addr); if get_config_print_mem() then print_mem("tag[" ^ BitStr(tag_addr_to_addr(tag_addr)) ^ "] <- " ^ (if tag then "1" else "0")); - MEMw_tag(EXTZ(tag_addr), tag); + MEMw_tag(zero_extend(tag_addr), tag); /* If the write crosses a cap_size alignment boundary then we need * to write the tag for the subsequent region. Writes greater than * cap_size that might span more than two regions are not supported. @@ -88,7 +88,7 @@ function __WriteRAM_Meta(addr, width, tag) = { if tag_addr != tag_addr2 then { if get_config_print_mem() then print_mem("tag[" ^ BitStr(tag_addr_to_addr(tag_addr2)) ^ "] <- " ^ (if tag then "1" else "0")); - MEMw_tag(EXTZ(tag_addr2), tag); + MEMw_tag(zero_extend(tag_addr2), tag); } } @@ -96,7 +96,7 @@ function __WriteRAM_Meta(addr, width, tag) = { val __ReadRAM_Meta : forall 'n. (xlenbits, atom('n)) -> mem_meta effect {rmemt} function __ReadRAM_Meta(addr, width) = { let tag_addr = addr_to_tag_addr(addr); - let tag = MEMr_tag(EXTZ(tag_addr)); + let tag = MEMr_tag(zero_extend(tag_addr)); if get_config_print_mem() then print_mem("tag[R," ^ BitStr(tag_addr_to_addr(tag_addr)) ^ "] -> " ^ (if tag then "1" else "0")); tag From 1e1e69557d258881330de8c2daa9651c2fc182c7 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Fri, 12 Jan 2024 04:30:34 +0000 Subject: [PATCH 4/9] Catch up to internal_error() changes Adapts Alex's 3e6a55f69ee74ba5dcbd63506f992151870c24a6 --- src/cheri_addr_checks.sail | 8 ++++---- src/cheri_insts.sail | 4 ++-- src/cheri_pte.sail | 2 +- src/cheri_ptw.sail | 2 +- src/cheri_regs.sail | 4 ++-- src/cheri_sys_exceptions.sail | 18 +++++++++--------- 6 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/cheri_addr_checks.sail b/src/cheri_addr_checks.sail index 8688e84..ba2fbbe 100644 --- a/src/cheri_addr_checks.sail +++ b/src/cheri_addr_checks.sail @@ -176,10 +176,10 @@ function ext_data_get_addr(base_reg : regidx, offset : xlenbits, acc : AccessTyp Read(Data) => (auth_val.permit_load, true ), Write(Data) => (true , auth_val.permit_store), ReadWrite(Data, Data) => (auth_val.permit_load, auth_val.permit_store), - Execute() => internal_error("ext_data_get_addr for Execute"), - Read(_) => internal_error("ext_data_get_addr for Read(_)"), - Write(_) => internal_error("ext_data_get_addr for Write(_)"), - ReadWrite(_, _) => internal_error("ext_data_get_addr for ReadWrite(_, _)") + Execute() => internal_error(__FILE__, __LINE__,"ext_data_get_addr for Execute"), + Read(_) => internal_error(__FILE__, __LINE__,"ext_data_get_addr for Read(_)"), + Write(_) => internal_error(__FILE__, __LINE__,"ext_data_get_addr for Write(_)"), + ReadWrite(_, _) => internal_error(__FILE__, __LINE__,"ext_data_get_addr for ReadWrite(_, _)") }; if not(auth_val.tag) then diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index 380a6a9..a19456b 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -765,7 +765,7 @@ function clause execute LoadCapImm(cd, cs1, imm) = { handle_mem_exception(vaddrBits, E_Load_Addr_Align()); RETIRE_FAIL } else match translateAddr(vaddrBits, Read(Cap)) { - TR_Failure(E_Extension(_), _) => { internal_error("unexpected cheri exception for cap load") }, + TR_Failure(E_Extension(_), _) => { internal_error(__FILE__, __LINE__,"unexpected cheri exception for cap load") }, TR_Failure(e, _) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL }, TR_Address(addr, ptw_info) => { let c = mem_read_cap(addr, false, false, false); @@ -854,7 +854,7 @@ function clause execute StoreCapImm(cs2, cs1, imm) = { let res : MemoryOpResult(bool) = mem_write_cap(addr, cs2_val, false, false, false); match (res) { MemValue(true) => RETIRE_SUCCESS, - MemValue(false) => internal_error("store got false from mem_write_value"), + MemValue(false) => internal_error(__FILE__, __LINE__,"store got false from mem_write_value"), MemException(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL } } } diff --git a/src/cheri_pte.sail b/src/cheri_pte.sail index 223e4b9..9f4b029 100644 --- a/src/cheri_pte.sail +++ b/src/cheri_pte.sail @@ -136,7 +136,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, (ReadWrite(_), Supervisor) => (p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)), (Execute(), Supervisor) => p.U() == 0b0 & p.X() == 0b1, - (_, Machine) => internal_error("m-mode mem perm check") + (_, Machine) => internal_error(__FILE__, __LINE__,"m-mode mem perm check") }; let e = Mk_Ext_PTE_Bits(ext); diff --git a/src/cheri_ptw.sail b/src/cheri_ptw.sail index 5f0b30f..e3acc9a 100644 --- a/src/cheri_ptw.sail +++ b/src/cheri_ptw.sail @@ -102,7 +102,7 @@ function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> (ReadWrite(_, Cap), PTW_Ext_Error(AT_CAP_ERR)) => E_Extension(EXC_SAMO_CAP_PAGE_FAULT), /* No other operations should raise CHERI-specific page faults */ - (_, PTW_Ext_Error(_)) => internal_error("Unexpected PTW Extension Error"), + (_, PTW_Ext_Error(_)) => internal_error(__FILE__, __LINE__,"Unexpected PTW Extension Error"), /* For other exceptions, Cap and Data accesses fault in the same way. */ (ReadWrite(_, _), PTW_Access()) => E_SAMO_Access_Fault(), diff --git a/src/cheri_regs.sail b/src/cheri_regs.sail index d99c083..042c8ea 100644 --- a/src/cheri_regs.sail +++ b/src/cheri_regs.sail @@ -82,7 +82,7 @@ function rC r = { 13 => x13, 14 => x14, 15 => x15, - _ => internal_error("Invalid capability register") + _ => internal_error(__FILE__, __LINE__,"Invalid capability register") } } @@ -108,7 +108,7 @@ function wC (r, v) = { 13 => x13 = v, 14 => x14 = v, 15 => x15 = v, - _ => internal_error("Invalid capability register") + _ => internal_error(__FILE__, __LINE__,"Invalid capability register") }; if (r != 0) then { rvfi_wX(r, v.address); diff --git a/src/cheri_sys_exceptions.sail b/src/cheri_sys_exceptions.sail index 61bc64a..1f86e78 100644 --- a/src/cheri_sys_exceptions.sail +++ b/src/cheri_sys_exceptions.sail @@ -76,18 +76,18 @@ function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) - assert(representable, "mepcc should always be representable"); MEPCC = mepcc }, - _ => internal_error("unsupported") + _ => internal_error(__FILE__, __LINE__,"unsupported") } } /* used for traps and ECALL */ function prepare_trap_vector(p : Privilege, c : Mcause) -> xlenbits = { - if p != Machine then internal_error("unsupported"); + if p != Machine then internal_error(__FILE__, __LINE__,"unsupported"); let tcc : Capability = MTCC; match tvec_addr(Mk_Mtvec(tcc.address), c) { Some(addr) => { nextPCC = tcc; addr }, /* XXX addr could be unrepresentable or sealing violation! */ - None() => internal_error("Invalid tvec mode") + None() => internal_error(__FILE__, __LINE__,"Invalid tvec mode") } } @@ -102,7 +102,7 @@ function prepare_trap_vector(p : Privilege, c : Mcause) -> xlenbits = { */ val get_xret_target : Privilege -> xlenbits effect {escape, rreg} function get_xret_target(p) = { - if p != Machine then internal_error("unsupported"); + if p != Machine then internal_error(__FILE__, __LINE__,"unsupported"); let cap : Capability = MEPCC; legalize_xepc(cap.address) } @@ -116,12 +116,12 @@ function get_xret_target(p) = { */ val set_xret_target : (Privilege, xlenbits) -> xlenbits effect {escape} function set_xret_target(p, value) = { - internal_error("unsupported"); + internal_error(__FILE__, __LINE__,"unsupported"); } val prepare_xret_target : (Privilege) -> xlenbits effect {rreg, wreg, escape} function prepare_xret_target(p) = { - if p != Machine then internal_error("unsupported"); + if p != Machine then internal_error(__FILE__, __LINE__,"unsupported"); /* Similar to prepare_trap_vector above we need to return the absolute address destined for PC, rather than the offset (architecutral PC) */ @@ -153,16 +153,16 @@ function get_utvec() -> xlenbits = zeros() function set_mtvec(value : xlenbits) -> xlenbits = { - internal_error("unsupported"); + internal_error(__FILE__, __LINE__,"unsupported"); zeros() } function set_stvec(value : xlenbits) -> xlenbits = { - internal_error("unsupported"); + internal_error(__FILE__, __LINE__,"unsupported"); zeros() } function set_utvec(value : xlenbits) -> xlenbits = { - internal_error("unsupported"); + internal_error(__FILE__, __LINE__,"unsupported"); zeros() } From d7d372beb6eec684e6607bdb4c037785868dd17b Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Fri, 12 Jan 2024 04:32:00 +0000 Subject: [PATCH 5/9] Include minimal V ext files from base model --- Makefile | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Makefile b/Makefile index 4a7acf6..255c39d 100644 --- a/Makefile +++ b/Makefile @@ -16,6 +16,7 @@ SAIL_RV64_XLEN := $(SAIL_RISCV_MODEL_DIR)/riscv_xlen64.sail SAIL_XLEN = $(SAIL_$(ARCH)_XLEN) SAIL_FLEN = $(SAIL_RISCV_MODEL_DIR)/riscv_flen_D.sail +SAIL_VLEN = $(SAIL_RISCV_MODEL_DIR)/riscv_vlen.sail # Instruction sources, depending on target SAIL_CHECK_SRCS = $(SAIL_RISCV_MODEL_DIR)/riscv_addr_checks_common.sail \ @@ -62,6 +63,7 @@ PRELUDE = $(SAIL_RISCV_MODEL_DIR)/prelude.sail \ $(SAIL_RISCV_MODEL_DIR)/prelude_mapping.sail \ $(SAIL_XLEN) \ $(SAIL_FLEN) \ + $(SAIL_VLEN) \ $(SAIL_CHERI_MODEL_DIR)/cheri_prelude.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_types.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_cap_common.sail \ @@ -80,6 +82,9 @@ SAIL_REGS_SRCS = $(SAIL_CHERI_MODEL_DIR)/cheri_reg_type.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_regs.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_pc_access.sail +SAIL_REGS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_vreg_type.sail \ + $(SAIL_RISCV_MODEL_DIR)/riscv_vext_regs.sail + SAIL_ARCH_SRCS = $(PRELUDE) \ $(SAIL_RISCV_MODEL_DIR)/riscv_types_common.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_riscv_types.sail \ From 6accac1e1a6d02ff7d99b12d4bac131aa9d657f9 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Sat, 13 Jan 2024 18:11:36 +0000 Subject: [PATCH 6/9] Catch up with sail-riscv --- Makefile | 3 ++- src/cheri_prelude.sail | 9 --------- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/Makefile b/Makefile index 255c39d..21330d6 100644 --- a/Makefile +++ b/Makefile @@ -60,7 +60,6 @@ SAIL_VM_SRCS += $(SAIL_$(ARCH)_VM_SRCS) # Non-instruction sources PRELUDE = $(SAIL_RISCV_MODEL_DIR)/prelude.sail \ - $(SAIL_RISCV_MODEL_DIR)/prelude_mapping.sail \ $(SAIL_XLEN) \ $(SAIL_FLEN) \ $(SAIL_VLEN) \ @@ -111,12 +110,14 @@ SAIL_ARCH_RVFI_SRCS = \ SAIL_STEP_SRCS = $(SAIL_RISCV_MODEL_DIR)/riscv_step_common.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_step_ext.sail \ + $(SAIL_RISCV_MODEL_DIR)/riscv_decode_ext.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_decode_ext.sail \ $(SAIL_RISCV_MODEL_DIR)/riscv_fetch.sail \ $(SAIL_RISCV_MODEL_DIR)/riscv_step.sail RVFI_STEP_SRCS = $(SAIL_RISCV_MODEL_DIR)/riscv_step_common.sail \ $(SAIL_RISCV_MODEL_DIR)/riscv_step_rvfi.sail \ + $(SAIL_RISCV_MODEL_DIR)/riscv_decode_ext.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_decode_ext.sail \ $(SAIL_RISCV_MODEL_DIR)/riscv_fetch_rvfi.sail \ $(SAIL_RISCV_MODEL_DIR)/riscv_step.sail diff --git a/src/cheri_prelude.sail b/src/cheri_prelude.sail index b877def..e2b5344 100644 --- a/src/cheri_prelude.sail +++ b/src/cheri_prelude.sail @@ -68,15 +68,6 @@ val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt } val MAX : forall 'n, 'n >= 0 . atom('n) -> atom(2 ^ 'n - 1) effect pure function MAX(n) = pow2(n) - 1 -val not = {coq:"negb", _:"not"} : bool -> bool - -/*! - * THIS converts a boolean to a bit in the conventional way by mapping `true` to - * `bitone` and `false` to `bitzero`. - */ -val bool_to_bit : bool -> bit -function bool_to_bit x = if x then bitone else bitzero - /*! * align_down(n, bv) returns the given bit vector, bv, aligned down to a power * of two by clearing the least significant n bits. From 124bdaa0a432eb471ad62f2ebf69caf6f9bb5b2b Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Sat, 13 Jan 2024 18:13:56 +0000 Subject: [PATCH 7/9] Update patches to upsteram sail-riscv --- ...for-CHERI-MCU-E-not-I-not-U-not-S-no.patch | 34 +++++++------- ...ng-of-msatus.MIE-in-M-mode-only-case.patch | 10 ++-- ...-or-writing-upper-16-registers-TODO-.patch | 12 ++--- ...utput-only-MMIO-UART-for-terminal-ou.patch | 41 ++++++++--------- ...mmand-line-arguments-to-enable-or-di.patch | 46 +++++++++---------- ...ion-trace-option-that-prints-only-on.patch | 35 +++++++------- ...riscv_sim-disable-tracing-by-default.patch | 8 ++-- ...tif-exit-code-through-to-exit-so-we-.patch | 12 ++--- ...anism-to-track-new-lines-in-terminal.patch | 44 +++++++++++------- 9 files changed, 127 insertions(+), 115 deletions(-) diff --git a/riscv_patches/0001-Initialise-misa-for-CHERI-MCU-E-not-I-not-U-not-S-no.patch b/riscv_patches/0001-Initialise-misa-for-CHERI-MCU-E-not-I-not-U-not-S-no.patch index 896131d..ab6dc6a 100644 --- a/riscv_patches/0001-Initialise-misa-for-CHERI-MCU-E-not-I-not-U-not-S-no.patch +++ b/riscv_patches/0001-Initialise-misa-for-CHERI-MCU-E-not-I-not-U-not-S-no.patch @@ -1,35 +1,35 @@ -From d5a0048e5274cb1ce81030cfccc68060ce1183a4 Mon Sep 17 00:00:00 2001 +From 47c0bc46ee6152b89addb9432945b140bfe7fe3d Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 31 Oct 2022 14:19:28 +0000 -Subject: [PATCH 01/10] Initialise misa for CHERI-MCU: E not I, not U, not S, - not A. +Subject: [PATCH 1/9] Initialise misa for CHERI-MCU: E not I, not U, not S, not + A. --- model/riscv_sys_control.sail | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail -index 6204ae5..9e684d9 100644 +index 3830725..914caec 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail -@@ -552,12 +552,13 @@ function init_sys() -> unit = { - mhartid = EXTZ(0b0); +@@ -556,12 +556,13 @@ function init_sys() -> unit = { + mhartid = zero_extend(0b0); misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); -- misa->A() = 0b1; /* atomics */ -+ // misa->A() = 0b1; /* atomics */ - misa->C() = bool_to_bits(sys_enable_rvc()); /* RVC */ -- misa->I() = 0b1; /* base integer ISA */ -+ // misa->I() = 0b1; /* base integer ISA */ +- misa->A() = 0b1; /* atomics */ ++ // misa->A() = 0b1; /* atomics */ + misa->C() = bool_to_bits(sys_enable_rvc()); /* RVC */ +- misa->I() = 0b1; /* base integer ISA */ ++ // misa->I() = 0b1; /* base integer ISA */ + misa->E() = 0b1; - misa->M() = 0b1; /* integer multiply/divide */ -- misa->U() = 0b1; /* user-mode */ -- misa->S() = 0b1; /* supervisor-mode */ -+ misa->U() = 0b0; /* user-mode */ -+ misa->S() = 0b0; /* supervisor-mode */ + misa->M() = 0b1; /* integer multiply/divide */ +- misa->U() = 0b1; /* user-mode */ +- misa->S() = 0b1; /* supervisor-mode */ ++ misa->U() = 0b0; /* user-mode */ ++ misa->S() = 0b0; /* supervisor-mode */ + misa->V() = bool_to_bits(sys_enable_vext()); /* vector extension */ if sys_enable_fdext() & sys_enable_zfinx() - then internal_error("F and Zfinx cannot both be enabled!"); -- 2.39.2 diff --git a/riscv_patches/0002-Fix-handling-of-msatus.MIE-in-M-mode-only-case.patch b/riscv_patches/0002-Fix-handling-of-msatus.MIE-in-M-mode-only-case.patch index 180a9d4..424b44d 100644 --- a/riscv_patches/0002-Fix-handling-of-msatus.MIE-in-M-mode-only-case.patch +++ b/riscv_patches/0002-Fix-handling-of-msatus.MIE-in-M-mode-only-case.patch @@ -1,7 +1,7 @@ -From 8f054703175f4f1421b4638cfca50ba1e4e283bd Mon Sep 17 00:00:00 2001 +From 848c46be16d338cca297ca1e19527406f75befb5 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 31 Oct 2022 14:21:17 +0000 -Subject: [PATCH 02/10] Fix handling of msatus.MIE in M-mode only case. +Subject: [PATCH 2/9] Fix handling of msatus.MIE in M-mode only case. Previously if neither user or supervisor mode are present dispatchInterrupt ignored mstatus.MIE leading to an infinite interrupt @@ -11,12 +11,12 @@ loop. 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail -index 9e684d9..54a8daf 100644 +index 914caec..6b2aa42 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail -@@ -341,10 +341,14 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege +@@ -345,10 +345,14 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege */ - if (~ (haveUsrMode())) | ((~ (haveSupMode())) & (~ (haveNExt()))) then { + if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then { assert(priv == Machine, "invalid current privilege"); - let enabled_pending = mip.bits() & mie.bits(); - match findPendingInterrupt(enabled_pending) { diff --git a/riscv_patches/0003-Crash-if-reading-or-writing-upper-16-registers-TODO-.patch b/riscv_patches/0003-Crash-if-reading-or-writing-upper-16-registers-TODO-.patch index a6e0a28..56f341b 100644 --- a/riscv_patches/0003-Crash-if-reading-or-writing-upper-16-registers-TODO-.patch +++ b/riscv_patches/0003-Crash-if-reading-or-writing-upper-16-registers-TODO-.patch @@ -1,18 +1,18 @@ -From 6970cd7d361b44f9ca52a5abd4a0e6c4ac550482 Mon Sep 17 00:00:00 2001 +From d2f3d2cefbe1257a6f7eb5d1aa82a8eccab066e8 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 31 Oct 2022 14:49:45 +0000 -Subject: [PATCH 03/10] Crash if reading or writing upper 16 registers: TODO - this should really be reserved instruction trap. +Subject: [PATCH 3/9] Crash if reading or writing upper 16 registers: TODO this + should really be reserved instruction trap. --- model/riscv_regs.sail | 32 -------------------------------- 1 file changed, 32 deletions(-) diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail -index a65c6c5..d9ef101 100644 +index 15e7613..4ff7871 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail -@@ -128,22 +128,6 @@ function rX r = { +@@ -130,22 +130,6 @@ function rX r = { 13 => x13, 14 => x14, 15 => x15, @@ -35,7 +35,7 @@ index a65c6c5..d9ef101 100644 _ => {assert(false, "invalid register number"); zero_reg} }; regval_from_reg(v) -@@ -181,22 +165,6 @@ function wX (r, in_v) = { +@@ -183,22 +167,6 @@ function wX (r, in_v) = { 13 => x13 = v, 14 => x14 = v, 15 => x15 = v, diff --git a/riscv_patches/0004-Add-very-basic-output-only-MMIO-UART-for-terminal-ou.patch b/riscv_patches/0004-Add-very-basic-output-only-MMIO-UART-for-terminal-ou.patch index e42d4af..fea446d 100644 --- a/riscv_patches/0004-Add-very-basic-output-only-MMIO-UART-for-terminal-ou.patch +++ b/riscv_patches/0004-Add-very-basic-output-only-MMIO-UART-for-terminal-ou.patch @@ -1,8 +1,7 @@ -From 812e68c5745c8e220c3ba67374a6d889a6c9ec63 Mon Sep 17 00:00:00 2001 +From a64a1c55a35e95d8303156e52cca02d48a9e161e Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 31 Oct 2022 14:59:58 +0000 -Subject: [PATCH 04/10] Add very basic output-only MMIO UART for terminal - output. +Subject: [PATCH 4/9] Add very basic output-only MMIO UART for terminal output. Mapped at 0x10000100 to match flute, with address hardcoded in a similar way to CLINT. Should make this configurable. @@ -15,12 +14,12 @@ similar way to CLINT. Should make this configurable. 5 files changed, 95 insertions(+), 4 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c -index 2572dbc..7a257fc 100644 +index fbd63fa..71600d2 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c -@@ -58,6 +58,13 @@ mach_bits plat_clint_base(unit u) - mach_bits plat_clint_size(unit u) - { return rv_clint_size; } +@@ -108,6 +108,13 @@ mach_bits plat_clint_size(unit u) + return rv_clint_size; + } +mach_bits plat_uart_base(unit u) +{ return rv_uart_base; } @@ -33,10 +32,10 @@ index 2572dbc..7a257fc 100644 { reservation = addr; diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h -index 5335a90..a9b98bb 100644 +index 4b6541f..9a3f25a 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h -@@ -25,6 +25,9 @@ mach_bits plat_get_16_random_bits(); +@@ -27,6 +27,9 @@ mach_bits plat_get_16_random_bits(); mach_bits plat_clint_base(unit); mach_bits plat_clint_size(unit); @@ -47,10 +46,10 @@ index 5335a90..a9b98bb 100644 unit load_reservation(mach_bits); bool match_reservation(mach_bits); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c -index b1504a7..9aca0b7 100644 +index 15ff8ad..75f77e9 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c -@@ -37,6 +37,9 @@ uint64_t rv_16_random_bits(void) { +@@ -40,6 +40,9 @@ uint64_t rv_16_random_bits(void) uint64_t rv_clint_base = UINT64_C(0x2000000); uint64_t rv_clint_size = UINT64_C(0xc0000); @@ -61,10 +60,10 @@ index b1504a7..9aca0b7 100644 uint64_t rv_insns_per_tick = UINT64_C(100); diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h -index 165fb94..34edd1e 100644 +index e5c562a..0a6329e 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h -@@ -29,6 +29,9 @@ extern uint64_t rv_16_random_bits(void); +@@ -32,6 +32,9 @@ extern uint64_t rv_16_random_bits(void); extern uint64_t rv_clint_base; extern uint64_t rv_clint_size; @@ -75,10 +74,10 @@ index 165fb94..34edd1e 100644 extern uint64_t rv_insns_per_tick; diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail -index ea27f48..eb8946d 100644 +index 579a118..71960c2 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail -@@ -124,6 +124,10 @@ val plat_rom_size = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_si +@@ -126,6 +126,10 @@ val plat_rom_size = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_si val plat_clint_base = {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits val plat_clint_size = {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits @@ -89,7 +88,7 @@ index ea27f48..eb8946d 100644 /* Location of HTIF ports */ val plat_htif_tohost = {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits function plat_htif_tohost () = to_bits(sizeof(xlen), elf_tohost ()) -@@ -183,6 +187,18 @@ function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlen +@@ -185,6 +189,18 @@ function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlen function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) @@ -108,7 +107,7 @@ index ea27f48..eb8946d 100644 /* CLINT (Core Local Interruptor), based on Spike. */ val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int -@@ -452,20 +468,77 @@ function htif_tick() = { +@@ -454,20 +470,77 @@ function htif_tick() = { /* Top-level MMIO dispatch */ $ifndef RVFI_DII function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = @@ -143,7 +142,7 @@ index ea27f48..eb8946d 100644 +function uart_load(t, addr, width) = { + let offset = addr - plat_uart_base(); + /* We only support reading the status register, which always indicates ready to write output */ -+ if offset == UART_OFFSET_LINE_STATUS & ('n == 4) ++ if offset == zero_extend(UART_OFFSET_LINE_STATUS) & ('n == 4) + then { + let result = 0b100000; /* TXBufEmpty always */ + if get_config_print_platform() @@ -164,12 +163,12 @@ index ea27f48..eb8946d 100644 +function uart_store(addr, width, data) = { + let offset = addr - plat_uart_base(); + /* only support writing to the data register for output, ignore other writes */ -+ if offset == UART_OFFSET_DATA & ('n == 8 | 'n == 4) then { ++ if offset == zero_extend(UART_OFFSET_DATA) & ('n == 8 | 'n == 4) then { + if get_config_print_platform() + then print_platform("uart[" ^ BitStr(offset) ^ "] <- " ^ BitStr(data)); + if UART_DLAB == bitzero then plat_term_write(data[7..0]); + MemValue(true) -+ } else if offset == UART_OFFSET_LINE_CTL & ('n == 8 | 'n == 4) then { ++ } else if offset == zero_extend(UART_OFFSET_LINE_CTL) & ('n == 8 | 'n == 4) then { + if get_config_print_platform() + then print_platform("uart[" ^ BitStr(offset) ^ "] <- " ^ BitStr(data)); + UART_DLAB = data[7]; @@ -189,7 +188,7 @@ index ea27f48..eb8946d 100644 then clint_load(t, paddr, width) else if within_htif_readable(paddr, width) & (1 <= 'n) then htif_load(t, paddr, width) -@@ -476,7 +549,9 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_acc +@@ -478,7 +551,9 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_acc } function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = diff --git a/riscv_patches/0005-riscv_sim-Add-command-line-arguments-to-enable-or-di.patch b/riscv_patches/0005-riscv_sim-Add-command-line-arguments-to-enable-or-di.patch index 6417673..e675453 100644 --- a/riscv_patches/0005-riscv_sim-Add-command-line-arguments-to-enable-or-di.patch +++ b/riscv_patches/0005-riscv_sim-Add-command-line-arguments-to-enable-or-di.patch @@ -1,7 +1,7 @@ -From 41c00661efdc44da5f606941e833ba0395c51e5c Mon Sep 17 00:00:00 2001 +From a03f2b539f022bd64cdec1baba6bd0c8dba22846 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 31 Oct 2022 14:46:27 +0000 -Subject: [PATCH 05/10] riscv_sim: Add command line arguments to enable or +Subject: [PATCH 5/9] riscv_sim: Add command line arguments to enable or disable use of boot ROM. This adds command line arguments --boot-rom and --no-boot-rom to @@ -13,14 +13,14 @@ the simulator just sets the initial PC to the entry point. For backwards compatibility the default is to use the boot-rom unless NO_BOOT_ROM is defined during compilation. --- - c_emulator/riscv_sim.c | 20 ++++++++++++++++++-- - 1 file changed, 18 insertions(+), 2 deletions(-) + c_emulator/riscv_sim.c | 17 +++++++++++++++-- + 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c -index 5ad83e9..787714e 100644 +index 13d1653..08aa211 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c -@@ -76,6 +76,13 @@ bool config_print_reg = true; +@@ -83,6 +83,13 @@ bool config_print_reg = true; bool config_print_mem_access = true; bool config_print_platform = true; bool config_print_rvfi = false; @@ -32,42 +32,42 @@ index 5ad83e9..787714e 100644 +#endif +; - void set_config_print(char *var, bool val) { - if (var == NULL || strcmp("all", var) == 0) { -@@ -131,6 +138,8 @@ static struct option options[] = { - {"no-trace", optional_argument, 0, 'V'}, - {"inst-limit", required_argument, 0, 'l'}, - {"enable-zfinx", no_argument, 0, 'x'}, -+ {"boot-rom", no_argument, &config_use_boot_rom, true}, -+ {"no-boot-rom", no_argument, &config_use_boot_rom, false}, + void set_config_print(char *var, bool val) + { +@@ -142,6 +149,8 @@ static struct option options[] = { + {"inst-limit", required_argument, 0, 'l' }, + {"enable-zfinx", no_argument, 0, 'x' }, + {"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM}, ++ {"boot-rom", no_argument, &config_use_boot_rom, true}, ++ {"no-boot-rom", no_argument, &config_use_boot_rom, false}, #ifdef SAILCOV - {"sailcov-file", required_argument, 0, 'c'}, + {"sailcov-file", required_argument, 0, 'c' }, #endif -@@ -146,7 +155,10 @@ static void print_usage(const char *argv0, int ec) +@@ -156,10 +165,10 @@ static void print_usage(const char *argv0, int ec) #endif struct option *opt = options; while (opt->name) { -- fprintf(stdout, "\t -%c\t --%s\n", (char)opt->val, opt->name); +- if (isprint(opt->val)) + if (opt->flag == NULL) -+ fprintf(stdout, "\t -%c\t --%s\n", (char)opt->val, opt->name); -+ else + fprintf(stdout, "\t -%c\t --%s\n", (char)opt->val, opt->name); + else +- fprintf(stdout, "\t \t --%s\n", opt->name); + fprintf(stdout, "\t\t --%s\n", opt->name); opt++; } exit(ec); -@@ -551,7 +563,11 @@ void init_sail(uint64_t elf_entry) +@@ -601,7 +610,11 @@ void init_sail(uint64_t elf_entry) zPC = elf_entry; } else #endif -- init_sail_reset_vector(elf_entry); + if (config_use_boot_rom) { -+ init_sail_reset_vector(elf_entry); + init_sail_reset_vector(elf_entry); + } else { + zPC = elf_entry; + } // this is probably unnecessary now; remove - if (!rv_enable_rvc) z_set_Misa_C(&zmisa, 0); + if (!rv_enable_rvc) -- 2.39.2 diff --git a/riscv_patches/0006-Add-a-new-exception-trace-option-that-prints-only-on.patch b/riscv_patches/0006-Add-a-new-exception-trace-option-that-prints-only-on.patch index 257b38a..37312f5 100644 --- a/riscv_patches/0006-Add-a-new-exception-trace-option-that-prints-only-on.patch +++ b/riscv_patches/0006-Add-a-new-exception-trace-option-that-prints-only-on.patch @@ -1,7 +1,7 @@ -From 951cbc162ecdef31361e2dddf5bd84bd77ce9b44 Mon Sep 17 00:00:00 2001 +From 7fdf336470e32419126b205908b8ec1cc34234d3 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 18 Jan 2023 11:03:36 +0000 -Subject: [PATCH 06/10] Add a new 'exception' trace option that prints only on +Subject: [PATCH 6/9] Add a new 'exception' trace option that prints only on interrupts and exceptions. --- @@ -23,10 +23,10 @@ index f8f3eb3..dcbb32d 100644 extern bool config_print_platform; +extern bool config_print_exception; diff --git a/c_emulator/riscv_prelude.c b/c_emulator/riscv_prelude.c -index 92f8415..ad5a831 100644 +index 143a152..f65c591 100644 --- a/c_emulator/riscv_prelude.c +++ b/c_emulator/riscv_prelude.c -@@ -50,3 +50,8 @@ bool get_config_print_platform(unit u) +@@ -55,3 +55,8 @@ bool get_config_print_platform(unit u) { return (config_print_platform) ? true : false; } @@ -53,10 +53,10 @@ index 9ac33aa..84a4090 100644 +bool get_config_print_exception(unit u); \ No newline at end of file diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c -index 787714e..648c4c9 100644 +index 08aa211..b37103b 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c -@@ -76,6 +76,7 @@ bool config_print_reg = true; +@@ -83,6 +83,7 @@ bool config_print_reg = true; bool config_print_mem_access = true; bool config_print_platform = true; bool config_print_rvfi = false; @@ -64,7 +64,7 @@ index 787714e..648c4c9 100644 int config_use_boot_rom = #ifdef NO_BOOT_ROM false -@@ -91,6 +92,7 @@ void set_config_print(char *var, bool val) { +@@ -99,6 +100,7 @@ void set_config_print(char *var, bool val) config_print_reg = val; config_print_platform = val; config_print_rvfi = val; @@ -72,23 +72,24 @@ index 787714e..648c4c9 100644 } else if (strcmp("instr", var) == 0) { config_print_instr = val; } else if (strcmp("reg", var) == 0) { -@@ -101,8 +103,10 @@ void set_config_print(char *var, bool val) { +@@ -109,9 +111,11 @@ void set_config_print(char *var, bool val) config_print_rvfi = val; } else if (strcmp("platform", var) == 0) { config_print_platform = val; + } else if (strcmp("exception", var) == 0) { + config_print_exception = val; } else { -- fprintf(stderr, "Unknown trace category: '%s' (should be instr|reg|mem|platform|all)\n", var); -+ fprintf(stderr, "Unknown trace category: '%s' (should be instr|reg|mem|exception|platform|all)\n", var); + fprintf(stderr, "Unknown trace category: '%s' (should be %s)\n", +- "instr|reg|mem|platform|all", var); ++ "instr|reg|mem|exception|platform|all", var); exit(1); } } diff --git a/model/prelude.sail b/model/prelude.sail -index 6e6718b..29646e2 100644 +index 3e05a96..52947aa 100644 --- a/model/prelude.sail +++ b/model/prelude.sail -@@ -175,6 +175,7 @@ val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endl +@@ -164,6 +164,7 @@ val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endl val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool @@ -96,19 +97,19 @@ index 6e6718b..29646e2 100644 val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool // defaults for other backends -@@ -182,6 +183,7 @@ function get_config_print_instr () = false +@@ -171,6 +172,7 @@ function get_config_print_instr () = false function get_config_print_reg () = false function get_config_print_mem () = false function get_config_print_platform () = false +function get_config_print_exception () = false - val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) - val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) + val sign_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) + val zero_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) diff --git a/model/riscv_step.sail b/model/riscv_step.sail -index 40c0c80..5ba0e72 100644 +index 550f11a..146a168 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail -@@ -77,8 +77,8 @@ function step(step_no : int) -> bool = { +@@ -88,8 +88,8 @@ function step(step_no : int) -> bool = { let (retired, stepped) : (Retired, bool) = match dispatchInterrupt(cur_privilege) { Some(intr, priv) => { diff --git a/riscv_patches/0007-riscv_sim-disable-tracing-by-default.patch b/riscv_patches/0007-riscv_sim-disable-tracing-by-default.patch index ba36822..3130626 100644 --- a/riscv_patches/0007-riscv_sim-disable-tracing-by-default.patch +++ b/riscv_patches/0007-riscv_sim-disable-tracing-by-default.patch @@ -1,7 +1,7 @@ -From 487fe4de8060b5856d048904cc3d4ea3646f620e Mon Sep 17 00:00:00 2001 +From 1607644330f02e9e79380a8255ed3f215d88ff97 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 23 Jan 2023 15:04:55 +0000 -Subject: [PATCH 07/10] riscv_sim: disable tracing by default. +Subject: [PATCH 7/9] riscv_sim: disable tracing by default. The current default is excessively verbose, meaning most invocations require -V to disable verbose tracing, sometimes followed by options @@ -11,10 +11,10 @@ to selectively re-enable tracing. 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c -index 648c4c9..8fde33f 100644 +index b37103b..55d04ce 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c -@@ -71,12 +71,12 @@ uint64_t mem_sig_start = 0; +@@ -78,12 +78,12 @@ uint64_t mem_sig_start = 0; uint64_t mem_sig_end = 0; int signature_granularity = 4; diff --git a/riscv_patches/0008-riscv_sim-Pass-htif-exit-code-through-to-exit-so-we-.patch b/riscv_patches/0008-riscv_sim-Pass-htif-exit-code-through-to-exit-so-we-.patch index 8533acd..d7e8f7f 100644 --- a/riscv_patches/0008-riscv_sim-Pass-htif-exit-code-through-to-exit-so-we-.patch +++ b/riscv_patches/0008-riscv_sim-Pass-htif-exit-code-through-to-exit-so-we-.patch @@ -1,25 +1,25 @@ -From 93f474ef62752f9695fc65ff8c1d3da2ae25c8de Mon Sep 17 00:00:00 2001 +From 4be78b16b219dbed06649feaf494ae115580fa7a Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 26 Jan 2023 13:56:21 +0000 -Subject: [PATCH 08/10] riscv_sim: Pass htif exit code through to exit so we - can easily test it when running tests. +Subject: [PATCH 8/9] riscv_sim: Pass htif exit code through to exit so we can + easily test it when running tests. --- c_emulator/riscv_sim.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c -index 8fde33f..4bcff94 100644 +index 55d04ce..cdb1868 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c -@@ -964,7 +964,7 @@ void run_sail(void) +@@ -1034,7 +1034,7 @@ dump_state: if (diverged) { /* TODO */ } - finish(diverged); + finish(diverged | zhtif_exit_code); - step_exception: + step_exception: fprintf(stderr, "Sail exception!"); -- 2.39.2 diff --git a/riscv_patches/0009-Add-a-hacky-mechanism-to-track-new-lines-in-terminal.patch b/riscv_patches/0009-Add-a-hacky-mechanism-to-track-new-lines-in-terminal.patch index d6ec3f9..90d28f9 100644 --- a/riscv_patches/0009-Add-a-hacky-mechanism-to-track-new-lines-in-terminal.patch +++ b/riscv_patches/0009-Add-a-hacky-mechanism-to-track-new-lines-in-terminal.patch @@ -1,19 +1,19 @@ -From abca61fad742ce147f8877862f072a28df700e2b Mon Sep 17 00:00:00 2001 +From 4b555538e3fdf552799b5eae2f422c0aeb6a699f Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 3 Feb 2023 13:13:17 +0000 -Subject: [PATCH 09/10] Add a hacky mechanism to track new lines in terminal - and trace output and insert extra new lines to keep them separate. +Subject: [PATCH 9/9] Add a hacky mechanism to track new lines in terminal and + trace output and insert extra new lines to keep them separate. --- c_emulator/riscv_platform_impl.c | 6 ++++++ - c_emulator/riscv_prelude.c | 20 ++++++++++++++++++++ - 2 files changed, 26 insertions(+) + c_emulator/riscv_prelude.c | 24 ++++++++++++++++++++++-- + 2 files changed, 28 insertions(+), 2 deletions(-) diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c -index 9aca0b7..e554d09 100644 +index 75f77e9..c181bb4 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c -@@ -44,9 +44,15 @@ uint64_t rv_htif_tohost = UINT64_C(0x80001000); +@@ -47,9 +47,15 @@ uint64_t rv_htif_tohost = UINT64_C(0x80001000); uint64_t rv_insns_per_tick = UINT64_C(100); int term_fd = 1; // set during startup @@ -30,12 +30,12 @@ index 9aca0b7..e554d09 100644 + have_newline = c == '\n'; } diff --git a/c_emulator/riscv_prelude.c b/c_emulator/riscv_prelude.c -index ad5a831..2235ba0 100644 +index f65c591..2b8d3df 100644 --- a/c_emulator/riscv_prelude.c +++ b/c_emulator/riscv_prelude.c -@@ -1,33 +1,53 @@ - #include "riscv_prelude.h" +@@ -2,37 +2,57 @@ #include "riscv_config.h" + #include "riscv_platform_impl.h" +/* Attempt to keep track of whether output is at the start of a line so that we + * can produce nicer output if trace output interrupts terminal output. */ @@ -44,13 +44,14 @@ index ad5a831..2235ba0 100644 +void ensure_newline() +{ + if (!have_newline) -+ putchar('\n'); ++ fputc('\n', trace_log); +} + unit print_string(sail_string prefix, sail_string msg) { +- printf("%s%s\n", prefix, msg); + ensure_newline(); - printf("%s%s\n", prefix, msg); ++ fprintf(trace_log, "%s%s\n", prefix, msg); + have_newline = true; return UNIT; } @@ -58,7 +59,8 @@ index ad5a831..2235ba0 100644 unit print_instr(sail_string s) { + ensure_newline(); - if (config_print_instr) printf("%s\n", s); + if (config_print_instr) + fprintf(trace_log, "%s\n", s); + have_newline = true; return UNIT; } @@ -66,7 +68,8 @@ index ad5a831..2235ba0 100644 unit print_reg(sail_string s) { + ensure_newline(); - if (config_print_reg) printf("%s\n", s); + if (config_print_reg) + fprintf(trace_log, "%s\n", s); + have_newline = true; return UNIT; } @@ -74,7 +77,8 @@ index ad5a831..2235ba0 100644 unit print_mem_access(sail_string s) { + ensure_newline(); - if (config_print_mem_access) printf("%s\n", s); + if (config_print_mem_access) + fprintf(trace_log, "%s\n", s); + have_newline = true; return UNIT; } @@ -82,11 +86,19 @@ index ad5a831..2235ba0 100644 unit print_platform(sail_string s) { + ensure_newline(); - if (config_print_platform) printf("%s\n", s); + if (config_print_platform) + fprintf(trace_log, "%s\n", s); + have_newline = true; return UNIT; } +@@ -59,4 +79,4 @@ bool get_config_print_platform(unit u) + bool get_config_print_exception(unit u) + { + return (config_print_exception) ? true : false; +-} +\ No newline at end of file ++} -- 2.39.2 From a79815be42c1952ff75884f5ff59b1fd079302b4 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Sun, 21 Jan 2024 20:44:55 +0000 Subject: [PATCH 8/9] Add cheri_step_rvfi.sail This is a strict subset of the sail-riscv model's riscv_step_rvfi.sail to omit fregs absent in CHERIoT. --- Makefile | 2 +- src/cheri_step_rvfi.sail | 87 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 88 insertions(+), 1 deletion(-) create mode 100644 src/cheri_step_rvfi.sail diff --git a/Makefile b/Makefile index 21330d6..32588c9 100644 --- a/Makefile +++ b/Makefile @@ -116,7 +116,7 @@ SAIL_STEP_SRCS = $(SAIL_RISCV_MODEL_DIR)/riscv_step_common.sail \ $(SAIL_RISCV_MODEL_DIR)/riscv_step.sail RVFI_STEP_SRCS = $(SAIL_RISCV_MODEL_DIR)/riscv_step_common.sail \ - $(SAIL_RISCV_MODEL_DIR)/riscv_step_rvfi.sail \ + $(SAIL_CHERI_MODEL_DIR)/cheri_step_rvfi.sail \ $(SAIL_RISCV_MODEL_DIR)/riscv_decode_ext.sail \ $(SAIL_CHERI_MODEL_DIR)/cheri_decode_ext.sail \ $(SAIL_RISCV_MODEL_DIR)/riscv_fetch_rvfi.sail \ diff --git a/src/cheri_step_rvfi.sail b/src/cheri_step_rvfi.sail new file mode 100644 index 0000000..73dbba4 --- /dev/null +++ b/src/cheri_step_rvfi.sail @@ -0,0 +1,87 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +/* Step hooks for rvfi. */ + +function ext_fetch_hook(f : FetchResult) -> FetchResult = f + +function ext_pre_step_hook() -> unit = () + +function ext_post_step_hook() -> unit = { + /* record the next pc */ + rvfi_pc_data->rvfi_pc_wdata() = zero_extend(get_arch_pc()) +} + +val ext_init : unit -> unit +function ext_init() = { + init_base_regs(); + ext_rvfi_init(); + () +} From 0c38f6b2ded3828647e588e3f95f28a2a624f78a Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Mon, 22 Jan 2024 22:15:16 +0000 Subject: [PATCH 9/9] Make accessing !RV32E registers trap, not crash --- ...-or-writing-upper-16-registers-TODO-.patch | 63 ------- ...eading-or-writing-upper-16-registers.patch | 157 ++++++++++++++++++ 2 files changed, 157 insertions(+), 63 deletions(-) delete mode 100644 riscv_patches/0003-Crash-if-reading-or-writing-upper-16-registers-TODO-.patch create mode 100644 riscv_patches/0003-Trap-if-reading-or-writing-upper-16-registers.patch diff --git a/riscv_patches/0003-Crash-if-reading-or-writing-upper-16-registers-TODO-.patch b/riscv_patches/0003-Crash-if-reading-or-writing-upper-16-registers-TODO-.patch deleted file mode 100644 index 56f341b..0000000 --- a/riscv_patches/0003-Crash-if-reading-or-writing-upper-16-registers-TODO-.patch +++ /dev/null @@ -1,63 +0,0 @@ -From d2f3d2cefbe1257a6f7eb5d1aa82a8eccab066e8 Mon Sep 17 00:00:00 2001 -From: Robert Norton -Date: Mon, 31 Oct 2022 14:49:45 +0000 -Subject: [PATCH 3/9] Crash if reading or writing upper 16 registers: TODO this - should really be reserved instruction trap. - ---- - model/riscv_regs.sail | 32 -------------------------------- - 1 file changed, 32 deletions(-) - -diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail -index 15e7613..4ff7871 100644 ---- a/model/riscv_regs.sail -+++ b/model/riscv_regs.sail -@@ -130,22 +130,6 @@ function rX r = { - 13 => x13, - 14 => x14, - 15 => x15, -- 16 => x16, -- 17 => x17, -- 18 => x18, -- 19 => x19, -- 20 => x20, -- 21 => x21, -- 22 => x22, -- 23 => x23, -- 24 => x24, -- 25 => x25, -- 26 => x26, -- 27 => x27, -- 28 => x28, -- 29 => x29, -- 30 => x30, -- 31 => x31, - _ => {assert(false, "invalid register number"); zero_reg} - }; - regval_from_reg(v) -@@ -183,22 +167,6 @@ function wX (r, in_v) = { - 13 => x13 = v, - 14 => x14 = v, - 15 => x15 = v, -- 16 => x16 = v, -- 17 => x17 = v, -- 18 => x18 = v, -- 19 => x19 = v, -- 20 => x20 = v, -- 21 => x21 = v, -- 22 => x22 = v, -- 23 => x23 = v, -- 24 => x24 = v, -- 25 => x25 = v, -- 26 => x26 = v, -- 27 => x27 = v, -- 28 => x28 = v, -- 29 => x29 = v, -- 30 => x30 = v, -- 31 => x31 = v, - _ => assert(false, "invalid register number") - }; - if (r != 0) then { --- -2.39.2 - diff --git a/riscv_patches/0003-Trap-if-reading-or-writing-upper-16-registers.patch b/riscv_patches/0003-Trap-if-reading-or-writing-upper-16-registers.patch new file mode 100644 index 0000000..ad35ce0 --- /dev/null +++ b/riscv_patches/0003-Trap-if-reading-or-writing-upper-16-registers.patch @@ -0,0 +1,157 @@ +From 5ec8de4794c67ab98dd13603bd0e88d9c80d2f95 Mon Sep 17 00:00:00 2001 +From: Robert Norton +Date: Mon, 31 Oct 2022 14:49:45 +0000 +Subject: [PATCH 3/9] Trap if reading or writing upper 16 registers + +--- + model/riscv_regs.sail | 70 ++---------------------------------------- + model/riscv_step.sail | 9 ++++++ + model/riscv_types.sail | 12 ++++++-- + 3 files changed, 22 insertions(+), 69 deletions(-) + +diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail +index 15e7613..28bc0c3 100644 +--- a/model/riscv_regs.sail ++++ b/model/riscv_regs.sail +@@ -93,22 +93,6 @@ register x12 : regtype + register x13 : regtype + register x14 : regtype + register x15 : regtype +-register x16 : regtype +-register x17 : regtype +-register x18 : regtype +-register x19 : regtype +-register x20 : regtype +-register x21 : regtype +-register x22 : regtype +-register x23 : regtype +-register x24 : regtype +-register x25 : regtype +-register x26 : regtype +-register x27 : regtype +-register x28 : regtype +-register x29 : regtype +-register x30 : regtype +-register x31 : regtype + + val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits + function rX r = { +@@ -130,23 +114,7 @@ function rX r = { + 13 => x13, + 14 => x14, + 15 => x15, +- 16 => x16, +- 17 => x17, +- 18 => x18, +- 19 => x19, +- 20 => x20, +- 21 => x21, +- 22 => x22, +- 23 => x23, +- 24 => x24, +- 25 => x25, +- 26 => x26, +- 27 => x27, +- 28 => x28, +- 29 => x29, +- 30 => x30, +- 31 => x31, +- _ => {assert(false, "invalid register number"); zero_reg} ++ _ => throw Error_not_rv32e_register() + }; + regval_from_reg(v) + } +@@ -183,23 +151,7 @@ function wX (r, in_v) = { + 13 => x13 = v, + 14 => x14 = v, + 15 => x15 = v, +- 16 => x16 = v, +- 17 => x17 = v, +- 18 => x18 = v, +- 19 => x19 = v, +- 20 => x20 = v, +- 21 => x21 = v, +- 22 => x22 = v, +- 23 => x23 = v, +- 24 => x24 = v, +- 25 => x25 = v, +- 26 => x26 = v, +- 27 => x27 = v, +- 28 => x28 = v, +- 29 => x29 = v, +- 30 => x30 = v, +- 31 => x31 = v, +- _ => assert(false, "invalid register number") ++ _ => throw Error_not_rv32e_register() + }; + if (r != 0) then { + rvfi_wX(r, in_v); +@@ -324,21 +276,5 @@ function init_base_regs () = { + x12 = zero_reg; + x13 = zero_reg; + x14 = zero_reg; +- x15 = zero_reg; +- x16 = zero_reg; +- x17 = zero_reg; +- x18 = zero_reg; +- x19 = zero_reg; +- x20 = zero_reg; +- x21 = zero_reg; +- x22 = zero_reg; +- x23 = zero_reg; +- x24 = zero_reg; +- x25 = zero_reg; +- x26 = zero_reg; +- x27 = zero_reg; +- x28 = zero_reg; +- x29 = zero_reg; +- x30 = zero_reg; +- x31 = zero_reg ++ x15 = zero_reg + } +diff --git a/model/riscv_step.sail b/model/riscv_step.sail +index 550f11a..25e0ca9 100644 +--- a/model/riscv_step.sail ++++ b/model/riscv_step.sail +@@ -68,6 +68,15 @@ + /* SUCH DAMAGE. */ + /*=======================================================================================*/ + ++function try_execute (x : ast) -> Retired = { ++ try { ++ execute(x) ++ } catch { ++ Error_not_rv32e_register() => { handle_illegal(); RETIRE_FAIL }, ++ e => throw e /* Rethrow other execptions */ ++ } ++} ++ + /* The emulator fetch-execute-interrupt dispatch loop. */ + + /* returns whether to increment the step count in the trace */ +diff --git a/model/riscv_types.sail b/model/riscv_types.sail +index 14916c7..5152ef8 100644 +--- a/model/riscv_types.sail ++++ b/model/riscv_types.sail +@@ -134,8 +134,16 @@ function arch_to_bits(a : Architecture) -> arch_xlen = + /* model-internal exceptions */ + + union exception = { +- Error_not_implemented : string, +- Error_internal_error : unit ++ /* ++ * This is not the proper way to do this, but it is surely the simplest: we ++ * we allow instructions to object to their operands rather than patching the ++ * encdec mapping to do the right thing. (That would be extensive, because ++ * the `ast` type does not have an encapsulated notion of a register selector ++ * distinct from the underlying bit slice of the instruction.) ++ */ ++ Error_not_rv32e_register : unit, ++ Error_not_implemented : string, ++ Error_internal_error : unit + } + + val not_implemented : forall ('a : Type). string -> 'a +-- +2.39.2 +