From 43c4dfa3075b7fa3d88fb5e0d811ae83d0223426 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Fri, 27 Dec 2024 13:01:56 +0100 Subject: [PATCH] o1vm/riscv32im: implement jal --- o1vm/resources/programs/riscv32im/bin/jal | Bin 0 -> 464 bytes o1vm/resources/programs/riscv32im/src/jal.S | 25 +++++++ .../src/interpreters/riscv32im/interpreter.rs | 69 ++++++++++++++++-- o1vm/tests/test_riscv_elf.rs | 17 +++++ 4 files changed, 103 insertions(+), 8 deletions(-) create mode 100755 o1vm/resources/programs/riscv32im/bin/jal create mode 100644 o1vm/resources/programs/riscv32im/src/jal.S diff --git a/o1vm/resources/programs/riscv32im/bin/jal b/o1vm/resources/programs/riscv32im/bin/jal new file mode 100755 index 0000000000000000000000000000000000000000..4b662e82bf985d6fc7771dad29581bc0af8c1734 GIT binary patch literal 464 zcma)2F;2rk5F9&%L`nm?2Y^IFWhF-nS_-HrD5$Y)$AOb#INe<$6d{55LO#F)=y(`N zJRr=*Txc0pI--S#g{8m?NUkAqmrsm?Z2g-N6&6poblBH$u(`) zEl#x2c9b{T4)a3XR9l@-q%2M4oy?bJTHjYSgY-=^pN+&6Mf1>_ne!DLkoh|wTqsIp zp?(a=Hs8vM5S%IJp_YI6F9rCeNy(hX;@@Wai21ayA)+^ivb5m I+wL#-1Jcw#761SM literal 0 HcmV?d00001 diff --git a/o1vm/resources/programs/riscv32im/src/jal.S b/o1vm/resources/programs/riscv32im/src/jal.S new file mode 100644 index 0000000000..191cdfbb3e --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/jal.S @@ -0,0 +1,25 @@ +.section .text +.global _start + +# t0 <- t0 + t1 +add_t0_t1: + add t0, t0, t1 + ret + +_start: + li t0, 5 + li t1, 7 + # Could be jalr + # jal without offset + jal ra, add_t0_t1 + + # exit + li a0, 0 + li a1, 0 + li a2, 0 + li a3, 0 + li a4, 0 + li a5, 0 + li a6, 0 + li a7, 42 + ecall diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index ad029b0a81..91f100e911 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2482,14 +2482,30 @@ pub fn interpret_utype(env: &mut Env, instr: UInstruction) /// Interpret an UJ-type instruction. /// The encoding of an UJ-type instruction is as follows: /// ```text -/// | 31 12 | 11 7 | 6 0 | -/// | immediate | rd | opcode | +/// | 31 12 | 11 7 | 6 0 | +/// | imm[20|10:1|11|19:12] | rd | opcode | /// ``` /// Following the documentation found /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf) +/// +/// The interpretation of the immediate is as follow: +/// ```text +/// imm_20 = instruction[31] +/// imm_10_1 = instruction[30..21] +/// imm_11 = instruction[20] +/// imm_19_12 = instruction[19..12] +/// +/// imm = imm_20 << 19 + +/// imm_19_12 << 11 + +/// imm_11 << 10 + +/// imm_10_1 +/// +/// # The immediate is then sign-extended. The sign-extension is in the bit imm20 +/// imm = imm << 1 +/// ``` pub fn interpret_ujtype(env: &mut Env, instr: UJInstruction) { let instruction_pointer = env.get_instruction_pointer(); - let _next_instruction_pointer = env.get_next_instruction_pointer(); + let next_instruction_pointer = env.get_next_instruction_pointer(); let instruction = { let v0 = env.read_memory(&instruction_pointer); @@ -2514,18 +2530,55 @@ pub fn interpret_ujtype(env: &mut Env, instr: UJInstruction }; env.range_check8(&rd, 5); - // FIXME: trickier - let _imm = { + let imm20 = { let pos = env.alloc_scratch(); - unsafe { env.bitmask(&instruction, 32, 12, pos) } + unsafe { env.bitmask(&instruction, 32, 31, pos) } + }; + env.assert_boolean(&imm20); + + let imm10_1 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 31, 21, pos) } + }; + env.range_check16(&imm10_1, 10); + + let imm11 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 21, 20, pos) } + }; + env.assert_boolean(&imm11); + + let imm19_12 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 20, 12, pos) } + }; + env.range_check8(&imm19_12, 8); + + let offset = { + imm10_1.clone() * Env::constant(1 << 1) + + imm11.clone() * Env::constant(1 << 11) + + imm19_12.clone() * Env::constant(1 << 12) + + imm20.clone() * Env::constant(1 << 20) }; // FIXME: check correctness of decomposition + match instr { UJInstruction::JumpAndLink => { - unimplemented!("JumpAndLink") + let offset = env.sign_extend(&offset, 21); + let new_addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness(&instruction_pointer, &offset, res_scratch, overflow_scratch) + }; + res + }; + env.write_register(&rd, next_instruction_pointer.clone()); + env.set_instruction_pointer(new_addr.clone()); + env.set_next_instruction_pointer(new_addr + Env::constant(4u32)); } - }; + } } pub fn interpret_syscall(env: &mut Env, _instr: SyscallInstruction) { diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index 1046d2198b..d73e008b8e 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -430,3 +430,20 @@ fn test_mul_overflow() { assert_eq!(witness.registers[T2], 276447232); } + +#[test] +fn test_jal() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/jal", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 12); + assert_eq!(witness.registers[T1], 7); +}