Skip to content

Commit 7b54773

Browse files
CharlyCstCharlyCst
committed
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.
1 parent 37c8021 commit 7b54773

File tree

8 files changed

+76
-16
lines changed

8 files changed

+76
-16
lines changed

‎model_checking/sail_prelude/lib.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,9 @@ pub fn sys_enable_fdext(_unit: ()) -> bool {
5757
}
5858

5959
pub fn sys_enable_zfinx(_unit: ()) -> bool {
60-
true
60+
// An implementation can either have the F Xor the Zfinx (Z-F-in-X) extenstion enabled, not
61+
// both at the same time. For the reference implementation we pick the F extension.
62+
false
6163
}
6264

6365
pub fn sys_enable_writable_fiom(_unit: ()) -> bool {

‎model_checking/src/lib.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -77,15 +77,13 @@ pub fn read_csr() {
7777

7878
let mut csr_register = generate_csr_register();
7979

80-
let is_mstatus = csr_register == 0b001100000000;
81-
let is_sstatus = csr_register == 0b000100000000;
8280
let is_mepc = csr_register == 0b001101000001;
8381
let is_sepc = csr_register == 0b000101000001;
8482
let is_sie = csr_register == 0b000100000100;
8583
let is_seed = csr_register == 0b000000010101;
8684

87-
// TODO: Adapt the last 6 registers for the symbolic verification
88-
if is_mstatus || is_sstatus || is_mepc || is_sepc || is_sie || is_seed {
85+
// TODO: Adapt the last 4 registers for the symbolic verification
86+
if is_mepc || is_sepc || is_sie || is_seed {
8987
csr_register = 0;
9088
}
9189

‎model_checking/src/symbolic.rs

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,7 @@ pub fn new_ctx() -> VirtContext {
7171
2 => 0b11,
7272
_ => unreachable!(),
7373
};
74+
let xlen = 0b10; // X-len fixed at 64 bits
7475

7576
// Add other csr
7677
ctx.hart_id = any!();
@@ -92,7 +93,14 @@ pub fn new_ctx() -> VirtContext {
9293
ctx.csr.mepc = any!(usize) & (!0b11);
9394
ctx.csr.mtval = any!();
9495
// ctx.csr.mtval2 = any!(); - TODO: What should we do with this?
95-
ctx.csr.mstatus = any!(usize) & !(0b11 << mstatus::MPP_OFFSET) | (mpp << mstatus::MPP_OFFSET);
96+
ctx.csr.mstatus =
97+
any!(usize) & !mstatus::MPP_FILTER & !mstatus::SXL_FILTER & !mstatus::UXL_FILTER
98+
| (mpp << mstatus::MPP_OFFSET)
99+
| (xlen << mstatus::SXL_OFFSET)
100+
| (xlen << mstatus::UXL_OFFSET);
101+
// We fix the endianess to little endian
102+
ctx.csr.mstatus =
103+
ctx.csr.mstatus & !mstatus::UBE_FILTER & !mstatus::SBE_FILTER & !mstatus::MBE_OFFSET;
96104
// ctx.csr.mtinst = any!();
97105
ctx.csr.mconfigptr = any!();
98106
// ctx.csr.stvec = any!();
@@ -125,7 +133,7 @@ pub fn new_ctx() -> VirtContext {
125133
ctx.csr.misa &= !misa::N;
126134

127135
// We fix the architecture type to 64 bits
128-
ctx.csr.misa = (0b10 << 62) | (ctx.csr.misa & ((1 << 62) - 1));
136+
ctx.csr.misa = (xlen << 62) | (ctx.csr.misa & ((1 << 62) - 1));
129137

130138
// We must have support for U and S modes in Miralis
131139
ctx.csr.misa |= misa::U;

‎qemu-riscv64-virt.dtb

4.19 KB
Binary file not shown.

‎src/Cargo.toml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,5 +34,8 @@ tiny-keccak = { version = "2.0.0", features = ["sha3"] }
3434
# running unit tests.
3535
userspace = []
3636

37+
[lints.rust]
38+
unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] }
39+
3740
[lints.clippy]
3841
result_unit_err = "allow"

‎src/arch/mod.rs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -284,7 +284,9 @@ pub mod mstatus {
284284
| MBE_FILTER;
285285

286286
/// Constant to filter out WPRI fields of sstatus
287-
pub const SSTATUS_FILTER: usize = SIE_FILTER
287+
pub const SSTATUS_FILTER: usize = UIE_FILTER
288+
| SIE_FILTER
289+
| UPIE_FILTER
288290
| SPIE_FILTER
289291
| UBE_FILTER
290292
| SPP_FILTER
@@ -297,12 +299,18 @@ pub mod mstatus {
297299
| SD_FILTER;
298300

299301
// Mstatus fields constants
302+
/// UIE
303+
pub const UIE_OFFSET: usize = 0;
304+
pub const UIE_FILTER: usize = 0b1 << UIE_OFFSET;
300305
/// SIE
301306
pub const SIE_OFFSET: usize = 1;
302307
pub const SIE_FILTER: usize = 0b1 << SIE_OFFSET;
303308
/// MIE
304309
pub const MIE_OFFSET: usize = 3;
305310
pub const MIE_FILTER: usize = 0b1 << MIE_OFFSET;
311+
/// UPIE
312+
pub const UPIE_OFFSET: usize = 4;
313+
pub const UPIE_FILTER: usize = 0b1 << UPIE_OFFSET;
306314
/// SPIE
307315
pub const SPIE_OFFSET: usize = 5;
308316
pub const SPIE_FILTER: usize = 0b1 << SPIE_OFFSET;

‎src/debug.rs

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,24 @@ macro_rules! warn_once {
2121

2222
pub(crate) use warn_once;
2323

24+
// ————————————————————————————— Unimplemented —————————————————————————————— //
25+
26+
/// Mark a code path as not yet implemented, causing a runtime panic.
27+
///
28+
/// This macro si equivalent to the standard [unimplemented!], except it makes model checking with
29+
/// Kani succeed when reached rather than fail.
30+
///
31+
/// See [Kani discussion](https://github.com/model-checking/kani/discussions/3746) for background.
32+
macro_rules! unimplemented {
33+
($($arg:tt)*) => {
34+
#[cfg(kani)]
35+
kani::assume(false);
36+
unimplemented!($($arg)*);
37+
};
38+
}
39+
40+
pub(crate) use unimplemented;
41+
2442
// ———————————————————————————— Max Stack Usage ————————————————————————————— //
2543

2644
/// A well known memory pattern

‎src/virt/csr.rs

Lines changed: 31 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
use super::{VirtContext, VirtCsr};
77
use crate::arch::mstatus::{MBE_FILTER, SBE_FILTER, UBE_FILTER};
88
use crate::arch::pmp::pmpcfg;
9-
use crate::arch::{hstatus, menvcfg, mie, mstatus, Arch, Architecture, Csr, Register};
9+
use crate::arch::{hstatus, menvcfg, mie, misa, mstatus, Arch, Architecture, Csr, Register};
1010
use crate::{debug, MiralisContext, Plat, Platform};
1111

1212
/// A module exposing the traits to manipulate registers of a virtual context.
@@ -57,7 +57,7 @@ impl RegisterContextGetter<Csr> for VirtContext {
5757
fn get(&self, register: Csr) -> usize {
5858
match register {
5959
Csr::Mhartid => self.hart_id,
60-
Csr::Mstatus => self.csr.mstatus & mstatus::MSTATUS_FILTER,
60+
Csr::Mstatus => self.csr.mstatus,
6161
Csr::Misa => self.csr.misa,
6262
Csr::Mie => self.csr.mie,
6363
Csr::Mip => {
@@ -302,15 +302,15 @@ impl HwRegisterContextSetter<Csr> for VirtContext {
302302
);
303303
// MBE - We currently don't implement the feature as it is a very nice feature
304304
if new_value & MBE_FILTER != 0 {
305-
todo!("MBE filter is not implemented - please implement it");
305+
debug::unimplemented!("MBE filter is not implemented - please implement it");
306306
}
307307
// SBE - We currently don't implement the feature as it is a very nice feature
308308
if new_value & SBE_FILTER != 0 {
309-
todo!("SBE filter is not implemented - please implement it");
309+
debug::unimplemented!("SBE filter is not implemented - please implement it");
310310
}
311311
// UBE - We currently don't implement the feature as it is a very nice feature
312312
if new_value & UBE_FILTER != 0 {
313-
todo!("UBE filter is not implemented - please implement it");
313+
debug::unimplemented!("UBE filter is not implemented - please implement it");
314314
}
315315
// TVM & TSR are read only when no S-mode is available
316316
if !mctx.hw.extensions.has_s_extension {
@@ -342,8 +342,15 @@ impl HwRegisterContextSetter<Csr> for VirtContext {
342342
0,
343343
);
344344
}
345-
// VS : 9 : read-only 0 (v registers)
346-
VirtCsr::set_csr_field(&mut new_value, mstatus::VS_OFFSET, mstatus::VS_FILTER, 0);
345+
// VS : 9 : read-only 0 if no supervisor and no v registers
346+
if !mctx.hw.extensions.has_s_extension {
347+
VirtCsr::set_csr_field(
348+
&mut new_value,
349+
mstatus::VS_OFFSET,
350+
mstatus::VS_FILTER,
351+
0,
352+
);
353+
}
347354
// XS : 15 : read-only 0 (NO FS nor VS)
348355
VirtCsr::set_csr_field(&mut new_value, mstatus::XS_OFFSET, mstatus::XS_FILTER, 0);
349356
// SD : 63 : read-only 0 (if NO FS/VS/XS)
@@ -353,7 +360,8 @@ impl HwRegisterContextSetter<Csr> for VirtContext {
353360
mstatus::SD_FILTER,
354361
if mctx.hw.extensions.has_s_extension {
355362
let fs: usize = (value & mstatus::FS_FILTER) >> mstatus::FS_OFFSET;
356-
if fs != 0 {
363+
let vs: usize = (value & mstatus::VS_FILTER) >> mstatus::VS_OFFSET;
364+
if fs == 0b11 || vs == 0b11 {
357365
0b1
358366
} else {
359367
0b0
@@ -362,6 +370,21 @@ impl HwRegisterContextSetter<Csr> for VirtContext {
362370
0
363371
},
364372
);
373+
// UIE and UPIE should be zero if user-space interrupts are disabled
374+
if self.csr.misa & misa::N == 0 {
375+
VirtCsr::set_csr_field(
376+
&mut new_value,
377+
mstatus::UIE_OFFSET,
378+
mstatus::UIE_FILTER,
379+
0,
380+
);
381+
VirtCsr::set_csr_field(
382+
&mut new_value,
383+
mstatus::UPIE_OFFSET,
384+
mstatus::UPIE_FILTER,
385+
0,
386+
);
387+
}
365388

366389
self.csr.mstatus = new_value;
367390
}

0 commit comments

Comments
 (0)