From bb0d63f4e79e2ba947b59761f15325119418381d Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Tue, 23 Apr 2024 13:34:25 +0200 Subject: [PATCH] MIPS/Store32: add missing constraint checking the decomposition --- optimism/src/mips/interpreter.rs | 9 +++++++++ optimism/src/mips/tests.rs | 7 ++++--- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/optimism/src/mips/interpreter.rs b/optimism/src/mips/interpreter.rs index 52495b9d76..5c6db9ae03 100644 --- a/optimism/src/mips/interpreter.rs +++ b/optimism/src/mips/interpreter.rs @@ -2278,6 +2278,15 @@ pub fn interpret_itype(env: &mut Env, instr: ITypeInstructi }, ] }; + // Checking that v is the correct decomposition. + { + let res = value + - v0.clone() * Env::constant(1 << 24) + - v1.clone() * Env::constant(1 << 16) + - v2.clone() * Env::constant(1 << 8) + - v3.clone(); + env.is_zero(&res) + }; env.write_memory(&addr, v0); env.write_memory(&(addr.clone() + Env::constant(1)), v1); env.write_memory(&(addr.clone() + Env::constant(2)), v2); diff --git a/optimism/src/mips/tests.rs b/optimism/src/mips/tests.rs index 259b73e1c9..0ff276df9b 100644 --- a/optimism/src/mips/tests.rs +++ b/optimism/src/mips/tests.rs @@ -78,9 +78,10 @@ fn test_mips_number_constraints() { JumpAndLink => assert_num_constraints(&instr, 3), }, IType(itype) => match itype { - BranchLeqZero | BranchGtZero | BranchLtZero | BranchGeqZero | Store8 | Store16 - | Store32 => assert_num_constraints(&instr, 0), - BranchEq | BranchNeq => assert_num_constraints(&instr, 2), + BranchLeqZero | BranchGtZero | BranchLtZero | BranchGeqZero | Store8 | Store16 => { + assert_num_constraints(&instr, 0) + } + BranchEq | BranchNeq | Store32 => assert_num_constraints(&instr, 2), AddImmediate | AddImmediateUnsigned | SetLessThanImmediate