Skip to content

Commit

Permalink
fix(ssa): conditionalise array indexes under IF statements (#1395)
Browse files Browse the repository at this point in the history
* Condionalize also array access index

* Adds regression test

* Code review
  • Loading branch information
guipublic authored and kevaundray committed Jun 6, 2023
1 parent 4e1560c commit b857f44
Show file tree
Hide file tree
Showing 7 changed files with 130 additions and 13 deletions.
9 changes: 9 additions & 0 deletions crates/nargo_cli/tests/test_data/array_dynamic/Prover.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
x = [104, 101, 108, 108, 111]
z = "59"
t = "10"
index = [0,1,2,3,4]
index2 = [0,1,2,3,4]
offset = 1
sublen = 2


32 changes: 32 additions & 0 deletions crates/nargo_cli/tests/test_data/array_dynamic/src/main.nr
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@

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

//regression for issue 1283
let mut s = 0;
let x3 = [246,159,32,176,8];
for i in 0..5 {
s += x3[index[i]];
}
assert(s!=0);

if 3 < (sublen as u32) {
assert(index[offset + 3] == index2[3]);
}
}

fn dyn_array(mut x: [u32; 5], y: Field, z: Field) {
assert(x[y] == 111);
assert(x[z] == 101);
x[z] = 0;
assert(x[y] == 111);
assert(x[1] == 0);
if y as u32 < 10 {
x[y] = x[y] - 2;
} else {
x[y] = 0;
}
assert(x[4] == 109);
}
17 changes: 13 additions & 4 deletions crates/noirc_evaluator/src/ssa/acir_gen/acir_mem.rs
Original file line number Diff line number Diff line change
Expand Up @@ -264,11 +264,20 @@ impl AcirMem {
}

