[all-commits] [llvm/llvm-project] ea8e32: [analyzer][Z3] Restore the original timeout of 15s...

[Kristóf Umann via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: ea8e328ae2bea9d9a7d556ef4d791fa116f7de18
      https://github.com/llvm/llvm-project/commit/ea8e328ae2bea9d9a7d556ef4d791fa116f7de18
  Author: Kristóf Umann <dkszelethus at gmail.com>
  Date:   2024-12-13 (Fri, 13 Dec 2024)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
    M clang/test/Analysis/analyzer-config.c
    M clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp

  Log Message:
  -----------
  [analyzer][Z3] Restore the original timeout of 15s (#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.

---------

Co-authored-by: Balazs Benics <benicsbalazs at gmail.com>



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