SailBugfix: pmp_cfg_idx must be multiplied by two

The pmpcfg registers have a stride of two, therefore we also need to multiply the pmp_cfg_idx by two.

Author: francois141

model_checking/src/lib.rs

@@ -158,10 +158,7 @@ pub fn fences() {
 #[cfg_attr(kani, kani::proof)]
 #[cfg_attr(test, test)]
 pub fn read_csr() {
-    let (mut ctx, mctx, mut sail_ctx) = symbolic::new_symbolic_contexts();
-
-    // Infinite number of pmps for the formal verification
-    ctx.nb_pmp = usize::MAX;
+    let (ctx, mctx, mut sail_ctx) = symbolic::new_symbolic_contexts();
 
     let csr_register = generate_csr_register();
 

src/virt/csr.rs

@@ -91,7 +91,7 @@ impl RegisterContextGetter<Csr> for VirtContext {
                     log::warn!("Invalid pmpcfg {}", pmp_cfg_idx);
                     return 0;
                 }
-                if pmp_cfg_idx >= self.nb_pmp / 8 {
+                if pmp_cfg_idx >= 2 * self.nb_pmp / 8 {
                     // This PMP is not emulated
                     return 0;
                 }