[DNM, WIP] 2024/01 catch up with dependencies

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 \
@@ -59,9 +60,9 @@ 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) \
           $(SAIL_CHERI_MODEL_DIR)/cheri_prelude.sail \
           $(SAIL_CHERI_MODEL_DIR)/cheri_types.sail \
           $(SAIL_CHERI_MODEL_DIR)/cheri_cap_common.sail \
@@ -80,6 +81,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 \
@@ -106,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_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 \
                  $(SAIL_RISCV_MODEL_DIR)/riscv_step.sail

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

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 <[email protected]>
 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
 

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 <[email protected]>
 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) {

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 <[email protected]>
+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
+