From 2aeb0fd5a3d1b07bc28f3b14b39452c25e8b5cc7 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 26 Dec 2024 11:44:09 +0100 Subject: [PATCH 1/2] o1vm/riscv32im: being strict on scope It is mostly to simplify formal verification tools generating Coq/Lean from Rust code --- .../src/interpreters/riscv32im/interpreter.rs | 39 ++++++++++++------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index e51d7574d4..bab2dcd7cf 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1523,9 +1523,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sub: x[rd] = x[rs1] - x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let underflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); let local_rd = unsafe { + let underflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); let (local_rd, _underflow) = env.sub_witness(&local_rs1, &local_rs2, rd_scratch, underflow_scratch); local_rd @@ -1895,11 +1895,12 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // addi: x[rd] = x[rs1] + sext(immediate) let local_rs1 = env.read_register(&(rs1.clone())); let local_imm = env.sign_extend(&imm, 12); - let overflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { - let (local_rd, _overflow) = - env.add_witness(&local_rs1, &local_imm, rd_scratch, overflow_scratch); + let local_rd = { + let overflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); + let (local_rd, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_imm, rd_scratch, overflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1910,8 +1911,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // xori: x[rd] = x[rs1] ^ sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.xor_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.xor_witness(&local_rs1, &local_imm, 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)); @@ -1920,8 +1923,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // ori: x[rd] = x[rs1] | sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.or_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.or_witness(&local_rs1, &local_imm, 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)); @@ -1930,8 +1935,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // andi: x[rd] = x[rs1] & sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.and_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.and_witness(&local_rs1, &local_imm, 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)); @@ -2438,8 +2445,10 @@ pub fn interpret_utype(env: &mut Env, instr: UInstruction) UInstruction::LoadUpperImmediate => { // lui: x[rd] = sext(immediate[31:12] << 12) let local_imm = { - let pos = env.alloc_scratch(); - let shifted_imm = unsafe { env.shift_left(&imm, &Env::constant(12), pos) }; + let shifted_imm = { + let pos = env.alloc_scratch(); + unsafe { env.shift_left(&imm, &Env::constant(12), pos) } + }; env.sign_extend(&shifted_imm, 32) }; env.write_register(&rd, local_imm); From ff890834f5d004c2f158d89abdcf3f4955a31d42 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Thu, 26 Dec 2024 11:50:04 +0100 Subject: [PATCH 2/2] o1vm/riscv32im: place correctly the unsafe keyword --- .../src/interpreters/riscv32im/interpreter.rs | 50 ++++++++++--------- 1 file changed, 26 insertions(+), 24 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index bab2dcd7cf..ad029b0a81 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1507,11 +1507,12 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) // add: x[rd] = x[rs1] + x[rs2] let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let overflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { - let (local_rd, _overflow) = - env.add_witness(&local_rs1, &local_rs2, rd_scratch, overflow_scratch); + let local_rd = { + let overflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); + let (local_rd, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_rs2, rd_scratch, overflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1523,11 +1524,12 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sub: x[rd] = x[rs1] - x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let underflow_scratch = env.alloc_scratch(); let rd_scratch = env.alloc_scratch(); - let (local_rd, _underflow) = - env.sub_witness(&local_rs1, &local_rs2, rd_scratch, underflow_scratch); + let (local_rd, _underflow) = unsafe { + env.sub_witness(&local_rs1, &local_rs2, rd_scratch, underflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1539,9 +1541,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sll: x[rd] = x[rs1] << x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let rd_scratch = env.alloc_scratch(); - env.shift_left(&local_rs1, &local_rs2, rd_scratch) + unsafe { env.shift_left(&local_rs1, &local_rs2, rd_scratch) } }; env.write_register(&rd, local_rd); @@ -1552,9 +1554,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* slt: x[rd] = (x[rs1] < x[rs2]) ? 1 : 0 */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let rd_scratch = env.alloc_scratch(); - env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) + unsafe { env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) } }; env.write_register(&rd, local_rd); @@ -1565,9 +1567,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sltu: x[rd] = (x[rs1] < (u)x[rs2]) ? 1 : 0 */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.test_less_than(&local_rs1, &local_rs2, pos) + unsafe { env.test_less_than(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1578,9 +1580,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* xor: x[rd] = x[rs1] ^ x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.xor_witness(&local_rs1, &local_rs2, pos) + unsafe { env.xor_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1591,9 +1593,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* srl: x[rd] = x[rs1] >> x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.shift_right(&local_rs1, &local_rs2, pos) + unsafe { env.shift_right(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1604,9 +1606,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sra: x[rd] = x[rs1] >> x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.shift_right_arithmetic(&local_rs1, &local_rs2, pos) + unsafe { env.shift_right_arithmetic(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1617,9 +1619,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* or: x[rd] = x[rs1] | x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.or_witness(&local_rs1, &local_rs2, pos) + unsafe { env.or_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1630,9 +1632,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* and: x[rd] = x[rs1] & x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.and_witness(&local_rs1, &local_rs2, pos) + unsafe { env.and_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd);