E5a: a summary line, --quiet, --verbose, and --list-functions

clang/include/clang/AST/ASTContext.h

@@ -155,6 +155,10 @@ struct LoopContractInfo {
   SourceLocation MayDiverge;
   /// The heap the loop may write, read in each iteration's state.
   SmallVector<Expr *, 2> Modifies;
+  /// A range-based for loop's position, cppverify::index, which its clauses
+  /// may name: an implicit variable, the number of elements before the
+  /// current one.
+  VarDecl *Index = nullptr;
 
   /// The clauses' expressions, as written.
   SmallVector<Stmt *, 8> children() const {

clang/include/clang/AST/ASTDumper.h

@@ -53,6 +53,7 @@ class ASTDumper : public ASTNodeTraverser<ASTDumper, TextNodeDumper> {
   void VisitWhileStmt(const WhileStmt *S);
   void VisitDoStmt(const DoStmt *S);
   void VisitForStmt(const ForStmt *S);
+  void VisitCXXForRangeStmt(const CXXForRangeStmt *S);
 };
 
 } // namespace clang

clang/include/clang/AST/RecursiveASTVisitor.h

@@ -2667,6 +2667,7 @@ DEF_TRAVERSE_STMT(ObjCForCollectionStmt, {})
 DEF_TRAVERSE_STMT(ObjCAutoreleasePoolStmt, {})
 
 DEF_TRAVERSE_STMT(CXXForRangeStmt, {
+  TRY_TO(TraverseLoopContract(S));
   if (!getDerived().shouldVisitImplicitCode()) {
     if (S->getInit())
       TRY_TO_TRAVERSE_OR_ENQUEUE_STMT(S->getInit());

clang/include/clang/Basic/CppVerifyConstructs.def

@@ -53,6 +53,7 @@ CPPVERIFY_CONSTRUCT(Exists, "exists", Expression)
 CPPVERIFY_CONSTRUCT(Choose, "choose", Expression)
 CPPVERIFY_CONSTRUCT(Old, "old", Expression)
 CPPVERIFY_CONSTRUCT(Result, "result", Expression)
+CPPVERIFY_CONSTRUCT(Index, "index", Expression)
 CPPVERIFY_CONSTRUCT(Trigger, "trigger", Expression)
 
 #undef CPPVERIFY_CONSTRUCT

clang/include/clang/Basic/DiagnosticParseKinds.td

@@ -1961,6 +1961,9 @@ def err_contract_redeclaration : Error<
   "contract clauses may only be specified on one declaration of a function">;
 def err_result_outside_postcondition : Error<
   "'cppverify::result' can only be used in postconditions">;
+def err_cppverify_index_outside_range_for : Error<
+  "'cppverify::index' is the position of a range-based for loop, in its "
+  "contract">;
 def err_result_in_old_expression : Error<
   "'cppverify::result' has no value in the function pre-state">;
 def err_old_outside_postcondition : Error<

clang/include/clang/Parse/Parser.h

@@ -7668,6 +7668,9 @@ class Parser : public CodeCompletionHandler {
   /// How many quantifier bodies enclose the current expression, where
   /// trigger(term) marks a pattern.
   unsigned QuantifierBodyDepth = 0;
+  /// The cppverify::index of the range-based for loop whose contract is
+  /// being parsed.
+  VarDecl *CppVerifyRangeIndex = nullptr;
   /// True while parsing the operand of old(...).
   bool InOldExpression = false;
 

clang/lib/AST/ASTDumper.cpp

@@ -252,6 +252,19 @@ void ASTDumper::VisitForStmt(const ForStmt *S) {
     Visit(D, "decreases");
 }
 
+void ASTDumper::VisitCXXForRangeStmt(const CXXForRangeStmt *S) {
+  ASTNodeTraverser::VisitCXXForRangeStmt(S);
+  if (!Ctx)
+    return;
+  const LoopContractInfo *LCI = Ctx->getLoopContract(S);
+  if (!LCI)
+    return;
+  for (const Expr *E : LCI->Invariants)
+    Visit(E, "invariant");
+  for (const Expr *D : LCI->Decreases)
+    Visit(D, "decreases");
+}
+
 //===----------------------------------------------------------------------===//
 // Type method implementations
 //===----------------------------------------------------------------------===//

clang/lib/AST/StmtPrinter.cpp

@@ -53,6 +53,7 @@
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Compiler.h"
 #include "llvm/Support/ErrorHandling.h"
+#include "llvm/Support/SaveAndRestore.h"
 #include "llvm/Support/raw_ostream.h"
 #include <cassert>
 #include <optional>
@@ -73,6 +74,8 @@ namespace {
     PrintingPolicy Policy;
     std::string NL;
     const ASTContext *Context;
+    /// The position of the range-based for loop whose clauses are printed.
+    const VarDecl *RangeIndex = nullptr;
 
   public:
     StmtPrinter(raw_ostream &os, PrinterHelper *helper,
@@ -490,6 +493,15 @@ void StmtPrinter::VisitCXXForRangeStmt(CXXForRangeStmt *Node) {
   OS << " : ";
   PrintExpr(Node->getRangeInit());
   OS << ")";
+  const LoopContractInfo *LCI =
+      Context ? Context->getLoopContract(Node) : nullptr;
+  {
+    llvm::SaveAndRestore<const VarDecl *> Index(RangeIndex,
+                                                LCI ? LCI->Index : nullptr);
+    printLoopContract(
+        OS, Context, Node, [&]() -> raw_ostream & { return Indent(1); },
+        [&](Expr *E) { PrintExpr(E); }, NL);
+  }
   PrintControlledStmt(Node->getBody());
 }
 
@@ -1481,6 +1493,10 @@ void StmtPrinter::VisitConstantExpr(ConstantExpr *Node) {
 
 void StmtPrinter::VisitDeclRefExpr(DeclRefExpr *Node) {
   ValueDecl *VD = Node->getDecl();
+  if (RangeIndex && VD == RangeIndex) {
+    OS << "cppverify::index";
+    return;
+  }
   if (const auto *OCED = dyn_cast<OMPCapturedExprDecl>(VD)) {
     OCED->getInit()->IgnoreImpCasts()->printPretty(OS, nullptr, Policy);
     return;

clang/lib/Headers/cppverify.h

@@ -128,6 +128,10 @@ enum __construct {
   /// The return value, in postconditions.
   result __attribute__((unavailable("cppverify::result is the return value "
                                     "in a postcondition"))),
+  /// In the contract of a range-based for loop: the number of elements
+  /// before the current one, from 0 to the size of the range.
+  index __attribute__((unavailable("cppverify::index is the position of a "
+                                   "range-based for loop in its contract"))),
   /// After a spec function returning bool: the least predicate its body
   /// defines, true exactly where a finite derivation shows it.
   inductive __attribute__((unavailable("cppverify::inductive follows a spec "

clang/lib/Parse/ParseCppVerify.cpp

@@ -1245,6 +1245,15 @@ ExprResult Parser::ParseCppVerifyExpression() {
     return ParseOldExpr();
   case CppVerifyConstruct::Result:
     return ParseResultExpr();
+  case CppVerifyConstruct::Index: {
+    const SourceLocation Loc = ConsumeCppVerify();
+    if (!CppVerifyRangeIndex) {
+      Diag(Loc, diag::err_cppverify_index_outside_range_for);
+      return ExprError();
+    }
+    return Actions.BuildDeclRefExpr(
+        CppVerifyRangeIndex, CppVerifyRangeIndex->getType(), VK_LValue, Loc);
+  }
   case CppVerifyConstruct::Trigger: {
     // trigger(term) in a quantifier body marks term as an instantiation
     // pattern.

clang/lib/Parse/ParseStmt.cpp

@@ -2309,10 +2309,24 @@ StmtResult Parser::ParseForStatement(SourceLocation *TrailingElseLoc,
   // Match the ')'.
   T.consumeClose();
 
-  // CppVerify: loop contract clauses before the body.
+  // CppVerify: loop contract clauses before the body. A range-based for
+  // loop's contract may name its position, cppverify::index.
   LoopContractInfo ForContract;
-  if (getLangOpts().VerifyContracts)
+  if (getLangOpts().VerifyContracts) {
+    VarDecl *RangeIndex = nullptr;
+    if (ForRangeInfo.ParsedForRangeDecl()) {
+      ASTContext &Ctx = Actions.getASTContext();
+      QualType IndexType = Ctx.getPointerDiffType();
+      RangeIndex = VarDecl::Create(
+          Ctx, Actions.getContractBinderContext(), ForLoc, ForLoc,
+          &Ctx.Idents.get("__cppverify_index"), IndexType,
+          Ctx.getTrivialTypeSourceInfo(IndexType, ForLoc), SC_None);
+      RangeIndex->setImplicit();
+    }
+    llvm::SaveAndRestore<VarDecl *> Index(CppVerifyRangeIndex, RangeIndex);
     ParseLoopContractClauses(ForContract);
+    ForContract.Index = RangeIndex;
+  }
 
   // C++ Coroutines [stmt.iter]:
   //   'co_await' can only be used for a range-based for statement.
@@ -2434,8 +2448,13 @@ StmtResult Parser::ParseForStatement(SourceLocation *TrailingElseLoc,
     return Actions.FinishCXXExpansionStmt(ForRangeStmt.get(), Body.get());
   }
 
-  if (ForRangeInfo.ParsedForRangeDecl())
-    return Actions.FinishCXXForRangeStmt(ForRangeStmt.get(), Body.get());
+  if (ForRangeInfo.ParsedForRangeDecl()) {
+    StmtResult RangeResult =
+        Actions.FinishCXXForRangeStmt(ForRangeStmt.get(), Body.get());
+    if (getLangOpts().VerifyContracts)
+      attachLoopContract(RangeResult, ForContract);
+    return RangeResult;
+  }
 
   StmtResult ForResult = Actions.ActOnForStmt(
       ForLoc, T.getOpenLocation(), FirstPart.get(), SecondPart, ThirdPart,

clang/lib/Sema/TreeTransform.h

@@ -9430,9 +9430,14 @@ TreeTransform<Derived>::TransformCXXForRangeStmt(CXXForRangeStmt *S) {
 
   SemaRef.OpenACC().ActOnForStmtEnd(S->getBeginLoc(), Body);
 
+  std::optional<LoopContractInfo> Contract;
+  bool ContractChanged = false;
+  if (getDerived().TransformLoopContract(S, Contract, ContractChanged))
+    return StmtError();
+
   // Body has changed but we didn't rebuild the for-range statement. Rebuild
   // it now so we have a new statement to attach the body to.
-  if (Body.get() != S->getBody() && NewStmt.get() == S) {
+  if ((Body.get() != S->getBody() || ContractChanged) && NewStmt.get() == S) {
     NewStmt = getDerived().RebuildCXXForRangeStmt(
         S->getForLoc(), S->getCoawaitLoc(), Init.get(), S->getColonLoc(),
         Range.get(), Begin.get(), End.get(), Cond.get(), Inc.get(),
@@ -9444,7 +9449,11 @@ TreeTransform<Derived>::TransformCXXForRangeStmt(CXXForRangeStmt *S) {
   if (NewStmt.get() == S)
     return S;
 
-  return FinishCXXForRangeStmt(NewStmt.get(), Body.get());
+  StmtResult Result = FinishCXXForRangeStmt(NewStmt.get(), Body.get());
+  if (Contract && Result.isUsable())
+    SemaRef.Context.getOrCreateLoopContract(Result.get()) =
+        std::move(*Contract);
+  return Result;
 }
 
 template <typename Derived>
@@ -18464,6 +18473,8 @@ VarDecl *TreeTransform<Derived>::TransformContractBinder(VarDecl *Binder) {
       SemaRef.Context, Context, Binder->getBeginLoc(),
       Binder->getLocation(), Binder->getIdentifier(), Binder->getType(),
       Binder->getTypeSourceInfo(), SC_None);
+  if (Binder->isImplicit())
+    New->setImplicit();
   getDerived().transformedLocalDecl(Binder, {New});
   return New;
 }
@@ -18588,6 +18599,9 @@ bool TreeTransform<Derived>::TransformLoopContract(
   if (!From)
     return false;
   To.emplace();
+  // A range-based for loop's cppverify::index is declared with its contract.
+  if (From->Index)
+    To->Index = getDerived().TransformContractBinder(From->Index);
   bool Invalid = false;
   auto Keep = [&](Expr *Old, ExprResult New, SmallVectorImpl<Expr *> &Out) {
     if (!New.isUsable()) {

clang/lib/Verify/Backend/Obligation.cpp

@@ -269,6 +269,8 @@ ObligationKind verify::obligationKind(ProofObligationKind Kind) {
     return ObligationKind::Deallocation;
   case ProofObligationKind::MissingReturn:
     return ObligationKind::MissingReturn;
+  case ProofObligationKind::Unreachable:
+    return ObligationKind::Unreachable;
   case ProofObligationKind::Unsupported:
     return ObligationKind::Unsupported;
   }
@@ -319,6 +321,8 @@ const char *verify::obligationKindName(ObligationKind Kind) {
     return "deallocation";
   case ObligationKind::MissingReturn:
     return "missing-return";
+  case ObligationKind::Unreachable:
+    return "unreachable";
   case ObligationKind::Unsupported:
     return "unsupported";
   }
@@ -2116,6 +2120,14 @@ class ObligationBuilder {
         N->Children.push_back(std::move(Rhs));
       return N;
     }
+    // Its requirement is checked where it is evaluated; its value is true.
+    case VExpr::Require: {
+      auto N = std::make_unique<VCExpr>(VCExpr::BoolLit);
+      setBoolSort(*N);
+      N->Loc = E->Loc;
+      N->BoolVal = true;
+      return N;
+    }
     }
     return fail("unsupported VCR expression kind " +
                 std::to_string(static_cast<unsigned>(E->K)));

clang/lib/Verify/Backend/Obligation.h

@@ -272,6 +272,7 @@ enum class ObligationKind {
   Frame,
   Deallocation,
   MissingReturn,
+  Unreachable,
   Unsupported
 };
 

clang/lib/Verify/Backend/ObligationSerialization.cpp

@@ -327,6 +327,8 @@ uint8_t obligationTag(ObligationKind Kind) {
     return 20;
   case ObligationKind::MissingReturn:
     return 21;
+  case ObligationKind::Unreachable:
+    return 23;
   case ObligationKind::Unsupported:
     return 22;
   }
@@ -382,6 +384,8 @@ std::optional<ObligationKind> obligationFromTag(uint8_t Tag, uint32_t Version) {
     return ObligationKind::MissingReturn;
   case 22:
     return ObligationKind::Unsupported;
+  case 23:
+    return ObligationKind::Unreachable;
   default:
     return std::nullopt;
   }

clang/lib/Verify/Driver/DumpIR.cpp

@@ -206,6 +206,15 @@ void verify::dumpVExpr(const VExpr *E, llvm::raw_ostream &OS, unsigned Depth) {
       dumpVExpr(O->Rhs.get(), OS, Depth + 1);
     break;
   }
+  case VExpr::Require: {
+    const auto *R = static_cast<const VRequireExpr *>(E);
+    OS << "require "
+       << obligationKindName(
+              obligationKind(static_cast<ProofObligationKind>(R->ProofKind)))
+       << "\n";
+    dumpVExpr(R->Cond.get(), OS, Depth + 1);
+    break;
+  }
   }
 }