From b32afd03e52be0b1ce4775dc2e56ca60aa6f55ac Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 23 Dec 2024 16:23:40 +0100 Subject: [PATCH 1/2] o1vm/riscv32im: additional documentation when dividing by zero --- o1vm/src/interpreters/riscv32im/interpreter.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index e960a93fb4..f2cb725bc9 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1286,6 +1286,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, @@ -1314,6 +1318,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, From 27a0dd4865fb24815c8b8c8e64d7e590a9ff2da4 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 23 Dec 2024 16:23:57 +0100 Subject: [PATCH 2/2] o1vm/riscv32im: test dividing by zero --- .../programs/riscv32im/bin/div_by_zero | Bin 0 -> 456 bytes .../programs/riscv32im/bin/divu_by_zero | Bin 0 -> 456 bytes .../programs/riscv32im/src/div_by_zero.S | 19 +++++++++++ .../programs/riscv32im/src/divu_by_zero.S | 19 +++++++++++ o1vm/tests/test_riscv_elf.rs | 30 ++++++++++++++++++ 5 files changed, 68 insertions(+) create mode 100755 o1vm/resources/programs/riscv32im/bin/div_by_zero create mode 100755 o1vm/resources/programs/riscv32im/bin/divu_by_zero create mode 100644 o1vm/resources/programs/riscv32im/src/div_by_zero.S create mode 100644 o1vm/resources/programs/riscv32im/src/divu_by_zero.S 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 0000000000000000000000000000000000000000..57cd40f70db51171753060c0f6f10029cba63f67 GIT binary patch literal 456 zcma)2F;2rk5L{mfM4|!R2asq|S>(tED4?RG#yT5EoD_p~w~0_19+3~E;0HW`C-DJh zY;0P_nw{Cz?wxPnZ}0E2ERz97zJ-}0E}?TIN6@8Qh>`BSH+R+Di5SJB{0G7hJn28rNPG zo^It@S3EK7LX{%xyRfQXsv3>(O|w}qXuNM;d$W$If)mNpbJD23lw9jKmAtzv_o^|J w8?E^d|HUa9`D#3++o3{n#R%?*I0w1ME(tED4?RG#yT5EoD_p~w~0_19+3~E;0HW~r|`BSH+R+Di5SJB{0G7hJn28rNPG zo^It@S3EK7LX{%xyRfQXsv3>(O|w}qXuNM;d$W$If)mNpbJD23lw9jKmAtzv_o^|J w8?E^d|HUa9`D#3++o3{n#R%?*I0w1ME::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(); + } +}