Skip to content

chore(ACIR): expand signed div and mod in SSA #10039

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
asterite merged 7 commits into from
Oct 1, 2025
Merged

chore(ACIR): expand signed div and mod in SSA #10039

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
5f52499
Expand signed division in SSA instead of in ACIR
asterite Sep 30, 2025
1b95bf1
Handle mod too
asterite Sep 30, 2025
7a6e625
Comment
asterite Sep 30, 2025
d14b340
Remove ACIR code, and do one more pass after removing bit shifts (for…
asterite Sep 30, 2025
6479bc5
Expand signed math only once
asterite Sep 30, 2025
c55676e
Typos
asterite Oct 1, 2025
7bd2ed2
Test that we detect -128 i8 / -1 overflow
asterite Oct 1, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 4 additions & 96 deletions compiler/noirc_evaluator/src/acir/acir_context/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -597,10 +597,8 @@ impl<F: AcirField> AcirContext<F> {
self.euclidean_division_var(lhs, rhs, bit_size, predicate)?;
Ok(quotient_var)
}
NumericType::Signed { bit_size } => {
let (quotient_var, _remainder_var) =
self.signed_division_var(lhs, rhs, bit_size, predicate)?;
Ok(quotient_var)
NumericType::Signed { .. } => {
unreachable!("Signed division should have been removed before ACIRgen")
}
}
}
Expand Down Expand Up @@ -1083,96 +1081,6 @@ impl<F: AcirField> AcirContext<F> {
Ok(())
}

// Returns the 2-complement of lhs, using the provided sign bit in 'leading'
// if leading is zero, it returns lhs
// if leading is one, it returns 2^bit_size-lhs
fn two_complement(
&mut self,
lhs: AcirVar,
leading: AcirVar,
max_bit_size: u32,
) -> Result<AcirVar, RuntimeError> {
let max_power_of_two = self.add_constant(power_of_two::<F>(max_bit_size - 1));

let intermediate = self.sub_var(max_power_of_two, lhs)?;
let intermediate = self.mul_var(intermediate, leading)?;

self.add_mul_var(lhs, F::from(2_u128), intermediate)
}

/// Returns the quotient and remainder such that lhs = rhs * quotient + remainder
/// and |remainder| < |rhs|
/// and remainder has the same sign than lhs
/// Note that this is not the euclidean division, where we have instead remainder < |rhs|
fn signed_division_var(
&mut self,
lhs: AcirVar,
rhs: AcirVar,
bit_size: u32,
predicate: AcirVar,
) -> Result<(AcirVar, AcirVar), RuntimeError> {
// We derive the signed division from the unsigned euclidean division.
// note that this is not euclidean division!
// If `x` is a signed integer, then `sign(x)x >= 0`
// so if `a` and `b` are signed integers, we can do the unsigned division:
// `sign(a)a = q1*sign(b)b + r1`
// => `a = sign(a)sign(b)q1*b + sign(a)r1`
// => `a = qb+r`, with `|r|<|b|` and `a` and `r` have the same sign.

assert_ne!(bit_size, 0, "signed integer should have at least one bit");

// 2^{max_bit size-1}
let max_power_of_two = self.add_constant(power_of_two::<F>(bit_size - 1));
let zero = self.add_constant(F::zero());
let one = self.add_constant(F::one());

// Get the sign bit of rhs by computing rhs / max_power_of_two
let (rhs_leading, _) = self.euclidean_division_var(rhs, max_power_of_two, bit_size, one)?;

// Get the sign bit of lhs by computing lhs / max_power_of_two
let (lhs_leading, _) = self.euclidean_division_var(lhs, max_power_of_two, bit_size, one)?;

// Signed to unsigned:
let unsigned_lhs = self.two_complement(lhs, lhs_leading, bit_size)?;
let unsigned_rhs = self.two_complement(rhs, rhs_leading, bit_size)?;

// Performs the division using the unsigned values of lhs and rhs
let (q1, r1) =
self.euclidean_division_var(unsigned_lhs, unsigned_rhs, bit_size, predicate)?;

// Unsigned to signed: derive q and r from q1,r1 and the signs of lhs and rhs
// Quotient sign is lhs sign * rhs sign, whose resulting sign bit is the XOR of the sign bits
let q_sign = self.xor_var(lhs_leading, rhs_leading, AcirType::unsigned(1))?;
let quotient = self.two_complement(q1, q_sign, bit_size)?;
let remainder = self.two_complement(r1, lhs_leading, bit_size)?;

// Issue #5129 - When q1 is zero and quotient sign is -1, we compute -0=2^{bit_size},
// which is not valid because we do not wrap integer operations
// Similar case can happen with the remainder.
let q_is_0 = self.eq_var(q1, zero)?;
let q_is_not_0 = self.not_var(q_is_0, AcirType::unsigned(1))?;
let quotient = self.mul_var(quotient, q_is_not_0)?;
let r_is_0 = self.eq_var(r1, zero)?;
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))?;

