verify: Keep the state of a loop whose condition is the constant false

clang/lib/Verify/Frontend/ASTConverter.cpp

@@ -2977,17 +2977,41 @@ ASTConverter::convertLoopFootprints(const LoopContractInfo &LCI) {
   return Out;
 }
 
+/// A loop whose condition is the constant false never repeats its body.
+static bool neverRepeats(const Stmt *Loop, const ASTContext &Ctx) {
+  const Expr *Cond = nullptr;
+  if (const auto *W = dyn_cast<WhileStmt>(Loop))
+    Cond = W->getCond();
+  else if (const auto *D = dyn_cast<DoStmt>(Loop))
+    Cond = D->getCond();
+  else if (const auto *F = dyn_cast<ForStmt>(Loop))
+    Cond = F->getCond();
+  if (!Cond || Cond->isValueDependent())
+    return false;
+  std::optional<llvm::APSInt> Value = Cond->getIntegerConstantExpr(Ctx);
+  return Value && Value->isZero();
+}
+
+std::unique_ptr<VExpr> ASTConverter::convertLoopCondition(const Stmt *Loop,
+                                                          const Expr *Cond) {
+  if (neverRepeats(Loop, Ctx))
+    return std::make_unique<VLiteralExpr>(false, VType::makeBool(),
+                                          Cond->getExprLoc());
+  return convertExpr(Cond);
+}
+
 bool ASTConverter::checkLoopTermination(const Stmt *Loop, bool HasMeasure) {
   const LoopContractInfo *LCI = Ctx.getLoopContract(Loop);
   const bool MayDiverge = LCI && LCI->MayDiverge.isValid();
+  const bool Terminates = HasMeasure || neverRepeats(Loop, Ctx);
   if (InGhost || CurrentFn->IsProof) {
     if (MayDiverge) {
       Errors.push_back(CurrentFn->Name +
                        ": proof-only loops must terminate; "
                        "cppverify::decreases(*) is not allowed");
       return false;
     }
-    if (!HasMeasure) {
+    if (!Terminates) {
       Errors.push_back(CurrentFn->Name +
                        ": proof-only loops require a decreases clause");
       return false;
@@ -2997,7 +3021,7 @@ bool ASTConverter::checkLoopTermination(const Stmt *Loop, bool HasMeasure) {
   if (MayDiverge) {
     if (CurrentFn->DivergenceLoc.isInvalid())
       CurrentFn->DivergenceLoc = LCI->MayDiverge;
-  } else if (!HasMeasure && !CurrentFn->IsSpec &&
+  } else if (!Terminates && !CurrentFn->IsSpec &&
              CurrentFn->UnmeasuredLoop.isInvalid()) {
     CurrentFn->UnmeasuredLoop = Loop->getBeginLoc();
   }
@@ -6021,7 +6045,7 @@ ASTConverter::convertStmtBody(const Stmt *S) {
                        ": while condition declarations are unsupported");
       return Out;
     }
-    auto Cond = convertExpr(WS->getCond());
+    auto Cond = convertLoopCondition(WS, WS->getCond());
     if (!Cond)
       return Out;
     std::vector<std::unique_ptr<VExpr>> Invariants;
@@ -6069,7 +6093,7 @@ ASTConverter::convertStmtBody(const Stmt *S) {
     // observed. Preserve definite initialization from that mandatory pass.
     const std::set<std::string> AfterFirst = InitializedValues;
     const bool AfterFirstReachable = InitializationPathReachable;
-    auto Cond = convertExpr(DS->getCond());
+    auto Cond = convertLoopCondition(DS, DS->getCond());
     if (!Cond) {
       InitializedValues = Before;
       InitializationPathReachable = BeforeReachable;
@@ -6129,7 +6153,7 @@ ASTConverter::convertStmtBody(const Stmt *S) {
       leaveAutomaticScope(Out, FS->getEndLoc());
       return Out;
     }
-    auto Cond = convertExpr(FS->getCond());
+    auto Cond = convertLoopCondition(FS, FS->getCond());
     if (!Cond) {
       leaveAutomaticScope(Out, FS->getEndLoc());
       return Out;

clang/lib/Verify/Frontend/ASTConverter.h

@@ -103,6 +103,9 @@ class ASTConverter {
   /// Handled clear for anything else.
   std::unique_ptr<VExpr> convertCollection(const Expr *E, bool &Handled);
   bool checkLoopTermination(const Stmt *Loop, bool HasMeasure);
+  /// The condition of \p Loop: the constant false when it never repeats.
+  std::unique_ptr<VExpr> convertLoopCondition(const Stmt *Loop,
+                                              const Expr *Cond);
   bool isTriggerMarked(const Expr *E) const;
   void markTrigger(std::unique_ptr<VExpr> &Result, const Expr *E);
   /// A modifies footprint: an lvalue, or the cells p[lo : n].

clang/lib/Verify/Transform/Passivize.cpp

@@ -5583,6 +5583,10 @@ class PassivizerImpl {
       if (!W.Modifies.empty() && Modified.count(VHeapName))
         if (auto It = Renames.find(VHeapName); It != Renames.end())
           LoopEntryHeap = It->second;
+      // A loop whose condition is the constant false changes nothing.
+      std::unique_ptr<VExpr> Enters = isFalseLiteral(W.Cond.get())
+                                          ? makeBoolLiteral(false, W.Loc)
+                                          : cloneVExpr(Active.get());
       for (const std::string &Name : Modified) {
         auto Previous = Renames.find(Name);
         if (Previous == Renames.end())
@@ -5591,7 +5595,7 @@ class PassivizerImpl {
         const std::string HeadName = bump(Name);
         Renames[Name] = HeadName;
         emitInactiveFrame(P, PreviousName, HeadName, typeForName(Name),
-                          Active.get(), W.Loc);
+                          Enters.get(), W.Loc);
         if (Framed && Name == VHeapName) {
           const bool OnlyCells =
               !WriteRegions.empty() &&

clang/test/Verify/suite/loop_zero_iterations.cpp

@@ -0,0 +1,106 @@
+// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s
+// RUN: %cpp-verify --lower-only --dump-ir=2 %s -- 2>&1 | FileCheck %s --check-prefix=DUMP
+//
+// A loop whose condition is the constant false never repeats its body: it
+// needs no measure, and the state after it is the state before it.
+
+int wf(int x)
+  cppverify::pre(0 <= x && x <= 100)
+  cppverify::post(cppverify::result == x)
+{
+  int r = x;
+  while (false) {
+    r = r + 1;
+  }
+  return r;
+}
+// CHECK-DAG: Verified: wf [backend=z3]
+
+#define SWAP_INT(a, b) do { int t_ = (a); (a) = (b); (b) = t_; } while (0)
+
+int swapped_diff(int x, int y)
+  cppverify::pre(0 <= x && x <= 100 && 0 <= y && y <= 100)
+  cppverify::post(cppverify::result == y - x)
+{
+  int a = x;
+  int b = y;
+  SWAP_INT(a, b);
+  return a - b;
+}
+// CHECK-DAG: Verified: swapped_diff [backend=z3]
+
+int for_false(int x)
+  cppverify::pre(0 <= x && x <= 100)
+  cppverify::post(cppverify::result == x)
+{
+  int r = x;
+  for (int i = 0; false; i = i + 1)
+    r = r + i;
+  return r;
+}
+// CHECK-DAG: Verified: for_false [backend=z3]
+
+// Any other loop is described by its invariant, also where it does not run.
+int entry_false(int x)
+  cppverify::pre(0 <= x && x <= 100)
+  cppverify::post(cppverify::result == x + 5)
+{
+  int i = 5;
+  while (i < 3)
+    cppverify::decreases(3 - i)
+  {
+    i = i + 1;
+  }
+  return x + i;
+}
+// CHECK-DAG: error: verification failed: entry_false
+
+int runs_twice(int x)
+  cppverify::pre(0 <= x && x <= 100)
+  cppverify::post(cppverify::result == x + 2)
+{
+  int r = x;
+  int i = 0;
+  while (i < 2)
+    cppverify::decreases(2 - i)
+  {
+    r = r + 1;
+    i = i + 1;
+  }
+  return r;
+}
+// CHECK-DAG: error: verification failed: runs_twice
+
+// And a measure, when its condition is not the constant false.
+int unmeasured(int n)
+  cppverify::pre(0 <= n && n <= 100)
+  cppverify::post(cppverify::result == n)
+{
+  int i = 0;
+  while (i < n)
+    cppverify::invariant(0 <= i && i <= n)
+  {
+    i = i + 1;
+  }
+  return i;
+}
+// CHECK-DAG: Unresolved: unmeasured [backend=z3] [reason=decreases.missing]
+
+cppverify::proof int ghost_never(int n)
+  cppverify::pre(0 <= n && n <= 100)
+  cppverify::post(cppverify::result == n)
+{
+  int k = n;
+  while (false) {
+    k = k + 1;
+  }
+  return k;
+}
+// CHECK-DAG: Verified: ghost_never [backend=z3]
+
+// The variables the loop modifies keep their values.
+// DUMP-LABEL: passive wf
+// DUMP:      {{^ *}}false{{$}}
+// DUMP-NEXT: {{^ *}}=={{$}}
+// DUMP-NEXT: {{^ *}}r_2{{$}}
+// DUMP-NEXT: {{^ *}}r_1{{$}}

clang/test/Verify/suite/old_loop_invariant_definedness_fail.cpp

@@ -8,7 +8,7 @@ int reject_old_entry_overflow(int value)
   do {
     value = 0;
   } while (false)
-    cppverify::invariant(cppverify::old(value + 1) == cppverify::old(value + 1));
+    cppverify::invariant(cppverify::old((int)(value + 1)) == cppverify::old((int)(value + 1)));
   return value;
 }
 
@@ -19,7 +19,7 @@ int reject_quantified_old_entry_overflow(int value)
   do {
     value = 0;
   } while (false)
-    cppverify::invariant(cppverify::old(cppverify::forall(i, 0, 2, value + i == value + i)));
+    cppverify::invariant(cppverify::old(cppverify::forall(i, 0, 2, (int)(value + i) == (int)(value + i))));
   return value;
 }
 
@@ -34,7 +34,7 @@ int reject_old_entry_null_dereference(int *pointer, int *replacement)
   return 0;
 }
 
-// CHECK-DAG: error: verification failed: reject_old_entry_overflow
-// CHECK-DAG: error: verification failed: reject_quantified_old_entry_overflow
-// CHECK-DAG: error: verification failed: reject_old_entry_null_dereference
+// CHECK-DAG: error: verification failed: reject_old_entry_overflow [{{.*}}::overflow@
+// CHECK-DAG: error: verification failed: reject_quantified_old_entry_overflow [{{.*}}::overflow@
+// CHECK-DAG: error: verification failed: reject_old_entry_null_dereference [{{.*}}::dereference@
 

docs/ARCHITECTURE.md

@@ -397,7 +397,10 @@ at each `continue` (obligation kind `frame`, located at the footprint).
 
 **Termination.** An executable loop without `cppverify::decreases` contributes no
 measure obligation, and the driver reports the function `Unresolved` with
-`decreases.missing` unless BMC proved the unwinding. `cppverify::decreases(*)` marks the
+`decreases.missing` unless BMC proved the unwinding or the loop's condition is
+the constant false, so that it never repeats: the converter gives such a loop
+(`while (false)`, the `do { ... } while (0)` of a macro) the condition
+`false`, and its havoc keeps every value. `cppverify::decreases(*)` marks the
 function as possibly divergent: its proof, and the proof of every caller, is
 reported `[partial]`. Calls within an executable or proof recursion cycle
 assert the decrease of the shared measure at the call site.

docs/DESIGN.md

@@ -195,10 +195,14 @@ while (i < n)
 ```
 
 - `cppverify::invariant(expr)`: must hold on entry and be preserved by each iteration.
+  A loop whose condition is the constant false keeps every value it would
+  change: after `while (false) { ... }` the state is the one before it.
 - `cppverify::decreases(expr [, expr...])`: termination measure. Single expression must be non-negative and strictly decreasing. Tuple form is lex-ordered: `cppverify::decreases(a, b)` means `(a, b)` strictly decreases lexicographically, and only the first component that changes must stay non-negative.
 - Verification is total correctness, as in Verus: every executable loop needs
-  `cppverify::decreases`. Without one the function is `Unresolved` with reason
-  `decreases.missing`, unless BMC proves the loop's unwinding.
+  `cppverify::decreases`, unless its condition is the constant false, so that
+  it never repeats (`while (false)`, the `do { ... } while (0)` of a macro).
+  Without one the function is `Unresolved` with reason `decreases.missing`,
+  unless BMC proves the loop's unwinding.
   `cppverify::decreases(*)` on a loop or an executable function allows divergence; the
   proof then covers only executions that terminate, and that function and
   every caller are reported `Verified ... [partial]` with a warning (JSON
@@ -329,7 +333,8 @@ cppverify::ghost {
 - May assign only ghost-local variables and their direct dot-fields; executable
   locals, globals, pointees, executable calls, and enclosing-function returns
   are rejected.
-- Ghost loops require `cppverify::decreases`, because the loop is absent at runtime.
+- Ghost loops require `cppverify::decreases`, because the loop is absent at runtime,
+  unless their condition is the constant false.
 - Stripped entirely by CodeGen — zero runtime cost.
 - `cppverify::ghost T x = e;` declares a ghost variable in the enclosing function scope,
   like Verus's `let ghost`: later ghost code, assertions, and loop invariants

website/source/book/part-ii/ch12-loops-in-practice.rst

@@ -112,7 +112,9 @@ Every loop needs ``cppverify::decreases``
 -----------------------------------------
 
 Verification is total correctness, as in Verus. A loop without ``cppverify::decreases``
-leaves its function ``Unresolved`` with reason ``decreases.missing``. When a
+leaves its function ``Unresolved`` with reason ``decreases.missing``, unless
+its condition is the constant false (the ``do { ... } while (0)`` of a macro):
+such a loop never repeats. When a
 loop really may run forever (an event loop, a server), say so with
 ``cppverify::decreases(*)``: the function is then proved for the executions that
 terminate and reported ``Verified ... [partial]``, and so is every caller.

website/source/language/functions-loops.rst

@@ -220,11 +220,14 @@ obligations:
 
 Verification is total correctness, as in Verus: an executable loop without
 ``cppverify::decreases`` leaves its function ``Unresolved`` with reason
-``decreases.missing``. ``cppverify::decreases(*)`` allows a loop (or an executable
-function) to diverge; its function and every caller are then reported
-``Verified ... [partial]``, proved only for the executions that terminate.
-Ghost-block and proof-function loops are erased at runtime and must have a
-real measure; ``cppverify::decreases(*)`` is rejected there.
+``decreases.missing``, unless its condition is the constant false, so that it
+never repeats (``while (false)``, the ``do { ... } while (0)`` of a macro).
+Such a loop keeps the state it starts in. ``cppverify::decreases(*)`` allows a
+loop (or an executable function) to diverge; its function and every caller
+are then reported ``Verified ... [partial]``, proved only for the executions
+that terminate. Ghost-block and proof-function loops are erased at runtime and
+must have a real measure, unless their condition is the constant false;
+``cppverify::decreases(*)`` is rejected there.
 
 Nobody knows whether this loop ends for every start, so it has no measure:
 

website/source/language/limitations.rst

@@ -34,7 +34,8 @@ Meaning of a result
 ``Verified`` means the selected backend proved the generated verification
 condition. It does not certify uncontracted functions, linked libraries, the
 operating system, or any contract marked ``[[cppverify::trusted]]``. Proofs
-are of total correctness: every executable loop needs ``cppverify::decreases``. A proof
+are of total correctness: every executable loop needs ``cppverify::decreases``,
+unless its condition is the constant false. A proof
 that holds only for terminating executions (after ``cppverify::decreases(*)``) is marked
 ``[partial]``, one that relies on a trusted contract ``[trusts=f]``, and one
 that no execution reaches ``[vacuous]``. A caller whose proof relies on a