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 StoreWordLeft #2318

Closed
wants to merge 5 commits into from
Closed

Unit test for StoreWordLeft #2318

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
f44d94c
fix interpreter swl with cannon instruction and unit test
querolita Jun 13, 2024
c25491a
add comment to explain why we increase addresses in memory
querolita Jun 13, 2024
371679d
print updated instruction counter when exit code
querolita Jun 13, 2024
22a8c60
Merge branch 'master' into zkvm/mips/test-swl
querolita Jun 13, 2024
f74aaf6
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
34 changes: 22 additions & 12 deletions o1vm/src/mips/interpreter.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2374,15 +2374,17 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
unsafe { env.bitmask(&addr, 2, 0, pos) }
};

let overwrite_3 = env.equal(&byte_subaddr, &Env::constant(0));
let overwrite_2 = env.equal(&byte_subaddr, &Env::constant(1)) + overwrite_3.clone();
let overwrite_1 = env.equal(&byte_subaddr, &Env::constant(2)) + overwrite_2.clone();
let overwrite_0 = env.equal(&byte_subaddr, &Env::constant(3)) + overwrite_1.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));

// From docs: "EffAddr is the address of the most-significant of
// four consecutive bytes forming a word in memory"
let m0 = env.read_memory(&addr);
let m1 = env.read_memory(&(addr.clone() + Env::constant(1)));
let m2 = env.read_memory(&(addr.clone() + Env::constant(2)));
let m3 = env.read_memory(&(addr.clone() + Env::constant(3)));
// No need to define m3 as mem(addr+3) because it is never used in swl

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

// if mod = 0 -> r0 r1 r2 r3
// if mod = 1 -> m0 r0 r1 r2
// if mod = 2 -> m0 m1 r0 r1
// if mod = 3 -> m0 m1 m2 r0
let v0 = {
let pos = env.alloc_scratch();
env.copy(
&(overwrite_0.clone() * r0 + (Env::constant(1) - overwrite_0) * m0),
&(r0.clone() * mod_0.clone()
+ m0 * (mod_1.clone() + mod_2.clone() + mod_3.clone())),
pos,
)
};
let v1 = {
let pos = env.alloc_scratch();
env.copy(
&(overwrite_1.clone() * r1 + (Env::constant(1) - overwrite_1) * m1),
&(r1.clone() * mod_0.clone()
+ r0.clone() * mod_1.clone()
+ m1 * (mod_2.clone() + mod_3.clone())),
pos,
)
};
let v2 = {
let pos = env.alloc_scratch();
env.copy(
&(overwrite_2.clone() * r2 + (Env::constant(1) - overwrite_2) * m2),
&(r2.clone() * mod_0.clone()
+ r1.clone() * mod_1.clone()
+ r0.clone() * mod_2.clone()
+ m2 * mod_3.clone()),
pos,
)
};
let v3 = {
let pos = env.alloc_scratch();
env.copy(
&(overwrite_3.clone() * r3 + (Env::constant(1) - overwrite_3) * m3),
pos,
)
env.copy(&(r3 * mod_0 + r2 * mod_1 + r1 * mod_2 + r0 * mod_3), pos)
};

// Big-endian: most significant bytes into smaller addresses
env.write_memory(&addr, v0);
env.write_memory(&(addr.clone() + Env::constant(1)), v1);
env.write_memory(&(addr.clone() + Env::constant(2)), v2);
Expand Down
76 changes: 76 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,82 @@ mod unit {
interpret_itype(&mut dummy_env, ITypeInstruction::Load32);
assert_eq!(dummy_env.registers.general_purpose[4], exp_v);
}

#[test]
fn test_unit_swl_instruction() {
// swl instruction
// case 0x2a: swl
// val := rt >> ((rs & 3) * 8)
// mask := uint32(0xFFFFFFFF) >> ((rs & 3) * 8)
// return (mem & ^mask) | val

// Instruction: 0b101010 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);

// Number of bytes that will be kept on the right of memory
let shift_left = (addr & 3) * 8;

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

let mask = 0xFFFFFFFFu32 >> shift_left;

// Initial value of the memory
let mem = &dummy_env.memory[0];
let mem = &mem.1;
let v0 = mem[addr as usize];
let v1 = mem[(addr + 1) as usize];
let v2 = mem[(addr + 2) as usize];
let v3 = mem[(addr + 3) as usize];

// Big endian: small addresses of memory represent more significant
let memory =
((v0 as u32) << 24) + ((v1 as u32) << 16) + ((v2 as u32) << 8) + (v3 as u32);

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

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

// Check the memory after the instruction
let mem = &dummy_env.memory[0];
let mem = &mem.1;
let v0 = mem[addr as usize];
let v1 = mem[(addr + 1) as usize];
let v2 = mem[(addr + 2) as usize];
let v3 = mem[(addr + 3) as usize];

assert_eq!(v0, bitmask(exp_v, 32, 24) as u8);
assert_eq!(v1, bitmask(exp_v, 24, 16) as u8);
assert_eq!(v2, bitmask(exp_v, 16, 8) as u8);
assert_eq!(v3, bitmask(exp_v, 8, 0) as u8);
}
}
}

Expand Down