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.

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

Unit test for LoadWordRight #2293

Draft
wants to merge 12 commits into
base: master
Choose a base branch
from
Draft
50 changes: 32 additions & 18 deletions o1vm/src/mips/interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2153,20 +2153,29 @@ 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
// 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.
// Because we shift the bytes in memory to the right, we need to access smaller
// addresses of memory.
//
// From docs: "EffAddr is the address of the least-significant of
// four consecutive bytes word in memory"
//
// Big-endian notation here
let m0 = env.read_memory(&(addr.clone() - Env::constant(3)));
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);

let [r0, r1, r2, r3] = {
// No need to compute r3 as bitmask(reg,8,0,pos) as it is not used
let [r0, r1, r2] = {
let initial_register_value = env.read_register(&rt);
[
{
Expand All @@ -2184,22 +2193,27 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
let pos = env.alloc_scratch();
unsafe { env.bitmask(&initial_register_value, 16, 8, pos) }
},
{
// FIXME: Requires a range check
let pos = env.alloc_scratch();
unsafe { env.bitmask(&initial_register_value, 8, 0, pos) }
},
]
};

// if mod = 0 -> r0 r1 r2 m0
// if mod = 1 -> r0 r1 m0 m1
// if mod = 2 -> r0 m0 m1 m2
// if mod = 3 -> m0 m1 m2 m3
let value = {
let value = ((overwrite_0.clone() * m0 + (Env::constant(1) - overwrite_0) * r0)
* Env::constant(1 << 24))
+ ((overwrite_1.clone() * m1 + (Env::constant(1) - overwrite_1) * r1)
* Env::constant(1 << 16))
+ ((overwrite_2.clone() * m2 + (Env::constant(1) - overwrite_2) * r2)
* Env::constant(1 << 8))
+ (overwrite_3.clone() * m3 + (Env::constant(1) - overwrite_3) * r3);
let value = Env::constant(1 << 24)
* (r0 * (mod_0.clone() + mod_1.clone() + mod_2.clone())
+ m0.clone() * mod_3.clone())
+ Env::constant(1 << 16)
* (r1 * (mod_0.clone() + mod_1.clone())
+ m0.clone() * mod_2.clone()
+ m1.clone() * mod_3.clone())
+ Env::constant(1 << 8)
* (r2 * mod_0.clone()
+ m0.clone() * mod_1.clone()
+ m1.clone() * mod_2.clone()
+ m2.clone() * mod_3.clone())
+ (m0 * mod_0 + m1 * mod_1 + m2 * mod_2 + m3 * mod_3);
let pos = env.alloc_scratch();
env.copy(&value, pos)
};
Expand Down
65 changes: 63 additions & 2 deletions o1vm/src/mips/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -155,8 +155,8 @@ mod unit {
{
let dummy_preimage_oracle = OnDiskPreImageOracle;
let mut env = WEnv {
// Set it to 2 to run 1 instruction that access registers if
instruction_counter: 2,
// Set it to an arbitrary "large" number
instruction_counter: 10,
// Only 8kb of memory (two PAGE_ADDRESS_SIZE)
memory: vec![
// Read/write memory
Expand Down Expand Up @@ -454,6 +454,67 @@ mod unit {
interpret_itype(&mut dummy_env, ITypeInstruction::Load32);
assert_eq!(dummy_env.registers.general_purpose[4], exp_v);
}

#[test]
fn test_unit_lwr_instruction() {
// lwr instruction
// val := mem >> (24 - (rs&3)*8)
// mask := uint32(0xFFFFFFFF) >> (24 - (rs&3)*8)
// return (rt & ^mask) | val

// Instruction: 0b100110 10101 00001 0000000001000000
// lwr 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(4u32..4000u32);
let base = dummy_env.registers[rs];
// The effective address
let (addr, ovf) = base.overflowing_add(offset);
assert!(!ovf);

let shift_right = 24 - (dummy_env.registers[rs] & 3) * 8;
let mask = 0xFFFFFFFF >> shift_right;

let mem = &dummy_env.memory[0];
let mem = &mem.1;

// Here starts the least significant byte of the word we will load
let m3 = mem[addr as usize];
let m2 = mem[(addr - 1) as usize];
let m1 = mem[(addr - 2) as usize];
let m0 = mem[(addr - 3) 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 val = memory >> shift_right;

let exp_v = (dummy_env.registers[dst] & !mask) | val;

write_instruction(
&mut dummy_env,
InstructionParts {
op_code: 0b100010,
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::LoadWordRight);

assert_eq!(dummy_env.registers[dst], exp_v);
}
}
}

Expand Down