E14: contracts of files verified apart, checked together

clang/include/clang/Frontend/FrontendOptions.h

@@ -525,6 +525,10 @@ class FrontendOptions {
   /// (in the format produced by -fdump-record-layouts).
   std::string OverrideRecordLayoutsFile;
 
+  /// Where CppVerify writes the contracts this file verifies and those it
+  /// assumes from other files, for cpp-verify --check-contracts.
+  std::string VerifyContractsOut;
+
   /// Auxiliary triple for CUDA/HIP/SYCL compilation.
   std::string AuxTriple;
 

clang/include/clang/Options/Options.td

@@ -2531,6 +2531,12 @@ defm verify_contracts : BoolFOption<"verify-contracts",
 // default once contracts are enabled, and -fno-verify turns compilation into a
 // syntax/semantics-only "light check". It implies -fverify-contracts (handled in
 // the driver) because it is meaningless without the contract language.
+def fverify_contracts_out_EQ : Joined<["-"], "fverify-contracts-out=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<file>">,
+  HelpText<"Write the contracts CppVerify verifies in this file and those it "
+           "assumes from other files, for cpp-verify --check-contracts">,
+  MarshallingInfoString<FrontendOpts<"VerifyContractsOut">>;
 def fno_verify : Flag<["-"], "fno-verify">, Group<f_clang_Group>,
   Visibility<[ClangOption, CC1Option]>,
   HelpText<"Check contract syntax and semantics but skip CppVerify SMT verification "

clang/lib/CodeGen/CodeGenAction.cpp

@@ -244,7 +244,8 @@ bool BackendConsumer::LinkInModules(llvm::Module *M) {
 void BackendConsumer::HandleTranslationUnit(ASTContext &C) {
   std::optional<std::future<verify::CppVerifyAsyncResult>> VerifyFuture;
   if (verify::shouldRunCppVerify(CI))
-    VerifyFuture = verify::startCppVerifyAsync(C);
+    VerifyFuture =
+        verify::startCppVerifyAsync(C, CI.getFrontendOpts().VerifyContractsOut);
 
   {
     llvm::TimeTraceScope TimeScope("Frontend");

clang/lib/Driver/ToolChains/Clang.cpp

@@ -6698,6 +6698,7 @@ void Clang::ConstructJob(Compilation &C, const JobAction &JA,
   // -fno-verify skips the SMT step. It is meaningless without the contract
   // language, so when neither -f/-fno-verify-contracts was given it implies
   // -fverify-contracts, yielding a syntax/semantics-only "light check".
+  Args.AddLastArg(CmdArgs, options::OPT_fverify_contracts_out_EQ);
   if (Args.hasArg(options::OPT_fno_verify)) {
     CmdArgs.push_back("-fno-verify");
     if (!Args.hasArg(options::OPT_fverify_contracts) &&

clang/lib/Verify/Backend/CVC5Backend.cpp

@@ -2727,6 +2727,7 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module,
   // One check may not spend the whole query.
   auto checkLimits = [&] {
     CertifyLimits Limits;
+    Limits.Times = times();
     Limits.Deadline = QueryDeadline;
     const unsigned CapMs = CertifyTimeoutMs ? *CertifyTimeoutMs : TimeoutMs / 2;
     if (CapMs > 0) {

clang/lib/Verify/Backend/Certify.cpp

@@ -3744,6 +3744,7 @@ CertifyResult verify::certifyCounterexample(const ObligationModule &Module,
                                             const LogicExpr &Query,
                                             CandidateModel &Model,
                                             const CertifyLimits &Limits) {
+  TimeInto Checking(Limits.Times ? &Limits.Times->Certification : nullptr);
   CertifyResult Result;
   auto Run = [&] {
     Evaluator Definitions(Module, Model, Limits, View::Definitions);

clang/lib/Verify/Backend/Certify.h

@@ -154,6 +154,8 @@ struct CertifyLimits {
   /// Set when Deadline is the time one counterexample check may take, not
   /// the query's: the message then says so.
   std::optional<unsigned> CheckTimeoutMs;
+  /// Where the checks' time is counted, for --time-report.
+  BackendTimes *Times = nullptr;
 };
 
 /// A logical application at concrete arguments whose model value differs from

clang/lib/Verify/Backend/Timing.h

@@ -0,0 +1,44 @@
+//===--- Timing.h - Where a function's verification spends its time -----===//
+#ifndef LLVM_CLANG_VERIFY_BACKEND_TIMING_H
+#define LLVM_CLANG_VERIFY_BACKEND_TIMING_H
+
+#include <atomic>
+#include <chrono>
+#include <cstdint>
+
+namespace clang {
+namespace verify {
+
+/// The time the backends of one function's verification spend, in
+/// nanoseconds: solving is the wall time in VerifyBackend::verify, induction
+/// the part of it spent on inductions, and certification the time of the
+/// counterexample checks, summed over checks that may run at once.
+struct BackendTimes {
+  std::atomic<uint64_t> Solving{0};
+  std::atomic<uint64_t> Induction{0};
+  std::atomic<uint64_t> Certification{0};
+};
+
+/// Adds the time from its construction to its destruction to a counter, if
+/// there is one.
+class TimeInto {
+  std::atomic<uint64_t> *Counter;
+  std::chrono::steady_clock::time_point Start;
+
+public:
+  explicit TimeInto(std::atomic<uint64_t> *Counter)
+      : Counter(Counter), Start(std::chrono::steady_clock::now()) {}
+  TimeInto(const TimeInto &) = delete;
+  TimeInto &operator=(const TimeInto &) = delete;
+  ~TimeInto() {
+    if (Counter)
+      Counter->fetch_add(std::chrono::duration_cast<std::chrono::nanoseconds>(
+                             std::chrono::steady_clock::now() - Start)
+                             .count());
+  }
+};
+
+} // namespace verify
+} // namespace clang
+
+#endif

clang/lib/Verify/Backend/VerifyBackend.cpp

@@ -59,6 +59,10 @@ class BMCVerifyBackend : public VerifyBackend {
                                              /*ReuseVerifiedQueries=*/true)),
         MaxUnrollBound(UnrollBound) {}
   llvm::StringRef getName() const override { return "bmc"; }
+  void setTimes(std::shared_ptr<BackendTimes> T) override {
+    Z3->setTimes(T);
+    VerifyBackend::setTimes(std::move(T));
+  }
   std::optional<unsigned>
   queryTimeoutMs(const ObligationModule &Module) const override {
     return Z3->queryTimeoutMs(Module);
@@ -232,6 +236,11 @@ class PortfolioVerifyBackend : public VerifyBackend {
         MaxQueryNodes(Execution.MaxQueryNodes) {}
 
   llvm::StringRef getName() const override { return "portfolio"; }
+  void setTimes(std::shared_ptr<BackendTimes> T) override {
+    Z3->setTimes(T);
+    CVC5->setTimes(T);
+    VerifyBackend::setTimes(std::move(T));
+  }
   std::optional<unsigned>
   queryTimeoutMs(const ObligationModule &Module) const override {
     return Z3->queryTimeoutMs(Module);
@@ -499,6 +508,7 @@ void verify::requestInterrupt() { InterruptFlag.store(true); }
 bool verify::interruptRequested() { return InterruptFlag.load(); }
 
 VerifyResult VerifyBackend::verify(const ObligationModule &Module) {
+  TimeInto Solving(Times ? &Times->Solving : nullptr);
   VerifyResult Result = verifyDirect(Module);
   if (Module.Attempt != ModuleAttempt::Primary ||
       Result.Status != VerifyStatus::Unresolved ||
@@ -522,6 +532,7 @@ VerifyResult VerifyBackend::verify(const ObligationModule &Module) {
   }
   setDeadline(Until);
   llvm::scope_exit Restore([&] { setDeadline(Saved); });
+  TimeInto Inducting(Times ? &Times->Induction : nullptr);
   std::vector<std::string> Tried;
   for (const InductionScheme &Scheme : inductionSchemes(Module)) {
     if (Until && std::chrono::steady_clock::now() >= *Until)
@@ -614,6 +625,9 @@ VerifyResult VerifyBackend::verifyDirect(const ObligationModule &Module) {
   VerifyResult Result = verifyModule(Module);
   if (Result.BackendName.empty())
     Result.BackendName = getName().str();
+  for (VerifyResult &More : Result.MoreFailures)
+    if (More.BackendName.empty())
+      More.BackendName = Result.BackendName;
   if (!Capabilities.ProducesVerificationVerdict &&
       Result.Status != VerifyStatus::Exported &&
       Result.Status != VerifyStatus::Unresolved) {
@@ -686,6 +700,11 @@ class RaceVerifyBackend : public VerifyBackend {
         MaxQueryNodes(Execution.MaxQueryNodes) {}
 
   llvm::StringRef getName() const override { return "race"; }
+  void setTimes(std::shared_ptr<BackendTimes> T) override {
+    Z3->setTimes(T);
+    CVC5->setTimes(T);
+    VerifyBackend::setTimes(std::move(T));
+  }
   std::optional<unsigned>
   queryTimeoutMs(const ObligationModule &Module) const override {
     return Z3->queryTimeoutMs(Module);

clang/lib/Verify/Backend/VerifyBackend.h

@@ -3,6 +3,7 @@
 #define LLVM_CLANG_VERIFY_BACKEND_VERIFYBACKEND_H
 
 #include "Obligation.h"
+#include "Timing.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/ThreadPool.h"
 #include <chrono>
@@ -146,6 +147,9 @@ struct VerifyResult {
   std::string Message;
   std::vector<VerifyModelValue> Model;
   std::vector<VerifyTraceEvent> Trace;
+  /// The failing obligations after this one, in order, each with its own
+  /// counterexample, as many as the run's MaxFailures allows.
+  std::vector<VerifyResult> MoreFailures;
   std::string ObligationId;
   std::optional<ObligationKind> ObligationType;
   /// For a certified counterexample: the value of every free variable of the
@@ -217,6 +221,10 @@ class VerifyBackend {
     FunctionDeadline = D;
     applyDeadline(D);
   }
+  /// Counts the time this backend spends into \p T, for --time-report.
+  virtual void setTimes(std::shared_ptr<BackendTimes> T) {
+    Times = std::move(T);
+  }
   /// Stops the work in progress, from any thread: queries running end
   /// unresolved and no further one starts, until resume().
   virtual void cancel() {}
@@ -232,9 +240,11 @@ class VerifyBackend {
   /// Limits the queries that start from now on to \p D.
   virtual void
   applyDeadline(std::optional<std::chrono::steady_clock::time_point> D) {}
+  BackendTimes *times() const { return Times.get(); }
 
 private:
   std::optional<std::chrono::steady_clock::time_point> FunctionDeadline;
+  std::shared_ptr<BackendTimes> Times;
 };
 
 /// Race: Z3 and cvc5 at once, the first proof or certified counterexample
@@ -287,6 +297,9 @@ struct BackendExecutionOptions {
   /// unresolved. Interactive fallback backends can consume those unresolved
   /// obligations without spending a second whole-module timeout budget.
   bool SkipWholeModuleRetry = false;
+  /// How many failing obligations of a module are reported, each with its
+  /// own counterexample; 0 reports every one.
+  unsigned MaxFailures = 1;
   /// Solve the whole-module query once, at the full budget, and report it:
   /// no per-obligation queries, refinement fallback, or induction. For small
   /// auxiliary questions such as the vacuity checks.