mirror of
https://github.com/llvm/llvm-project.git
synced 2025-04-18 03:36:37 +00:00
55391f85ac
If we have a refutation Z3 query timed out (UNDEF), allow a couple of retries to improve stability of the query. By default allow 2 retries, which will give us in maximum of 3 solve attempts per query. Retries should help mitigating flaky Z3 queries. See the details in the following RFC: https://discourse.llvm.org/t/analyzer-rfc-retry-z3-crosscheck-queries-on-timeout/83711 Note that with each attempt, we spend more time per query. Currently, we have a 15 seconds timeout per query - which are also in effect for the retry attempts. --- Why should this help? In short, retrying queries should bring stability because if a query runs long it's more likely that it did so due to some runtime anomaly than it's on the edge of succeeding. This is because most queries run quick, and the queries that run long, usually run long by a fair amount. Consequently, retries should improve the stability of the outcome of the Z3 query. In general, the retries shouldn't increase the overall analysis time because it's really rare we hit the 0.1% of the cases when we would do retries. But keep in mind that the retry attempts can add up if many retries are allowed, or the individual query timeout is large. CPP-5920
43 lines
1.9 KiB
C++
43 lines
1.9 KiB
C++
// Check the default config.
|
|
// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ConfigDumper 2>&1 \
|
|
// RUN: | FileCheck %s --match-full-lines
|
|
// CHECK: crosscheck-with-z3-max-attempts-per-query = 3
|
|
|
|
// RUN: rm -rf %t && mkdir %t
|
|
// RUN: %host_cxx -shared -fPIC \
|
|
// RUN: %S/z3/Inputs/MockZ3_solver_check.cpp \
|
|
// RUN: -o %t/MockZ3_solver_check.so
|
|
|
|
// DEFINE: %{mocked_clang} = \
|
|
// DEFINE: LD_PRELOAD="%t/MockZ3_solver_check.so" \
|
|
// DEFINE: %clang_cc1 %s -analyze -setup-static-analyzer \
|
|
// DEFINE: -analyzer-config crosscheck-with-z3=true \
|
|
// DEFINE: -analyzer-checker=core
|
|
|
|
// DEFINE: %{attempts} = -analyzer-config crosscheck-with-z3-max-attempts-per-query
|
|
|
|
// RUN: not %clang_analyze_cc1 %{attempts}=0 2>&1 | FileCheck %s --check-prefix=VERIFY-INVALID
|
|
// VERIFY-INVALID: invalid input for analyzer-config option 'crosscheck-with-z3-max-attempts-per-query', that expects a positive value
|
|
|
|
// RUN: Z3_SOLVER_RESULTS="UNDEF" %{mocked_clang} %{attempts}=1 -verify=refuted
|
|
// RUN: Z3_SOLVER_RESULTS="UNSAT" %{mocked_clang} %{attempts}=1 -verify=refuted
|
|
// RUN: Z3_SOLVER_RESULTS="SAT" %{mocked_clang} %{attempts}=1 -verify=accepted
|
|
|
|
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF" %{mocked_clang} %{attempts}=2 -verify=refuted
|
|
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNSAT" %{mocked_clang} %{attempts}=2 -verify=refuted
|
|
// RUN: Z3_SOLVER_RESULTS="UNDEF,SAT" %{mocked_clang} %{attempts}=2 -verify=accepted
|
|
|
|
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNDEF" %{mocked_clang} %{attempts}=3 -verify=refuted
|
|
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNSAT" %{mocked_clang} %{attempts}=3 -verify=refuted
|
|
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT" %{mocked_clang} %{attempts}=3 -verify=accepted
|
|
|
|
|
|
// REQUIRES: z3, asserts, shell, system-linux
|
|
|
|
// refuted-no-diagnostics
|
|
|
|
int div_by_zero_test(int b) {
|
|
if (b) {}
|
|
return 100 / b; // accepted-warning {{Division by zero}}
|
|
}
|