H5: a ring buffer case study, and the four things it needed

README.md

@@ -157,17 +157,26 @@ and `docs/UB-CHECKING.md`.
 ./build/bin/cpp-verify --timeout=10000 --solver-rlimit=2000000 file.cpp
 ./build/bin/cpp-verify --int-encoding=bitvector file.cpp         # auto (default) | integer | bitvector
 ./build/bin/cpp-verify --diagnostics-format=json file.cpp        # JSON Lines, for editors/CI
+./build/bin/cpp-verify --diagnostics-format=sarif file.cpp       # SARIF 2.1.0, for code scanning
 ./build/bin/cpp-verify --obligation-out=goals.cpv file.cpp       # backend-neutral archive
 ./build/bin/cpp-verify --dump-ir=1,2,3,4 file.cpp                # VCR, passive, Obligation IR, Z3
+./build/bin/cpp-verify --dump-smt2=queries file.cpp              # each solver query as an SMT-LIB script
 ```
 
 Z3 runs support deterministic isolated solving (`--jobs`) and positive-proof reuse
 (`--proof-cache`). A query past `--timeout` or `--solver-rlimit` is reported as
 *unresolved* rather than hanging — never as verified. `--int-encoding` only chooses
 how machine integers reach the solver; every choice is exact, so it can change speed
-but never a verdict. A failure names the function and the obligation that failed,
-`<function identity>::<kind>@line:column`, e.g.
-`verification failed: abs [fn_5f5a3361627369::overflow@5:3]`.
+but never a verdict. A failure is a compiler error at the failing source, naming
+the function and the kind of check, with its counterexample and path as notes;
+without its precondition, `abs` gives:
+
+```text
+abs.cpp:4:3: error: verification failed: abs [overflow] [backend=z3] [reason=counterexample]
+    4 |   return x < 0 ? -x : x;
+      |   ^
+abs.cpp:4:3: note: counterexample: x = -2147483648
+```
 
 Chained modular calls (e.g. `return inc(inc(x))`) are lowered to temporaries automatically.
 See [Chapter 17](https://swayaminsync.github.io/cpp-verify/book/part-ii/ch17-backends-modular-calls.html).

clang/cmake/modules/CppVerifyZ3.cmake

@@ -85,7 +85,7 @@ function(cppverify_z3_build_external)
       -DCMAKE_INSTALL_PREFIX:PATH=${_install}
       -DCMAKE_POSITION_INDEPENDENT_CODE:BOOL=ON
       -DZ3_BUILD_LIBZ3_SHARED:BOOL=OFF
-      -DZ3_BUILD_EXECUTABLE:BOOL=OFF
+      -DZ3_BUILD_EXECUTABLE:BOOL=ON
       -DZ3_BUILD_TEST_EXECUTABLES:BOOL=OFF
       -DZ3_BUILD_DOCUMENTATION:BOOL=OFF
       -DZ3_ENABLE_EXAMPLE_TARGETS:BOOL=OFF
@@ -107,6 +107,9 @@ function(cppverify_z3_build_external)
   # sources include the headers must depend on this target as well.
   set_property(GLOBAL PROPERTY CPPVERIFY_Z3_EP_TARGET cppverify_z3_ep)
   set_property(GLOBAL PROPERTY CPPVERIFY_Z3_ORIGIN vendored)
+  # Z3's own shell, which replays the scripts --dump-smt2 writes in tests.
+  set_property(GLOBAL PROPERTY CPPVERIFY_Z3_SHELL
+    "${_install}/bin/z3${CMAKE_EXECUTABLE_SUFFIX}")
 endfunction()
 
 function(cppverify_z3_try_system out_var)
@@ -143,6 +146,11 @@ function(cppverify_z3_try_system out_var)
   if(_target)
     message(STATUS "CppVerify: using system Z3 (${_target})")
     set_property(GLOBAL PROPERTY CPPVERIFY_Z3_ORIGIN system)
+    find_program(CPPVERIFY_SYSTEM_Z3_SHELL z3)
+    if(CPPVERIFY_SYSTEM_Z3_SHELL)
+      set_property(GLOBAL PROPERTY CPPVERIFY_Z3_SHELL
+        "${CPPVERIFY_SYSTEM_Z3_SHELL}")
+    endif()
   endif()
   set(${out_var} "${_target}" PARENT_SCOPE)
 endfunction()

clang/include/clang/Basic/DiagnosticFrontendKinds.td

@@ -116,6 +116,10 @@ def err_fe_invalid_plugin_name : Error<
     "unable to find plugin '%0'">;
 def err_fe_cppverify_failed : Error<
     "cppverify: %0">;
+def err_cppverify_result : Error<"%0">;
+def warn_cppverify_result : Warning<"%0">, InGroup<CppVerify>;
+def remark_cppverify_result : Remark<"%0">, InGroup<CppVerify>;
+def note_cppverify_result : Note<"%0">;
 def err_fe_expected_compiler_job : Error<
     "unable to handle compilation, expected exactly one compiler job in '%0'">;
 def err_fe_expected_clang_command : Error<

clang/include/clang/Basic/DiagnosticGroups.td

@@ -1798,6 +1798,9 @@ Results can be filtered by function name by passing
 def : DiagGroup<"frame-larger-than=", [BackendFrameLargerThan]>;
 def BackendPlugin : DiagGroup<"backend-plugin">;
 def RemarkBackendPlugin : DiagGroup<"remark-backend-plugin">;
+// cpp-verify's results in a compilation: its warnings, and its proofs as
+// remarks.
+def CppVerify : DiagGroup<"cppverify">;
 def BackendOptimizationRemark : DiagGroup<"pass">;
 def BackendOptimizationRemarkMissed : DiagGroup<"pass-missed">;
 def BackendOptimizationRemarkAnalysis : DiagGroup<"pass-analysis">;

clang/include/clang/Basic/DiagnosticIDs.h

@@ -36,7 +36,7 @@ enum class Group;
 enum {
   DIAG_SIZE_COMMON = 300,
   DIAG_SIZE_DRIVER = 400,
-  DIAG_SIZE_FRONTEND = 200,
+  DIAG_SIZE_FRONTEND = 250,
   DIAG_SIZE_SERIALIZATION = 120,
   DIAG_SIZE_LEX = 500,
   DIAG_SIZE_PARSE = 800,

clang/lib/Parse/ParseCppVerify.cpp

@@ -1146,6 +1146,16 @@ StmtResult Parser::ParseContractAssert() {
       ContractAssertStmt(CALoc, LParenLoc, RParenLoc, Cond.get(), By);
 }
 
+/// \p Fn, the function a hide, reveal, or reveal_with_fuel names: a spec
+/// template specialization such as `at<4>` is an overload set until it is
+/// resolved to the one specialization it names.
+static ExprResult resolveNamedFunction(Sema &Actions, ExprResult Fn) {
+  if (Fn.isUsable() &&
+      Fn.get()->getType() == Actions.getASTContext().OverloadTy)
+    return Actions.CheckPlaceholderExpr(Fn.get());
+  return Fn;
+}
+
 /// Parse cppverify::reveal_with_fuel(fn, depth);
 StmtResult Parser::ParseRevealWithFuel() {
   SourceLocation Loc = ConsumeCppVerify();
@@ -1157,7 +1167,8 @@ StmtResult Parser::ParseRevealWithFuel() {
   }
   SourceLocation LParenLoc = ConsumeParen();
 
-  ExprResult Fn = finishCppVerifyExpression(ParseAssignmentExpression());
+  ExprResult Fn = resolveNamedFunction(
+      Actions, finishCppVerifyExpression(ParseAssignmentExpression()));
   if (Fn.isInvalid() || Tok.isNot(tok::comma)) {
     if (!Fn.isInvalid())
       Diag(Tok, diag::err_contract_expected_comma)
@@ -1193,7 +1204,8 @@ StmtResult Parser::ParseHideSpec() {
     return StmtError();
   }
   SourceLocation LParenLoc = ConsumeParen();
-  ExprResult Fn = finishCppVerifyExpression(ParseAssignmentExpression());
+  ExprResult Fn = resolveNamedFunction(
+      Actions, finishCppVerifyExpression(ParseAssignmentExpression()));
   if (Fn.isInvalid()) {
     SkipUntil(tok::r_paren, StopAtSemi);
     return StmtError();
@@ -1216,7 +1228,8 @@ StmtResult Parser::ParseRevealSpec() {
     return StmtError();
   }
   SourceLocation LParenLoc = ConsumeParen();
-  ExprResult Fn = finishCppVerifyExpression(ParseAssignmentExpression());
+  ExprResult Fn = resolveNamedFunction(
+      Actions, finishCppVerifyExpression(ParseAssignmentExpression()));
   if (Fn.isInvalid()) {
     SkipUntil(tok::r_paren, StopAtSemi);
     return StmtError();

clang/lib/Verify/Backend/CVC5Backend.cpp

@@ -4,6 +4,7 @@
 #include "ChildProcess.h"
 #include "ObligationSerialization.h"
 #include "ObligationSimplify.h"
+#include "QueryDump.h"
 #include "TaskGroup.h"
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/STLFunctionalExtras.h"
@@ -2406,6 +2407,18 @@ static bool printsSequencesReversed(const std::string &SolverPath) {
   return Reversed;
 }
 
+/// The options cvc5 runs with, as names and values; a flag has no value.
+static std::vector<std::pair<std::string, std::string>>
+cvc5Options(unsigned TimeoutMs, unsigned ResourceLimit) {
+  std::vector<std::pair<std::string, std::string>> Options = {
+      {"seed", "0"}, {"sat-random-seed", "0"}, {"dump-models", ""}};
+  if (TimeoutMs != 0)
+    Options.push_back({"tlimit-per", std::to_string(TimeoutMs)});
+  if (ResourceLimit != 0)
+    Options.push_back({"rlimit-per", std::to_string(ResourceLimit)});
+  return Options;
+}
+
 static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
                          unsigned TimeoutMs, unsigned ResourceLimit,
                          uint64_t MemoryLimitMB,
@@ -2452,12 +2465,9 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
   }
   llvm::FileRemover RemoveError(ErrorPath);
 
-  std::vector<std::string> OwnedArgs = {SolverPath, "--lang=smt2", "--seed=0",
-                                        "--sat-random-seed=0", "--dump-models"};
-  if (TimeoutMs != 0)
-    OwnedArgs.push_back("--tlimit-per=" + std::to_string(TimeoutMs));
-  if (ResourceLimit != 0)
-    OwnedArgs.push_back("--rlimit-per=" + std::to_string(ResourceLimit));
+  std::vector<std::string> OwnedArgs = {SolverPath, "--lang=smt2"};
+  for (const auto &[Name, Value] : cvc5Options(TimeoutMs, ResourceLimit))
+    OwnedArgs.push_back("--" + Name + (Value.empty() ? "" : "=" + Value));
   OwnedArgs.push_back(InputPath.str().str());
   llvm::SmallVector<llvm::StringRef, 8> Args;
   for (const std::string &Argument : OwnedArgs)
@@ -2777,8 +2787,21 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module,
       }
       Budget = static_cast<unsigned>(Remaining);
     }
+    QueryDump Dump;
+    if (queryDumpEnabled()) {
+      // The command line's options as commands, so that `cvc5 FILE` runs
+      // the query as cpp-verify did.
+      std::string Options;
+      for (const auto &[Name, Value] : cvc5Options(Budget, ResourceLimit))
+        Options += "(set-option :" + Name + " " +
+                   (Value.empty() ? "true" : Value) + ")\n";
+      Dump.start(&Module, Query, "cvc5", "at " + SolverPath, Options, *Script);
+    }
     SolverRun Run = runCVC5(SolverPath, *Script, Budget, ResourceLimit,
                             MemoryLimitMB, &Cancelled);
+    Dump.finish(
+        Run.Output ? llvm::StringRef(*Run.Output).split('\n').first.trim().str()
+                   : "no answer (" + Run.Failure.Message + ")");
     auto giveUp = [&](llvm::StringRef Outcome) {
       RefinementDecision Exhausted = Refinement.exhausted(Outcome);
       Result.Reason = Exhausted.Reason;
@@ -2809,6 +2832,8 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module,
           Result.Status = VerifyStatus::Failed;
           Result.Reason = VerifyReason::Counterexample;
           Result.CertifiedWith = std::move(Certified.Evidence);
+          describeCounterexample(Module, *Query, Candidate, Result,
+                                 checkLimits());
           return Result;
         }
       } else {
@@ -2876,6 +2901,8 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module,
       Result.Status = VerifyStatus::Failed;
       Result.Reason = VerifyReason::Counterexample;
       Result.CertifiedWith = Certified.Evidence;
+      describeCounterexample(Module, *Query, Candidate, Result,
+                             checkLimits());
       return Result;
     }
     if (Decision.Next == RefinementDecision::Action::Stop) {
@@ -2897,6 +2924,8 @@ VerifyResult CVC5VerifyBackend::verifyObligation(const ObligationModule &Module,
   Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId;
   Result.ObligationType = Item.Kind;
   Result.Location = Item.Loc;
+  Result.BeginLocation = Item.BeginLoc;
+  Result.EndLocation = Item.EndLoc;
   Result.Source = Item.Source;
   if (Result.Status == VerifyStatus::Unresolved)
     Result.Message = "proof obligation " + Result.ObligationId +

clang/lib/Verify/Backend/Certify.cpp

@@ -4187,15 +4187,79 @@ verify::candidateValues(const ObligationModule &Module, const LogicExpr &Query,
         It != Module.DiagnosticVariables.end() ? It->second.DisplayName : Name;
     Value.InternalName = Name;
     Value.Sort = Sort;
-    if (It != Module.DiagnosticVariables.end())
+    if (It != Module.DiagnosticVariables.end()) {
       Value.Source = It->second.Source;
+      Value.Reference = It->second.Reference;
+    }
     if (std::optional<LogicValue> Given = Model.constant(Name, Sort))
       Value.Value = formatLogicValue(*Given);
     Values.push_back(std::move(Value));
   }
   return Values;
 }
 
+void verify::describeCounterexample(const ObligationModule &Module,
+                                    const LogicExpr &Query,
+                                    CandidateModel &Model, VerifyResult &Result,
+                                    const CertifyLimits &Limits) {
+  auto evaluated = [&](const LogicExpr *Term) -> std::optional<LogicValue> {
+    if (!Term)
+      return std::nullopt;
+    return evaluateTerm(Module, *Term, Model, Limits);
+  };
+  auto truth = [&](const LogicExpr *Term) -> std::optional<bool> {
+    std::optional<LogicValue> Value = evaluated(Term);
+    if (!Value || Value->K != LogicValue::Kind::Bool)
+      return std::nullopt;
+    return Value->Truth;
+  };
+  const Obligation *Failing = nullptr;
+  for (const Obligation &Item : Module.Obligations)
+    if (Item.CounterexampleQuery.get() == &Query) {
+      Failing = &Item;
+      break;
+    }
+  if (Failing)
+    Result.Assignment = counterexampleAssignment(*Failing, Model);
+
+  // In the order Z3's models list them, by internal name.
+  Result.Model = candidateValues(Module, Query, Model);
+  llvm::sort(Result.Model,
+             [](const VerifyModelValue &A, const VerifyModelValue &B) {
+               return A.InternalName < B.InternalName;
+             });
+  for (VerifyModelValue &Value : Result.Model)
+    if (auto It = Module.DiagnosticVariables.find(Value.InternalName);
+        It != Module.DiagnosticVariables.end() && It->second.Guard)
+      Value.OnPath = truth(It->second.Guard.get());
+
+  Result.Trace.clear();
+  const uint64_t Count =
+      Failing ? std::min<uint64_t>(Failing->TraceEventCount,
+                                   Module.TraceEvents.size())
+              : 0;
+  for (uint64_t I = 0; I != Count; ++I) {
+    const DiagnosticTraceEvent &Event = Module.TraceEvents[I];
+    std::optional<bool> Active = truth(Event.Guard.get());
+    if (Active == false)
+      continue;
+    VerifyTraceEvent Step;
+    Step.Kind = Event.Kind;
+    Step.Message = Event.Message;
+    Step.Loc = Event.Loc;
+    Step.Source = Event.Source;
+    Step.Active = Active;
+    for (const DiagnosticTraceValue &Value : Event.Values) {
+      std::optional<LogicValue> Given = evaluated(Value.Value.get());
+      Step.Values.push_back(
+          {Value.Label, Value.Value->Sort,
+           Given ? std::optional<std::string>(formatLogicValue(*Given))
+                 : std::nullopt});
+    }
+    Result.Trace.push_back(std::move(Step));
+  }
+}
+
 std::string verify::shownApplication(const ObligationModule &Module,
                                      const LogicExpr &Application,
                                      CandidateModel &Model,

clang/lib/Verify/Backend/Certify.h

@@ -252,6 +252,16 @@ std::vector<VerifyModelValue> candidateValues(const ObligationModule &Module,
                                               const LogicExpr &Query,
                                               CandidateModel &Model);
 
+/// Describes in \p Result the counterexample \p Model gives \p Query, an
+/// obligation's counterexample query, as a failure shows it: the source
+/// variables' values, each version marked on the path or off it, and the
+/// steps of the obligation's path, each with its values. What the model
+/// leaves open stays undetermined.
+void describeCounterexample(const ObligationModule &Module,
+                            const LogicExpr &Query, CandidateModel &Model,
+                            VerifyResult &Result,
+                            const CertifyLimits &Limits = {});
+
 /// \p Application with its arguments' values under \p Model, as
 /// "fibo(1000000000)".
 std::string shownApplication(const ObligationModule &Module,

clang/lib/Verify/Backend/Induction.cpp

@@ -21,6 +21,7 @@ std::unique_ptr<LogicExpr> node(LogicExpr::Kind K, LogicSort Sort,
   Node->Sort = Sort;
   if (At) {
     Node->Loc = At->Loc;
+    Node->BeginLoc = At->BeginLoc;
     Node->EndLoc = At->EndLoc;
     Node->Source = At->Source;
   }
@@ -722,6 +723,7 @@ ObligationModule copyObligationModule(const ObligationModule &Module) {
     Same.StableId = Item.StableId;
     Same.Kind = Item.Kind;
     Same.Loc = Item.Loc;
+    Same.BeginLoc = Item.BeginLoc;
     Same.EndLoc = Item.EndLoc;
     Same.Source = Item.Source;
     Same.TraceEventCount = Item.TraceEventCount;