[all-commits] [llvm/llvm-project] 55391f: [analyzer] Retry UNDEF Z3 queries 2 times by defau...

[Balazs Benics via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 55391f85acc7e7a14ea2ef3c1a4bd8f3df990426
      https://github.com/llvm/llvm-project/commit/55391f85acc7e7a14ea2ef3c1a4bd8f3df990426
  Author: Balazs Benics <benicsbalazs at gmail.com>
  Date:   2025-01-06 (Mon, 06 Jan 2025)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
    M clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
    M clang/lib/Frontend/CompilerInvocation.cpp
    M clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
    M clang/test/Analysis/analyzer-config.c
    A clang/test/Analysis/z3-crosscheck-max-attempts.cpp
    M clang/test/Analysis/z3/D83660.c
    R clang/test/Analysis/z3/Inputs/MockZ3_solver_check.c
    A clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp
    M clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp

  Log Message:
  -----------
  [analyzer] Retry UNDEF Z3 queries 2 times by default (#120239)

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



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications