[all-commits] [llvm/llvm-project] ae570d: Reland "[analyzer] Harden safeguards for Z3 query ...

[Balazs Benics via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: ae570d82e8c021f45209830db8c9c7bb79bed394
      https://github.com/llvm/llvm-project/commit/ae570d82e8c021f45209830db8c9c7bb79bed394
  Author: Balazs Benics <benicsbalazs at gmail.com>
  Date:   2024-07-01 (Mon, 01 Jul 2024)

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

  Log Message:
  -----------
  Reland "[analyzer] Harden safeguards for Z3 query times" (#97298)

This is exactly as originally landed in #95129,
but now the minimal Z3 version was increased to meet this change in #96682.

https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4

---

This patch is a functional change.
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520

As a result of this patch, individual Z3 queries in refutation will be
bound by 300ms. Every report equivalence class will be processed in at
most 1 second.

The heuristic should have only really marginal observable impact -
except for the cases when we had big report eqclasses with long-running
(15s) Z3 queries, where previously CSA effectively halted. After this
patch, CSA will tackle such extreme cases as well.

(cherry picked from commit eacc3b3504be061f7334410dd0eb599688ba103a)



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