diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs index 592baec8a55..9ad9400bf41 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs @@ -457,8 +457,11 @@ impl Instruction { // `ArrayGet`s which read from "known good" indices from an array should not need a predicate. // This extra out of bounds (OOB) check is only inserted in the ACIR runtime. // Thus, in Brillig an `ArrayGet` is always a pure operation in isolation and - // it is expected that OOB checks are inserted separately. - dfg.runtime().is_acir() && !dfg.is_safe_index(*index, *array) + // it is expected that OOB checks are inserted separately. However, it would + // not be safe to separate the `ArrayGet` from the OOB constraints that precede it, + // because while it could read an array index, the returned data could be invalid, + // and fail at runtime if we tried using it in the wrong context. + !dfg.is_safe_index(*index, *array) } Instruction::EnableSideEffectsIf { .. } | Instruction::ArraySet { .. } => true, @@ -558,10 +561,13 @@ impl Instruction { // `ArrayGet`s which read from "known good" indices from an array have no side effects // This extra out of bounds (OOB) check is only inserted in the ACIR runtime. // Thus, in Brillig an `ArrayGet` is always a pure operation in isolation and - // it is expected that OOB checks are inserted separately. - ArrayGet { array, index, offset: _ } => { - dfg.runtime().is_acir() && !dfg.is_safe_index(*index, *array) - } + // it is expected that OOB checks are inserted separately. However, it would not + // be safe to separate the `ArrayGet` from its corresponding OOB constraints in Brillig, + // as a value read from an array at an invalid index could cause failures when subsequently + // used in the wrong context. Since we use this information to decide whether to hoist + // instructions during deduplication, we consider unsafe values as potentially having + // indirect side effects. + ArrayGet { array, index, offset: _ } => !dfg.is_safe_index(*index, *array), // ArraySet has side effects ArraySet { .. } => true, diff --git a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs index f39dffbd432..637ff06990b 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs @@ -876,7 +876,7 @@ fn can_be_hoisted(instruction: &Instruction, function: &Function) -> CanBeHoiste MakeArray { .. } => function.runtime().is_acir().into(), // These can have different behavior depending on the predicate. - Binary(_) | ArrayGet { .. } | ArraySet { .. } => { + Binary(_) | ArraySet { .. } | ArrayGet { .. } => { if !instruction.requires_acir_gen_predicate(&function.dfg) { Yes } else { @@ -2043,8 +2043,8 @@ mod test { #[test_case("u32", 0, 10, 0, true, "eq", 5, true, "loop empty, but eq is safe")] #[test_case("u32", 5, 10, 10, true, "shr", 1, true, "loop executes, shr ok")] #[test_case("u32", 5, 10, 0, true, "shr", 1, false, "loop empty, shr ok")] - #[test_case("u32", 5, 10, 10, true, "shr", 10, true, "shr overflow, and loop executes")] - #[test_case("u32", 5, 10, 0, true, "shr", 10, false, "shr overflow, but loop empty")] + #[test_case("u32", 5, 10, 10, true, "shr", 32, true, "shr overflow, and loop executes")] + #[test_case("u32", 5, 10, 0, true, "shr", 32, false, "shr overflow, but loop empty")] #[test_case("u32", 5, 10, 10, true, "shl", 1, true, "loop executes, shl ok")] #[test_case("u32", 5, 10, 0, true, "shl", 1, false, "loop empty, shl ok")] #[test_case("u32", 5, 10, 10, true, "shl", 32, true, "shl overflow, and loop executes")] @@ -2331,11 +2331,13 @@ mod control_dependence { assert_ssa_snapshot, ssa::{ interpreter::{errors::InterpreterError, tests::from_constant}, - ir::types::NumericType, + ir::{function::RuntimeType, types::NumericType}, opt::{assert_normalized_ssa_equals, assert_ssa_does_not_change, unrolling::Loops}, ssa_gen::Ssa, }, }; + use noirc_frontend::monomorphization::ast::InlineType; + use test_case::test_case; #[test] fn do_not_hoist_unsafe_mul_in_control_dependent_block() { @@ -3490,4 +3492,38 @@ mod control_dependence { let loop_ = loops.yet_to_unroll.pop().unwrap(); assert!(!loop_.is_fully_executed(&loops.cfg)); } + + #[test_case(RuntimeType::Brillig(InlineType::default()))] + #[test_case(RuntimeType::Acir(InlineType::default()))] + fn do_not_hoist_unsafe_array_get_from_control_dependent_block(runtime: RuntimeType) { + // We use an unknown index v0 to index an array, but only if v1 is true, + // so we should not hoist the constraint or the array_get into the header. + // Hoisting the array operation and indexing with an invalid `v0` would + // not cause an OOB in Brillig, however the returned value would be invalid, + // causing knockdown loop invariant instructions to fail when the loop is not meant to fail. + let src = format!( + r#" + {runtime} impure fn main f0 {{ + b0(v0: u32, v1: u1): + v2 = make_array [u8 0, u8 1] : [u8; 2] + jmp b1(u32 0) + b1(v3: u32): + v4 = lt v3, u32 2 + jmpif v4 then: b2, else: b3 + b2(): + jmpif v2 then: b4, else: b5 + b3(): + return + b4(): + constrain v0 == u32 0, "Index out of bounds" + v5 = array_get v2, index v0 -> u8 + jmp b5() + b5(): + v6 = unchecked_add v3, u32 1 + jmp b1(v6) + }} + "# + ); + assert_ssa_does_not_change(&src, Ssa::loop_invariant_code_motion); + } } diff --git a/test_programs/execution_success/regression_9804/Nargo.toml b/test_programs/execution_success/regression_9804/Nargo.toml new file mode 100644 index 00000000000..e967d011d16 --- /dev/null +++ b/test_programs/execution_success/regression_9804/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "regression_9804" +type = "bin" +authors = [""] + +[dependencies] \ No newline at end of file diff --git a/test_programs/execution_success/regression_9804/Prover.toml b/test_programs/execution_success/regression_9804/Prover.toml new file mode 100644 index 00000000000..1e0742d9467 --- /dev/null +++ b/test_programs/execution_success/regression_9804/Prover.toml @@ -0,0 +1,3 @@ +a = 10 +b = false +return = 0 diff --git a/test_programs/execution_success/regression_9804/src/main.nr b/test_programs/execution_success/regression_9804/src/main.nr new file mode 100644 index 00000000000..3a7d205bf6d --- /dev/null +++ b/test_programs/execution_success/regression_9804/src/main.nr @@ -0,0 +1,12 @@ +fn main(a: u32, b: bool) -> pub Field { + let mut s = 0; + let c = [[1, 2]]; + for _ in 0..2 { + if b { + let d = c[a]; + let e = d[0]; + s += e; + } + } + s +} diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_9804/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_9804/execute__tests__expanded.snap new file mode 100644 index 00000000000..4aa8433cd0e --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_9804/execute__tests__expanded.snap @@ -0,0 +1,16 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: expanded_code +--- +fn main(a: u32, b: bool) -> pub Field { + let mut s: Field = 0_Field; + let c: [[Field; 2]; 1] = [[1_Field, 2_Field]]; + for _ in 0_u32..2_u32 { + if b { + let d: [Field; 2] = c[a]; + let e: Field = d[0_u32]; + s = s + e; + } + } + s +} diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_9804/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_9804/execute__tests__stdout.snap new file mode 100644 index 00000000000..b351c7c655c --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_9804/execute__tests__stdout.snap @@ -0,0 +1,5 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: stdout +--- +[regression_9804] Circuit output: 0x00 diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_9805/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_9805/execute__tests__expanded.snap new file mode 100644 index 00000000000..f45cf77bb67 --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_9805/execute__tests__expanded.snap @@ -0,0 +1,14 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: expanded_code +--- +fn main(a: u32, b: bool) -> pub bool { + let c: [Field; 2] = [0_Field, 1_Field]; + for _ in 0_u32..2_u32 { + if b { + let d: Field = c[a]; + println(d); + } + } + true +} diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/regression_9805/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/regression_9805/execute__tests__stdout.snap new file mode 100644 index 00000000000..4f0b84214ab --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/regression_9805/execute__tests__stdout.snap @@ -0,0 +1,5 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: stdout +--- +[regression_9805] Circuit output: true