Trap if reading or writing upper 16 registers

Author: rmn30

model/riscv_regs.sail

@@ -31,22 +31,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 = {
@@ -68,23 +52,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)
 }
@@ -121,23 +89,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);
@@ -262,21 +214,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
 }

model/riscv_step.sail

@@ -6,6 +6,15 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+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 */
@@ -56,7 +65,7 @@ function step(step_no : int) -> bool = {
             /* check for RVC once here instead of every RVC execute clause. */
             if haveRVC() then {
               nextPC = PC + 2;
-              (execute(ast), true)
+              (try_execute(ast), true)
              } else {
               handle_illegal();
               (RETIRE_FAIL, true)
@@ -70,7 +79,7 @@ function step(step_no : int) -> bool = {
               print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
             };
             nextPC = PC + 4;
-            (execute(ast), true)
+            (try_execute(ast), true)
           }
         }
       }

model/riscv_types.sail

@@ -72,8 +72,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