https://github.com/steakhal created
https://github.com/llvm/llvm-project/pull/209443
Commit db28e48d67e3b0c44d88be9ea2d28eca2d239a9a 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
From 70dd3d0d100d576ee29f21bd07be95b1ee5ab0dc Mon Sep 17 00:00:00 2001
From: Balazs Benics <[email protected]>
Date: Tue, 14 Jul 2026 12:16:20 +0100
Subject: [PATCH] [analyzer][NFC] Fix UnSatAtErrorNodeDueToRefinedConstraint
test after smarter range inference
Commit db28e48d67e3b0c44d88be9ea2d28eca2d239a9a 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
---
.../FalsePositiveRefutationBRVisitorTest.cpp | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git
a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
index 5d92cb906a154..0c73d8fa44b95 100644
--- a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
+++ b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
@@ -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);
}
}
})";
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
