diff --git a/o1vm/resources/programs/riscv32im/bin/div_by_zero b/o1vm/resources/programs/riscv32im/bin/div_by_zero new file mode 100755 index 0000000000..57cd40f70d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/div_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/divu_by_zero b/o1vm/resources/programs/riscv32im/bin/divu_by_zero new file mode 100755 index 0000000000..494eedac4b Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/divu_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/src/div_by_zero.S b/o1vm/resources/programs/riscv32im/src/div_by_zero.S new file mode 100644 index 0000000000..5f8c490924 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/div_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Signed division by zero (div) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + div t2, t0, t1 # t2 = t0 / t1 (Expected: division by zero) + + # Custom exit syscall + 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/resources/programs/riscv32im/src/divu_by_zero.S b/o1vm/resources/programs/riscv32im/src/divu_by_zero.S new file mode 100644 index 0000000000..b44ff50479 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/divu_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Unsigned division by zero (div) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + divu t2, t0, t1 # t2 = t0 / t1 (Expected: division by zero) + + # Custom exit syscall + 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 a7cfa3ca29..e51d7574d4 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1280,6 +1280,10 @@ pub trait InterpreterEnv { /// There are no constraints on the returned values; callers must manually add constraints to /// ensure that the pair of returned values correspond to the given values `x` and `y`, and /// that they fall within the desired range. + /// + /// Division by zero will create a panic! exception. The RISC-V + /// specification leaves the case unspecified, and therefore we prefer to + /// forbid this case while building the witness. unsafe fn div_signed( &mut self, x: &Self::Variable, @@ -1308,6 +1312,10 @@ pub trait InterpreterEnv { /// There are no constraints on the returned values; callers must manually add constraints to /// ensure that the pair of returned values correspond to the given values `x` and `y`, and /// that they fall within the desired range. + /// + /// Division by zero will create a panic! exception. The RISC-V + /// specification leaves the case unspecified, and therefore we prefer to + /// forbid this case while building the witness. unsafe fn div( &mut self, x: &Self::Variable, diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index 952bcda41c..81491a1b6d 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -356,3 +356,33 @@ fn test_slt() { assert_eq!(witness.registers[T5], 0); assert_eq!(witness.registers[T6], 0); } + +#[test] +#[should_panic] +fn test_div_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/div_by_zero", + )); + 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(); + } +} + +#[test] +#[should_panic] +fn test_divu_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/divu_by_zero", + )); + 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(); + } +}