fix(detect): model continue exits and memory stores in truncated loops

Two gaps in the loop-exit soundness rule from 6adcc24, both found in
review and reproduced as Proved always-conditions:

- `continue` was not an escape. The walkers drop an arm that ends in
  `continue` (it always leaves the iteration), so iterations that took it
  were never modeled, yet the unroll still counted as exact and the
  loop's variables were not havocked:
    for (i = 0; i < 2; i++) { if (y) continue; x++; }  if (x == 2)
  was "always true" although y != 0 gives x == 0. containsLoopEscape now
  treats a continue that targets the loop as an escape (a switch
  captures break but not continue; a nested loop captures both).

- Havocking a truncated loop reset scalar variables only. Array element
  and member stores from the partial unroll survived:
    for (i = 0; i < n && i < 4; i++) buf[i] = 1;  if (buf[0] == 1)
  was "always true" although n == 0 leaves buf[0] == 0. The unroll now
  records the base variables of array/member stores and replaces their
  arrays/values with fresh ones of the same sort; a store through a
  pointer havocs every tracked heap array (SymbolicEnv::havocHeapArrays)
  and marks the env over-approximated. The three walkers share this via
  LoopUnrollExits::havoc.

Tests (test_loop_exit_soundness): continue, local-array and heap-pointer
stores are no longer Proved by dead-branch, always-condition or
unreachable; the exact constant-bound loop stays Proved (negative
control). A pointer-mutating call inside the loop (review #9) did not
reproduce for unreachable; its case is kept as a regression guard.

include/fold/detect/loop_havoc.hpp

@@ -26,9 +26,9 @@ void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
 // access-path facts: after this, nothing about their post-loop values is known.
 void havocAssignedVars(SymbolicEnv& env, const std::vector<const clang::VarDecl*>& vars);
 
-// A `break` or `goto` in `body` that leaves the loop (a `break` inside a nested
+// A `break`, `continue` or `goto` in `body` that leaves the loop's iteration
-// loop or switch does not). Such an exit carries state the unroll never
+// (a `break` inside a nested loop or switch, or a `continue` inside a nested
-// follows.
+// loop, does not). Such an exit carries state the unroll never follows.
 [[nodiscard]] bool containsLoopEscape(const clang::Stmt* body);
 
 // Whether a bounded unroll saw every way out of a loop.
@@ -58,9 +58,16 @@ class LoopUnrollExits {
     // The unroll left the loop along its only exit.
     [[nodiscard]] bool exact() const { return exact_ && exited_; }
 
+    // Havoc the loop's post-state: assigned variables become unknown, and when
+    // the body stores through an array element, member or pointer, the env is
+    // marked over-approximated because that state is not havocked.
+    void havoc(SymbolicEnv& env, const std::vector<const clang::VarDecl*>& vars) const;
+
   private:
     bool exact_ = true;
     bool exited_ = false;
+    std::vector<const clang::VarDecl*> memory_bases_;
+    bool unknown_memory_write_ = false;
 };
 
 } // namespace fold::detect

include/fold/symbolic/encoder.hpp

