D6: cvc5 counterexamples in source terms, with their path

README.md

@@ -157,6 +157,7 @@ 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
 ```
@@ -165,9 +166,16 @@ Z3 runs support deterministic isolated solving (`--jobs`) and positive-proof reu
 (`--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/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/Verify/Backend/CVC5Backend.cpp

@@ -2809,6 +2809,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 +2878,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 +2901,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;

clang/lib/Verify/Backend/Obligation.cpp

@@ -558,6 +558,15 @@ static bool validateSource(const ObligationSource &Source, std::string &Error) {
     Error = "source range end precedes its start";
     return false;
   }
+  if ((Source.BeginLine == 0) != (Source.BeginColumn == 0)) {
+    Error = "source range has an incomplete begin";
+    return false;
+  }
+  if (Source.BeginLine > Source.Line ||
+      (Source.BeginLine == Source.Line && Source.BeginColumn > Source.Column)) {
+    Error = "source range begins after its anchor";
+    return false;
+  }
   return true;
 }
 
@@ -1960,8 +1969,10 @@ class ObligationBuilder {
 
   std::unique_ptr<VCExpr> fromVExpr(const VExpr *E) {
     auto Result = fromVExprImpl(E);
-    if (Result && E)
+    if (Result && E) {
+      Result->BeginLoc = E->BeginLoc;
       Result->EndLoc = E->EndLoc;
+    }
     return Result;
   }
 
@@ -2389,8 +2400,9 @@ class ObligationBuilder {
         fail("invalid diagnostic variable sort in obligation lowering");
         continue;
       }
-      M.DiagnosticVariables[InternalName] = {
-          Variable.DisplayName, Sort, Variable.Loc, Variable.EndLoc, {}};
+      DiagnosticVariable &Diagnostic = M.DiagnosticVariables[InternalName];
+      Diagnostic = {Variable.DisplayName, Sort, Variable.Loc, Variable.EndLoc};
+      Diagnostic.Reference = Variable.Reference;
     }
     auto traceKind = [](PassiveTraceKind Kind) {
       switch (Kind) {
@@ -2432,6 +2444,17 @@ class ObligationBuilder {
             {Value.Label, lowerDiagnosticExpr(Value.Value.get())});
       M.TraceEvents.push_back(std::move(Lowered));
     }
+    auto Everywhere = std::make_unique<VCExpr>(VCExpr::BoolLit);
+    setBoolSort(*Everywhere);
+    Everywhere->BoolVal = true;
+    const LogicExprRef OnEveryPath(std::move(Everywhere));
+    for (const auto &[InternalName, Variable] : P.ModelVariables)
+      if (auto It = M.DiagnosticVariables.find(InternalName);
+          It != M.DiagnosticVariables.end())
+        It->second.Guard =
+            Variable.Guard
+                ? LogicExprRef(lowerDiagnosticExpr(Variable.Guard.get()))
+                : OnEveryPath;
 
     std::vector<std::unique_ptr<VCExpr>> EntryAssumes;
     for (const auto &Entry : P.EntryAssumes)
@@ -2523,6 +2546,7 @@ class ObligationBuilder {
           ConditionWP->Premise = It->second.empty() ? "fact" : It->second;
       }
       ConditionWP->Loc = Condition->Loc;
+      ConditionWP->BeginLoc = Condition->BeginLoc;
       ConditionWP->EndLoc = Condition->EndLoc;
       return ConditionWP;
     };
@@ -2539,12 +2563,14 @@ class ObligationBuilder {
       Item.Kind = Kind;
       Item.Note = Note;
       Item.Loc = Condition->Loc;
+      Item.BeginLoc = Condition->BeginLoc;
       Item.EndLoc = Condition->EndLoc;
       Item.TraceEventCount = TraceEventCount;
       Item.Id = Identity + "::obligation:" + std::to_string(++ObligationIndex);
       Item.Goal = makeGoal(Condition);
       Item.CounterexampleQuery = vcNot(cloneLogicExpr(Item.Goal.get()));
       Item.CounterexampleQuery->Loc = Condition->Loc;
+      Item.CounterexampleQuery->BeginLoc = Condition->BeginLoc;
       Item.CounterexampleQuery->EndLoc = Condition->EndLoc;
       M.Obligations.push_back(std::move(Item));
     };