// Load array values into InternalVars
// If create_witness is true, we create witnesses for values that do not have witness
pub(super) fn load_array(&mut self, array: &MemArray) -> Vec<InternalVar> {
pub(super) fn load_array(
&mut self,
array: &MemArray,
evaluator: &mut Evaluator,
) -> Vec<InternalVar> {
vecmap(0..array.len, |offset| {
self.load_array_element_constant_index(array, offset)
.expect("infallible: array out of bounds error")
operations::load::evaluate_with(
array,
&InternalVar::from(FieldElement::from(offset as i128)),
self,
None,
evaluator,
)
.expect("infallible: array out of bounds error")
})
}

Expand Down
4 changes: 2 additions & 2 deletions crates/noirc_evaluator/src/ssa/acir_gen/operations/cmp.rs
Original file line number Diff line number Diff line change
Expand Up @@ -126,8 +126,8 @@ fn array_eq(
// Fetch the elements in both `MemArrays`s, these are `InternalVar`s
// We then convert these to `Expressions`
let internal_var_to_expr = |internal_var: InternalVar| internal_var.expression().clone();
let a_values = vecmap(memory_map.load_array(a), internal_var_to_expr);
let b_values = vecmap(memory_map.load_array(b), internal_var_to_expr);
let a_values = vecmap(memory_map.load_array(a, evaluator), internal_var_to_expr);
let b_values = vecmap(memory_map.load_array(b, evaluator), internal_var_to_expr);

constraints::arrays_eq_predicate(&a_values, &b_values, evaluator)
}
20 changes: 15 additions & 5 deletions crates/noirc_evaluator/src/ssa/acir_gen/operations/load.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,14 @@ use crate::{
ssa::{
acir_gen::{acir_mem::AcirMem, internal_var_cache::InternalVarCache, InternalVar},
context::SsaContext,
mem::{self, ArrayId},
mem::{self, ArrayId, MemArray},
node::NodeId,
},
Evaluator,
};

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

// Same as evaluate(), but using MemArray and InternalVar instead of ArrayId and NodeId
pub(crate) fn evaluate_with(
array: &MemArray,
index: &InternalVar,
acir_mem: &mut AcirMem,
location: Option<Location>,
evaluator: &mut Evaluator,
) -> Result<InternalVar, RuntimeError> {
if let Some(idx) = index.to_const() {
let idx = mem::Memory::as_u32(idx);
// Check to see if the index has gone out of bounds
let array_length = mem_array.len;
let array_length = array.len;
if idx >= array_length {
return Err(RuntimeError {
location,
Expand All @@ -40,14 +50,14 @@ pub(crate) fn evaluate(
});
}

let array_element = acir_mem.load_array_element_constant_index(mem_array, idx);
let array_element = acir_mem.load_array_element_constant_index(array, idx);
if let Some(element) = array_element {
return Ok(element);
}
}

let w = evaluator.add_witness_to_cs();
acir_mem.add_to_trace(&array_id, index.to_expression(), w.into(), Expression::zero());
acir_mem.add_to_trace(&array.id, index.to_expression(), w.into(), Expression::zero());
Ok(InternalVar::from_witness(w))
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ pub(crate) fn evaluate(
let objects = match Memory::deref(ctx, *node_id) {
Some(a) => {
let array = &ctx.mem[a];
memory_map.load_array(array)
memory_map.load_array(array, evaluator)
}
None => {
vec![var_cache.get_or_compute_internal_var_unwrap(*node_id, evaluator, ctx)]
Expand Down
59 changes: 58 additions & 1 deletion crates/noirc_evaluator/src/ssa/conditional.rs
Original file line number Diff line number Diff line change
Expand Up @@ -577,6 +577,36 @@ impl DecisionTree {
DecisionTree::short_circuit(ctx, stack, ass_value, &error, *location)?;
return Ok(false);
}
} else {
// we use a 0 index when the predicate is false, to avoid out-of-bound issues
let ass_value = Self::unwrap_predicate(ctx, &Some(ass_value));
let op = Operation::Cast(ass_value);
let pred = ctx.add_instruction(Instruction::new(
op,
ctx.object_type(*index),
Some(stack.block),
));
stack.push(pred);
let op = Operation::Binary(node::Binary {
lhs: *index,
rhs: pred,
operator: BinaryOp::Mul,
predicate: None,
});
let idx = ctx.add_instruction(Instruction::new(
op,
ObjectType::native_field(),
Some(stack.block),
));
optimizations::simplify_id(ctx, idx).unwrap();
stack.push(idx);

let ins2 = ctx.instruction_mut(ins_id);
ins2.operation = Operation::Load {
array_id: *array_id,
index: idx,
location: *location,
};
}
stack.push(ins_id);
}
Expand Down Expand Up @@ -651,10 +681,37 @@ impl DecisionTree {
if !stack.is_new_array(ctx, array_id) && ctx.under_assumption(ass_value) {
let pred =
Self::and_conditions(Some(ass_value), *predicate, stack, ctx);
// we use a 0 index when the predicate is false and index is not constant, to avoid out-of-bound issues
let idx = if ctx.get_as_constant(*index).is_some() {
*index
} else {
let op = Operation::Cast(Self::unwrap_predicate(ctx, &pred));

let cast = ctx.add_instruction(Instruction::new(
op,
ctx.object_type(*index),
Some(stack.block),
));
stack.push(cast);
let op = Operation::Binary(node::Binary {
lhs: *index,
rhs: cast,
operator: BinaryOp::Mul,
predicate: None,
});
let idx = ctx.add_instruction(Instruction::new(
op,
ObjectType::native_field(),
Some(stack.block),
));
optimizations::simplify_id(ctx, idx).unwrap();
stack.push(idx);
idx
};
let ins2 = ctx.instruction_mut(ins_id);
ins2.operation = Operation::Store {
array_id: *array_id,
index: *index,
index: idx,
value: *value,
predicate: pred,
location: *location,
Expand Down

0 comments on commit b857f44

Please sign in to comment.