fix(ssa): Replace pop from 0-length slice with constraint and defaults

compiler/noirc_evaluator/src/ssa/ir/instruction.rs

@@ -391,9 +391,17 @@ impl Instruction {
             Instruction::Call { func, .. } => match dfg[*func] {
                 Value::Function(id) => !matches!(dfg.purity_of(id), Some(Purity::Pure)),
                 Value::Intrinsic(intrinsic) => {
-                    // These utilize `noirc_evaluator::acir::Context::get_flattened_index` internally
-                    // which uses the side effects predicate.
-                    matches!(intrinsic, Intrinsic::SliceInsert | Intrinsic::SliceRemove)
+                    match intrinsic {
+                        // These utilize `noirc_evaluator::acir::Context::get_flattened_index` internally
+                        // which uses the side effects predicate.
+                        Intrinsic::SliceInsert | Intrinsic::SliceRemove => true,
+                        // Technically these don't use the side effects predicate, but they fail on empty slices,
+                        // and by pretending that they require the predicate, we can preserve any current side
+                        // effect variable in the SSA and use it to optimize out memory operations that we know
+                        // would fail, but they shouldn't because they might be disabled.
+                        Intrinsic::SlicePopFront | Intrinsic::SlicePopBack => true,
+                        _ => false,
+                    }
                 }
                 _ => false,
             },

compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs

@@ -275,23 +275,23 @@ mod test {
     }
 
     #[test]
-    fn remove_enable_side_effects_for_slice_pop_back() {
+    fn keep_enable_side_effects_for_slice_pop_back() {
         let src = get_slice_intrinsic_src(
             "v13, v14, v15",
             &Intrinsic::SlicePopBack.to_string(),
             ") -> (u32, [Field], Field)",
         );
-        verify_all_enable_side_effects_removed(&src);
+        verify_ssa_unchanged(&src);
     }
 
     #[test]
-    fn remove_enable_side_effects_for_slice_pop_front() {
+    fn keep_enable_side_effects_for_slice_pop_front() {
         let src = get_slice_intrinsic_src(
             "v13, v14, v15",
             &Intrinsic::SlicePopFront.to_string(),
             ") -> (Field, u32, [Field])",
         );
-        verify_all_enable_side_effects_removed(&src);
+        verify_ssa_unchanged(&src);
     }
 
     #[test]

compiler/noirc_evaluator/src/ssa/opt/remove_unreachable_instructions.rs

@@ -17,11 +17,11 @@ use crate::ssa::{
         dfg::DataFlowGraph,
         function::{Function, FunctionId},
         instruction::{
-            Binary, BinaryOp, ConstrainError, Instruction, TerminatorInstruction,
+            Binary, BinaryOp, ConstrainError, Instruction, Intrinsic, TerminatorInstruction,
             binary::{BinaryEvaluationResult, eval_constant_binary_op},
         },
         types::{NumericType, Type},
-        value::ValueId,
+        value::{Value, ValueId},
     },
     opt::simple_optimization::SimpleOptimizationContext,
     ssa_gen::Ssa,
@@ -89,19 +89,17 @@ impl Function {
                 if !instruction.requires_acir_gen_predicate(context.dfg) {
                     return;
                 }
-                // Remove the current instruction and insert defaults for the results.
-                context.remove_current_instruction();
-
-                let result_ids = context.dfg.instruction_results(context.instruction_id).to_vec();
-
-                for result_id in result_ids {
-                    let typ = &context.dfg.type_of_value(result_id);
-                    let default_value = zeroed_value(context.dfg, func_id, block_id, typ);
-                    context.replace_value(result_id, default_value);
-                }
+                remove_and_replace_with_defaults(context, func_id, block_id);
                 return;
             }
 
+            // Check if the current predicate is known to be enabled.
+            let is_predicate_constant_one =
+                || match context.dfg.get_numeric_constant(side_effects_condition) {
+                    Some(predicate) => predicate.is_one(),
+                    None => false, // The predicate is a variable
+                };
+
             match instruction {
                 Instruction::Constrain(lhs, rhs, _) => {
                     let Some(lhs_constant) = context.dfg.get_numeric_constant(*lhs) else {
@@ -133,15 +131,8 @@ impl Function {
                         let requires_acir_gen_predicate =
                             binary.requires_acir_gen_predicate(context.dfg);
 
-                        // Check if the current predicate is known to be enabled.
-                        let is_predicate_constant_one =
-                            match context.dfg.get_numeric_constant(side_effects_condition) {
-                                Some(predicate) => predicate.is_one(),
-                                None => false, // The predicate is a variable
-                            };
-
                         let fails_under_predicate =
-                            requires_acir_gen_predicate && !is_predicate_constant_one;
+                            requires_acir_gen_predicate && !is_predicate_constant_one();
 
                         // Insert the instruction right away so we can add a constrain immediately after it
                         context.insert_current_instruction();
@@ -194,12 +185,7 @@ impl Function {
                     };
 
                     if array_op_always_fails {
-                        let is_predicate_constant_one =
-                            match context.dfg.get_numeric_constant(side_effects_condition) {
-                                Some(predicate) => predicate.is_one(),
-                                None => false, // The predicate is a variable
-                            };
-                        current_block_reachability = if is_predicate_constant_one {
+                        current_block_reachability = if is_predicate_constant_one() {
                             // If we have an array that contains references we no longer need to bother with resolution of those references.
                             // However, we want a trap to still be triggered by an OOB array access.
                             // Thus, we can replace our array with dummy numerics to avoid unnecessary allocations
@@ -244,6 +230,42 @@ impl Function {
                         };
                     }
                 }
+                // Intrinsic Slice operations in ACIR on empty arrays need to be replaced with a (conditional) constraint.
+                // In Brillig they will be protected by an access constraint, which, if known to fail, will make the block unreachable.
+                Instruction::Call { func, arguments } if context.dfg.runtime().is_acir() => {
+                    if let Value::Intrinsic(Intrinsic::SlicePopBack | Intrinsic::SlicePopFront) =
+                        &context.dfg[*func]
+                    {
+                        let length = arguments.iter().next().unwrap_or_else(|| {
+                            unreachable!("slice operations have 2 arguments: [length, slice]")
+                        });
+                        let is_empty =
+                            context.dfg.get_numeric_constant(*length).is_some_and(|v| v.is_zero());
+                        // If the compiler knows the slice is empty, there is no point trying to pop from it, we know it will fail.
+                        // Barretenberg doesn't handle memory operations with predicates, so we can't rely on those to disable the operation
+                        // based on the current side effect variable. Instead we need to replace it with a conditional constraint.
+                        if is_empty {
+                            let always_fail = is_predicate_constant_one();
+
+                            // We might think that if the predicate is constant 1, we can leave the pop as it will always fail.
+                            // However by turning the block Unreachable, ACIR-gen would create empty bytecode and not fail the circuit.
+                            insert_constraint(
+                                context,
+                                block_id,
+                                side_effects_condition,
+                                "Index out of bounds".to_string(),
+                            );
+
+                            current_block_reachability = if always_fail {
+                                context.remove_current_instruction();
+                                Reachability::Unreachable
+                            } else {
+                                remove_and_replace_with_defaults(context, func_id, block_id);
+                                Reachability::UnreachableUnderPredicate
+                            };
+                        }
+                    }
+                }
                 _ => (),
             };
 
@@ -344,6 +366,37 @@ fn zeroed_value(
     }
 }
 
+/// Remove the current instruction and replace it with default values.
+fn remove_and_replace_with_defaults(
+    context: &mut SimpleOptimizationContext<'_, '_>,
+    func_id: FunctionId,
+    block_id: BasicBlockId,
+) {
+    context.remove_current_instruction();
+
+    let result_ids = context.dfg.instruction_results(context.instruction_id).to_vec();
+
+    for result_id in result_ids {
+        let typ = &context.dfg.type_of_value(result_id);
+        let default_value = zeroed_value(context.dfg, func_id, block_id, typ);
+        context.replace_value(result_id, default_value);
+    }
+}
+
+/// Insert a `constrain 0 == <predicate>, "<msg>"` instruction.
+fn insert_constraint(
+    context: &mut SimpleOptimizationContext<'_, '_>,
+    block_id: BasicBlockId,
+    predicate: ValueId,
+    msg: String,
+) {
+    let zero = context.dfg.make_constant(0_u128.into(), NumericType::bool());
+    let message = Some(ConstrainError::StaticString(msg));
+    let instruction = Instruction::Constrain(zero, predicate, message);
+    let call_stack = context.dfg.get_instruction_call_stack_id(context.instruction_id);
+    context.dfg.insert_instruction_and_results(instruction, block_id, None, call_stack);
+}
+
 #[cfg(test)]
 mod test {
     use crate::{
@@ -871,11 +924,11 @@ mod test {
         let src = "
         acir(inline) predicate_pure fn main f0 {
           b0():
-            v0 = allocate -> &mut u8                      
-            store u8 0 at v0                               
+            v0 = allocate -> &mut u8
+            store u8 0 at v0
             v2 = make_array [u8 0, v0] : [(u8, &mut u8); 1]
-            v4 = array_get v2, index u32 2 -> u8         
-            v6 = array_get v2, index u32 3 -> &mut u8      
+            v4 = array_get v2, index u32 2 -> u8
+            v6 = array_get v2, index u32 3 -> &mut u8
             return v4
         }
         ";
@@ -904,11 +957,11 @@ mod test {
         let src = "
         brillig(inline) predicate_pure fn main f0 {
           b0():
-            v0 = allocate -> &mut u8                      
-            store u8 0 at v0                               
+            v0 = allocate -> &mut u8
+            store u8 0 at v0
             v2 = make_array [u8 0, v0] : [(u8, &mut u8); 1]
-            v4 = array_get v2, index u32 2 -> u8         
-            v6 = array_get v2, index u32 3 -> &mut u8      
+            v4 = array_get v2, index u32 2 -> u8
+            v6 = array_get v2, index u32 3 -> &mut u8
             return v4
         }
         ";
@@ -917,4 +970,57 @@ mod test {
         let ssa = ssa.remove_unreachable_instructions();
         assert_normalized_ssa_equals(ssa, src);
     }
+
+    #[test]
+    fn transforms_failing_slice_pop_with_constraint_and_default() {
+        let src = "
+        acir(inline) predicate_pure fn main f0 {
+          b0(v0: u1):
+            v1 = make_array [] : [u32]
+            enable_side_effects v0
+            v4, v5, v6 = call slice_pop_front(u32 0, v1) -> (u32, u32, [u32])
+            enable_side_effects u1 1
+            return u32 1
+        }
+        ";
+
+        let ssa = Ssa::from_str(src).unwrap();
+        let ssa = ssa.remove_unreachable_instructions();
+
+        assert_ssa_snapshot!(ssa, @r#"
+        acir(inline) predicate_pure fn main f0 {
+          b0(v0: u1):
+            v1 = make_array [] : [u32]
+            enable_side_effects v0
+            constrain u1 0 == v0, "Index out of bounds"
+            v3 = make_array [] : [u32]
+            enable_side_effects u1 1
+            return u32 1
+        }
+        "#);
+    }
+
+    #[test]
+    fn transforms_failing_slice_pop_if_always_enabled() {
+        let src = "
+        acir(inline) predicate_pure fn main f0 {
+          b0(v0: u1):
+            v1 = make_array [] : [u32]
+            v4, v5, v6 = call slice_pop_front(u32 0, v1) -> (u32, u32, [u32])
+            return v4
+        }
+        ";
+
+        let ssa = Ssa::from_str(src).unwrap();
+        let ssa = ssa.remove_unreachable_instructions();
+
+        assert_ssa_snapshot!(ssa, @r#"
+        acir(inline) predicate_pure fn main f0 {
+          b0(v0: u1):
+            v1 = make_array [] : [u32]
+            constrain u1 0 == u1 1, "Index out of bounds"
+            unreachable
+        }
+        "#);
+    }
 }

compiler/noirc_evaluator/src/ssa/ssa_gen/mod.rs

@@ -1081,16 +1081,19 @@ impl FunctionContext<'_> {
                 Intrinsic::SliceRemove => {
                     self.codegen_access_check(arguments[2], arguments[0]);
                 }
-                Intrinsic::SlicePopFront | Intrinsic::SlicePopBack => {
-                    // If the slice was empty, ACIR would fail appropriately as we check memory block sizes,
-                    // but for Brillig we need to lay down an explicit check. By doing this in the SSA we
-                    // might be able to optimize this away later.
-                    if self.builder.current_function.runtime().is_brillig() {
-                        let zero = self
-                            .builder
-                            .numeric_constant(0u32, NumericType::Unsigned { bit_size: 32 });
-                        self.codegen_access_check(zero, arguments[0]);
-                    }
+                Intrinsic::SlicePopFront | Intrinsic::SlicePopBack
+                    if self.builder.current_function.runtime().is_brillig() =>
+                {
+                    // We need to put in a constraint to protect against accessing empty slices:
+                    // * In Brillig this is essential, otherwise it would read an unrelated piece of memory.
+                    // * In ACIR we do have protection against reading empty slices (it returns "Index Out of Bounds"), so we don't get invalid reads.
+                    //   The memory operations in ACIR ignore the side effect variables, so even if we added a constraint here, it could still fail
+                    //   when it inevitably tries to read from an empty slice anyway. We have to handle that by removing operations which are known
+                    //   to fail and replace them with conditional constraints that do take the side effect into account.
+                    // By doing this in the SSA we might be able to optimize this away later.
+                    let zero =
+                        self.builder.numeric_constant(0u32, NumericType::Unsigned { bit_size: 32 });
+                    self.codegen_access_check(zero, arguments[0]);
                 }
                 _ => {
                     // Do nothing as the other intrinsics do not require checks

test_programs/execution_failure/regression_9489/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "regression_9489"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_failure/regression_9489/Prover.toml

@@ -0,0 +1 @@
+return = 1

test_programs/execution_failure/regression_9489/src/main.nr

@@ -0,0 +1,5 @@
+global G_A: [str<0>] = &[];
+fn main() -> pub bool {
+    let _ = G_A.pop_front().0;
+    true
+}

test_programs/execution_success/regression_9467/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "regression_9467"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_success/regression_9467/Prover.toml

@@ -0,0 +1,2 @@
+b = false
+return = [1, 2]

test_programs/execution_success/regression_9467/src/main.nr

@@ -0,0 +1,8 @@
+fn main(b: bool) -> pub (u32, u32) {
+    let s0: [u32] = &[];
+    let s1: [u32] = &[10];
+    let s2 = if b { s1 } else { s0 };
+    let i1 = if b { s0.pop_back().1 } else { 1 };
+    let i2 = if b { s2.pop_front().0 } else { 2 };
+    (i1, i2)
+}