[clang] [analyzer] Retry UNDEF Z3 queries 2 times by default (PR #120239)
DonĂ¡t Nagy via cfe-commits
cfe-commits at lists.llvm.org
Tue Jan 7 01:32:32 PST 2025
NagyDonat wrote:
My first idea is a "down to earth", not so modern, but more backwards compatible approach:
- the analyzer option type stays plain `unsigned`;
- we introduce a new method called `validateAnalyzerOptionValues()` or something similar;
- in this method we specify that `if (Z3CrosscheckMaxAttemptsPerQuery == 0) { /* report invalid argument error */ }`
- in the future if anybody wants to specify some precondition about an analyzer option _or_ about connections between multiple analyzer options, they can put it into this method.
Unlike your approach, this solution has a short inelegant phase in the execution where the invalid value 0 is stored in `Z3CrosscheckMaxAttemptsPerQuery`; however it has several advantages:
- I think you can avoid patching the `AnalyzerOptions` initialization -- the worst thing that can happen is that a downstream user initializes `AnalyzerOptions` without checking the invariants, which is unfortunate but not breaking;
- I think it will lead to shorter code;
- a single invariant check in the code will cover both the default and the user-specified values;
- (note that the "default values are valid" sanity check is automatically performed by all the lit tests that start the analyzer without any analyzer options);
- in the future it can express preconditions that connect multiple analyzer options (e.g. `minSomething` must be strictly less than `maxSomething`).
WDYT?
https://github.com/llvm/llvm-project/pull/120239
More information about the cfe-commits
mailing list