From 071f4c79171efa3721e598809e3aadfc8c3478c7 Mon Sep 17 00:00:00 2001 From: Robert Norton <1412774+rmn30@users.noreply.github.com> Date: Mon, 6 Mar 2023 18:18:33 +0000 Subject: [PATCH] Add wildcard cases to matches to suppress Sail warnings. (#197) Sail tries to check for pattern match completeness and issues warnings but this often gives false positives: see discussion at https://github.com/rems-project/sail/issues/191 . To suppress these we add a wildcard case that raises an internal error. There is effectively no behaviour change as these would previously have resulted in a match error at runtime and they should be unreachable anyway. At the same time we change the DOUBLE case in memory access paths to allow for xlen > 64. Following discussion on the PR I also changed internal_error to take a file and line number as an argument to aid with debugging. Fixes: https://github.com/riscv/sail-riscv/issues/194 --- model/riscv_analysis.sail | 24 ++++++------ model/riscv_insts_aext.sail | 14 +++---- model/riscv_insts_base.sail | 35 ++++++++++-------- model/riscv_insts_fext.sail | 27 ++++++++------ model/riscv_mem.sail | 4 +- model/riscv_pmp_regs.sail | 16 +++++--- model/riscv_pte.sail | 2 +- model/riscv_sys_control.sail | 4 +- model/riscv_sys_exceptions.sail | 2 +- model/riscv_sys_regs.sail | 2 +- model/riscv_types.sail | 65 ++++++++++++++++++++++++--------- model/riscv_types_kext.sail | 3 +- model/riscv_vmem_rv32.sail | 4 +- model/riscv_vmem_rv64.sail | 6 +-- model/riscv_vmem_sv32.sail | 2 +- model/riscv_vmem_sv39.sail | 2 +- 16 files changed, 127 insertions(+), 85 deletions(-) diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail index 6124ec2c6..14cba3b62 100644 --- a/model/riscv_analysis.sail +++ b/model/riscv_analysis.sail @@ -151,7 +151,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (true, false) => IK_mem_read (Read_RISCV_acquire), (true, true) => IK_mem_read (Read_RISCV_strong_acquire), - _ => internal_error("LOAD type not implemented in initial_analysis") + _ => internal_error(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis") } }, STORE(imm, rs2, rs1, width, aq, rl) => { @@ -164,7 +164,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (false, true) => IK_mem_write (Write_RISCV_release), (true, true) => IK_mem_write (Write_RISCV_strong_release), - _ => internal_error("STORE type not implemented in initial_analysis") + _ => internal_error(__FILE__, __LINE__, "STORE type not implemented in initial_analysis") } }, ADDIW(imm, rs, rd) => { @@ -196,14 +196,14 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (), - _ => internal_error("barrier type not implemented in initial_analysis") + _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis") }; }, FENCE_TSO(pred, succ) => { ik = match (pred, succ) { (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso), - _ => internal_error("barrier type not implemented in initial_analysis") + _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis") }; }, FENCEI() => { @@ -217,7 +217,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (false, false) => IK_mem_read (Read_RISCV_reserved), (true, false) => IK_mem_read (Read_RISCV_reserved_acquire), (true, true) => IK_mem_read (Read_RISCV_reserved_strong_acquire), - (false, true) => internal_error("LOADRES type not implemented in initial_analysis") + (false, true) => internal_error(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis") }; }, STORECON(aq, rl, rs2, rs1, width, rd) => { @@ -230,7 +230,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (false, true) => IK_mem_write (Write_RISCV_conditional_release), (true, true) => IK_mem_write (Write_RISCV_conditional_strong_release), - (true, false) => internal_error("STORECON type not implemented in initial_analysis") + (true, false) => internal_error(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis") }; }, AMO(op, aq, rl, rs2, rs1, width, rd) => { @@ -324,7 +324,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (true, false) => IK_mem_read (Read_RISCV_acquire), (true, true) => IK_mem_read (Read_RISCV_strong_acquire), - _ => internal_error("LOAD type not implemented in initial_analysis") + _ => internal_error(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis") } }, STORE(imm, rs2, rs1, width, aq, rl) => { @@ -337,7 +337,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (false, true) => IK_mem_write (Write_RISCV_release), (true, true) => IK_mem_write (Write_RISCV_strong_release), - _ => internal_error("STORE type not implemented in initial_analysis") + _ => internal_error(__FILE__, __LINE__, "STORE type not implemented in initial_analysis") } }, ADDIW(imm, rs, rd) => { @@ -368,14 +368,14 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (), - _ => internal_error("barrier type not implemented in initial_analysis") + _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis") }; }, FENCE_TSO(pred, succ) => { ik = match (pred, succ) { (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()), - _ => internal_error("barrier type not implemented in initial_analysis") + _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis") }; }, FENCEI() => { @@ -389,7 +389,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (false, false) => IK_mem_read (Read_RISCV_reserved), (true, false) => IK_mem_read (Read_RISCV_reserved_acquire), (true, true) => IK_mem_read (Read_RISCV_reserved_strong_acquire), - (false, true) => internal_error("LOADRES type not implemented in initial_analysis") + (false, true) => internal_error(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis") }; }, STORECON(aq, rl, rs2, rs1, width, rd) => { @@ -402,7 +402,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst (false, true) => IK_mem_write (Write_RISCV_conditional_release), (true, true) => IK_mem_write (Write_RISCV_conditional_strong_release), - (true, false) => internal_error("STORECON type not implemented in initial_analysis") + (true, false) => internal_error(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis") }; }, AMO(op, aq, rl, rs2, rs1, width, rd) => { diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index eee5cea5e..1fb995c46 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -151,7 +151,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { (HALF, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false), (WORD, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false), (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false), - _ => internal_error("Unexpected AMO width") + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") } } } @@ -215,7 +215,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error("STORECON expected word or double") + _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") }; match (eares) { MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, @@ -226,7 +226,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq & rl, rl, true), (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq & rl, rl, true), (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq & rl, rl, true), - _ => internal_error("STORECON expected word or double") + _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") }; match (res) { MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); RETIRE_SUCCESS }, @@ -287,7 +287,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { (HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true), (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error("Unexpected AMO width") + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") }; let is_unsigned : bool = match op { AMOMINU => true, @@ -308,7 +308,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { (HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, aq & rl, true)), (WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)), (DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)), - _ => internal_error("Unexpected AMO width") + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") }; match (mval) { MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, @@ -340,11 +340,11 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { (HALF, _) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true), (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), - _ => internal_error("Unexpected AMO width") + _ => internal_error(__FILE__, __LINE__, "Unexpected AMO width") }; match (wval) { MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS }, - MemValue(false) => { internal_error("AMO got false from mem_write_value") }, + MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } } diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 38b357bbe..071c3a9af 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -394,15 +394,16 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(paddr, _) => - match (width, sizeof(xlen)) { - (BYTE, _) => - process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned), - (HALF, _) => - process_load(rd, vaddr, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned), - (WORD, _) => - process_load(rd, vaddr, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned), - (DOUBLE, 64) => - process_load(rd, vaddr, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned) + match (width) { + BYTE => + process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned), + HALF => + process_load(rd, vaddr, mem_read(Read(Data), paddr, 2, aq, rl, false), is_unsigned), + WORD => + process_load(rd, vaddr, mem_read(Read(Data), paddr, 4, aq, rl, false), is_unsigned), + DOUBLE if sizeof(xlen) >= 64 => + process_load(rd, vaddr, mem_read(Read(Data), paddr, 8, aq, rl, false), is_unsigned), + _ => report_invalid_width(__FILE__, __LINE__, width, "load") } } } @@ -459,15 +460,17 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, MemValue(_) => { let rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { - (BYTE, _) => mem_write_value(paddr, 1, rs2_val[7..0], aq, rl, false), - (HALF, _) => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false), - (WORD, _) => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false), - (DOUBLE, 64) => mem_write_value(paddr, 8, rs2_val, aq, rl, false) + let res : MemoryOpResult(bool) = match (width) { + BYTE => mem_write_value(paddr, 1, rs2_val[7..0], aq, rl, false), + HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl, false), + WORD => mem_write_value(paddr, 4, rs2_val[31..0], aq, rl, false), + DOUBLE if sizeof(xlen) >= 64 + => mem_write_value(paddr, 8, rs2_val, aq, rl, false), + _ => report_invalid_width(__FILE__, __LINE__, width, "store"), }; 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(vaddr, e); RETIRE_FAIL } } } @@ -864,7 +867,7 @@ function clause execute SFENCE_VMA(rs1, rs2) = { Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus.TVM()) { (Some(_), 0b1) => { handle_illegal(); RETIRE_FAIL }, (Some(_), 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS }, - (_, _) => internal_error("unimplemented sfence architecture") + (_, _) => internal_error(__FILE__, __LINE__, "unimplemented sfence architecture") }, Machine => { flush_TLB(asid, addr); RETIRE_SUCCESS } } diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 07234edfd..7bfc43ffc 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -384,14 +384,15 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { let (aq, rl, res) = (false, false, false); - match (width, sizeof(flen)) { - (BYTE, _) => { handle_illegal(); RETIRE_FAIL }, - (HALF, _) => + match (width) { + BYTE => { handle_illegal(); RETIRE_FAIL }, + HALF => process_fload16(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, res)), - (WORD, _) => + WORD => process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)), - (DOUBLE, 64) => - process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)) + DOUBLE if sizeof(flen) >= 64 => + process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)), + _ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"), } } } @@ -431,7 +432,7 @@ val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired effect {escape, function process_fstore(vaddr, value) = match value { 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(vaddr, e); RETIRE_FAIL } } @@ -458,11 +459,13 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, MemValue(_) => { let rs2_val = F(rs2); - match (width, sizeof(flen)) { - (BYTE, _) => { handle_illegal(); RETIRE_FAIL }, - (HALF, _) => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)), - (WORD, _) => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), - (DOUBLE, 64) => process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)) + match (width) { + BYTE => { handle_illegal(); RETIRE_FAIL }, + HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)), + WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), + DOUBLE if sizeof(flen) >= 64 => + process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)), + _ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"), }; } } diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 0ec855522..bc8078124 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -163,7 +163,7 @@ function rvfi_read (addr, width, result) = { MemValue(v, _) => if width <= 16 then { rvfi_mem_data->rvfi_mem_rdata() = sail_zero_extend(v, 256); rvfi_mem_data->rvfi_mem_rmask() = rvfi_encode_width_mask(width) } - else { internal_error("Expected at most 16 bytes here!") }, + else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") }, MemException(_) => () }; } @@ -237,7 +237,7 @@ function rvfi_write (addr, width, value, meta) = { rvfi_mem_data->rvfi_mem_wdata() = sail_zero_extend(value,256); rvfi_mem_data->rvfi_mem_wmask() = rvfi_encode_width_mask(width); } else { - internal_error("Expected at most 16 bytes here!"); + internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!"); } } $else diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index a5e21edf5..43e2d5dac 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -145,11 +145,13 @@ function pmpReadCfgReg(n) = { 0 => append(pmp3cfg.bits(), append(pmp2cfg.bits(), append(pmp1cfg.bits(), pmp0cfg.bits()))), 1 => append(pmp7cfg.bits(), append(pmp6cfg.bits(), append(pmp5cfg.bits(), pmp4cfg.bits()))), 2 => append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))), - 3 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), pmp12cfg.bits()))) + 3 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), pmp12cfg.bits()))), + _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg read") } - else match n { // sizeof(xlen) == 64 + else match n { // sizeof(xlen) >= 64 0 => append(pmp7cfg.bits(), append(pmp6cfg.bits(), append(pmp5cfg.bits(), append(pmp4cfg.bits(), append(pmp3cfg.bits(), append(pmp2cfg.bits(), append(pmp1cfg.bits(), pmp0cfg.bits()))))))), - 2 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), append(pmp12cfg.bits(), append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))))))) + 2 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), append(pmp12cfg.bits(), append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))))))), + _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg read") } } @@ -187,9 +189,10 @@ function pmpWriteCfgReg(n, v) = { pmp13cfg = pmpWriteCfg(pmp13cfg, v[15..8]); pmp14cfg = pmpWriteCfg(pmp14cfg, v[23..16]); pmp15cfg = pmpWriteCfg(pmp15cfg, v[31..24]); - } + }, + _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg write") } - else if sizeof(xlen) == 64 + else if sizeof(xlen) >= 64 then match n { 0 => { pmp0cfg = pmpWriteCfg(pmp0cfg, v[7 ..0]); pmp1cfg = pmpWriteCfg(pmp1cfg, v[15..8]); @@ -208,7 +211,8 @@ function pmpWriteCfgReg(n, v) = { pmp13cfg = pmpWriteCfg(pmp13cfg, v[47..40]); pmp14cfg = pmpWriteCfg(pmp14cfg, v[55..48]); pmp15cfg = pmpWriteCfg(pmp15cfg, v[63..56]) - } + }, + _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg write") } } diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail index d11d475e7..a95b20d1b 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -131,7 +131,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, (ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), (Execute(), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1), - (_, Machine) => internal_error("m-mode mem perm check") + (_, Machine) => internal_error(__FILE__, __LINE__, "m-mode mem perm check") } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6204ae59e..1d401aeb2 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -428,7 +428,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen mstatus->SPP() = match cur_privilege { User => 0b0, Supervisor => 0b1, - Machine => internal_error("invalid privilege for s-mode trap") + Machine => internal_error(__FILE__, __LINE__, "invalid privilege for s-mode trap") }; stval = tval(info); sepc = pc; @@ -560,7 +560,7 @@ function init_sys() -> unit = { misa->S() = 0b1; /* supervisor-mode */ if sys_enable_fdext() & sys_enable_zfinx() - then internal_error("F and Zfinx cannot both be enabled!"); + then internal_error(__FILE__, __LINE__, "F and Zfinx cannot both be enabled!"); /* We currently support both F and D */ misa->F() = bool_to_bits(sys_enable_fdext()); /* single-precision */ diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index bbfabcc1f..94e57dc3f 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -86,7 +86,7 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = { }; match tvec_addr(tvec, cause) { Some(epc) => epc, - None() => internal_error("Invalid tvec mode") + None() => internal_error(__FILE__, __LINE__, "Invalid tvec mode") } } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 9cc503442..04a6fe410 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -339,7 +339,7 @@ function cur_Architecture() -> Architecture = { }; match architecture(a) { Some(a) => a, - None() => internal_error("Invalid current architecture") + None() => internal_error(__FILE__, __LINE__, "Invalid current architecture") } } diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 3e24698f8..9b9323ee9 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -128,6 +128,23 @@ function arch_to_bits(a : Architecture) -> arch_xlen = RV128 => 0b11 } + +/* model-internal exceptions */ + +union exception = { + Error_not_implemented : string, + Error_internal_error : unit +} + +val not_implemented : forall ('a : Type). string -> 'a effect {escape} +function not_implemented message = throw(Error_not_implemented(message)) + +val internal_error : forall ('a : Type). (string, int, string) -> 'a effect {escape} +function internal_error(file, line, s) = { + assert (false, file ^ ":" ^ string_of_int(line) ^ ": " ^ s); + throw Error_internal_error() +} + /* privilege levels */ type priv_level = bits(2) @@ -141,12 +158,17 @@ function privLevel_to_bits (p) = Machine => 0b11 } +/*! + * Converts the given 2-bit privilege level code to the [Privilege] enum. + * Calling with a reserved code will result in an internal error. + */ val privLevel_of_bits : priv_level -> Privilege function privLevel_of_bits (p) = match (p) { 0b00 => User, 0b01 => Supervisor, - 0b11 => Machine + 0b11 => Machine, + 0b10 => internal_error(__FILE__, __LINE__, "Invalid privilege level: " ^ BitStr(p)) } val privLevel_to_str : Privilege -> string @@ -301,22 +323,6 @@ function exceptionType_to_str(e) = overload to_str = {exceptionType_to_str} -/* model-internal exceptions */ - -union exception = { - Error_not_implemented : string, - Error_internal_error : unit -} - -val not_implemented : forall ('a : Type). string -> 'a effect {escape} -function not_implemented message = throw(Error_not_implemented(message)) - -val internal_error : forall ('a : Type). string -> 'a effect {escape} -function internal_error(s) = { - assert (false, s); - throw Error_internal_error() -} - /* trap modes */ type tv_mode = bits(2) @@ -445,3 +451,28 @@ function word_width_bytes width = match width { WORD => 4, DOUBLE => 8 } + +/*! + * Raise an internal error reporting that width w is invalid for access kind, k, + * and current xlen. The file name and line number should be passed in as the + * first two arguments using the __FILE__ and __LINE__ built-in macros. + * This is mainly used to supress Sail warnings about incomplete matches and + * should be unreachable. See https://github.com/riscv/sail-riscv/issues/194 + * and https://github.com/riscv/sail-riscv/pull/197 . + */ +val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a effect {escape} +function report_invalid_width(f , l, w, k) -> 'a = { + /* + * Ideally we would call internal_error here but this triggers a Sail bug, + * https://github.com/rems-project/sail/issues/203 in versions < 0.15.1, so + * we work around this by manually inlining. + * TODO when we are happy to require Sail >= 0.15.1 uncomment the following + * and remove the rest of the function. + */ + // internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^ + // " with xlen=" ^ string_of_int(sizeof(xlen))); + assert (false, f ^ ":" ^ string_of_int(l) ^ ": " ^ "Invalid width, " + ^ size_mnemonic(w) ^ ", for " ^ k ^ " with xlen=" + ^ string_of_int(sizeof(xlen))); + throw Error_internal_error() +} diff --git a/model/riscv_types_kext.sail b/model/riscv_types_kext.sail index 2c49706f2..78a4754ab 100644 --- a/model/riscv_types_kext.sail +++ b/model/riscv_types_kext.sail @@ -87,7 +87,8 @@ function aes_decode_rcon(r) = { 0x6 => 0x00000040, 0x7 => 0x00000080, 0x8 => 0x0000001b, - 0x9 => 0x00000036 + 0x9 => 0x00000036, + _ => internal_error(__FILE__, __LINE__, "Unexpected AES r") /* unreachable -- required to silence Sail warning */ } } diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index 07ff8b76b..4da87fd9b 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -87,7 +87,7 @@ function translationMode(priv) = { let s = Mk_Satp32(satp[31..0]); if s.Mode() == 0b0 then Sbare else Sv32 }, - _ => internal_error("unsupported address translation arch") + _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") } } } @@ -112,7 +112,7 @@ function translateAddr_priv(vAddr, ac, effPriv) = { TR_Address(pa, ext_ptw) => TR_Address(to_phys_addr(pa), ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) }, - _ => internal_error("unsupported address translation scheme") + _ => internal_error(__FILE__, __LINE__, "unsupported address translation scheme") } } diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index 155063843..191427bea 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -101,14 +101,14 @@ function translationMode(priv) = { let mbits : satp_mode = Mk_Satp64(satp).Mode(); match satp64Mode_of_bits(RV64, mbits) { Some(m) => m, - None() => internal_error("invalid RV64 translation mode in satp") + None() => internal_error(__FILE__, __LINE__, "invalid RV64 translation mode in satp") } }, Some(RV32) => { let s = Mk_Satp32(satp[31..0]); if s.Mode() == 0b0 then Sbare else Sv32 }, - _ => internal_error("unsupported address translation arch") + _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") } } } @@ -143,7 +143,7 @@ function translateAddr_priv(vAddr, ac, effPriv) = { } else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw) }, - _ => internal_error("unsupported address translation scheme") + _ => internal_error(__FILE__, __LINE__, "unsupported address translation scheme") } } diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index 5eb622202..2b1784415 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -211,7 +211,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* update page table */ match mem_write_value_priv(to_phys_addr(EXTZ(ent.pteAddr)), 4, n_pte.bits(), Supervisor, false, false, false) { MemValue(_) => (), - MemException(e) => internal_error("invalid physical address in TLB") + MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw) } diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 75010918a..31fbdea47 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -205,7 +205,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* update page table */ match mem_write_value_priv(EXTZ(ent.pteAddr), 8, n_pte.bits(), Supervisor, false, false, false) { MemValue(_) => (), - MemException(e) => internal_error("invalid physical address in TLB") + MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw) }