Skip to content

Commit ddca3b4

Browse files
authored
fix(ssa): conditionalise array indexes under IF statements (#1395)
* Condionalize also array access index * Adds regression test * Code review
1 parent d5571ad commit ddca3b4

File tree

7 files changed

+98
-15
lines changed

7 files changed

+98
-15
lines changed

crates/nargo_cli/tests/test_data/array_dynamic/Prover.toml

+3
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,8 @@ x = [104, 101, 108, 108, 111]
22
z = "59"
33
t = "10"
44
index = [0,1,2,3,4]
5+
index2 = [0,1,2,3,4]
6+
offset = 1
7+
sublen = 2
58

69

crates/nargo_cli/tests/test_data/array_dynamic/src/main.nr

+6-2
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,20 @@
11

2-
fn main(x: [u32; 5], mut z: u32, t: u32, index: [Field;5]) {
2+
fn main(x: [u32; 5], mut z: u32, t: u32, index: [Field;5], index2: [Field;5], offset: Field, sublen: Field) {
33
let idx = (z - 5*t - 5) as Field;
44
//dynamic array test
55
dyn_array(x, idx, idx - 3);
66

7-
// regression for issue 1283
7+
//regression for issue 1283
88
let mut s = 0;
99
let x3 = [246,159,32,176,8];
1010
for i in 0..5 {
1111
s += x3[index[i]];
1212
}
1313
assert(s!=0);
14+
15+
if 3 < (sublen as u32) {
16+
assert(index[offset + 3] == index2[3]);
17+
}
1418
}
1519

1620
fn dyn_array(mut x: [u32; 5], y: Field, z: Field) {

crates/noirc_evaluator/src/ssa/acir_gen/acir_mem.rs

+13-4
Original file line numberDiff line numberDiff line change
@@ -263,11 +263,20 @@ impl AcirMem {
263263
}
264264

265265
// Load array values into InternalVars
266-
// If create_witness is true, we create witnesses for values that do not have witness
267-
pub(super) fn load_array(&mut self, array: &MemArray) -> Vec<InternalVar> {
266+
pub(super) fn load_array(
267+
&mut self,
268+
array: &MemArray,
269+
evaluator: &mut Evaluator,
270+
) -> Vec<InternalVar> {
268271
vecmap(0..array.len, |offset| {
269-
self.load_array_element_constant_index(array, offset)
270-
.expect("infallible: array out of bounds error")
272+
operations::load::evaluate_with(
273+
array,
274+
&InternalVar::from(FieldElement::from(offset as i128)),
275+
self,
276+
None,
277+
evaluator,
278+
)
279+
.expect("infallible: array out of bounds error")
271280
})
272281
}
273282

crates/noirc_evaluator/src/ssa/acir_gen/operations/cmp.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -126,8 +126,8 @@ fn array_eq(
126126
// Fetch the elements in both `MemArrays`s, these are `InternalVar`s
127127
// We then convert these to `Expressions`
128128
let internal_var_to_expr = |internal_var: InternalVar| internal_var.expression().clone();
129-
let a_values = vecmap(memory_map.load_array(a), internal_var_to_expr);
130-
let b_values = vecmap(memory_map.load_array(b), internal_var_to_expr);
129+
let a_values = vecmap(memory_map.load_array(a, evaluator), internal_var_to_expr);
130+
let b_values = vecmap(memory_map.load_array(b, evaluator), internal_var_to_expr);
131131

132132
constraints::arrays_eq_predicate(&a_values, &b_values, evaluator)
133133
}

crates/noirc_evaluator/src/ssa/acir_gen/operations/load.rs

+15-5
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,14 @@ use crate::{
66
ssa::{
77
acir_gen::{acir_mem::AcirMem, internal_var_cache::InternalVarCache, InternalVar},
88
context::SsaContext,
9-
mem::{self, ArrayId},
9+
mem::{self, ArrayId, MemArray},
1010
node::NodeId,
1111
},
1212
Evaluator,
1313
};
1414

1515
// Returns a variable corresponding to the element at the provided index in the array
16-
// Returns None if index is constant and out-of-bound.
16+
// Returns an error if index is constant and out-of-bound.
1717
pub(crate) fn evaluate(
1818
array_id: ArrayId,
1919
index: NodeId,
@@ -25,11 +25,21 @@ pub(crate) fn evaluate(
2525
) -> Result<InternalVar, RuntimeError> {
2626
let mem_array = &ctx.mem[array_id];
2727
let index = var_cache.get_or_compute_internal_var_unwrap(index, evaluator, ctx);
28+
evaluate_with(mem_array, &index, acir_mem, location, evaluator)
29+
}
2830

31+
// Same as evaluate(), but using MemArray and InternalVar instead of ArrayId and NodeId
32+
pub(crate) fn evaluate_with(
33+
array: &MemArray,
34+
index: &InternalVar,
35+
acir_mem: &mut AcirMem,
36+
location: Option<Location>,
37+
evaluator: &mut Evaluator,
38+
) -> Result<InternalVar, RuntimeError> {
2939
if let Some(idx) = index.to_const() {
3040
let idx = mem::Memory::as_u32(idx);
3141
// Check to see if the index has gone out of bounds
32-
let array_length = mem_array.len;
42+
let array_length = array.len;
3343
if idx >= array_length {
3444
return Err(RuntimeError {
3545
location,
@@ -40,13 +50,13 @@ pub(crate) fn evaluate(
4050
});
4151
}
4252

43-
let array_element = acir_mem.load_array_element_constant_index(mem_array, idx);
53+
let array_element = acir_mem.load_array_element_constant_index(array, idx);
4454
if let Some(element) = array_element {
4555
return Ok(element);
4656
}
4757
}
4858

4959
let w = evaluator.add_witness_to_cs();
50-
acir_mem.add_to_trace(&array_id, index.to_expression(), w.into(), Expression::zero());
60+
acir_mem.add_to_trace(&array.id, index.to_expression(), w.into(), Expression::zero());
5161
Ok(InternalVar::from_witness(w))
5262
}

crates/noirc_evaluator/src/ssa/acir_gen/operations/return.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ pub(crate) fn evaluate(
3232
let objects = match Memory::deref(ctx, *node_id) {
3333
Some(a) => {
3434
let array = &ctx.mem[a];
35-
memory_map.load_array(array)
35+
memory_map.load_array(array, evaluator)
3636
}
3737
None => {
3838
vec![var_cache.get_or_compute_internal_var_unwrap(*node_id, evaluator, ctx)]

crates/noirc_evaluator/src/ssa/conditional.rs

+58-1
Original file line numberDiff line numberDiff line change
@@ -577,6 +577,36 @@ impl DecisionTree {
577577
DecisionTree::short_circuit(ctx, stack, ass_value, &error, *location)?;
578578
return Ok(false);
579579
}
580+
} else {
581+
// we use a 0 index when the predicate is false, to avoid out-of-bound issues
582+
let ass_value = Self::unwrap_predicate(ctx, &Some(ass_value));
583+
let op = Operation::Cast(ass_value);
584+
let pred = ctx.add_instruction(Instruction::new(
585+
op,
586+
ctx.object_type(*index),
587+
Some(stack.block),
588+
));
589+
stack.push(pred);
590+
let op = Operation::Binary(node::Binary {
591+
lhs: *index,
592+
rhs: pred,
593+
operator: BinaryOp::Mul,
594+
predicate: None,
595+
});
596+
let idx = ctx.add_instruction(Instruction::new(
597+
op,
598+
ObjectType::native_field(),
599+
Some(stack.block),
600+
));
601+
optimizations::simplify_id(ctx, idx).unwrap();
602+
stack.push(idx);
603+
604+
let ins2 = ctx.instruction_mut(ins_id);
605+
ins2.operation = Operation::Load {
606+
array_id: *array_id,
607+
index: idx,
608+
location: *location,
609+
};
580610
}
581611
stack.push(ins_id);
582612
}
@@ -651,10 +681,37 @@ impl DecisionTree {
651681
if !stack.is_new_array(ctx, array_id) && ctx.under_assumption(ass_value) {
652682
let pred =
653683
Self::and_conditions(Some(ass_value), *predicate, stack, ctx);
684+
// we use a 0 index when the predicate is false and index is not constant, to avoid out-of-bound issues
685+
let idx = if ctx.get_as_constant(*index).is_some() {
686+
*index
687+
} else {
688+
let op = Operation::Cast(Self::unwrap_predicate(ctx, &pred));
689+
690+
let cast = ctx.add_instruction(Instruction::new(
691+
op,
692+
ctx.object_type(*index),
693+
Some(stack.block),
694+
));
695+
stack.push(cast);
696+
let op = Operation::Binary(node::Binary {
697+
lhs: *index,
698+
rhs: cast,
699+
operator: BinaryOp::Mul,
700+
predicate: None,
701+
});
702+
let idx = ctx.add_instruction(Instruction::new(
703+
op,
704+
ObjectType::native_field(),
705+
Some(stack.block),
706+
));
707+
optimizations::simplify_id(ctx, idx).unwrap();
708+
stack.push(idx);
709+
idx
710+
};
654711
let ins2 = ctx.instruction_mut(ins_id);
655712
ins2.operation = Operation::Store {
656713
array_id: *array_id,
657-
index: *index,
714+
index: idx,
658715
value: *value,
659716
predicate: pred,
660717
location: *location,

0 commit comments

Comments
 (0)