From 2c0c7b269c5b7fdc09e4c415815e1f0dc1030fbd Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 25 Nov 2024 09:53:01 -0500 Subject: [PATCH 1/4] implementation for shift left logical immediate --- o1vm/src/interpreters/riscv32im/interpreter.rs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 5fe7535c60..54070f55ce 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1752,7 +1752,19 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } IInstruction::ShiftLeftLogicalImmediate => { - unimplemented!("ShiftLeftLogicalImmediate") + // slli: x[rd] = x[rs1] << shamt + let local_rs1 = env.read_register(&rs1); + let shamt = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&imm, 4, 0, pos) } + }; + // parse shamt from imm as 20-24 of instruction and 0-4 wrt to imm + let rd_scratch = env.alloc_scratch(); + let local_rd = unsafe { env.shift_left(&local_rs1, &shamt, rd_scratch) }; + + env.write_register(&rd, local_rd); + env.set_instruction_pointer(next_instruction_pointer.clone()); + env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); } IInstruction::ShiftRightLogicalImmediate => { unimplemented!("ShiftRightLogicalImmediate") From 29b12a8df5b163e173a6b48c2513ac9bcdae69eb Mon Sep 17 00:00:00 2001 From: svv232 Date: Wed, 11 Dec 2024 11:19:28 -0500 Subject: [PATCH 2/4] correctly parse the shant --- o1vm/src/interpreters/riscv32im/interpreter.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 54070f55ce..eefccaee39 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1756,7 +1756,7 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) let local_rs1 = env.read_register(&rs1); let shamt = { let pos = env.alloc_scratch(); - unsafe { env.bitmask(&imm, 4, 0, pos) } + unsafe { env.bitmask(&imm, 5, 0, pos) } }; // parse shamt from imm as 20-24 of instruction and 0-4 wrt to imm let rd_scratch = env.alloc_scratch(); From c5a30739b7defda1c61443ce54f8e44eb41cc4ff Mon Sep 17 00:00:00 2001 From: svv232 Date: Wed, 11 Dec 2024 11:22:49 -0500 Subject: [PATCH 3/4] keep the standard variable allocation syntax for interpreter variables for clarity --- o1vm/src/interpreters/riscv32im/interpreter.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index eefccaee39..c5e52c2760 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1759,8 +1759,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) unsafe { env.bitmask(&imm, 5, 0, pos) } }; // parse shamt from imm as 20-24 of instruction and 0-4 wrt to imm - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.shift_left(&local_rs1, &shamt, rd_scratch) }; + let local_rd = { + let pos = env.alloc_scratch(); + unsafe { env.shift_left(&local_rs1, &shamt, pos) } + }; env.write_register(&rd, local_rd); env.set_instruction_pointer(next_instruction_pointer.clone()); From 4ba3d5836550e46e78fabb849b0be26850e0ddf8 Mon Sep 17 00:00:00 2001 From: svv232 Date: Wed, 11 Dec 2024 12:37:25 -0500 Subject: [PATCH 4/4] parse the shamt at the top level and add correct range and value check --- .../src/interpreters/riscv32im/interpreter.rs | 23 ++++++++++++++----- 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index c5e52c2760..7113ea56c6 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1637,6 +1637,21 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) env.range_check16(&imm, 12); + let shamt = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&imm, 5, 0, pos) } + }; + env.range_check8(&shamt, 5); + + let imm_header = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&imm, 12, 5, pos) } + }; + env.range_check8(&imm_header, 7); + + // check the correctness of the immediate and shamt + env.add_constraint(imm.clone() - (imm_header.clone() * Env::constant(1 << 5)) - shamt.clone()); + // check correctness of decomposition env.add_constraint( instruction @@ -1754,14 +1769,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) IInstruction::ShiftLeftLogicalImmediate => { // slli: x[rd] = x[rs1] << shamt let local_rs1 = env.read_register(&rs1); - let shamt = { - let pos = env.alloc_scratch(); - unsafe { env.bitmask(&imm, 5, 0, pos) } - }; - // parse shamt from imm as 20-24 of instruction and 0-4 wrt to imm + let local_rd = { let pos = env.alloc_scratch(); - unsafe { env.shift_left(&local_rs1, &shamt, pos) } + unsafe { env.shift_left(&local_rs1, &shamt.clone(), pos) } }; env.write_register(&rd, local_rd);