Transfer general purpose registers in adapters.rs

Ultimately we are also interested in verifying the formal registers. This commits extends the adapters to transfer the general purpose registers between the two contexts.

Author: francois141

model_checking/src/adapters.rs

@@ -78,6 +78,39 @@ pub fn miralis_to_sail(ctx: &VirtContext) -> SailVirtCtx {
     sail_ctx.vtype = BitField::new(ctx.csr.vtype as u64);
     sail_ctx.vlenb = BitVector::new(ctx.csr.vlenb as u64);
 
+    // Transfer the general purpose registers
+    sail_ctx.x1 = BitVector::new(ctx.regs[0] as u64);
+    sail_ctx.x2 = BitVector::new(ctx.regs[1] as u64);
+    sail_ctx.x3 = BitVector::new(ctx.regs[2] as u64);
+    sail_ctx.x4 = BitVector::new(ctx.regs[3] as u64);
+    sail_ctx.x5 = BitVector::new(ctx.regs[4] as u64);
+    sail_ctx.x6 = BitVector::new(ctx.regs[5] as u64);
+    sail_ctx.x7 = BitVector::new(ctx.regs[6] as u64);
+    sail_ctx.x8 = BitVector::new(ctx.regs[7] as u64);
+    sail_ctx.x9 = BitVector::new(ctx.regs[8] as u64);
+    sail_ctx.x10 = BitVector::new(ctx.regs[9] as u64);
+    sail_ctx.x11 = BitVector::new(ctx.regs[10] as u64);
+    sail_ctx.x12 = BitVector::new(ctx.regs[11] as u64);
+    sail_ctx.x13 = BitVector::new(ctx.regs[12] as u64);
+    sail_ctx.x14 = BitVector::new(ctx.regs[13] as u64);
+    sail_ctx.x15 = BitVector::new(ctx.regs[14] as u64);
+    sail_ctx.x16 = BitVector::new(ctx.regs[15] as u64);
+    sail_ctx.x17 = BitVector::new(ctx.regs[16] as u64);
+    sail_ctx.x18 = BitVector::new(ctx.regs[17] as u64);
+    sail_ctx.x19 = BitVector::new(ctx.regs[18] as u64);
+    sail_ctx.x20 = BitVector::new(ctx.regs[19] as u64);
+    sail_ctx.x21 = BitVector::new(ctx.regs[20] as u64);
+    sail_ctx.x22 = BitVector::new(ctx.regs[21] as u64);
+    sail_ctx.x23 = BitVector::new(ctx.regs[22] as u64);
+    sail_ctx.x24 = BitVector::new(ctx.regs[23] as u64);
+    sail_ctx.x25 = BitVector::new(ctx.regs[24] as u64);
+    sail_ctx.x26 = BitVector::new(ctx.regs[25] as u64);
+    sail_ctx.x27 = BitVector::new(ctx.regs[26] as u64);
+    sail_ctx.x28 = BitVector::new(ctx.regs[27] as u64);
+    sail_ctx.x29 = BitVector::new(ctx.regs[28] as u64);
+    sail_ctx.x30 = BitVector::new(ctx.regs[29] as u64);
+    sail_ctx.x31 = BitVector::new(ctx.regs[30] as u64);
+
     sail_ctx
 }
 
@@ -351,6 +384,39 @@ pub fn sail_to_miralis(sail_ctx: SailVirtCtx) -> VirtContext {
     ctx.csr.vtype = sail_ctx.vtype.bits.bits() as usize;
     ctx.csr.vlenb = sail_ctx.vlenb.bits() as usize;
 
+    // Transfer the general purpose registers
+    ctx.regs[0] = sail_ctx.x1.bits as usize;
+    ctx.regs[1] = sail_ctx.x2.bits as usize;
+    ctx.regs[2] = sail_ctx.x3.bits as usize;
+    ctx.regs[3] = sail_ctx.x4.bits as usize;
+    ctx.regs[4] = sail_ctx.x5.bits as usize;
+    ctx.regs[5] = sail_ctx.x6.bits as usize;
+    ctx.regs[6] = sail_ctx.x7.bits as usize;
+    ctx.regs[7] = sail_ctx.x8.bits as usize;
+    ctx.regs[8] = sail_ctx.x9.bits as usize;
+    ctx.regs[9] = sail_ctx.x10.bits as usize;
+    ctx.regs[10] = sail_ctx.x11.bits as usize;
+    ctx.regs[11] = sail_ctx.x12.bits as usize;
+    ctx.regs[12] = sail_ctx.x13.bits as usize;
+    ctx.regs[13] = sail_ctx.x14.bits as usize;
+    ctx.regs[14] = sail_ctx.x15.bits as usize;
+    ctx.regs[15] = sail_ctx.x16.bits as usize;
+    ctx.regs[16] = sail_ctx.x17.bits as usize;
+    ctx.regs[17] = sail_ctx.x18.bits as usize;
+    ctx.regs[18] = sail_ctx.x19.bits as usize;
+    ctx.regs[19] = sail_ctx.x20.bits as usize;
+    ctx.regs[20] = sail_ctx.x21.bits as usize;
+    ctx.regs[21] = sail_ctx.x22.bits as usize;
+    ctx.regs[22] = sail_ctx.x23.bits as usize;
+    ctx.regs[23] = sail_ctx.x24.bits as usize;
+    ctx.regs[24] = sail_ctx.x25.bits as usize;
+    ctx.regs[25] = sail_ctx.x26.bits as usize;
+    ctx.regs[26] = sail_ctx.x27.bits as usize;
+    ctx.regs[27] = sail_ctx.x28.bits as usize;
+    ctx.regs[28] = sail_ctx.x29.bits as usize;
+    ctx.regs[29] = sail_ctx.x30.bits as usize;
+    ctx.regs[30] = sail_ctx.x31.bits as usize;
+
     ctx
 }