Skip to content

Commit

Permalink
Add wildcard cases to matches to suppress Sail warnings. (riscv#197)
Browse files Browse the repository at this point in the history 
Sail tries to check for pattern match completeness and issues warnings
but this often gives false positives: see discussion at
rems-project/sail#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: riscv#194
  • Loading branch information
@rmn30
rmn30 authored Mar 6, 2023
1 parent 5d0ed1b commit 071f4c7
Show file tree
Hide file tree
Showing 16 changed files with 127 additions and 85 deletions.
24 changes: 12 additions & 12 deletions model/riscv_analysis.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) => {
Expand All @@ -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) => {
Expand Down Expand Up @@ -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() => {
Expand All @@ -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) => {
Expand All @@ -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) => {
Expand Down Expand Up @@ -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) => {
Expand All @@ -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) => {
Expand Down Expand Up @@ -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() => {
Expand All @@ -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) => {
Expand All @@ -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) => {
Expand Down
14 changes: 7 additions & 7 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")
}
}
}
Expand Down Expand Up @@ -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 },
Expand All @@ -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 },
Expand Down Expand Up @@ -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,
Expand All @@ -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 },
Expand Down Expand Up @@ -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 }
}
}
Expand Down
35 changes: 19 additions & 16 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")
}
}
}
Expand Down Expand Up @@ -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 }
}
}
Expand Down Expand Up @@ -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 }
}
Expand Down
27 changes: 15 additions & 12 deletions model/riscv_insts_fext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
}
}
}
Expand Down Expand Up @@ -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 }
}

Expand All @@ -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"),
};
}
}
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(_) => ()
};
}
Expand Down Expand Up @@ -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
Expand Down
16 changes: 10 additions & 6 deletions model/riscv_pmp_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")
}
}

Expand Down Expand Up @@ -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]);
Expand All @@ -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")
}
}

Expand Down
Loading

0 comments on commit 071f4c7

Please sign in to comment.