[all-commits] [llvm/llvm-project] eacc3b: [analyzer] Harden safeguards for Z3 query times

[Balazs Benics via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: eacc3b3504be061f7334410dd0eb599688ba103a
      https://github.com/llvm/llvm-project/commit/eacc3b3504be061f7334410dd0eb599688ba103a
  Author: Balazs Benics <benicsbalazs at gmail.com>
  Date:   2024-06-18 (Tue, 18 Jun 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:
  -----------
  [analyzer] Harden safeguards for Z3 query times

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.

Reviewers: NagyDonat, haoNoQ, Xazax-hun, Szelethus, mikhailramalho

Reviewed By: NagyDonat

Pull Request: https://github.com/llvm/llvm-project/pull/95129



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