@@ -131,6 +131,15 @@ class SymbolicEnv {
     void createHeapArray(const z3::expr& ptr, unsigned count, unsigned elem_size);
     std::optional<ArrayInfo> getHeapArray(const z3::expr& ptr) const;
     void updateHeapArray(const z3::expr& ptr, const z3::expr& new_array);
+    // Replace every tracked heap array with a fresh array of the same sort: a
+    // store through an unknown pointer may have written any of them.
+    void havocHeapArrays() {
+        static unsigned counter = 0;
+        for (auto& [_, info] : heap_arrays_) {
+            const std::string name = "heap_array_havoc_" + std::to_string(counter++);
+            info.array = ctx_->constant(name.c_str(), info.array.get_sort());
+        }
+    }
     void removeHeapArray(const z3::expr& ptr);
 
     std::optional<z3::expr> tryGetMember(const std::string& key) const {

src/detect/always_condition.cpp

@@ -330,7 +330,7 @@ class AlwaysConditionWalker {
         // is "the loop ran some prefix of iterations": keeping it would prove
         // post-loop conditions from a trip count the program need not take.
         if (opaque_loop || !exits.exact()) {
-            havocAssignedVars(env, assigned);
+            exits.havoc(env, assigned);
             env.restorePath(entry_path);
         }
         return true;

src/detect/dead_branch.cpp

@@ -354,7 +354,7 @@ class BodyWalker {
         // is "the loop ran some prefix of iterations": keeping it would prove
         // post-loop conditions from a trip count the program need not take.
         if (opaque_loop || !exits.exact()) {
-            havocAssignedVars(env, assigned);
+            exits.havoc(env, assigned);
             path = entry_path;
         }
         return true;

src/detect/loop_havoc.cpp

@@ -82,32 +82,141 @@ void havocAssignedVars(SymbolicEnv& env, const std::vector<const clang::VarDecl*
 namespace {
 
 // Walks a loop body tracking how many loops/switches enclose each statement,
-// so only a break that targets the loop being unrolled counts.
+// so only a break or continue that targets the loop being unrolled counts. A
-bool escapes(const clang::Stmt* stmt, int breakable_depth) {
+// switch captures `break` but not `continue`.
+bool escapes(const clang::Stmt* stmt, int breakable_depth, int loop_depth) {
     if (!stmt)
         return false;
     if (clang::isa<clang::GotoStmt>(stmt) || clang::isa<clang::IndirectGotoStmt>(stmt))
         return true;
     if (clang::isa<clang::BreakStmt>(stmt))
         return breakable_depth == 0;
-    const bool breakable = clang::isa<clang::ForStmt>(stmt) || clang::isa<clang::WhileStmt>(stmt) ||
+    // The walkers drop an arm that ends in `continue` (it always leaves the
-                           clang::isa<clang::DoStmt>(stmt) ||
+    // iteration), so the iterations that took it are never modeled.
-                           clang::isa<clang::CXXForRangeStmt>(stmt) ||
+    if (clang::isa<clang::ContinueStmt>(stmt))
-                           clang::isa<clang::SwitchStmt>(stmt);
+        return loop_depth == 0;
+    const bool loop = clang::isa<clang::ForStmt>(stmt) || clang::isa<clang::WhileStmt>(stmt) ||
+                      clang::isa<clang::DoStmt>(stmt) || clang::isa<clang::CXXForRangeStmt>(stmt);
+    const bool breakable = loop || clang::isa<clang::SwitchStmt>(stmt);
     for (const clang::Stmt* child : stmt->children()) {
-        if (escapes(child, breakable_depth + (breakable ? 1 : 0)))
+        if (escapes(child, breakable_depth + (breakable ? 1 : 0), loop_depth + (loop ? 1 : 0)))
             return true;
     }
     return false;
 }
 
+// Stores that do not go through a plain variable: an array element, a member,
+// or a dereferenced pointer. Havocking assigned variables does not reach that
+// state. When the store's base is a named variable (`buf[i] = ...`,
+// `s.f = ...`), that variable is reported so its whole value can be havocked;
+// a store through an unknown pointer is only flagged.
+struct MemoryWrites {
+    std::vector<const clang::VarDecl*> bases;
+    bool unknown_target = false;
+};
+
+MemoryWrites collectMemoryWrites(const clang::Stmt* stmt) {
+    struct Visitor : clang::RecursiveASTVisitor<Visitor> {
+        MemoryWrites writes;
+        std::unordered_set<const clang::VarDecl*> seen;
+
+        void record(const clang::Expr* target) {
+            target = target->IgnoreParenImpCasts();
+            const clang::Expr* base = nullptr;
+            if (const auto* sub = clang::dyn_cast<clang::ArraySubscriptExpr>(target))
+                base = sub->getBase();
+            else if (const auto* mem = clang::dyn_cast<clang::MemberExpr>(target))
+                base = mem->isArrow() ? nullptr : mem->getBase();
+            else if (const auto* un = clang::dyn_cast<clang::UnaryOperator>(target);
+                     un && un->getOpcode() == clang::UO_Deref) {
+                writes.unknown_target = true;
+                return;
+            } else if (const auto* arrow = clang::dyn_cast<clang::MemberExpr>(target);
+                       arrow && arrow->isArrow()) {
+                writes.unknown_target = true;
+                return;
+            } else {
+                return;
+            }
+            if (!base) {
+                writes.unknown_target = true;
+                return;
+            }
+            // Walk nested subscripts/members (`m[i][j]`, `a.b.c`) to the variable.
+            for (;;) {
+                base = base->IgnoreParenImpCasts();
+                if (const auto* sub = clang::dyn_cast<clang::ArraySubscriptExpr>(base)) {
+                    base = sub->getBase();
+                    continue;
+                }
+                if (const auto* mem = clang::dyn_cast<clang::MemberExpr>(base);
+                    mem && !mem->isArrow()) {
+                    base = mem->getBase();
+                    continue;
+                }
+                break;
+            }
+            const auto* dre = clang::dyn_cast<clang::DeclRefExpr>(base);
+            const auto* vd = dre ? clang::dyn_cast<clang::VarDecl>(dre->getDecl()) : nullptr;
+            // Subscripting a pointer variable writes through it, not into it.
+            if (!vd || vd->getType()->isPointerType()) {
+                writes.unknown_target = true;
+                return;
+            }
+            vd = vd->getCanonicalDecl();
+            if (seen.insert(vd).second)
+                writes.bases.push_back(vd);
+        }
+        bool VisitBinaryOperator(clang::BinaryOperator* op) {
+            if (op && op->isAssignmentOp())
+                record(op->getLHS());
+            return true;
+        }
+        bool VisitUnaryOperator(clang::UnaryOperator* op) {
+            if (op && op->isIncrementDecrementOp())
+                record(op->getSubExpr());
+            return true;
+        }
+    } visitor;
+    if (stmt)
+        visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
+    return visitor.writes;
+}
+
 } // namespace
 
-bool containsLoopEscape(const clang::Stmt* body) { return escapes(body, 0); }
+bool containsLoopEscape(const clang::Stmt* body) { return escapes(body, 0, 0); }
 
 LoopUnrollExits::LoopUnrollExits(const clang::Stmt* body) {
     if (containsLoopEscape(body))
         exact_ = false;
+    auto writes = collectMemoryWrites(body);
+    memory_bases_ = std::move(writes.bases);
+    unknown_memory_write_ = writes.unknown_target;
+}
+
+void LoopUnrollExits::havoc(SymbolicEnv& env,
+                            const std::vector<const clang::VarDecl*>& vars) const {
+    havocAssignedVars(env, vars);
+    // Array element and member stores from the truncated unroll would survive
+    // the scalar havoc: replace each written aggregate with a fresh value of
+    // its sort.
+    static unsigned counter = 0;
+    auto fresh = [&](const z3::sort& sort) {
+        const std::string name = "loop_memory_havoc_" + std::to_string(counter++);
+        return env.ctx().constant(name.c_str(), sort);
+    };
+    for (const clang::VarDecl* vd : memory_bases_) {
+        if (auto array = env.getArray(vd))
+            env.updateArray(vd, fresh(array->array.get_sort()));
+        else if (auto current = env.tryGet(vd))
+            env.replace(vd, fresh(current->get_sort()));
+    }
+    // A store through a pointer may have written any tracked heap array.
+    if (unknown_memory_write_) {
+        env.havocHeapArrays();
+        env.markOverApproximated("loop-truncated-memory-write");
+    }
 }
 
 bool LoopUnrollExits::guard(bool may_continue, bool may_exit) {

src/detect/unreachable.cpp

@@ -274,7 +274,7 @@ class UnreachableBodyWalker {
         }
         // The same loop-exit soundness rule as dead-branch / always-condition.
         if (!exits.exact()) {
-            detect::havocAssignedVars(env, assigned);
+            exits.havoc(env, assigned);
             path = entry_path;
         }
         return true;

tests/unit/test_loop_exit_soundness.cpp

@@ -177,3 +177,50 @@ TEST_CASE("loop exits: exact only when the unroll leaves along the only exit", "
         CHECK_FALSE(stopped.exact());
     }
 }
+
+// Review finding: a `continue` arm is dropped by the walkers (the arm always
+// exits the iteration), so iterations that took it are not modeled even when
+// the guard sequence is exact. `x == 2` holds only when y == 0.
+const std::string kContinueLoop =
+    "int c(int y) { int x = 0; for (int i = 0; i < 2; i++) { if (y) continue; x++; }"
+    "  if (x == 2) return 1; return 0; }\n";
+
+TEST_CASE("a loop with continue is not treated as an exact unroll", "[loop][continue]") {
+    CHECK(proved(runAlways(kContinueLoop)) == 0);
+    CHECK(proved(runDead(kContinueLoop)) == 0);
+    CHECK(proved(runUnreachable(kContinueLoop)) == 0);
+}
+
+// Review finding: a truncated unroll havocs scalar variables but kept array
+// element writes from the partial unroll. With n == 0, buf[0] is never set.
+const std::string kArrayWriteLoop = "int w(unsigned n) { int buf[4] = {0, 0, 0, 0};"
+                                    "  for (unsigned i = 0; i < n && i < 4; i++) buf[i] = 1;"
+                                    "  if (buf[0] == 1) return 1; return 0; }\n";
+
+// The same through a pointer: the store may have reached any heap array.
+const std::string kPointerWriteLoop =
+    "#include <cstdlib>\n"
+    "int pw(unsigned n) { int* buf = static_cast<int*>(std::calloc(4, sizeof(int)));"
+    "  if (!buf) return 0;"
+    "  for (unsigned i = 0; i < n && i < 4; i++) buf[i] = 1;"
+    "  int r = buf[0] == 1 ? 1 : 0; std::free(buf); return r; }\n";
+
+TEST_CASE("array writes in a truncated loop do not survive into proofs", "[loop][memory]") {
+    CHECK(proved(runAlways(kArrayWriteLoop)) == 0);
+    CHECK(proved(runDead(kArrayWriteLoop)) == 0);
+    CHECK(proved(runUnreachable(kArrayWriteLoop)) == 0);
+    CHECK(proved(runAlways(kPointerWriteLoop)) == 0);
+    CHECK(proved(runDead(kPointerWriteLoop)) == 0);
+}
+
+// Review finding: unreachable omitted the opaque-loop rule. A call can change
+// the loop variable through a pointer, which assigned-variable collection
+// does not see.
+const std::string kOpaqueCallLoop = "void advance(int* p);\n"
+                                    "int u() { int i = 0; while (i < 3) { advance(&i); i++; }"
+                                    "  if (i != 3) { int k = i * 2; return k; } return 0; }\n";
+
+TEST_CASE("unreachable havocs loops that contain calls", "[unreachable][loop][opaque]") {
+    CHECK(proved(runUnreachable(kOpaqueCallLoop)) == 0);
+    CHECK(proved(runDead(kOpaqueCallLoop)) == 0);
+}