diff --git a/o1vm/src/mips/interpreter.rs b/o1vm/src/mips/interpreter.rs index 7126ca9e06..582d23b91d 100644 --- a/o1vm/src/mips/interpreter.rs +++ b/o1vm/src/mips/interpreter.rs @@ -2153,20 +2153,29 @@ pub fn interpret_itype(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); [ { @@ -2184,22 +2193,27 @@ pub fn interpret_itype(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) }; diff --git a/o1vm/src/mips/tests.rs b/o1vm/src/mips/tests.rs index 3d6b499f85..24be5b5d2b 100644 --- a/o1vm/src/mips/tests.rs +++ b/o1vm/src/mips/tests.rs @@ -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 @@ -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); + } } } diff --git a/o1vm/src/mips/witness.rs b/o1vm/src/mips/witness.rs index 2981a4f6ec..f54d5332d4 100644 --- a/o1vm/src/mips/witness.rs +++ b/o1vm/src/mips/witness.rs @@ -616,7 +616,8 @@ impl InterpreterEnv for Env Env { (opcode, instruction) } + /// Because MAX_NB_REG_ACC = 7 and MAX_NB_MEM_ACC = 12, at most the same + /// instruction will increase the instruction counter by MAX_ACC = 19. + /// + /// NOTE: actually, in practice it will be less than that, as there is no + /// single instruction that performs all of them. + /// + /// This means that the actual number of instructions executed will result + /// from dividing the instruction counter by MAX_ACC (floor). + pub fn instruction_counter_normalized(&self) -> u64 { + self.instruction_counter / MAX_ACC + } + /// Updates the instruction counter, accounting for the maximum number of /// register and memory accesses per instruction. /// Because MAX_NB_REG_ACC = 7 and MAX_NB_MEM_ACC = 12, at most the same @@ -1079,7 +1092,7 @@ impl Env { /// the real instruction counter and multiply it by MAX_ACC to have a unique /// representation of each step (which is helpful for debugging). pub fn update_instruction_counter(&mut self) { - self.instruction_counter = ((self.instruction_counter / MAX_ACC) + 1) * MAX_ACC; + self.instruction_counter = (self.instruction_counter_normalized() + 1) * MAX_ACC; } /// Execute a single step of the MIPS program. @@ -1101,7 +1114,8 @@ impl Env { self.halt = true; println!( "Halted as requested at step={} instruction={:?}", - self.instruction_counter, opcode + self.instruction_counter_normalized(), + opcode ); return opcode; } @@ -1114,7 +1128,7 @@ impl Env { if self.halt { println!( "Halted at step={} instruction={:?}", - self.instruction_counter / MAX_ACC, + self.instruction_counter_normalized(), opcode ); } @@ -1122,7 +1136,7 @@ impl Env { } fn should_trigger_at(&self, at: &StepFrequency) -> bool { - let m: u64 = self.instruction_counter; + let m: u64 = self.instruction_counter_normalized(); match at { StepFrequency::Never => false, StepFrequency::Always => true, @@ -1198,7 +1212,8 @@ impl Env { let _ = serde_json::to_writer(&mut writer, &s); info!( "Snapshot state in {}, step {}", - filename, self.instruction_counter + filename, + self.instruction_counter_normalized() ); writer.flush().expect("Flush writer failing") } @@ -1208,7 +1223,7 @@ impl Env { if self.should_trigger_at(at) { let elapsed = start.time.elapsed(); // Compute the step number removing the MAX_ACC factor - let step = self.instruction_counter / MAX_ACC; + let step = self.instruction_counter_normalized(); let pc = self.registers.current_instruction_pointer; // Get the 32-bits opcode