@@ -2612,6 +2638,9 @@ verify::validateObligationModule(const ObligationModule &M) {
     for (const DiagnosticTraceValue &Value : Event.Values)
       Roots.push_back(Value.Value.get());
   }
+  for (const auto &[InternalName, Variable] : M.DiagnosticVariables)
+    if (Variable.Guard)
+      Roots.push_back(Variable.Guard.get());
   Roots.push_back(M.CorrectnessGoal.get());
   Roots.push_back(M.CounterexampleQuery.get());
   for (const Obligation &Item : M.Obligations) {
@@ -2678,6 +2707,17 @@ verify::validateObligationModule(const ObligationModule &M) {
             llvm::inconvertibleErrorCode(),
             "obligation module has invalid diagnostic trace value");
   }
+  for (const auto &[InternalName, Variable] : M.DiagnosticVariables)
+    if (Variable.Guard &&
+        (!validateLogicExpr(Variable.Guard.get(), ValidationError,
+                            &WellFormed) ||
+         !validateLogicCalls(Variable.Guard.get(), M.LogicFunctions,
+                             ValidationError, &CallsChecked) ||
+         !ModuleScopes.validate(Variable.Guard.get(), ValidationError) ||
+         Variable.Guard->Sort.Kind != LogicSortKind::Bool))
+      return llvm::createStringError(
+          llvm::inconvertibleErrorCode(),
+          "obligation module has an invalid diagnostic variable guard");
   if (!validateLogicExpr(M.CorrectnessGoal.get(), ValidationError, &WellFormed))
     return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s",
                                    ValidationError.c_str());

clang/lib/Verify/Backend/Obligation.h

@@ -140,15 +140,24 @@ std::string formatLogicFeatures(LogicFeatureSet Features);
 const char *logicSortName(LogicSortKind Kind);
 std::string formatLogicSort(const LogicSort &Sort);
 
+/// Where a term comes from: its anchor (Line, Column), where a diagnostic
+/// points and a stable ID is built, in the source it spans, from its begin to
+/// the column after its last character.
 struct ObligationSource {
   std::string File;
   unsigned Line = 0;
   unsigned Column = 0;
   unsigned EndLine = 0;
   unsigned EndColumn = 0;
+  /// The start of the span, before the anchor (an operator's operands);
+  /// zero when it is the anchor.
+  unsigned BeginLine = 0;
+  unsigned BeginColumn = 0;
 
   bool isValid() const { return !File.empty() && Line != 0; }
   bool hasRange() const { return isValid() && EndLine != 0; }
+  unsigned beginLine() const { return BeginLine ? BeginLine : Line; }
+  unsigned beginColumn() const { return BeginLine ? BeginColumn : Column; }
 };
 
 class LogicExpr;
@@ -210,6 +219,7 @@ class LogicExpr : public llvm::ThreadSafeRefCountedBase<LogicExpr> {
   Kind K;
   LogicSort Sort;
   SourceLocation Loc;
+  SourceLocation BeginLoc;
   SourceLocation EndLoc;
   /// Where Loc lies, filled in by the driver once the term is built
   /// (annotateObligationSources): the one field written after a term is
@@ -313,6 +323,7 @@ struct Obligation {
   std::string StableId;
   ObligationKind Kind = ObligationKind::Assertion;
   SourceLocation Loc;
+  SourceLocation BeginLoc;
   SourceLocation EndLoc;
   ObligationSource Source;
   uint64_t TraceEventCount = 0;
@@ -329,6 +340,11 @@ struct DiagnosticVariable {
   SourceLocation Loc;
   SourceLocation EndLoc;
   ObligationSource Source;
+  /// A reference: its value is the address it refers to. Not archived.
+  bool Reference = false;
+  /// Where this version is defined, as PassiveModelVariable::Guard (true on
+  /// every path); null when unknown, as in an archive before version 4.
+  LogicExprRef Guard = nullptr;
 };
 
 struct LogicFunctionParameter {