Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Unit test for StoreWordRight #2319

Closed
wants to merge 5 commits into from
Closed

Unit test for StoreWordRight #2319

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
84c3ab4
unit test for swr for cannon instruction and fix interpreter
querolita Jun 13, 2024
8916b03
comment explaining why we decrease address in memory
querolita Jun 13, 2024
d77fafc
print updated instruction counter when exit code
querolita Jun 13, 2024
1a6c1db
Merge branch 'master' into zkvm/mips/test-swr
querolita Jun 13, 2024
36c2fdc
use normalized instruction counter for logs
querolita Jun 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 32 additions & 9 deletions o1vm/src/mips/interpreter.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2464,18 +2464,25 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
unsafe { env.bitmask(&addr, 2, 0, pos) }
};

let overwrite_0 = env.equal(&byte_subaddr, &Env::constant(3));
let overwrite_1 = env.equal(&byte_subaddr, &Env::constant(2)) + overwrite_0.clone();
let overwrite_2 = env.equal(&byte_subaddr, &Env::constant(1)) + overwrite_1.clone();
let overwrite_3 = env.equal(&byte_subaddr, &Env::constant(0)) + overwrite_2.clone();
let mod_0 = env.equal(&byte_subaddr, &Env::constant(0));
let mod_1 = env.equal(&byte_subaddr, &Env::constant(1));
let mod_2 = env.equal(&byte_subaddr, &Env::constant(2));
let mod_3 = env.equal(&byte_subaddr, &Env::constant(3));

// The `-3` here feels odd, but simulates the `<< 24` in cannon, and matches the
// behavior defined in the spec.
// See e.g. 'MIPS IV Instruction Set' Rev 3.2, Table A-31 for reference.
let m0 = env.read_memory(&(addr.clone() - Env::constant(3)));
//
// "EffAddr is the address of the least-significant of four consecutive bytes
// forming a word in memory"
//
// Because we shift the bytes in memory to the right, we need to access smaller
// addresses of memory.
// Big-endian notation here
let m1 = env.read_memory(&(addr.clone() - Env::constant(2)));
let m2 = env.read_memory(&(addr.clone() - Env::constant(1)));
let m3 = env.read_memory(&addr);
// No need to compute m0 as mem(addr-3) because it is not used here

let [r0, r1, r2, r3] = {
let initial_register_value = env.read_register(&rt);
Expand Down Expand Up @@ -2503,31 +2510,47 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
]
};

// if mod = 0 -> r3 m1 m2 m3
// if mod = 1 -> r2 r3 m2 m3
// if mod = 2 -> r1 r2 r3 m3
// if mod = 3 -> r0 r1 r2 r3
let v0 = {
let pos = env.alloc_scratch();
env.copy(
&(overwrite_0.clone() * r0 + (Env::constant(1) - overwrite_0) * m0),
&(r3.clone() * mod_0.clone()
+ r2.clone() * mod_1.clone()
+ r1.clone() * mod_2.clone()
+ r0 * mod_3.clone()),
pos,
)
};
let v1 = {
let pos = env.alloc_scratch();
env.copy(
&(overwrite_1.clone() * r1 + (Env::constant(1) - overwrite_1) * m1),
&(m1 * mod_0.clone()
+ r3.clone() * mod_1.clone()
+ r2.clone() * mod_2.clone()
+ r1 * mod_3.clone()),
pos,
)
};
// if mod = 0 -> r3 m1 m2 m3
// if mod = 1 -> r2 r3 m2 m3
// if mod = 2 -> r1 r2 r3 m3
// if mod = 3 -> r0 r1 r2 r3
let v2 = {
let pos = env.alloc_scratch();
env.copy(
&(overwrite_2.clone() * r2 + (Env::constant(1) - overwrite_2) * m2),
&(m2 * (mod_0.clone() + mod_1.clone())
+ r3.clone() * mod_2.clone()
+ r2 * mod_3.clone()),
pos,
)
};
let v3 = {
let pos = env.alloc_scratch();
env.copy(
&(overwrite_3.clone() * r3 + (Env::constant(1) - overwrite_3) * m3),
&(m3 * (mod_0.clone() + mod_1.clone() + mod_2.clone()) + r3 * mod_3),
pos,
)
};
Expand Down
75 changes: 75 additions & 0 deletions o1vm/src/mips/tests.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -454,6 +454,81 @@ mod unit {
interpret_itype(&mut dummy_env, ITypeInstruction::Load32);
assert_eq!(dummy_env.registers.general_purpose[4], exp_v);
}

#[test]
fn test_unit_swr_instruction() {
// swr instruction
// case 0x2e: swr
// val := rt << (24 - (rs&3)*8)
// mask := uint32(0xFFFFFFFF) << (24 - (rs&3)*8)
// return (mem & ^mask) | val

// Instruction: 0b101110 10101 00001 0000000001000000
// swl rt offset(21)

let mut rng = o1_utils::tests::make_test_rng(None);
let mut dummy_env = dummy_env(&mut rng);

// Values used in the instruction
let rs = 21;
let dst = 1;
let offset = sign_extend(64, 16);

// Set the base address to a small number so dummy_env does not ovf
dummy_env.registers[rs] = rng.gen_range(1000u32..4000u32);
let base = dummy_env.registers[rs];
// The effective address
let (addr, ovf) = base.overflowing_add(offset);
assert!(!ovf);

let shift_right = 24 - (addr & 3) * 8;

// This is the partial value that will be stored into memory
let val = dummy_env.registers[dst] << shift_right;

let mask = 0xFFFFFFFFu32 << shift_right;

// Initial value of the memory
let mem = &dummy_env.memory[0];
let mem = &mem.1;
let m0 = mem[(addr - 3) as usize];
let m1 = mem[(addr - 2) as usize];
let m2 = mem[(addr - 1) as usize];
let m3 = mem[addr as usize];

// Big endian: small addresses of memory represent more significant
let memory =
((m0 as u32) << 24) + ((m1 as u32) << 16) + ((m2 as u32) << 8) + (m3 as u32);

let exp_v = (memory & !mask) | val;

write_instruction(
&mut dummy_env,
InstructionParts {
op_code: 0b101110,
rs: rs as u32, // where base address is obtained from
rt: dst as u32, // destination
rd: 0b00000,
shamt: 0b00001, // offset = 64
funct: 0b000000,
},
);

interpret_itype(&mut dummy_env, ITypeInstruction::StoreWordRight);

// Check the memory after the instruction
let mem = &dummy_env.memory[0];
let mem = &mem.1;
let m0 = mem[(addr - 3) as usize];
let m1 = mem[(addr - 2) as usize];
let m2 = mem[(addr - 1) as usize];
let m3 = mem[addr as usize];

assert_eq!(m0, bitmask(exp_v, 32, 24) as u8);
assert_eq!(m1, bitmask(exp_v, 24, 16) as u8);
assert_eq!(m2, bitmask(exp_v, 16, 8) as u8);
assert_eq!(m3, bitmask(exp_v, 8, 0) as u8);
}
}
}

Expand Down