[analyzer][NFC] Reorganize Z3 report refutation #95128
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Created using spr 1.3.4
llvmbot
added
clang
|
@llvm/pr-subscribers-llvm-support @llvm/pr-subscribers-clang Author: Balazs Benics (steakhal) ChangesThis change keeps existing behavior, namely that if we hit a Z3 timeout This prepares for the commit "Harden safeguards for Z3 query times". Patch is 27.25 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/95128.diff 12 Files Affected:
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
index cc3d93aabafda..f97514955a591 100644
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -597,29 +597,6 @@ class SuppressInlineDefensiveChecksVisitor final : public BugReporterVisitor {
PathSensitiveBugReport &BR) override;
};
-/// The bug visitor will walk all the nodes in a path and collect all the
-/// constraints. When it reaches the root node, will create a refutation
-/// manager and check if the constraints are satisfiable
-class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
-private:
- /// Holds the constraints in a given path
- ConstraintMap Constraints;
-
-public:
- FalsePositiveRefutationBRVisitor();
-
- void Profile(llvm::FoldingSetNodeID &ID) const override;
-
- PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
- BugReporterContext &BRC,
- PathSensitiveBugReport &BR) override;
-
- void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
- PathSensitiveBugReport &BR) override;
- void addConstraints(const ExplodedNode *N,
- bool OverwriteConstraintsOnExistingSyms);
-};
-
/// The visitor detects NoteTags and displays the event notes they contain.
class TagVisitor : public BugReporterVisitor {
public:
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
new file mode 100644
index 0000000000000..3ec59e3037363
--- /dev/null
+++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
@@ -0,0 +1,66 @@
+//===- Z3CrosscheckVisitor.h - Crosscheck reports with Z3 -------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines the visitor and utilities around it for Z3 report
+// refutation.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
+#define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
+
+#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
+
+namespace clang::ento {
+
+/// The bug visitor will walk all the nodes in a path and collect all the
+/// constraints. When it reaches the root node, will create a refutation
+/// manager and check if the constraints are satisfiable.
+class Z3CrosscheckVisitor final : public BugReporterVisitor {
+public:
+ struct Z3Result {
+ std::optional<bool> IsSAT = std::nullopt;
+ };
+ explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);
+
+ void Profile(llvm::FoldingSetNodeID &ID) const override;
+
+ PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
+ BugReporterContext &BRC,
+ PathSensitiveBugReport &BR) override;
+
+ void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
+ PathSensitiveBugReport &BR) override;
+
+private:
+ void addConstraints(const ExplodedNode *N,
+ bool OverwriteConstraintsOnExistingSyms);
+
+ /// Holds the constraints in a given path.
+ ConstraintMap Constraints;
+ Z3Result &Result;
+};
+
+/// The oracle will decide if a report should be accepted or rejected based on
+/// the results of the Z3 solver.
+class Z3CrosscheckOracle {
+public:
+ enum Z3Decision {
+ AcceptReport, // The report was SAT.
+ RejectReport, // The report was UNSAT or UNDEF.
+ };
+
+ /// Makes a decision for accepting or rejecting the report based on the
+ /// result of the corresponding Z3 query.
+ static Z3Decision
+ interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Query);
+};
+
+} // namespace clang::ento
+
+#endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
\ No newline at end of file
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 5116a4c06850d..bf18c353b8508 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -34,7 +34,10 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
public:
SMTConstraintManager(clang::ento::ExprEngine *EE,
clang::ento::SValBuilder &SB)
- : SimpleConstraintManager(EE, SB) {}
+ : SimpleConstraintManager(EE, SB) {
+ Solver->setBoolParam("model", true); // Enable model finding
+ Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/);
+ }
virtual ~SMTConstraintManager() = default;
//===------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index 14ca507a16d55..c9a7fd0e035c2 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -35,6 +35,7 @@
#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
+#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
#include "clang/StaticAnalyzer/Core/Checker.h"
#include "clang/StaticAnalyzer/Core/CheckerManager.h"
#include "clang/StaticAnalyzer/Core/CheckerRegistryData.h"
@@ -86,6 +87,11 @@ STATISTIC(MaxValidBugClassSize,
"The maximum number of bug reports in the same equivalence class "
"where at least one report is valid (not suppressed)");
+STATISTIC(NumTimesReportPassesZ3, "Number of reports passed Z3");
+STATISTIC(NumTimesReportRefuted, "Number of reports refuted by Z3");
+STATISTIC(NumTimesReportEQClassWasExhausted,
+ "Number of times all reports of an equivalence class was refuted");
+
BugReporterVisitor::~BugReporterVisitor() = default;
void BugReporterContext::anchor() {}
@@ -2864,21 +2870,31 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
// If crosscheck is enabled, remove all visitors, add the refutation
// visitor and check again
R->clearVisitors();
- R->addVisitor<FalsePositiveRefutationBRVisitor>();
+ Z3CrosscheckVisitor::Z3Result CrosscheckResult;
+ R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult);
// We don't overwrite the notes inserted by other visitors because the
// refutation manager does not add any new note to the path
generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
+ switch (Z3CrosscheckOracle::interpretQueryResult(CrosscheckResult)) {
+ case Z3CrosscheckOracle::RejectReport:
+ ++NumTimesReportRefuted;
+ R->markInvalid("Infeasible constraints", /*Data=*/nullptr);
+ continue;
+ case Z3CrosscheckOracle::AcceptReport:
+ ++NumTimesReportPassesZ3;
+ break;
+ }
}
- // Check if the bug is still valid
- if (R->isValid())
- return PathDiagnosticBuilder(
- std::move(BRC), std::move(BugPath->BugPath), BugPath->Report,
- BugPath->ErrorNode, std::move(visitorNotes));
+ assert(R->isValid());
+ return PathDiagnosticBuilder(std::move(BRC), std::move(BugPath->BugPath),
+ BugPath->Report, BugPath->ErrorNode,
+ std::move(visitorNotes));
}
}
+ ++NumTimesReportEQClassWasExhausted;
return {};
}
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
index 487a3bd16b674..68dac65949117 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -3446,82 +3446,6 @@ UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC,
return nullptr;
}
-//===----------------------------------------------------------------------===//
-// Implementation of FalsePositiveRefutationBRVisitor.
-//===----------------------------------------------------------------------===//
-
-FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
- : Constraints(ConstraintMap::Factory().getEmptyMap()) {}
-
-void FalsePositiveRefutationBRVisitor::finalizeVisitor(
- BugReporterContext &BRC, const ExplodedNode *EndPathNode,
- PathSensitiveBugReport &BR) {
- // Collect new constraints
- addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
-
- // Create a refutation manager
- llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
- ASTContext &Ctx = BRC.getASTContext();
-
- // Add constraints to the solver
- for (const auto &I : Constraints) {
- const SymbolRef Sym = I.first;
- auto RangeIt = I.second.begin();
-
- llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
- RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
- /*InRange=*/true);
- while ((++RangeIt) != I.second.end()) {
- SMTConstraints = RefutationSolver->mkOr(
- SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
- RangeIt->From(), RangeIt->To(),
- /*InRange=*/true));
- }
-
- RefutationSolver->addConstraint(SMTConstraints);
- }
-
- // And check for satisfiability
- std::optional<bool> IsSAT = RefutationSolver->check();
- if (!IsSAT)
- return;
-
- if (!*IsSAT)
- BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
-}
-
-void FalsePositiveRefutationBRVisitor::addConstraints(
- const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
- // Collect new constraints
- ConstraintMap NewCs = getConstraintMap(N->getState());
- ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
-
- // Add constraints if we don't have them yet
- for (auto const &C : NewCs) {
- const SymbolRef &Sym = C.first;
- if (!Constraints.contains(Sym)) {
- // This symbol is new, just add the constraint.
- Constraints = CF.add(Constraints, Sym, C.second);
- } else if (OverwriteConstraintsOnExistingSyms) {
- // Overwrite the associated constraint of the Symbol.
- Constraints = CF.remove(Constraints, Sym);
- Constraints = CF.add(Constraints, Sym, C.second);
- }
- }
-}
-
-PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
- const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
- addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
- return nullptr;
-}
-
-void FalsePositiveRefutationBRVisitor::Profile(
- llvm::FoldingSetNodeID &ID) const {
- static int Tag = 0;
- ID.AddPointer(&Tag);
-}
-
//===----------------------------------------------------------------------===//
// Implementation of TagVisitor.
//===----------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
index 8672876c0608d..fb9394a519eb7 100644
--- a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -51,6 +51,7 @@ add_clang_library(clangStaticAnalyzerCore
SymbolManager.cpp
TextDiagnostics.cpp
WorkList.cpp
+ Z3CrosscheckVisitor.cpp
LINK_LIBS
clangAST
diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
new file mode 100644
index 0000000000000..20cd8434cbdc6
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
@@ -0,0 +1,118 @@
+//===- Z3CrosscheckVisitor.h - Crosscheck reports with Z3 -------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file declares the visitor and utilities around it for Z3 report
+// refutation.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
+#include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Statistic.h"
+#include "llvm/Support/SMTAPI.h"
+
+#define DEBUG_TYPE "Z3CrosscheckOracle"
+
+STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
+STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
+
+STATISTIC(NumTimesZ3QueryAcceptsReport,
+ "Number of Z3 queries accepting a report");
+STATISTIC(NumTimesZ3QueryRejectReport,
+ "Number of Z3 queries rejecting a report");
+
+using namespace clang;
+using namespace ento;
+
+Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)
+ : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}
+
+void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
+ const ExplodedNode *EndPathNode,
+ PathSensitiveBugReport &BR) {
+ // Collect new constraints
+ addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
+
+ // Create a refutation manager
+ llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
+ RefutationSolver->setBoolParam("model", true); // Enable model finding
+ RefutationSolver->setUnsignedParam("timeout", 15000); // ms
+
+ ASTContext &Ctx = BRC.getASTContext();
+
+ // Add constraints to the solver
+ for (const auto &[Sym, Range] : Constraints) {
+ auto RangeIt = Range.begin();
+
+ llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
+ RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true);
+ while ((++RangeIt) != Range.end()) {
+ SMTConstraints = RefutationSolver->mkOr(
+ SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
+ RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true));
+ }
+ RefutationSolver->addConstraint(SMTConstraints);
+ }
+
+ // And check for satisfiability
+ std::optional<bool> IsSAT = RefutationSolver->check();
+ Result = Z3Result{IsSAT};
+}
+
+void Z3CrosscheckVisitor::addConstraints(
+ const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
+ // Collect new constraints
+ ConstraintMap NewCs = getConstraintMap(N->getState());
+ ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
+
+ // Add constraints if we don't have them yet
+ for (auto const &[Sym, Range] : NewCs) {
+ if (!Constraints.contains(Sym)) {
+ // This symbol is new, just add the constraint.
+ Constraints = CF.add(Constraints, Sym, Range);
+ } else if (OverwriteConstraintsOnExistingSyms) {
+ // Overwrite the associated constraint of the Symbol.
+ Constraints = CF.remove(Constraints, Sym);
+ Constraints = CF.add(Constraints, Sym, Range);
+ }
+ }
+}
+
+PathDiagnosticPieceRef
+Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
+ PathSensitiveBugReport &) {
+ addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
+ return nullptr;
+}
+
+void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
+ static int Tag = 0;
+ ID.AddPointer(&Tag);
+}
+
+Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
+ const Z3CrosscheckVisitor::Z3Result &Query) {
+ ++NumZ3QueriesDone;
+
+ if (!Query.IsSAT.has_value()) {
+ // For backward compatibility, let's accept the first timeout.
+ ++NumTimesZ3TimedOut;
+ return AcceptReport;
+ }
+
+ if (Query.IsSAT.value()) {
+ ++NumTimesZ3QueryAcceptsReport;
+ return AcceptReport; // sat
+ }
+
+ ++NumTimesZ3QueryRejectReport;
+ return RejectReport; // unsat
+}
diff --git a/clang/test/Analysis/z3/crosscheck-statistics.c b/clang/test/Analysis/z3/crosscheck-statistics.c
new file mode 100644
index 0000000000000..7192824c5be31
--- /dev/null
+++ b/clang/test/Analysis/z3/crosscheck-statistics.c
@@ -0,0 +1,33 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s \
+// RUN: -analyzer-config crosscheck-with-z3=true \
+// RUN: -analyzer-stats 2>&1 | FileCheck %s
+
+// REQUIRES: z3
+
+// expected-error@1 {{Z3 refutation rate:1/2}}
+
+int accepting(int n) {
+ if (n == 4) {
+ n = n / (n-4); // expected-warning {{Division by zero}}
+ }
+ return n;
+}
+
+int rejecting(int n, int x) {
+ // Let's make the path infeasible.
+ if (2 < x && x < 5 && x*x == x*x*x) {
+ // Have the same condition as in 'accepting'.
+ if (n == 4) {
+ n = x / (n-4); // no-warning: refuted
+ }
+ }
+ return n;
+}
+
+// CHECK: 1 BugReporter - Number of times all reports of an equivalence class was refuted
+// CHECK-NEXT: 1 BugReporter - Number of reports passed Z3
+// CHECK-NEXT: 1 BugReporter - Number of reports refuted by Z3
+
+// CHECK: 1 Z3CrosscheckVisitor - Number of Z3 queries accepting a report
+// CHECK-NEXT: 1 Z3CrosscheckVisitor - Number of Z3 queries rejecting a report
+// CHECK-NEXT: 2 Z3CrosscheckVisitor - Number of Z3 queries done
diff --git a/clang/unittests/StaticAnalyzer/CMakeLists.txt b/clang/unittests/StaticAnalyzer/CMakeLists.txt
index ff34d5747cc81..dcc557b44fb31 100644
--- a/clang/unittests/StaticAnalyzer/CMakeLists.txt
+++ b/clang/unittests/StaticAnalyzer/CMakeLists.txt
@@ -21,6 +21,7 @@ add_clang_unittest(StaticAnalysisTests
SymbolReaperTest.cpp
SValTest.cpp
TestReturnValueUnderConstruction.cpp
+ Z3CrosscheckOracleTest.cpp
)
clang_target_link_libraries(StaticAnalysisTests
diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
new file mode 100644
index 0000000000000..efad4dd3f03b9
--- /dev/null
+++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
@@ -0,0 +1,59 @@
+//===- unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp ----------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
+#include "gtest/gtest.h"
+
+using namespace clang;
+using namespace ento;
+
+using Z3Result = Z3CrosscheckVisitor::Z3Result;
+using Z3Decision = Z3CrosscheckOracle::Z3Decision;
+
+static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport;
+static constexpr Z3Decision RejectReport = Z3Decision::RejectReport;
+
+static constexpr std::optional<bool> SAT = true;
+static constexpr std::optional<bool> UNSAT = false;
+static constexpr std::optional<bool> UNDEF = std::nullopt;
+
+namespace {
+
+struct Z3CrosscheckOracleTest : public testing::Test {
+ Z3Decision interpretQueryResult(const Z3Result &Result) const {
+ return Z3CrosscheckOracle::interpretQueryResult(Result);
+ }
+};
+
+TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) {
+ ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
+}
+
+TEST_F(Z3...
[truncated]
|
Created using spr 1.3.4
NagyDonat
approved these changes
Jun 13, 2024
There was a problem hiding this comment.
LGTM. I didn't deeply analyze all the small details of the commit, but it is clearly NFC (builds better infrastructure for follow-up commits), the implementation is clear and elegant (slightly better quality than what I can write) and the tests demonstrate that it's working.
IMO feel free to merge this and continue with the next commit.
|
Thanks for the review!
The problem is that currently one can't run tests with Z3 crosschecking. Consequently, no tests cover this functionality.
Please have a second look at the llvm-related changes. Z3 has a really dangerous C API. I shot myself in the foot literally 3 times while working on this PR. And btw notice that I removed the |
|
You can continue the review with #95129 - which is stacked on top of this one. |
OK, I'll re-check the footgun handling either today or tomorrow. |
NagyDonat
reviewed
Jun 14, 2024
There was a problem hiding this comment.
I tried to review the resource management code thoroughly, but I admit that I'm not skilled in this area -- I'm used to working in modern C++ and Python where these footguns are less relevant.
I found two classed that (if I understand correctly) violate the "rule of three", but I didn't find any acute issues.
Created using spr 1.3.4
|
Implement move-only rule-of-5 for:
|
steakhal
deleted the
users/steakhal/spr/analyzernfc-reorganize-z3-report-refutation
branch
|
Hi @steakhal and @NagyDonat , Does this patch have requirements on the Z3 version? I get |
I'm not aware. I used the latest Z3 when testing. I'll have a look. Edit: Do you have a build bot link, such that I could checkout the exact environment? |
Unfortunately not, I'm on our internal servers. |
|
From the logs you sent, its not clear to me which statianalyzer test fails. Could you point me to an exact gtest or file linenumber pair? |
|
It seems to be the following tests and they fail like |
|
Alright. I had a look and it's interesting. Thanks for reporting this, and I hope this helps. |
|
With the next patch eacc3b3 it fails on rlimit for me, but on this patch it's on timeout. |
|
I don't know really, I just noticed that main suddenly broke for us and bisected to this patch. |
If after the second patch the tests pass then I'm contemplated to say I'd go for upgrading Z3 requirements to 4.8.9, and accept that with my first commit would have failed the CI/tests with an old(er) Z3. |
The testcases fail botth on this and on the next patch. I just commented here because this is the first patch there are problems. I have to check with my team why we are on 4.8.8 and what we can upgrade to. In any case that won't happen today. |
This was referenced Jun 18, 2024
|
@mikaelholmen Please approve the revert PR then. |
steakhal
added a commit
that referenced
this pull request
Jun 18, 2024
Requested in: #95128 (comment) Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation" This reverts commit eacc3b3. This reverts commit 89c26f6.
Done. Thank you! |
steakhal
added a commit
that referenced
this pull request
Jun 26, 2024
steakhal
added a commit
that referenced
this pull request
Jul 1, 2024
This is exactly as originally landed in #95128, but now the minimal Z3 version was increased to meet this change in #96682. https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4 --- This change keeps existing behavior, namely that if we hit a Z3 timeout we will accept the report as "satisfiable". This prepares for the commit "Harden safeguards for Z3 query times". https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 (cherry picked from commit 89c26f6)
lravenclaw
pushed a commit
to lravenclaw/llvm-project
that referenced
this pull request
Jul 3, 2024
lravenclaw
pushed a commit
to lravenclaw/llvm-project
that referenced
this pull request
Jul 3, 2024
This is exactly as originally landed in llvm#95128, but now the minimal Z3 version was increased to meet this change in llvm#96682. https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4 --- This change keeps existing behavior, namely that if we hit a Z3 timeout we will accept the report as "satisfiable". This prepares for the commit "Harden safeguards for Z3 query times". https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 (cherry picked from commit 89c26f6)
kbluck
pushed a commit
to kbluck/llvm-project
that referenced
this pull request
Jul 6, 2024
This is exactly as originally landed in llvm#95128, but now the minimal Z3 version was increased to meet this change in llvm#96682. https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4 --- This change keeps existing behavior, namely that if we hit a Z3 timeout we will accept the report as "satisfiable". This prepares for the commit "Harden safeguards for Z3 query times". https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 (cherry picked from commit 89c26f6)
AlexisPerry
pushed a commit
to llvm-project-tlp/llvm-project
that referenced
this pull request
Jul 9, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This change keeps existing behavior, namely that if we hit a Z3 timeout
we will accept the report as "satisfiable".
This prepares for the commit "Harden safeguards for Z3 query times".
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520