Make mstatus spec-compliant

This commit fixes the divergences between our mstatus read & writes and
the formal Sail specification. Changes mostly concerns dirty flags for
floating points and vector registers, x-len configuration for U and
S-mode, as well as endianess.

model_checking/sail_prelude/lib.rs

@@ -57,7 +57,9 @@ pub fn sys_enable_fdext(_unit: ()) -> bool {
 }
 
 pub fn sys_enable_zfinx(_unit: ()) -> bool {
-    true
+    // An implementation can either have the F Xor the Zfinx (Z-F-in-X) extenstion enabled, not
+    // both at the same time. For the reference implementation we pick the F extension.
+    false
 }
 
 pub fn sys_enable_writable_fiom(_unit: ()) -> bool {

model_checking/src/lib.rs

@@ -77,15 +77,13 @@ pub fn read_csr() {
 
     let mut csr_register = generate_csr_register();
 
-    let is_mstatus = csr_register == 0b001100000000;
-    let is_sstatus = csr_register == 0b000100000000;
     let is_mepc = csr_register == 0b001101000001;
     let is_sepc = csr_register == 0b000101000001;
     let is_sie = csr_register == 0b000100000100;
     let is_seed = csr_register == 0b000000010101;
 
-    // TODO: Adapt the last 6 registers for the symbolic verification
-    if is_mstatus || is_sstatus || is_mepc || is_sepc || is_sie || is_seed {
+    // TODO: Adapt the last 4 registers for the symbolic verification
+    if is_mepc || is_sepc || is_sie || is_seed {
         csr_register = 0;
     }
 

model_checking/src/symbolic.rs

@@ -71,6 +71,7 @@ pub fn new_ctx() -> VirtContext {
         2 => 0b11,
         _ => unreachable!(),
     };
+    let xlen = 0b10; // X-len fixed at 64 bits
 
     // Add other csr
     ctx.hart_id = any!();
@@ -92,7 +93,14 @@ pub fn new_ctx() -> VirtContext {
     ctx.csr.mepc = any!(usize) & (!0b11);
     ctx.csr.mtval = any!();
     // ctx.csr.mtval2 = any!(); - TODO: What should we do with this?
-    ctx.csr.mstatus = any!(usize) & !(0b11 << mstatus::MPP_OFFSET) | (mpp << mstatus::MPP_OFFSET);
+    ctx.csr.mstatus =
+        any!(usize) & !mstatus::MPP_FILTER & !mstatus::SXL_FILTER & !mstatus::UXL_FILTER
+            | (mpp << mstatus::MPP_OFFSET)
+            | (xlen << mstatus::SXL_OFFSET)
+            | (xlen << mstatus::UXL_OFFSET);
+    // We fix the endianess to little endian
+    ctx.csr.mstatus =
+        ctx.csr.mstatus & !mstatus::UBE_FILTER & !mstatus::SBE_FILTER & !mstatus::MBE_OFFSET;
     // ctx.csr.mtinst = any!();
     ctx.csr.mconfigptr = any!();
     // ctx.csr.stvec = any!();
@@ -125,7 +133,7 @@ pub fn new_ctx() -> VirtContext {
     ctx.csr.misa &= !misa::N;
 
     // We fix the architecture type to 64 bits
-    ctx.csr.misa = (0b10 << 62) | (ctx.csr.misa & ((1 << 62) - 1));
+    ctx.csr.misa = (xlen << 62) | (ctx.csr.misa & ((1 << 62) - 1));
 
     // We must have support for U and S modes in Miralis
     ctx.csr.misa |= misa::U;

src/Cargo.toml

@@ -34,5 +34,8 @@ tiny-keccak = { version = "2.0.0", features = ["sha3"] }
 # running unit tests.
 userspace = []
 
+[lints.rust]
+unexpected_cfgs = { level = "warn",  check-cfg = ["cfg(kani)"] }
+
 [lints.clippy]
 result_unit_err = "allow"

src/arch/mod.rs

@@ -284,7 +284,9 @@ pub mod mstatus {
         | MBE_FILTER;
 
     /// Constant to filter out WPRI fields of sstatus
-    pub const SSTATUS_FILTER: usize = SIE_FILTER
+    pub const SSTATUS_FILTER: usize = UIE_FILTER
+        | SIE_FILTER
+        | UPIE_FILTER
         | SPIE_FILTER
         | UBE_FILTER
         | SPP_FILTER
@@ -297,12 +299,18 @@ pub mod mstatus {
         | SD_FILTER;
 
     // Mstatus fields constants
+    /// UIE
+    pub const UIE_OFFSET: usize = 0;
+    pub const UIE_FILTER: usize = 0b1 << UIE_OFFSET;
     /// SIE
     pub const SIE_OFFSET: usize = 1;
     pub const SIE_FILTER: usize = 0b1 << SIE_OFFSET;
     /// MIE
     pub const MIE_OFFSET: usize = 3;
     pub const MIE_FILTER: usize = 0b1 << MIE_OFFSET;
+    /// UPIE
+    pub const UPIE_OFFSET: usize = 4;
+    pub const UPIE_FILTER: usize = 0b1 << UPIE_OFFSET;
     /// SPIE
     pub const SPIE_OFFSET: usize = 5;
     pub const SPIE_FILTER: usize = 0b1 << SPIE_OFFSET;

src/debug.rs

@@ -21,6 +21,24 @@ macro_rules! warn_once {
 
 pub(crate) use warn_once;
 
+// ————————————————————————————— Unimplemented —————————————————————————————— //
+
+/// Mark a code path as not yet implemented, causing a runtime panic.
+///
+/// This macro si equivalent to the standard [unimplemented!], except it makes model checking with
+/// Kani succeed when reached rather than fail.
+///
+/// See [Kani discussion](https://github.com/model-checking/kani/discussions/3746) for background.
+macro_rules! unimplemented {
+   ($($arg:tt)*) => {
+       #[cfg(kani)]
+       kani::assume(false);
+       unimplemented!($($arg)*);
+    };
+}
+
+pub(crate) use unimplemented;
+
 // ———————————————————————————— Max Stack Usage ————————————————————————————— //
 
 /// A well known memory pattern

src/virt/csr.rs

@@ -6,7 +6,7 @@
 use super::{VirtContext, VirtCsr};
 use crate::arch::mstatus::{MBE_FILTER, SBE_FILTER, UBE_FILTER};
 use crate::arch::pmp::pmpcfg;
-use crate::arch::{hstatus, menvcfg, mie, mstatus, Arch, Architecture, Csr, Register};
+use crate::arch::{hstatus, menvcfg, mie, misa, mstatus, Arch, Architecture, Csr, Register};
 use crate::{debug, MiralisContext, Plat, Platform};
 
 /// A module exposing the traits to manipulate registers of a virtual context.
@@ -57,7 +57,7 @@ impl RegisterContextGetter<Csr> for VirtContext {
     fn get(&self, register: Csr) -> usize {
         match register {
             Csr::Mhartid => self.hart_id,
-            Csr::Mstatus => self.csr.mstatus & mstatus::MSTATUS_FILTER,
+            Csr::Mstatus => self.csr.mstatus,
             Csr::Misa => self.csr.misa,
             Csr::Mie => self.csr.mie,
             Csr::Mip => {
@@ -302,15 +302,15 @@ impl HwRegisterContextSetter<Csr> for VirtContext {
                 );
                 // MBE - We currently don't implement the feature as it is a very nice feature
                 if new_value & MBE_FILTER != 0 {
-                    todo!("MBE filter is not implemented - please implement it");
+                    debug::unimplemented!("MBE filter is not implemented - please implement it");
                 }
                 // SBE - We currently don't implement the feature as it is a very nice feature
                 if new_value & SBE_FILTER != 0 {
-                    todo!("SBE filter is not implemented - please implement it");
+                    debug::unimplemented!("SBE filter is not implemented - please implement it");
                 }
                 // UBE - We currently don't implement the feature as it is a very nice feature
                 if new_value & UBE_FILTER != 0 {
-                    todo!("UBE filter is not implemented - please implement it");
+                    debug::unimplemented!("UBE filter is not implemented - please implement it");
                 }
                 // TVM & TSR are read only when no S-mode is available
                 if !mctx.hw.extensions.has_s_extension {
@@ -342,8 +342,15 @@ impl HwRegisterContextSetter<Csr> for VirtContext {
                         0,
                     );
                 }
-                // VS : 9 : read-only 0 (v registers)
-                VirtCsr::set_csr_field(&mut new_value, mstatus::VS_OFFSET, mstatus::VS_FILTER, 0);
+                // VS : 9 : read-only 0 if no supervisor and no v registers
+                if !mctx.hw.extensions.has_s_extension {
+                    VirtCsr::set_csr_field(
+                        &mut new_value,
+                        mstatus::VS_OFFSET,
+                        mstatus::VS_FILTER,
+                        0,
+                    );
+                }
                 // XS : 15 : read-only 0 (NO FS nor VS)
                 VirtCsr::set_csr_field(&mut new_value, mstatus::XS_OFFSET, mstatus::XS_FILTER, 0);
                 // SD : 63 : read-only 0 (if NO FS/VS/XS)
@@ -353,7 +360,8 @@ impl HwRegisterContextSetter<Csr> for VirtContext {
                     mstatus::SD_FILTER,
                     if mctx.hw.extensions.has_s_extension {
                         let fs: usize = (value & mstatus::FS_FILTER) >> mstatus::FS_OFFSET;
-                        if fs != 0 {
+                        let vs: usize = (value & mstatus::VS_FILTER) >> mstatus::VS_OFFSET;
+                        if fs == 0b11 || vs == 0b11 {
                             0b1
                         } else {
                             0b0
@@ -362,6 +370,21 @@ impl HwRegisterContextSetter<Csr> for VirtContext {
                         0
                     },
                 );
+                // UIE and UPIE should be zero if user-space interrupts are disabled
+                if self.csr.misa & misa::N == 0 {
+                    VirtCsr::set_csr_field(
+                        &mut new_value,
+                        mstatus::UIE_OFFSET,
+                        mstatus::UIE_FILTER,
+                        0,
+                    );
+                    VirtCsr::set_csr_field(
+                        &mut new_value,
+                        mstatus::UPIE_OFFSET,
+                        mstatus::UPIE_FILTER,
+                        0,
+                    );
+                }
 
                 self.csr.mstatus = new_value;
             }