From 576cba36da935935716bb423569f05976a283645 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 9 Dec 2025 11:57:55 +0000
Subject: [PATCH] Fix segfault in k-induction step case with nested loops

The original code assumed loop_head->condition() always contained the
loop guard, but the loop head may not be a conditional goto instruction
(e.g., in nested loop scenarios). Fix by searching for the loop guard
in either the backedge or the forward goto at the loop head.

Also, processing a loop modifies the goto program (inserting
instructions and removing skips via remove_skip), which invalidates
iterators for nested loops. Only process outermost loops; inner loops
are handled as part of the outer loop body during unwinding.

Fixes: #5357

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 regression/k-induction/nested-loops/main.c    | 19 +++++
 regression/k-induction/nested-loops/test.desc | 11 +++
 src/goto-instrument/k_induction.cpp           | 75 ++++++++++++++++---
 3 files changed, 95 insertions(+), 10 deletions(-)
 create mode 100644 regression/k-induction/nested-loops/main.c
 create mode 100644 regression/k-induction/nested-loops/test.desc

diff --git a/regression/k-induction/nested-loops/main.c b/regression/k-induction/nested-loops/main.c
new file mode 100644
index 00000000000..1f0e1dbb26d
--- /dev/null
+++ b/regression/k-induction/nested-loops/main.c
@@ -0,0 +1,19 @@
+// Test case for nested loops in k-induction instrumentation.
+// This used to cause segmentation faults because the code incorrectly assumed
+// loop heads always have conditions and didn't handle nested loop iterator
+// invalidation.
+int main()
+{
+  unsigned i = 0;
+  unsigned j;
+  while(i < 2)
+  {
+    j = 0;
+    while(j < 2)
+    {
+      j++;
+    }
+    __CPROVER_assert(j == 2, "inner loop terminates at 2");
+    i++;
+  }
+}
diff --git a/regression/k-induction/nested-loops/test.desc b/regression/k-induction/nested-loops/test.desc
new file mode 100644
index 00000000000..d64f235d86d
--- /dev/null
+++ b/regression/k-induction/nested-loops/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+2
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting k-induction for k=2, base case$
+^Instrumenting k-induction for k=2, step case$
+^## Base case passes$
+^## Step case passes$
+--
+^warning: ignoring
diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp
index 05fcc37a6f1..e7f59fade94 100644
--- a/src/goto-instrument/k_induction.cpp
+++ b/src/goto-instrument/k_induction.cpp
@@ -11,11 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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"
@@ -55,24 +58,61 @@ class k_inductiont
 
   void k_induction();
 
+  static exprt find_loop_guard(
+    goto_programt::targett loop_head,
+    goto_programt::targett loop_exit,
+    const loopt &loop);
+
   void process_loop(
     const goto_programt::targett loop_head,
     const loopt &);
 };
 
+/// Find the loop guard expression. The 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
+exprt k_inductiont::find_loop_guard(
+  const goto_programt::targett loop_head,
+  const goto_programt::targett loop_exit,
+  const loopt &loop)
+{
+  // Find the backwards goto (backedge) for this loop
+  goto_programt::targett backedge;
+  bool found_backedge = false;
+  for(const auto &t : loop)
+  {
+    if(t->is_backwards_goto() && t->get_target() == loop_head)
+    {
+      backedge = t;
+      found_backedge = true;
+      break;
+    }
+  }
+
+  if(found_backedge && !backedge->condition().is_true())
+    return backedge->condition();
+
+  if(loop_head->is_goto())
+  {
+    if(loop_head->get_target() == loop_exit)
+      return boolean_negate(loop_head->condition());
+  }
+
+  return true_exprt();
+}
+
 void k_inductiont::process_loop(
   const goto_programt::targett loop_head,
   const loopt &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);
 
+  const exprt loop_guard = find_loop_guard(loop_head, loop_exit, loop);
+
   if(base_case)
   {
     // now unwind k times
@@ -157,12 +197,27 @@ void k_inductiont::process_loop(
 void k_inductiont::k_induction()
 {
   // iterate over the (natural) loops in the function
+  // Processing a loop modifies the goto program (inserting instructions and
+  // removing skips), which invalidates iterators in the natural_loops map for
+  // nested loops. We therefore only process outermost loops; inner loops are
+  // handled as part of the outer loop body during unwinding.
 
-  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);
+  for(const auto &[loop_head, loop] : natural_loops.loop_map)
+  {
+    bool is_nested = false;
+
+    for(const auto &[other_head, other_loop] : natural_loops.loop_map)
+    {
+      if(other_head != loop_head && other_loop.contains(loop_head))
+      {
+        is_nested = true;
+        break;
+      }
+    }
+
+    if(!is_nested)
+      process_loop(loop_head, loop);
+  }
 }
 
 void k_induction(