diff --git a/compiler/noirc_evaluator/src/ssa/checks/check_for_missing_brillig_constraints.rs b/compiler/noirc_evaluator/src/ssa/checks/check_for_missing_brillig_constraints.rs index e89937e32fe..c5180c02b0e 100644 --- a/compiler/noirc_evaluator/src/ssa/checks/check_for_missing_brillig_constraints.rs +++ b/compiler/noirc_evaluator/src/ssa/checks/check_for_missing_brillig_constraints.rs @@ -47,6 +47,7 @@ use crate::ssa::ir::function::{Function, FunctionId}; use crate::ssa::ir::instruction::{Instruction, InstructionId, Intrinsic}; use crate::ssa::ir::value::{Value, ValueId}; use crate::ssa::ssa_gen::Ssa; +use crate::ssa::visit_once_deque::VisitOnceDeque; use noirc_artifacts::ssa::{InternalBug, SsaReport}; use noirc_errors::Location; use rayon::prelude::*; @@ -347,7 +348,12 @@ impl DependencyContext { return; } - let current_tainted = BrilligTaintedIds::new(function, arguments, results); + // Expand arguments through MakeArray chains so that + // array element values are also tracked as call arguments + // (e.g. for `v1 = make_array [v0]; call f(v1)`, track v0 too) + let expanded_args = expand_args_through_make_array(function, arguments); + + let current_tainted = BrilligTaintedIds::new(function, &expanded_args, results); // Record arguments/results for each Brillig call for the check. // @@ -366,7 +372,7 @@ impl DependencyContext { if !wrapped_call_found { // Record the current call, remember the argument values involved self.tainted.insert(*instruction, current_tainted); - arguments.iter().for_each(|value| { + expanded_args.iter().for_each(|value| { self.call_arguments.entry(*value).or_default().push(*instruction); }); } @@ -412,7 +418,10 @@ impl DependencyContext { // (fixes #10547) if matches!( &function.dfg[*instruction], - Instruction::Cast(..) | Instruction::Truncate { .. } + Instruction::Cast(..) + | Instruction::Truncate { .. } + | Instruction::MakeArray { .. } + | Instruction::ArraySet { .. } ) && let Some(tainted_ids) = self.tainted.get_mut(call) { tainted_ids.arguments.extend(&arguments); @@ -538,6 +547,7 @@ impl DependencyContext { self.update_children(&arguments, &results); } Instruction::ArraySet { .. } + | Instruction::MakeArray { .. } | Instruction::Binary(..) | Instruction::Cast(..) | Instruction::IfElse { .. } @@ -550,7 +560,6 @@ impl DependencyContext { Instruction::Allocate | Instruction::DecrementRc { .. } | Instruction::IncrementRc { .. } - | Instruction::MakeArray { .. } | Instruction::Noop => {} } } @@ -664,6 +673,38 @@ fn intersecting(a: &HashSet, b: &HashSet) -> bool { a.intersection(b).next().is_some() } +/// Expand a set of call arguments by tracing through MakeArray and ArraySet instructions. +/// For example, if arguments contains v1 where `v1 = make_array [v0]`, +/// the result will contain both v1 and v0. For `v2 = array_set v1, index .., value v3`, +/// the result will contain v2, v3, and (recursively) the contents of v1. +/// Works recursively for nested arrays and chained array_sets. +fn expand_args_through_make_array(function: &Function, arguments: &[ValueId]) -> Vec { + let mut queue = VisitOnceDeque::default(); + queue.extend(arguments.iter().copied()); + let mut expanded = Vec::new(); + while let Some(arg) = queue.pop_front() { + expanded.push(arg); + let Value::Instruction { instruction, .. } = &function.dfg[arg] else { continue }; + match &function.dfg[*instruction] { + Instruction::MakeArray { elements, .. } => { + let non_constant_elements = + elements.iter().copied().filter(|elem| !is_numeric_constant(function, *elem)); + queue.extend(non_constant_elements); + } + Instruction::ArraySet { array, value, .. } => { + // Trace the source array (may be another ArraySet or MakeArray) + queue.push_back(*array); + // Trace the inserted value (contributes to the array content) + if !is_numeric_constant(function, *value) { + queue.push_back(*value); + } + } + _ => {} + } + } + expanded +} + #[cfg(test)] mod tests { use crate::ssa::Ssa; @@ -1209,22 +1250,45 @@ mod tests { #[test] #[traced_test] - #[should_panic = "Expected no warnings but found some."] fn constrain_on_array_element_links_to_input_array() { // Regression test for https://github.com/noir-lang/noir/issues/11807 let program = r#" acir(inline) predicate_pure fn main f0 { b0(v0: Field): v1 = make_array [v0] : [Field; 1] - v3 = call f1(v1) -> [Field; 1] // We pass v1 = [v0] to the Brillig function. - v5 = array_get v3, index u32 0 -> Field - constrain v5 == v0 // We constrain the result directly against v0, which should clear the Brillig call. + v3 = call f1(v1) -> Field + constrain v3 == v0 return v3 } brillig(inline) predicate_pure fn helper_func f1 { b0(v0: [Field; 1]): - v2 = array_get v0, index u32 1 minus 1 -> Field - v3 = make_array [v2] : [Field; 1] + v2 = array_get v0, index u32 0 -> Field + return v2 + } + "#; + + let mut ssa = Ssa::from_str(program).unwrap(); + let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true); + assert_eq!(ssa_level_warnings.len(), 0, "Expected no warnings but found some."); + } + + #[test] + #[traced_test] + fn constrain_on_nested_array_element_links_to_input_array() { + // Nested array variant: [[Field; 1]; 1] wrapping v0 + let program = r#" + acir(inline) predicate_pure fn main f0 { + b0(v0: Field): + v1 = make_array [v0] : [Field; 1] + v2 = make_array [v1] : [[Field; 1]; 1] + v4 = call f1(v2) -> Field + constrain v4 == v0 + return v4 + } + brillig(inline) predicate_pure fn helper_func f1 { + b0(v0: [[Field; 1]; 1]): + v2 = array_get v0, index u32 0 -> [Field; 1] + v3 = array_get v2, index u32 0 -> Field return v3 } "#; @@ -1233,4 +1297,98 @@ mod tests { let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true); assert_eq!(ssa_level_warnings.len(), 0, "Expected no warnings but found some."); } + + #[test] + #[traced_test] + fn array_set_with_variable_index_constrain_against_set_value() { + // Array built from constants, then array_set with a non-constant index + // inserts v0. Brillig result constrained against v0. + let program = r#" + acir(inline) predicate_pure fn main f0 { + b0(v0: Field, v1: u32): + v2 = make_array [Field 0, Field 0] : [Field; 2] + v3 = array_set v2, index v1, value v0 + v4 = call f1(v3) -> Field + constrain v4 == v0 + return v4 + } + brillig(inline) predicate_pure fn helper_func f1 { + b0(v0: [Field; 2]): + v2 = array_get v0, index u32 0 -> Field + return v2 + } + "#; + + let mut ssa = Ssa::from_str(program).unwrap(); + let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true); + assert_eq!( + ssa_level_warnings.len(), + 0, + "Expected no warnings: array_set value should be tracked as a call argument." + ); + } + + #[test] + #[traced_test] + fn array_set_on_param_array_constrain_against_original_element() { + // make_array [v0, v1], then array_set at non-constant index with v0. + // Brillig result constrained against v0 (which is both in the original + // make_array AND the array_set value). + let program = r#" + acir(inline) predicate_pure fn main f0 { + b0(v0: Field, v1: Field, v2: u32): + v3 = make_array [v0, v1] : [Field; 2] + v4 = array_set v3, index v2, value v0 + v5 = call f1(v4) -> Field + constrain v5 == v0 + return v5 + } + brillig(inline) predicate_pure fn helper_func f1 { + b0(v0: [Field; 2]): + v2 = array_get v0, index u32 0 -> Field + return v2 + } + "#; + + let mut ssa = Ssa::from_str(program).unwrap(); + let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true); + assert_eq!( + ssa_level_warnings.len(), + 0, + "Expected no warnings: array_set on make_array with params, constrained against original element." + ); + } + + #[test] + #[traced_test] + fn array_set_constrain_result_array_elements() { + // Brillig returns an array. We array_get each element and constrain + // against the values used in the array_set. Since the Brillig call's + // result is an array, the checker uses array element tracking. + let program = r#" + acir(inline) predicate_pure fn main f0 { + b0(v0: Field, v1: Field, v2: u32): + v3 = make_array [v0, Field 0] : [Field; 2] + v4 = array_set v3, index v2, value v1 + v5 = call f1(v4) -> [Field; 2] + v6 = array_get v5, index u32 0 -> Field + v7 = array_get v5, index u32 1 -> Field + constrain v6 == v0 + constrain v7 == v1 + return + } + brillig(inline) predicate_pure fn helper_func f1 { + b0(v0: [Field; 2]): + return v0 + } + "#; + + let mut ssa = Ssa::from_str(program).unwrap(); + let ssa_level_warnings = ssa.check_for_missing_brillig_constraints(true); + assert_eq!( + ssa_level_warnings.len(), + 0, + "Expected no warnings: both array elements constrained against inputs." + ); + } }