Cold-Air-Networks/mirror-llvm-project
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 7

[analyzer] Uplift UnSatAtErrorNodeDueToRefinedConstraint test after smarter range inference (#209443)

Browse source 
Commit db28e48d67 taught
`SymbolicRangeInferrer` to derive the range of
`BO_Add`/`BO_Sub`/`BO_Mul` symbols from their operands via
`inferFromCorners`. This broke
`FalsePositiveRefutationBRVisitorTestBase.UnSatAtErrorNodeDueToRefinedConstraintNoReport`.

The test relied on the analyzer not being able to bound `int y = x + n;`
(with `x:[0,2]`, `n:[1,2]`), so that `reportIfCanBeTrue(y == 5)` created
a false state that only the Z3 crosscheck could refute. Now the analyzer
natively bounds y to `[1,4]`, proves `y == 5` infeasible, and never
emits `CAN_BE_TRUE`, so the non-Z3 assertion lost its second line.

Addition can never produce a gap (the sum of two intervals is a full
interval), so the test's premise is no longer achievable with '+'.
Switch to multiplication: for `x:[0,2]`, `n:[1,2]` the reachable
products are `{0,1,2,4}`, but `inferFromCorners` over-approximates `x*n`
to the contiguous range `[0,4]`. So `y == 3` is inside the inferred
range (native manager returns `UNKNOWN -> CAN_BE_TRUE` emitted without
Z3) yet is genuinely unreachable (Z3 refutes `x*n == 3` -> report
invalidated with crosscheck). This restores the exact refutation-visitor
mechanism the test exercises.

Fixes up #209048.

This issue would have been caught if we had a CI running Z3, like
proposed in #184695.

Assisted-by: Claude Opus 4.8
This commit is contained in:
Balázs Benics 2026-07-14 14:16:13 +01:00 committed by GitHub
parent 37b8e765ce
commit c43967ca74
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
View file

@ -183,8 +183,10 @@ TEST_F(FalsePositiveRefutationBRVisitorTestBase,
if (n >= 1 && n <= 2) {
if (x >= 3)
return;
// x: [0,2] and n: [1,2]
int y = x + n; // y: '(x+n)' Which is in approximately between 1 and 4.
// x: [0,2] and n: [1,2], so the reachable products of 'x*n' are
// {0,1,2,4}. The range manager cannot represent this gap and
// over-approximates the symbol '(x*n)' to the contiguous range [0,4].
int y = x * n;
// Registers the symbol 'y' with the constraint [1, MAX] in the true
// branch.
@ -194,13 +196,14 @@ TEST_F(FalsePositiveRefutationBRVisitorTestBase,
// SAT. Therefore that report is NOT invalidated.
reachedWithNoContradiction(); // 'y' can be greater than zero. OK
// If we ask the analyzer whether the 'y' can be 5. It won't know,
// therefore, the state will be created where the 'y' expression is 5.
// If we ask the analyzer whether the 'y' can be 3. It won't know,
// because 3 is inside the over-approximated range [1,4], therefore
// the state will be created where the 'y' expression is 3.
// Although, this assumption is false!
// 'y' can not be 5 if the maximal value of both x and n is 2.
// 'x*n' can not be 3 given x: [0,2] and n: [1,2].
// The BugPath which become UnSAT in the ErrorNode with a refined
// constraint, should be invalidated.
reportIfCanBeTrue(y == 5);
reportIfCanBeTrue(y == 3);
}
}
})";