[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
Szelethus wrote: Oh, I'm so sorry I left this as-is, thank you so much for picking up the slack! Yes, everything looks great! https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
https://github.com/Szelethus closed https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
https://github.com/steakhal approved this pull request. https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
steakhal wrote: I took the time to update the branch with my recommendations. Please confirm if you agree with the current status. tldr; I only made sure the tests actually test what they intended now that the default threshold has changed. I also added a couple more tests where it made sense, along with a new test showcasing the original issue that motivated the presence of the now disabled thresholds. https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
https://github.com/steakhal updated https://github.com/llvm/llvm-project/pull/118291 >From 1fb92742a066444d4a074655704c8148ce1f8326 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Umann?= Date: Mon, 2 Dec 2024 11:21:05 +0100 Subject: [PATCH 1/5] [analyzer][Z3] Restore the original timeout of 15s Discussion here: https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520/15?u=szelethus The original patch, #97298 introduced new timeouts backed by thorough testing and measurements to keep the running time of Z3 within reasonable limits. The measurements also showed that only certain reports and certain TUs were responsible for the poor performance of Z3 refutation. Unfortunately, it seems like that on machines with different characteristics (slower machines) the current timeouts don't just axe 0.01% of reports, but many more as well. Considering that timeouts are inherently nondeterministic as a cutoff point, this lead reports sets being vastly different on the same projects with the same configuration. The discussion link shows that all configurations introduced in the patch with their default values lead to severa nondeterminism of the analyzer. As we, and others use the analyzer as a gating tool for PRs, we should revert to the original defaults. We should respect that * There are still parts of the analyzer that are either proven or suspected to contain nondeterministic code (like pointer sets), * A 15s timeout is more likely to hit the same reports every time on a wider range of machines, but is still inherently nondeterministic, but an infinite timeout leads to the tool hanging, * If you measure the performance of the analyzer on your machines, you can and should achieve some speedup with little or no observable nondeterminism. --- .../clang/StaticAnalyzer/Core/AnalyzerOptions.def | 15 +-- clang/test/Analysis/analyzer-config.c | 6 +++--- .../StaticAnalyzer/Z3CrosscheckOracleTest.cpp | 14 +++--- 3 files changed, 19 insertions(+), 16 deletions(-) diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def index 737bc8e86cfb6a..64fb11821a2656 100644 --- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def +++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def @@ -189,20 +189,23 @@ ANALYZER_OPTION( "crosscheck-with-z3-eqclass-timeout-threshold", "Set a timeout for bug report equivalence classes in milliseconds. " "If we exhaust this threshold, we will drop the bug report eqclass " -"instead of doing more Z3 queries. Set 0 for no timeout.", 700) +"instead of doing more Z3 queries. On fast machines, 700 is a sane value. " +"Set 0 for no timeout.", 0) ANALYZER_OPTION( unsigned, Z3CrosscheckTimeoutThreshold, "crosscheck-with-z3-timeout-threshold", -"Set a timeout for individual Z3 queries in milliseconds. " -"Set 0 for no timeout.", 300) +"Set a timeout for individual Z3 queries in milliseconds. On fast " +"machines, 400 is a sane value. " +"Set 0 for no timeout.", 15'000) ANALYZER_OPTION( unsigned, Z3CrosscheckRLimitThreshold, "crosscheck-with-z3-rlimit-threshold", -"Set the Z3 resource limit threshold. This sets a deterministic cutoff " -"point for Z3 queries, as longer queries usually consume more resources. " -"Set 0 for unlimited.", 400'000) +"Set the Z3 resource limit threshold. This sets a supposedly deterministic " +"cutoff point for Z3 queries, as longer queries usually consume more " +"resources. " +"Set 0 for unlimited.", 0) ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile, "report-in-main-source-file", diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c index 8eb869bac46f8f..0f1314aae9db57 100644 --- a/clang/test/Analysis/analyzer-config.c +++ b/clang/test/Analysis/analyzer-config.c @@ -41,9 +41,9 @@ // CHECK-NEXT: cplusplus.Move:WarnOn = KnownsAndLocals // CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false // CHECK-NEXT: crosscheck-with-z3 = false -// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 700 -// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 40 -// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 300 +// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 0 +// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 0 +// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 15000 // CHECK-NEXT: ctu-dir = "" // CHECK-NEXT: ctu-import-cpp-threshold = 8 // CHECK-NEXT: ctu-import-threshold = 24 diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp index ef07e47ee911b2..a8cb2782c7b72f 100644 --- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp +++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp @@ -38,8 +38,8
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
@@ -74,13 +74,13 @@ TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) {
}
TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
}
steakhal wrote:
I don't think these test reflect what they were testing anymore. Similar
argument goes for the rest of the test cases.
The test name suggests `UNSATWhenItGoesOverTime`, so we should pass a time that
meets this scenario with the new timeout of 15 seconds. I suppose `15'010_ms`
should suffice.
It would be also nice if we could showcase the difference of the non-default
(previous) config with using 400k rlimit and 300ms timeout to see if the
behavior still meets the expected behavior of we had.
It shouldn't be much of a burden to create that config - similar how the
`DefaultOpts` is made, and basically copy-paste the original tests. We could
have a separate fixture for it, called `Z3CrosscheckDefaultOracleTest` and a
`Z3CrosscheckCustomOracleTest` where the defaults are overridden. This way even
the PR diff would look nice.
https://github.com/llvm/llvm-project/pull/118291
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
@@ -189,20 +189,23 @@ ANALYZER_OPTION( "crosscheck-with-z3-eqclass-timeout-threshold", "Set a timeout for bug report equivalence classes in milliseconds. " "If we exhaust this threshold, we will drop the bug report eqclass " -"instead of doing more Z3 queries. Set 0 for no timeout.", 700) +"instead of doing more Z3 queries. On fast machines, 700 is a sane value. " +"Set 0 for no timeout.", 0) steakhal wrote: ```suggestion "instead of doing more Z3 queries. Setting this to 700 ms in conjunction with " "\"crosscheck-with-z3-timeout-threshold\" of 300 ms, would nicely guarantee " "that no bug report equivalence class can take longer than 1 second, " "effectively mitigating Z3 hangs during refutation. " "Set 0 for no timeout.", 0) ``` https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
@@ -189,20 +189,23 @@ ANALYZER_OPTION( "crosscheck-with-z3-eqclass-timeout-threshold", "Set a timeout for bug report equivalence classes in milliseconds. " "If we exhaust this threshold, we will drop the bug report eqclass " -"instead of doing more Z3 queries. Set 0 for no timeout.", 700) +"instead of doing more Z3 queries. On fast machines, 700 is a sane value. " +"Set 0 for no timeout.", 0) ANALYZER_OPTION( unsigned, Z3CrosscheckTimeoutThreshold, "crosscheck-with-z3-timeout-threshold", -"Set a timeout for individual Z3 queries in milliseconds. " -"Set 0 for no timeout.", 300) +"Set a timeout for individual Z3 queries in milliseconds. On fast " +"machines, 400 is a sane value. " +"Set 0 for no timeout.", 15'000) ANALYZER_OPTION( unsigned, Z3CrosscheckRLimitThreshold, "crosscheck-with-z3-rlimit-threshold", -"Set the Z3 resource limit threshold. This sets a deterministic cutoff " -"point for Z3 queries, as longer queries usually consume more resources. " -"Set 0 for unlimited.", 400'000) +"Set the Z3 resource limit threshold. This sets a supposedly deterministic " +"cutoff point for Z3 queries, as longer queries usually consume more " +"resources. " +"Set 0 for unlimited.", 0) steakhal wrote: ```suggestion "Set the Z3 resource limit threshold. This sets a supposedly deterministic " "cutoff point for Z3 queries, as longer queries usually consume more " "resources. " "400'000 should on average make Z3 queries run for up to 100ms on modern hardware." "Set 0 for unlimited.", 0) ``` Could you please confirm that we need to set this option to zero to not have flaky reports? https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
@@ -189,20 +189,23 @@ ANALYZER_OPTION( "crosscheck-with-z3-eqclass-timeout-threshold", "Set a timeout for bug report equivalence classes in milliseconds. " "If we exhaust this threshold, we will drop the bug report eqclass " -"instead of doing more Z3 queries. Set 0 for no timeout.", 700) +"instead of doing more Z3 queries. On fast machines, 700 is a sane value. " +"Set 0 for no timeout.", 0) ANALYZER_OPTION( unsigned, Z3CrosscheckTimeoutThreshold, "crosscheck-with-z3-timeout-threshold", -"Set a timeout for individual Z3 queries in milliseconds. " -"Set 0 for no timeout.", 300) +"Set a timeout for individual Z3 queries in milliseconds. On fast " +"machines, 400 is a sane value. " +"Set 0 for no timeout.", 15'000) steakhal wrote: Why did you mention 400 instead of 300 in `On fast machines, 400 is a sane value.` I also believe that to promote insensitivity, we should avoid using the word "sane". I think I've read that on [Google dev doc style](https://developers.google.com/style/inclusive-documentation), mentioned on [LLVM discourse](https://discourse.llvm.org/t/inclusive-language-in-llvm-can-we-rename-master-branch/55675/68. ```suggestion "Set a timeout for individual Z3 queries in milliseconds. " "On fast machines, 300 worked well in some cases. " "The lower it is, the higher the chances of having flaky issues. " "Having no timeout may hang the analyzer indefinitely. " "Set 0 for no timeout.", 15'000) ``` https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
https://github.com/steakhal requested changes to this pull request. I have no major concerns with this patch. I proposed some wording changes, and I think we should test the configuration we had for the defaults we had prior to this patch to showcase that what is the expected behavior for the situations that motivated the Z3 oracle. Thank you for proposing this. https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
https://github.com/steakhal edited https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
Szelethus wrote: > I also have some just-in-case measurements cooking to confirm that we don't > observe any nondeterminism with these values. Previous measurements of mine > were made with _all_ configs set to 0. Our downstream release goes off with > the patch totally reverted. Sanity check returned normal, no difference in between the report sets. https://codechecker-demo.eastus.cloudapp.azure.com/Default/reports?run=qtbase_v6.2.0_determinism_check15A_1&run=libwebm_libwebm-1.0.0.27_determinism_check15A_1&run=vim_v8.2.1920_determinism_check15A_1&newcheck=qtbase_v6.2.0_determinism_check15B_1&newcheck=libwebm_libwebm-1.0.0.27_determinism_check15B_1&newcheck=vim_v8.2.1920_determinism_check15B_1 https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
llvmbot wrote:
@llvm/pr-subscribers-clang-static-analyzer-1
Author: Kristóf Umann (Szelethus)
Changes
Discussion here:
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520/15?u=szelethus
The original patch, #97298 introduced new timeouts backed by thorough
testing and measurements to keep the running time of Z3 within reasonable
limits. The measurements also showed that only certain reports and certain TUs
were responsible for the poor performance of Z3 refutation.
Unfortunately, it seems like that on machines with different characteristics
(slower machines) the current timeouts don't just axe 0.01% of reports, but
many more as well. Considering that timeouts are inherently nondeterministic as
a cutoff point, this lead reports sets being vastly different on the same
projects with the same configuration. The discussion link shows that all
configurations introduced in the patch with their default values lead to severa
nondeterminism of the analyzer. As we, and others use the analyzer as a gating
tool for PRs, we should revert to the original defaults.
We should respect that
* There are still parts of the analyzer that are either proven or suspected to
contain nondeterministic code (like pointer sets),
* A 15s timeout is more likely to hit the same reports every time on a wider
range of machines, but is still inherently nondeterministic, but an infinite
timeout leads to the tool hanging,
* If you measure the performance of the analyzer on your machines, you can and
should achieve some speedup with little or no observable nondeterminism.
---
Full diff: https://github.com/llvm/llvm-project/pull/118291.diff
3 Files Affected:
- (modified) clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def (+9-6)
- (modified) clang/test/Analysis/analyzer-config.c (+3-3)
- (modified) clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp (+7-7)
``diff
diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
index 737bc8e86cfb6a..64fb11821a2656 100644
--- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
+++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
@@ -189,20 +189,23 @@ ANALYZER_OPTION(
"crosscheck-with-z3-eqclass-timeout-threshold",
"Set a timeout for bug report equivalence classes in milliseconds. "
"If we exhaust this threshold, we will drop the bug report eqclass "
-"instead of doing more Z3 queries. Set 0 for no timeout.", 700)
+"instead of doing more Z3 queries. On fast machines, 700 is a sane value. "
+"Set 0 for no timeout.", 0)
ANALYZER_OPTION(
unsigned, Z3CrosscheckTimeoutThreshold,
"crosscheck-with-z3-timeout-threshold",
-"Set a timeout for individual Z3 queries in milliseconds. "
-"Set 0 for no timeout.", 300)
+"Set a timeout for individual Z3 queries in milliseconds. On fast "
+"machines, 400 is a sane value. "
+"Set 0 for no timeout.", 15'000)
ANALYZER_OPTION(
unsigned, Z3CrosscheckRLimitThreshold,
"crosscheck-with-z3-rlimit-threshold",
-"Set the Z3 resource limit threshold. This sets a deterministic cutoff "
-"point for Z3 queries, as longer queries usually consume more resources. "
-"Set 0 for unlimited.", 400'000)
+"Set the Z3 resource limit threshold. This sets a supposedly deterministic
"
+"cutoff point for Z3 queries, as longer queries usually consume more "
+"resources. "
+"Set 0 for unlimited.", 0)
ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile,
"report-in-main-source-file",
diff --git a/clang/test/Analysis/analyzer-config.c
b/clang/test/Analysis/analyzer-config.c
index 8eb869bac46f8f..0f1314aae9db57 100644
--- a/clang/test/Analysis/analyzer-config.c
+++ b/clang/test/Analysis/analyzer-config.c
@@ -41,9 +41,9 @@
// CHECK-NEXT: cplusplus.Move:WarnOn = KnownsAndLocals
// CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false
// CHECK-NEXT: crosscheck-with-z3 = false
-// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 700
-// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 40
-// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 300
+// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 0
+// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 0
+// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 15000
// CHECK-NEXT: ctu-dir = ""
// CHECK-NEXT: ctu-import-cpp-threshold = 8
// CHECK-NEXT: ctu-import-threshold = 24
diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
index ef07e47ee911b2..a8cb2782c7b72f 100644
--- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
+++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
@@ -38,8 +38,8 @@ static const AnalyzerOptions DefaultOpts = [] {
// Remember to update the tests in this file when these values change.
/
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
https://github.com/NagyDonat approved this pull request. The commit which introduced the new Z3 timeout logic (https://github.com/llvm/llvm-project/pull/97298) was landed with my approval, but since then I realized that this was a mistake -- in particular the concrete fine-tuned default values provide a good fit for one particular computer speed and (as the experimental results show) behave badly on systems that are significantly slower than that. (This should have been obvious in hindsight, but I missed it.) Based on this I support restoring the legacy 15 second timeout which is good as a sane default value and ensures that even the slow computers finish practically all non-hanging Z3 calculations. Changing these `ANALYZER_OPTION`s might be useful for power users who can measure the speed of their worker nodes and configure some sharper timeouts that work for them in particular; but even that is a questionable decision, because with sharp timeouts a temporary loss of processing power (e.g. a job that's started in parallel on the same machine) can cause inconsistent results. https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
https://github.com/isuckatcs approved this pull request. https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
https://github.com/Szelethus created https://github.com/llvm/llvm-project/pull/118291 Discussion here: https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520/15?u=szelethus The original patch, #97298 introduced new timeouts backed by thorough testing and measurements to keep the running time of Z3 within reasonable limits. The measurements also showed that only certain reports and certain TUs were responsible for the poor performance of Z3 refutation. Unfortunately, it seems like that on machines with different characteristics (slower machines) the current timeouts don't just axe 0.01% of reports, but many more as well. Considering that timeouts are inherently nondeterministic as a cutoff point, this lead reports sets being vastly different on the same projects with the same configuration. The discussion link shows that all configurations introduced in the patch with their default values lead to severa nondeterminism of the analyzer. As we, and others use the analyzer as a gating tool for PRs, we should revert to the original defaults. We should respect that * There are still parts of the analyzer that are either proven or suspected to contain nondeterministic code (like pointer sets), * A 15s timeout is more likely to hit the same reports every time on a wider range of machines, but is still inherently nondeterministic, but an infinite timeout leads to the tool hanging, * If you measure the performance of the analyzer on your machines, you can and should achieve some speedup with little or no observable nondeterminism. From 1fb92742a066444d4a074655704c8148ce1f8326 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Umann?= Date: Mon, 2 Dec 2024 11:21:05 +0100 Subject: [PATCH] [analyzer][Z3] Restore the original timeout of 15s Discussion here: https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520/15?u=szelethus The original patch, #97298 introduced new timeouts backed by thorough testing and measurements to keep the running time of Z3 within reasonable limits. The measurements also showed that only certain reports and certain TUs were responsible for the poor performance of Z3 refutation. Unfortunately, it seems like that on machines with different characteristics (slower machines) the current timeouts don't just axe 0.01% of reports, but many more as well. Considering that timeouts are inherently nondeterministic as a cutoff point, this lead reports sets being vastly different on the same projects with the same configuration. The discussion link shows that all configurations introduced in the patch with their default values lead to severa nondeterminism of the analyzer. As we, and others use the analyzer as a gating tool for PRs, we should revert to the original defaults. We should respect that * There are still parts of the analyzer that are either proven or suspected to contain nondeterministic code (like pointer sets), * A 15s timeout is more likely to hit the same reports every time on a wider range of machines, but is still inherently nondeterministic, but an infinite timeout leads to the tool hanging, * If you measure the performance of the analyzer on your machines, you can and should achieve some speedup with little or no observable nondeterminism. --- .../clang/StaticAnalyzer/Core/AnalyzerOptions.def | 15 +-- clang/test/Analysis/analyzer-config.c | 6 +++--- .../StaticAnalyzer/Z3CrosscheckOracleTest.cpp | 14 +++--- 3 files changed, 19 insertions(+), 16 deletions(-) diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def index 737bc8e86cfb6a..64fb11821a2656 100644 --- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def +++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def @@ -189,20 +189,23 @@ ANALYZER_OPTION( "crosscheck-with-z3-eqclass-timeout-threshold", "Set a timeout for bug report equivalence classes in milliseconds. " "If we exhaust this threshold, we will drop the bug report eqclass " -"instead of doing more Z3 queries. Set 0 for no timeout.", 700) +"instead of doing more Z3 queries. On fast machines, 700 is a sane value. " +"Set 0 for no timeout.", 0) ANALYZER_OPTION( unsigned, Z3CrosscheckTimeoutThreshold, "crosscheck-with-z3-timeout-threshold", -"Set a timeout for individual Z3 queries in milliseconds. " -"Set 0 for no timeout.", 300) +"Set a timeout for individual Z3 queries in milliseconds. On fast " +"machines, 400 is a sane value. " +"Set 0 for no timeout.", 15'000) ANALYZER_OPTION( unsigned, Z3CrosscheckRLimitThreshold, "crosscheck-with-z3-rlimit-threshold", -"Set the Z3 resource limit threshold. This sets a deterministic cutoff " -"point for Z3 queries, as longer queries usually consume more resources. " -"Set 0 for unlimited.", 400'000) +"Set the Z3 resource limit threshold. This se
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
Szelethus wrote: I also have some just-in-case measurements cooking to confirm that we don't observe any nondeterminism with these values. Previous measurements of mine were made with _all_ configs set to 0. Our downstream release goes off with the patch totally reverted. https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)
graphite-app[bot] wrote: ## Your org has enabled the Graphite merge queue for merging into main Add the label “FP Bundles” to the PR and Graphite will automatically add it to the merge queue when it’s ready to merge. You must have a Graphite account and log in to Graphite in order to use the merge queue. Sign up using [this link](https://app.graphite.dev/invite/github/llvm?ref=merge-queue-instructions-comment&prId=5671480345). https://github.com/llvm/llvm-project/pull/118291 ___ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
