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

16 files changed, 127 insertions, 85 deletions

diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
index 6124ec2..14cba3b 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 eee5cea..1fb995c 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 38b357b..071c3a9 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 07234ed..7bfc43f 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 0ec8555..bc80781 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 a5e21ed..43e2d5d 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 d11d475..a95b20d 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 6204ae5..1d401ae 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 bbfabcc..94e57dc 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 9cc5034..04a6fe4 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 3e24698..9b9323e 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 2c49706..78a4754 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 07ff8b7..4da87fd 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 1550638..191427b 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 5eb6222..2b17844 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 7501091..31fbdea 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)
               }