From e70a06b2f90d5fdeab36c8269ef6a82b0b1133db Mon Sep 17 00:00:00 2001 From: Charly Castes Date: Mon, 23 Dec 2024 13:46:02 +0100 Subject: [PATCH] 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 | 4 ++- model_checking/src/lib.rs | 6 ++--- model_checking/src/symbolic.rs | 12 +++++++-- qemu-riscv64-virt.dtb | Bin 0 -> 4290 bytes src/Cargo.toml | 3 +++ src/arch/mod.rs | 10 +++++++- src/debug.rs | 18 +++++++++++++ src/virt/csr.rs | 39 +++++++++++++++++++++++------ 8 files changed, 76 insertions(+), 16 deletions(-) create mode 100644 qemu-riscv64-virt.dtb diff --git a/model_checking/sail_prelude/lib.rs b/model_checking/sail_prelude/lib.rs index f245e7db..d04c2902 100644 --- a/model_checking/sail_prelude/lib.rs +++ b/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 { diff --git a/model_checking/src/lib.rs b/model_checking/src/lib.rs index 5bfa4cfb..425ad893 100644 --- a/model_checking/src/lib.rs +++ b/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; } diff --git a/model_checking/src/symbolic.rs b/model_checking/src/symbolic.rs index 52990ad7..2c7d753c 100644 --- a/model_checking/src/symbolic.rs +++ b/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; diff --git a/qemu-riscv64-virt.dtb b/qemu-riscv64-virt.dtb new file mode 100644 index 0000000000000000000000000000000000000000..2792567cf094f47e06051e265df1c3359deba937 GIT binary patch literal 4290 zcmbVPO^6&t6s|TpYt$qg@h=2rlLg~pI+=Bo7(r#O;z17v^dOtwo|>6%R`2F|nWXXqg=o z=cBL*$Jl~WZ{~T0))Wia+uIHOZrDfR=dm4BrvsZ{7im=W^D+xJ$EJI}BZ5APkNdQ1 z`#9UuiwA=z2*mkHewlNxGrwLxfp&{&YkN{ax zTegoTu`zEiQQ74K@}R8*CoX_%#mB?<@8ewGKPQA(Bt@mnmihNd>It*tv^eHrl=mf`wwbKIsF&@-~3lwG<&Y9^} z3i@eehTZ2IOTW&0*ZC1=1w}a6pfEVfXKir^f__kXvumus=rI1LWFai|o}o1m;>mvovuX0VPn$2yLH(`TEdeh;dC5%NOV z_ZUiRkmrL`w+DIJ>nCOyf&*q3`& ztc6OG_}=px;;G3&5YNGRa*ccaKR8$5LizukJR|McnuDC&CeFK&k}|auAS|i?bw?zu5n4+ zQ3<~wj$h7rsI~6z3dF}Z9(Mx&ZKIdnxbm#$bS@0D8UWeoduUikr zyD0mC7rf$ZPFJ_E-e{u!1WF5fh^tl=>Nv{6fga&*5!-%0hWA3BC&uXajqm5(iEaA$ zayZL-I#qF=6;YLJrdq9<uM!jCCjd5xjjRxANax@5y);(3~f!d5lTj6%n ztA?tVMY!+}b*V>{+ueGCc39K+Gaw5?s01T zg>R1lJnasPNTxRRS2&Eu*V=qHy*!I>is3Iblr%Ml@%N-2!=Dutv&HPO2mky=S85Wa VW3A#ekGC3WF;y=gS0F}u{{ffkFN**G literal 0 HcmV?d00001 diff --git a/src/Cargo.toml b/src/Cargo.toml index 09b2658c..4d03852c 100644 --- a/src/Cargo.toml +++ b/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" diff --git a/src/arch/mod.rs b/src/arch/mod.rs index faba3b10..db6a8347 100644 --- a/src/arch/mod.rs +++ b/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; diff --git a/src/debug.rs b/src/debug.rs index 914ab6b1..308b5d65 100644 --- a/src/debug.rs +++ b/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 diff --git a/src/virt/csr.rs b/src/virt/csr.rs index 734a74b2..145c4f23 100644 --- a/src/virt/csr.rs +++ b/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 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 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 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 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 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; }