// This overflow check must also be under the predicate
let unsigned = self.mul_var(unsigned, predicate)?;

self.assert_neq_var(quotient, max_power_of_two, unsigned, Some(assert_message))?;

Ok((quotient, remainder))
}

/// Returns a variable which is constrained to be `lhs mod rhs`
pub(crate) fn modulo_var(
&mut self,
Expand All @@ -1190,8 +1098,8 @@ impl<F: AcirField> AcirContext<F> {
};

let (_, remainder_var) = match numeric_type {
NumericType::Signed { bit_size } => {
self.signed_division_var(lhs, rhs, bit_size, predicate)?
NumericType::Signed { .. } => {
unreachable!("Signed modulo should have been removed before ACIRgen")
}
_ => self.euclidean_division_var(lhs, rhs, bit_size, predicate)?,
};
Expand Down
27 changes: 0 additions & 27 deletions compiler/noirc_evaluator/src/acir/tests/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,33 +243,6 @@ fn derive_pedersen_generators_requires_constant_input() {
.expect_err("Should fail with assert constant");
}

#[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::<BTreeMap<_, _>>();
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(_), _)));
}

/// Convert the SSA input into ACIR and use ACVM to execute it
/// Returns the ACVM execution status and the value of the 'output' witness value,
/// unless the provided output is None or the ACVM fails during execution.
Expand Down
4 changes: 3 additions & 1 deletion compiler/noirc_evaluator/src/ssa/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,6 @@ pub struct ArtifactsAndWarnings(pub Artifacts, pub Vec<SsaReport>);
pub fn primary_passes(options: &SsaEvaluatorOptions) -> Vec<SsaPass<'_>> {
vec![
SsaPass::new(Ssa::expand_signed_checks, "expand signed checks"),
SsaPass::new(Ssa::expand_signed_math, "expand signed math"),
SsaPass::new(Ssa::remove_unreachable_functions, "Removing Unreachable Functions"),
SsaPass::new(Ssa::defunctionalize, "Defunctionalization"),
SsaPass::new_try(Ssa::inline_simple_functions, "Inlining simple functions")
Expand Down Expand Up @@ -175,6 +174,9 @@ pub fn primary_passes(options: &SsaEvaluatorOptions) -> Vec<SsaPass<'_>> {
SsaPass::new(Ssa::simplify_cfg, "Simplifying"),
SsaPass::new(Ssa::mem2reg, "Mem2Reg"),
SsaPass::new(Ssa::remove_bit_shifts, "Removing Bit Shifts"),
// Expand signed lt/div/mod after "Removing Bit Shifts" because that pass might
// introduce signed divisions.
SsaPass::new(Ssa::expand_signed_math, "Expand signed math"),
SsaPass::new(Ssa::simplify_cfg, "Simplifying"),
SsaPass::new(Ssa::flatten_cfg, "Flattening"),
// Run mem2reg once more with the flattened CFG to catch any remaining loads/stores
Expand Down
Loading
Loading