diff --git a/compiler/noirc_evaluator/src/acir/acir_context/mod.rs b/compiler/noirc_evaluator/src/acir/acir_context/mod.rs index 97f65bd941a..21d9f1d8233 100644 --- a/compiler/noirc_evaluator/src/acir/acir_context/mod.rs +++ b/compiler/noirc_evaluator/src/acir/acir_context/mod.rs @@ -1169,6 +1169,18 @@ impl> AcirContext { let r_is_not_0 = self.not_var(r_is_0, AcirType::unsigned(1))?; let remainder = self.mul_var(remainder, r_is_not_0)?; + // The quotient must be a valid signed integer. + // For instance -128/-1 = 128, but 128 is not a valid i8 + // Because it is the only possible overflow that can happen due to signed representation, + // we simply check for this case: quotient is negative, or distinct from 2^{bit_size-1} + // Indeed, negative quotient cannot 'overflow' because the division will not increase its absolute value + let assert_message = + self.generate_assertion_message_payload("Attempt to divide with overflow".to_string()); + let unsigned = self.not_var(q_sign, AcirType::unsigned(1))?; + // We just use `unsigned` for the predicate of assert_neq_var because if the `predicate` is false, the quotient + // we get from the unsigned division under the predicate will not be 2^{bit_size-1} anyways. + self.assert_neq_var(quotient, max_power_of_two, unsigned, Some(assert_message))?; + Ok((quotient, remainder)) } diff --git a/compiler/noirc_evaluator/src/acir/tests/mod.rs b/compiler/noirc_evaluator/src/acir/tests/mod.rs index 862eb81143c..61eb87259e6 100644 --- a/compiler/noirc_evaluator/src/acir/tests/mod.rs +++ b/compiler/noirc_evaluator/src/acir/tests/mod.rs @@ -1082,6 +1082,33 @@ fn test_operators( } } +#[test] +// Regression for https://github.com/noir-lang/noir/issues/9847 +fn signed_div_overflow() { + // Test that check -128 / -1 overflow for i8 + let src = r#" + acir(inline) predicate_pure fn main f0 { + b0(v1: i8, v2: i8): + v3 = div v1, v2 + return + } + "#; + + let ssa = Ssa::from_str(src).unwrap(); + let inputs = vec![FieldElement::from(128_u128), FieldElement::from(255_u128)]; + let inputs = inputs + .into_iter() + .enumerate() + .map(|(i, f)| (Witness(i as u32), f)) + .collect::>(); + let initial_witness = WitnessMap::from(inputs); + let output = None; + + // acir execution should fail to divide -128 / -1 + let acir_execution_result = execute_ssa(ssa, initial_witness.clone(), output.as_ref()); + assert!(matches!(acir_execution_result, (ACVMStatus::Failure(_), _))); +} + proptest! { #[test] fn test_binary_on_field(lhs in 0u128.., rhs in 0u128..) {