[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
mikaelholmen wrote: > @mikaelholmen Please approve the revert PR then. Done. Thank you! https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: @mikaelholmen Please approve the revert PR then. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
mikaelholmen wrote: > > 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. On my system, all > `StaticAnalysisTests` pass with 4.8.9 on `main`. Are you okay with upgrading > Z3 to at least 4.8.9 or preferably to latest (4.13.0)? 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. But I'm surprised that requirements were suddenly raised without warning. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: > 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 Z3. On my system, all `StaticAnalysisTests` pass with 4.8.9 on `main`. Are you okay with upgrading Z3 to at least 4.8.9 or preferably to latest (4.13.0)? https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
mikaelholmen wrote: I don't know really, I just noticed that main suddenly broke for us and bisected to this patch. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: > With the next patch > [eacc3b3](https://github.com/llvm/llvm-project/commit/eacc3b3504be061f7334410dd0eb599688ba103a) > it fails on rlimit for me, but on this patch it's on timeout. What do you suggest? Do you know a reliable minimal Z3 version which we should require? FYI I published [this](https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664) post about raising Z3 version requirement. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
mikaelholmen wrote: With the next patch eacc3b3504be061 it fails on rlimit for me, but on this patch it's on timeout. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: Alright. I had a look and it's interesting. For me, it crashes with `LLVM ERROR: Z3 error: unknown parameter 'rlimit'`, but that shouldn't matter. Actually `rlimit` should be available from 4.5.0, according to the [release notes](https://github.com/Z3Prover/z3/blob/master/RELEASE_NOTES.md) of Z3. That release note does not mention `rlimit` or `timeout` basically at all. However, by manual checking it seems that the from the very next patch release (4.8.9+) it compiles and passes the test you mentioned failing. I'd recommend you to upgrade Z3 to unblock your workflow. Given this, I'll propose an RFC later (in the upcoming weeks) to bump the minimal Z3 version to 4.8.9 (by one patch release), to follow the llvm guidelines. Thanks for reporting this, and I hope this helps. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
mikaelholmen wrote: It seems to be the following tests ``` FalsePositiveRefutationBRVisitorTestBase.UnSatInTheMiddleNoReport FalsePositiveRefutationBRVisitorTestBase.UnSatAtErrorNodeDueToRefinedConstraintNoReport FalsePositiveRefutationBRVisitorTestBase.UnSatAtErrorNodeWithNewSymbolNoReport ``` and they fail like ``` [ RUN ] FalsePositiveRefutationBRVisitorTestBase.UnSatAtErrorNodeWithNewSymbolNoReport LLVM ERROR: Z3 error: unknown parameter 'timeout' Legal parameters are: arith.auto_config_simplex (bool) (default: false) arith.bprop_on_pivoted_rows (bool) (default: true) arith.branch_cut_ratio (unsigned int) (default: 2) arith.dump_lemmas (bool) (default: false) arith.eager_eq_axioms (bool) (default: true) arith.enable_hnf (bool) (default: true) arith.greatest_error_pivot (bool) (default: false) arith.ignore_int (bool) (default: false) arith.int_eq_branch (bool) (default: false) arith.min (bool) (default: false) arith.nl (bool) (default: true) arith.nl.branching (bool) (default: true) arith.nl.gb (bool) (default: true) arith.nl.gr_q (unsigned int) (default: 10) arith.nl.grobner (bool) (default: true) arith.nl.grobner_cnfl_to_report (unsigned int) (default: 1) arith.nl.grobner_eqs_growth (unsigned int) (default: 10) arith.nl.grobner_expr_degree_growth (unsigned int) (default: 2) arith.nl.grobner_expr_size_growth (unsigned int) (default: 2) arith.nl.grobner_max_simplified (unsigned int) (default: 1) arith.nl.grobner_subs_fixed (unsigned int) (default: 2) arith.nl.horner (bool) (default: true) arith.nl.horner_frequency (unsigned int) (default: 4) arith.nl.horner_row_length_limit (unsigned int) (default: 10) arith.nl.horner_subs_fixed (unsigned int) (default: 2) arith.nl.order (bool) (default: true) arith.nl.rounds (unsigned int) (default: 1024) arith.nl.tangents (bool) (default: true) arith.print_ext_var_names (bool) (default: false) arith.print_stats (bool) (default: false) arith.propagate_eqs (bool) (default: true) arith.propagation_mode (unsigned int) (default: 2) arith.random_initial_value (bool) (default: false) arith.reflect (bool) (default: true) arith.rep_freq (unsigned int) (default: 0) arith.simplex_strategy (unsigned int) (default: 0) arith.solver (unsigned int) (default: 2) array.extensional (bool) (default: true) array.weak (bool) (default: false) auto_config (bool) (default: true) bv.enable_int2bv (bool) (default: true) bv.reflect (bool) (default: true) case_split (unsigned int) (default: 1) clause_proof (bool) (default: false) core.extend_nonlocal_patterns (bool) (default: false) core.extend_patterns (bool) (default: false) core.extend_patterns.max_distance (unsigned int) (default: 4294967295) core.minimize (bool) (default: false) core.validate (bool) (default: false) dack (unsigned int) (default: 1) dack.eq (bool) (default: false) dack.factor (double) (default: 0.1) dack.gc (unsigned int) (default: 2000) dack.gc_inv_decay (double) (default: 0.8) dack.threshold (unsigned int) (default: 10) delay_units (bool) (default: false) delay_units_threshold (unsigned int) (default: 32) dt_lazy_splits (unsigned int) (default: 1) ematching (bool) (default: true) induction (bool) (default: false) lemma_gc_strategy (unsigned int) (default: 0) logic (symbol) (default: ) macro_finder (bool) (default: false) max_conflicts (unsigned int) (default: 4294967295) mbqi (bool) (default: true) mbqi.force_template (unsigned int) (default: 10) mbqi.id (string) (default: ) mbqi.max_cexs (unsigned int) (default: 1) mbqi.max_cexs_incr (unsigned int) (default: 0) mbqi.max_iterations (unsigned int) (default: 1000) mbqi.trace (bool) (default: false) model (bool) (default: true) pb.conflict_frequency (unsigned int) (default: 1000) pb.learn_complements (bool) (default: true) phase_selection (unsigned int) (default: 3) proof (bool) (default: false) pull_nested_quantifiers (bool) (default: false) qi.cost (string) (default: (+ weight generation)) qi.eager_threshold (double) (default: 10.0) qi.lazy_threshold (double) (default: 20.0) qi.max_instances (unsigned int) (default: 4294967295) qi.max_multi_patterns (unsigned int) (default: 0) qi.profile (bool) (default: false) qi.profile_freq (unsigned int) (default: 4294967295) qi.quick_checker (unsigned int) (default: 0) quasi_macros (bool) (default: false) random_seed (unsigned int) (default: 0) refine_inj_axioms (bool) (default: true) relevancy (unsigned int) (default: 2) restart.max (unsigned int) (default: 4294967295) restart_factor (double) (default: 1.1) restart_strategy (unsigned int) (default: 1) restricted_quasi_macros (bool) (default: false) seq.split_w_len (bool) (default: true) seq.validate (bool) (default: false) str.aggressive_length_testing (bool) (default: false) str.aggressive_unroll_testing (bool) (default: true) str.aggressive_value_testing (bool) (default: false)
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: >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? https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
mikaelholmen wrote: > > Hi @steakhal and @NagyDonat , > > Does this patch have requirements on the Z3 version? > > I get > > `LLVM ERROR: Z3 error: unknown parameter 'timeout'` > > for the following testcases > > ``` > > Failed Tests (3): > > Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/24/188 > > Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/25/188 > > Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/26/188 > > ``` > > 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 what I can see we're using Z3 4.8.8-1 https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: > Hi @steakhal and @NagyDonat , > > Does this patch have requirements on the Z3 version? > > I get > ```LLVM ERROR: Z3 error: unknown parameter 'timeout'``` > for the following testcases > ``` > Failed Tests (3): > Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/24/188 > Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/25/188 > Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/26/188 > ``` > I'm not aware. I used the latest Z3 when testing. I'll have a look. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
mikaelholmen wrote: Hi @steakhal and @NagyDonat , Does this patch have requirements on the Z3 version? I get ```LLVM ERROR: Z3 error: unknown parameter 'timeout'``` for the following testcases ``` Failed Tests (3): Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/24/188 Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/25/188 Clang-Unit :: StaticAnalyzer/./StaticAnalysisTests/26/188 ``` https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/steakhal closed https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: Implement move-only rule-of-5 for: - `Z3Config` - `Z3Context` https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/steakhal updated
https://github.com/llvm/llvm-project/pull/95128
>From 6b9a5a6902c3efca6ac7d6a5dabc8950767560cc Mon Sep 17 00:00:00 2001
From: Balazs Benics
Date: Tue, 11 Jun 2024 16:53:46 +0200
Subject: [PATCH 1/2] =?UTF-8?q?[=F0=9D=98=80=F0=9D=97=BD=F0=9D=97=BF]=20in?=
=?UTF-8?q?itial=20version?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Created using spr 1.3.4
---
.../Core/BugReporter/BugReporterVisitors.h| 23
.../Core/BugReporter/Z3CrosscheckVisitor.h| 66 ++
.../Core/PathSensitive/SMTConstraintManager.h | 5 +-
clang/lib/StaticAnalyzer/Core/BugReporter.cpp | 28 -
.../Core/BugReporterVisitors.cpp | 76 ---
clang/lib/StaticAnalyzer/Core/CMakeLists.txt | 1 +
.../Core/Z3CrosscheckVisitor.cpp | 118 ++
.../test/Analysis/z3/crosscheck-statistics.c | 33 +
clang/unittests/StaticAnalyzer/CMakeLists.txt | 1 +
.../StaticAnalyzer/Z3CrosscheckOracleTest.cpp | 59 +
llvm/include/llvm/Support/SMTAPI.h| 19 +++
llvm/lib/Support/Z3Solver.cpp | 103 ---
12 files changed, 408 insertions(+), 124 deletions(-)
create mode 100644
clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
create mode 100644 clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
create mode 100644 clang/test/Analysis/z3/crosscheck-statistics.c
create mode 100644 clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
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 0..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 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 f
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
@@ -26,17 +28,10 @@ namespace {
class Z3Config {
NagyDonat wrote:
If I understand it correctly, rule of three/five dictates that the copy/move
assignment/construction of this class needs to be handled (or deleted).
https://github.com/llvm/llvm-project/pull/95128
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/NagyDonat commented: 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. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
@@ -50,16 +45,17 @@ void Z3ErrorHandler(Z3_context Context, Z3_error_code
Error) {
/// Wrapper for Z3 context
class Z3Context {
NagyDonat wrote:
Another class that manages a resource in a destructor, but does not handle
copy/move assignment/construction.
https://github.com/llvm/llvm-project/pull/95128
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/NagyDonat edited https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
NagyDonat wrote: > 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 proof=false configuration as that is the > default AFAIK, so that's why that is missing. OK, I'll re-check the footgun handling either today or tomorrow. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
@@ -434,6 +447,12 @@ class SMTSolver {
virtual bool isFPSupported() = 0;
virtual void print(raw_ostream &OS) const = 0;
+
+ /// Sets the requested option.
+ virtual void setBoolParam(StringRef Key, bool Value) = 0;
+ virtual void setUnsignedParam(StringRef Key, unsigned Value) = 0;
+
+ virtual std::unique_ptr getStatistics() const = 0;
NagyDonat wrote:
> It's not used in this PR, and I find it difficult to add test for.
Ok, that's completely fine, it doesn't cause any problems here.
https://github.com/llvm/llvm-project/pull/95128
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: You can continue the review with #95129 - which is stacked on top of this one. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
steakhal wrote: Thanks for the review! > 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. The problem is that currently one can't run tests with Z3 crosschecking. Consequently, no tests cover this functionality. The unit-tests in the next PR tests the Z3 oracle, which is not tight to the actual Z3 library in an ways. > IMO feel free to merge this and continue with the next commit. 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 `proof=false` configuration as that is the default AFAIK, so that's why that is missing. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
@@ -434,6 +447,12 @@ class SMTSolver {
virtual bool isFPSupported() = 0;
virtual void print(raw_ostream &OS) const = 0;
+
+ /// Sets the requested option.
+ virtual void setBoolParam(StringRef Key, bool Value) = 0;
+ virtual void setUnsignedParam(StringRef Key, unsigned Value) = 0;
+
+ virtual std::unique_ptr getStatistics() const = 0;
steakhal wrote:
It's not used in this PR, and I find it difficult to add test for.
However, in my next PR it's gonna be
[used](https://github.com/llvm/llvm-project/pull/95129/files#diff-7c4020235aab08e99f0a84abd569c43e01e5b0ce6ac2182ef1deda8b487734b5R88).
The dump methods are for just debugging, like for the other APIs. This way they
remain consistent.
https://github.com/llvm/llvm-project/pull/95128
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
@@ -434,6 +447,12 @@ class SMTSolver {
virtual bool isFPSupported() = 0;
virtual void print(raw_ostream &OS) const = 0;
+
+ /// Sets the requested option.
+ virtual void setBoolParam(StringRef Key, bool Value) = 0;
+ virtual void setUnsignedParam(StringRef Key, unsigned Value) = 0;
+
+ virtual std::unique_ptr getStatistics() const = 0;
NagyDonat wrote:
Is this method called anywhere?
https://github.com/llvm/llvm-project/pull/95128
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/NagyDonat edited https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/NagyDonat edited https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/NagyDonat approved this pull request. 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. https://github.com/llvm/llvm-project/pull/95128 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/steakhal updated
https://github.com/llvm/llvm-project/pull/95128
>From 6b9a5a6902c3efca6ac7d6a5dabc8950767560cc Mon Sep 17 00:00:00 2001
From: Balazs Benics
Date: Tue, 11 Jun 2024 16:53:46 +0200
Subject: [PATCH 1/2] =?UTF-8?q?[=F0=9D=98=80=F0=9D=97=BD=F0=9D=97=BF]=20in?=
=?UTF-8?q?itial=20version?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Created using spr 1.3.4
---
.../Core/BugReporter/BugReporterVisitors.h| 23
.../Core/BugReporter/Z3CrosscheckVisitor.h| 66 ++
.../Core/PathSensitive/SMTConstraintManager.h | 5 +-
clang/lib/StaticAnalyzer/Core/BugReporter.cpp | 28 -
.../Core/BugReporterVisitors.cpp | 76 ---
clang/lib/StaticAnalyzer/Core/CMakeLists.txt | 1 +
.../Core/Z3CrosscheckVisitor.cpp | 118 ++
.../test/Analysis/z3/crosscheck-statistics.c | 33 +
clang/unittests/StaticAnalyzer/CMakeLists.txt | 1 +
.../StaticAnalyzer/Z3CrosscheckOracleTest.cpp | 59 +
llvm/include/llvm/Support/SMTAPI.h| 19 +++
llvm/lib/Support/Z3Solver.cpp | 103 ---
12 files changed, 408 insertions(+), 124 deletions(-)
create mode 100644
clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
create mode 100644 clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
create mode 100644 clang/test/Analysis/z3/crosscheck-statistics.c
create mode 100644 clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
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 0..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 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 f
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
llvmbot wrote:
@llvm/pr-subscribers-clang-static-analyzer-1
@llvm/pr-subscribers-clang
Author: Balazs Benics (steakhal)
Changes
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
---
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:
- (modified)
clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h (-23)
- (added)
clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h (+66)
- (modified)
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
(+4-1)
- (modified) clang/lib/StaticAnalyzer/Core/BugReporter.cpp (+22-6)
- (modified) clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (-76)
- (modified) clang/lib/StaticAnalyzer/Core/CMakeLists.txt (+1)
- (added) clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp (+118)
- (added) clang/test/Analysis/z3/crosscheck-statistics.c (+33)
- (modified) clang/unittests/StaticAnalyzer/CMakeLists.txt (+1)
- (added) clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp (+59)
- (modified) llvm/include/llvm/Support/SMTAPI.h (+19)
- (modified) llvm/lib/Support/Z3Solver.cpp (+85-18)
``diff
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 0..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 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,
+ PathSensitive
[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)
https://github.com/steakhal created
https://github.com/llvm/llvm-project/pull/95128
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
>From 6b9a5a6902c3efca6ac7d6a5dabc8950767560cc Mon Sep 17 00:00:00 2001
From: Balazs Benics
Date: Tue, 11 Jun 2024 16:53:46 +0200
Subject: [PATCH] =?UTF-8?q?[=F0=9D=98=80=F0=9D=97=BD=F0=9D=97=BF]=20initia?=
=?UTF-8?q?l=20version?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Created using spr 1.3.4
---
.../Core/BugReporter/BugReporterVisitors.h| 23
.../Core/BugReporter/Z3CrosscheckVisitor.h| 66 ++
.../Core/PathSensitive/SMTConstraintManager.h | 5 +-
clang/lib/StaticAnalyzer/Core/BugReporter.cpp | 28 -
.../Core/BugReporterVisitors.cpp | 76 ---
clang/lib/StaticAnalyzer/Core/CMakeLists.txt | 1 +
.../Core/Z3CrosscheckVisitor.cpp | 118 ++
.../test/Analysis/z3/crosscheck-statistics.c | 33 +
clang/unittests/StaticAnalyzer/CMakeLists.txt | 1 +
.../StaticAnalyzer/Z3CrosscheckOracleTest.cpp | 59 +
llvm/include/llvm/Support/SMTAPI.h| 19 +++
llvm/lib/Support/Z3Solver.cpp | 103 ---
12 files changed, 408 insertions(+), 124 deletions(-)
create mode 100644
clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
create mode 100644 clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
create mode 100644 clang/test/Analysis/z3/crosscheck-statistics.c
create mode 100644 clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
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 0..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 IsSAT = std::nullopt;
+ };
+ explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);
+
+ void Profi
