Loops over local storage: an invariant's definedness at the head, and initialization kept across iterations

clang/include/clang/Basic/DiagnosticParseKinds.td

@@ -1991,9 +1991,5 @@ def warn_contract_template_unsupported : Warning<
   "contracts in %select{function|class}0 template %1 are not yet supported "
   "and are ignored">,
   InGroup<ContractUnsupported>;
-def warn_contract_member_function_unsupported : Warning<
-  "contracts on member functions are not yet supported and are ignored; "
-  "move the function out of the class or verify it as a free function">,
-  InGroup<ContractUnsupported>;
 
 } // end of Parser diagnostics

clang/include/clang/Parse/Parser.h

@@ -1311,6 +1311,12 @@ class Parser : public CodeCompletionHandler {
     /// The set of tokens that make up an exception-specification that
     /// has not yet been parsed.
     CachedTokens *ExceptionSpecTokens;
+
+    /// CppVerify: the contract clauses of the declarator, parsed in the
+    /// complete-class context as a function contract specifier is.
+    std::unique_ptr<CachedTokens> ContractTokens;
+    bool ContractIsSpec = false;
+    bool ContractIsProof = false;
   };
 
   /// LateParsedMemberInitializer - An initializer for a non-static class data
@@ -7592,6 +7598,14 @@ class Parser : public CodeCompletionHandler {
   bool isFunctionContractClause();
   void ParseFunctionContractClauses(ParsingDeclarator &D,
                                     FunctionContractClauses &Clauses);
+  /// The clauses at Tok, with the parameters and CurrentContractReturnType
+  /// already in place, and Clauses.Info.IsSpec and IsProof set.
+  void ParseFunctionContractClauseList(FunctionContractClauses &Clauses);
+  /// The clauses of an in-class member function declarator, cached for its
+  /// late-parsed declaration, where the class is complete.
+  std::unique_ptr<CachedTokens> MemberContractTokens;
+  bool MemberContractIsSpec = false;
+  bool MemberContractIsProof = false;
   void attachFunctionContract(Decl *Function, FunctionContractClauses &Clauses);
   /// A declaration ending in ';' after its clauses.
   Decl *

clang/lib/Parse/ParseCXXInlineMethods.cpp

@@ -566,6 +566,47 @@ void Parser::ParseLexedMethodDeclaration(LateParsedMethodDeclaration &LM) {
     LM.ExceptionSpecTokens = nullptr;
   }
 
+  // CppVerify: the contract clauses, with the parameters in scope and `this`
+  // as in the exception-specification.
+  if (std::unique_ptr<CachedTokens> Toks = std::move(LM.ContractTokens)) {
+    ParenBraceBracketBalancer BalancerRAIIObj(*this);
+    Token ContractEnd;
+    ContractEnd.startToken();
+    ContractEnd.setKind(tok::eof);
+    ContractEnd.setLocation(Toks->back().getEndLoc());
+    ContractEnd.setEofData(LM.Method);
+    Toks->push_back(ContractEnd);
+    Toks->push_back(Tok);
+    PP.EnterTokenStream(*Toks, true, /*IsReinject*/ true);
+    ConsumeAnyToken(/*ConsumeCodeCompletionTok=*/true);
+
+    FunctionDecl *Function = LM.Method->getAsFunction();
+    auto *Method = dyn_cast_or_null<CXXMethodDecl>(Function);
+    ParseScope FnScope(this, Scope::FnScope);
+    Sema::ContextRAII FnContext(Actions, Function, /*NewThisContext=*/false);
+    Sema::CXXThisScopeRAII ThisScope(
+        Actions, Method ? Method->getParent() : nullptr,
+        Method ? Method->getMethodQualifiers() : Qualifiers{},
+        Method && !Method->isStatic());
+
+    FunctionContractClauses Contract;
+    Contract.Info.IsSpec = LM.ContractIsSpec;
+    Contract.Info.IsProof = LM.ContractIsProof;
+    PendingClauseProofs.clear();
+    CurrentContractReturnType =
+        Function ? Function->getReturnType() : Actions.getASTContext().IntTy;
+    ParseFunctionContractClauseList(Contract);
+    if (Tok.isNot(tok::eof) || Tok.getEofData() != LM.Method)
+      Diag(Tok.getLocation(), diag::err_expected) << tok::semi;
+    attachFunctionContract(LM.Method, Contract);
+    PendingClauseProofs.clear();
+
+    while (Tok.isNot(tok::eof))
+      ConsumeAnyToken();
+    if (Tok.is(tok::eof) && Tok.getEofData() == LM.Method)
+      ConsumeAnyToken();
+  }
+
   InFunctionTemplateScope.Scopes.Exit();
 
   // Finish the delayed C++ method declaration.

clang/lib/Parse/ParseCppVerify.cpp

@@ -358,12 +358,19 @@ void Parser::ParseFunctionContractClauses(ParsingDeclarator &D,
     return;
 
   // Re-enter function parameters into scope so contract conditions can
-  // reference them. This mirrors ParseTrailingRequiresClause in
-  // ParseDeclCXX.cpp: create a FunctionPrototypeScope and push params.
+  // reference them. This mirrors ParseTrailingRequiresClauseWithScope in
+  // ParseDeclCXX.cpp: an out-of-line member's clauses are in its class's
+  // scope, with `this`, and a FunctionPrototypeScope holds the parameters.
+  CXXScopeSpec &SS = D.getCXXScopeSpec();
+  DeclaratorScopeObj DeclScopeObj(*this, SS);
+  if (SS.isValid() && Actions.ShouldEnterDeclaratorScope(getCurScope(), SS))
+    DeclScopeObj.EnterDeclaratorScope();
   ParseScope ContractParamScope(this, Scope::DeclScope |
                                           Scope::FunctionDeclarationScope |
                                           Scope::FunctionPrototypeScope);
   Actions.ActOnStartTrailingRequiresClause(getCurScope(), D);
+  std::optional<Sema::CXXThisScopeRAII> ThisScope;
+  InitCXXThisScopeForDeclaratorIfRelevant(D, D.getDeclSpec(), ThisScope);
 
   // Compute the return type from the full Declarator (not just the DeclSpec)
   // so that result in postconditions gets the correct type: pointers,
@@ -376,7 +383,13 @@ void Parser::ParseFunctionContractClauses(ParsingDeclarator &D,
     else
       CurrentContractReturnType = Actions.getASTContext().IntTy;
   }
+  ParseFunctionContractClauseList(Clauses);
+}
 
+void Parser::ParseFunctionContractClauseList(FunctionContractClauses &Clauses) {
+  FunctionContractInfo &I = Clauses.Info;
+  const bool IsSpecFn = I.IsSpec;
+  const bool IsProofFn = I.IsProof;
   llvm::SaveAndRestore<unsigned> ContextRAII(CppVerifyContextDepth,
                                              CppVerifyContextDepth + 1);
   // ACSL behaviors: pre and post clauses after behavior(name, assumes)
@@ -663,8 +676,14 @@ void Parser::attachFunctionContract(Decl *Result,
   // Templates are not verified yet: their clauses are ignored, as a member
   // function's are.
   if (FD->isTemplated() && !I.IsSpec && !I.IsProof) {
-    Diag(FD->getLocation(), diag::warn_contract_template_unsupported)
-        << 0 << FD;
+    // A member of a class template is named by its class.
+    const auto *Method = dyn_cast<CXXMethodDecl>(FD);
+    if (Method && Method->getParent()->isTemplated())
+      Diag(FD->getLocation(), diag::warn_contract_template_unsupported)
+          << 1 << Method->getParent();
+    else
+      Diag(FD->getLocation(), diag::warn_contract_template_unsupported)
+          << 0 << FD;
     return;
   }
   FunctionContractInfo &FCI = Ctx.getOrCreateFunctionContract(FD);

clang/lib/Parse/ParseDeclCXX.cpp

@@ -2364,6 +2364,10 @@ void Parser::HandleMemberFunctionDeclDelays(Declarator &DeclaratorInfo,
   // If there was a late-parsed exception-specification, we'll need a
   // late parse
   bool NeedLateParse = FTI.getExceptionSpecType() == EST_Unparsed;
+  // So do contract clauses (CppVerify).
+  std::unique_ptr<CachedTokens> ContractTokens =
+      std::move(MemberContractTokens);
+  NeedLateParse = NeedLateParse || ContractTokens;
 
   if (!NeedLateParse) {
     // Look ahead to see if there are any default args
@@ -2396,6 +2400,9 @@ void Parser::HandleMemberFunctionDeclDelays(Declarator &DeclaratorInfo,
       LateMethod->ExceptionSpecTokens = FTI.ExceptionSpecTokens;
       FTI.ExceptionSpecTokens = nullptr;
     }
+    LateMethod->ContractTokens = std::move(ContractTokens);
+    LateMethod->ContractIsSpec = MemberContractIsSpec;
+    LateMethod->ContractIsProof = MemberContractIsProof;
   }
 }
 
@@ -2980,19 +2987,27 @@ Parser::DeclGroupPtrTy Parser::ParseCXXClassMemberDeclaration(
     return nullptr;
   }
 
-  // CppVerify: contract clauses (pre/post/...) on in-class member functions are
-  // not yet modeled by the verifier, which handles free functions. Rather than
-  // emit a confusing "expected ';'", diagnose once and skip the clauses so the
-  // rest of the class still parses and the function is treated as uncontracted.
+  // CppVerify: the contract clauses of an in-class member function are parsed
+  // in the complete-class context, as a function contract specifier is (C++26
+  // [class.mem.general]), with the exception-specification and default
+  // arguments of its late-parsed declaration: their tokens are kept until
+  // then.
+  MemberContractTokens.reset();
   if (getLangOpts().VerifyContracts && DeclaratorInfo.isFunctionDeclarator() &&
       isFunctionContractClause()) {
-    Diag(Tok, diag::warn_contract_member_function_unsupported);
+    MemberContractTokens = std::make_unique<CachedTokens>();
+    MemberContractIsSpec =
+        DeclaratorInfo.getDeclSpec().isSpecFunctionSpecified();
+    MemberContractIsProof =
+        DeclaratorInfo.getDeclSpec().isProofFunctionSpecified();
     while (isFunctionContractClause()) {
+      MemberContractTokens->push_back(Tok);
       ConsumeCppVerify();
       if (Tok.is(tok::l_paren)) {
-        BalancedDelimiterTracker T(*this, tok::l_paren);
-        if (!T.consumeOpen())
-          T.skipToEnd();
+        MemberContractTokens->push_back(Tok);
+        ConsumeParen();
+        ConsumeAndStoreUntil(tok::r_paren, *MemberContractTokens,
+                             /*StopAtSemi=*/false, /*ConsumeFinalToken=*/true);
       }
     }
   }

clang/lib/Verify/Driver/Verifier.cpp

@@ -3081,13 +3081,33 @@ class Verifier {
         Converter.getUnverifiedCallers();
     for (const auto &[Loc, Message] : Converter.getWarnings())
       Diags.push_back({VerifyDiagnostic::Warning, Message, Loc});
+    // A construct the verifier does not represent costs its function alone:
+    // the function is Unresolved, its first error carrying the verdict, and
+    // the rest of the translation unit is verified. An error outside every
+    // function stops the run.
+    bool OutsideFunctions = false;
+    std::map<std::string, std::string> UnsupportedConstructs;
     for (const ConversionError &Err : Converter.getErrors()) {
       VerifyDiagnostic D{VerifyDiagnostic::Error, Err.Message,
                          Err.Range.getBegin()};
       D.Span = Err.Range;
+      if (Err.Function.empty())
+        OutsideFunctions = true;
+      else
+        D.FunctionName = Err.FunctionName;
+      if (!Err.Function.empty() &&
+          UnsupportedConstructs.emplace(Err.Function, Err.Message).second) {
+        VerifyResult R;
+        R.Status = VerifyStatus::Unresolved;
+        R.Reason = VerifyReason::UnsupportedConstruct;
+        R.Message = Err.Message;
+        D.Result = std::move(R);
+      }
       Diags.push_back(std::move(D));
     }
-    if (!Converter.getErrors().empty())
+    if (OutsideFunctions)
+      return false;
+    if (Functions.empty() && !UnsupportedConstructs.empty())
       return false;
     if (Functions.empty()) {
       if (Opts.LeanCertify) {
@@ -3213,7 +3233,7 @@ class Verifier {
     };
     const unsigned DumpLayers = Opts.DumpIRLayers;
     const bool MultiLayerDump = llvm::popcount(DumpLayers) > 1;
-    bool AllOk = true;
+    bool AllOk = UnsupportedConstructs.empty();
     bool AnyFailed = false;
     std::set<std::string> FailedCallers;
     // A spec whose termination is not established has no definition, so a
@@ -3562,12 +3582,35 @@ class Verifier {
         // which is reported only if it fails.
         if (Fn->Uninterpreted || (Fn->IsBuiltin && !Fn->NeedsDecreasesCheck))
           continue;
+        // What a function says depends on the definitions of the specs it
+        // reaches, so one that reaches a spec the verifier does not
+        // represent is not verified.
+        std::string ReliesOn;
+        for (const std::string &Spec : Fn->SpecDependencies)
+          if (auto It = FnMap.find(Spec);
+              It != FnMap.end() && It->second->UnsupportedConstruct)
+            ReliesOn += (ReliesOn.empty() ? "" : ", ") + It->second->Name;
+        if (!ReliesOn.empty()) {
+          AllOk = false;
+          VerifyResult R;
+          R.Status = VerifyStatus::Unresolved;
+          R.Reason = VerifyReason::UnsupportedConstruct;
+          R.Message = "relies on " + ReliesOn +
+                      ", which uses a construct the verifier does not support";
+          VerifyDiagnostic D{VerifyDiagnostic::Unresolved,
+                             Fn->Name + " [reason=construct.unsupported] (" +
+                                 R.Message + ")",
+                             Fn->DeclLoc, Fn->Name};
+          D.Result = std::move(R);
+          Diags.push_back(std::move(D));
+          continue;
+        }
         if (Fn->IsExternalContract) {
           if (Fn->IsTrusted)
             Diags.push_back({VerifyDiagnostic::Trusted,
                              Fn->Name + " (contract assumed, not verified)",
                              Fn->DeclLoc, Fn->Name});
-          else
+          else if (!Fn->UnsupportedConstruct)
             Diags.push_back(
                 {VerifyDiagnostic::Warning,
                  Fn->Name + " has a contract but no definition, so its callers "
@@ -4925,6 +4968,8 @@ class Verifier {
           auto Check = ContractChecks.find(Callee);
           if (Check != ContractChecks.end() && !settled(Check->second))
             Names += " (its clauses are not shown to be defined)";
+          else if (It != FnMap.end() && It->second->UnsupportedConstruct)
+            Names += " (it uses a construct the verifier does not support)";
           else if (It != FnMap.end() && It->second->IsExternalContract &&
                    !It->second->IsTrusted)
             Names += " (no definition; mark it [[cppverify::trusted]] to "
@@ -4959,9 +5004,12 @@ class Verifier {
             continue;
           // Definitions and frames of what the proof may reach;
           // postconditions and unfoldings where its module assumes them.
-          std::string Undefined, Unframed, Unproven, Unruled;
+          std::string Unsupported, Undefined, Unframed, Unproven, Unruled;
           for (const std::string &Identity : Reliance.Specs) {
-            if (UndefinedSpecs.count(Identity))
+            if (auto It = FnMap.find(Identity);
+                It != FnMap.end() && It->second->UnsupportedConstruct)
+              list(Unsupported, nameOf(Identity));
+            else if (UndefinedSpecs.count(Identity))
               list(Undefined, nameOf(Identity));
             else if (UnframedSpecs.count(Identity))
               list(Unframed, nameOf(Identity));
@@ -4978,7 +5026,12 @@ class Verifier {
           for (const std::string &Identity : Reliance.AssumedUnfoldings)
             if (Unproved.count(Identity) && !Reliance.Withheld.count(Identity))
               list(Unruled, nameOf(Identity));
-          if (!Undefined.empty())
+          if (!Unsupported.empty())
+            demote(Reliance.Index, VerifyReason::UnsupportedConstruct,
+                   "relies on " + Unsupported +
+                       ", which uses a construct the verifier does not "
+                       "support");
+          else if (!Undefined.empty())
             demote(Reliance.Index, VerifyReason::SpecTermination,
                    "relies on the definition of " + Undefined +
                        ", whose termination is not established");