Fix segfault in k-induction step case with nested loops

regression/k-induction/nested-loops/main.c

@@ -0,0 +1,21 @@
+// Test case for nested loops in k-induction instrumentation
+// This used to cause segmentation faults in CBMC versions 5.6 and 5.12
+// when using --step-case because the code incorrectly assumed loop heads
+// always have conditions and didn't handle nested loop iterator invalidation
+int nondet_condition();
+int main()
+{
+  int i = 0;
+  int j = 0;
+  while(i < 10)
+  {
+    while(nondet_condition() == 0)
+    {
+      j++;
+      if(j == 10)
+        j = 0;
+    }
+    __CPROVER_assert(j < 11, "should hold");
+    i++;
+  }
+}

regression/k-induction/nested-loops/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+2
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting k-induction for k=2, base case$
+^Instrumenting k-induction for k=2, step case$
+--
+^warning: ignoring

src/goto-instrument/k_induction.cpp

@@ -11,11 +11,14 @@ Author: Daniel Kroening, [email protected]
 
 #include "k_induction.h"
 
-#include <analyses/natural_loops.h>
-#include <analyses/local_may_alias.h>
+#include <util/expr_util.h>
+#include <util/std_expr.h>
 
 #include <goto-programs/remove_skip.h>
 
+#include <analyses/local_may_alias.h>
+#include <analyses/natural_loops.h>
+
 #include "havoc_utils.h"
 #include "loop_utils.h"
 #include "unwind.h"
@@ -66,13 +69,44 @@ void k_inductiont::process_loop(
 {
   PRECONDITION(!loop.empty());
 
-  // save the loop guard
-  const exprt loop_guard = loop_head->condition();
-
   // compute the loop exit
   goto_programt::targett loop_exit=
     get_loop_exit(loop);
 
+  // Find the loop guard. The loop condition can be in one of two places:
+  // 1. In the backwards goto at the end of the loop (the backedge)
+  // 2. In a forward goto at the loop head that targets the loop exit
+
+  // Find the backwards goto (backedge) for this loop
+  goto_programt::targett backedge = loop_exit;
+  for(loopt::const_iterator it = loop.begin(); it != loop.end(); ++it)
+  {
+    if((*it)->is_backwards_goto() && (*it)->get_target() == loop_head)
+    {
+      backedge = *it;
+      break;
+    }
+  }
+
+  exprt loop_guard;
+
+  if(backedge != loop_exit && !backedge->condition().is_true())
+  {
+    // condition in backedge
+    loop_guard = backedge->condition();
+  }
+  else if(loop_head->is_goto())
+  {
+    if(loop_head->get_target() == loop_exit) // condition in forward edge
+      loop_guard = boolean_negate(loop_head->condition());
+    else
+      loop_guard = true_exprt(); // unconditional loop
+  }
+  else
+  {
+    loop_guard = true_exprt(); // unconditional loop
+  }
+
   if(base_case)
   {
     // now unwind k times
@@ -157,12 +191,52 @@ void k_inductiont::process_loop(
 void k_inductiont::k_induction()
 {
   // iterate over the (natural) loops in the function
+  // We need to be careful with nested loops, as processing the outer loop
+  // might invalidate iterators for the inner loop. So we collect all loops
+  // first, then process only outermost loops.
+
+  std::vector<std::pair<goto_programt::targett, loopt>> loops_to_process;
 
   for(natural_loops_mutablet::loop_mapt::const_iterator
       l_it=natural_loops.loop_map.begin();
       l_it!=natural_loops.loop_map.end();
       l_it++)
-    process_loop(l_it->first, l_it->second);
+  {
+    // Check if this loop is nested within another loop
+    bool is_nested = false;
+    goto_programt::targett loop_head = l_it->first;
+
+    for(natural_loops_mutablet::loop_mapt::const_iterator other_it =
+          natural_loops.loop_map.begin();
+        other_it != natural_loops.loop_map.end();
+        other_it++)
+    {
+      if(other_it == l_it)
+        continue; // skip self
+
+      // Check if loop_head is contained within other_it's loop
+      const loopt &other_loop = other_it->second;
+      if(
+        std::find(other_loop.begin(), other_loop.end(), loop_head) !=
+        other_loop.end())
+      {
+        is_nested = true;
+        break;
+      }
+    }
+
+    // Only process outermost loops to avoid iterator invalidation
+    if(!is_nested)
+    {
+      loops_to_process.push_back(std::make_pair(l_it->first, l_it->second));
+    }
+  }
+
+  // Now process the outermost loops
+  for(auto &loop_pair : loops_to_process)
+  {
+    process_loop(loop_pair.first, loop_pair.second);
+  }
 }
 
 void k_induction(