llvmorg-github-actions[bot] wrote:
<!--LLVM PR SUMMARY COMMENT-->
@llvm/pr-subscribers-clang-static-analyzer-1
Author: Balázs Benics (steakhal)
<details>
<summary>Changes</summary>
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
---
Full diff: https://github.com/llvm/llvm-project/pull/209443.diff
1 Files Affected:
- (modified)
clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp (+9-6)
``````````diff
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);
}
}
})";
``````````
</details>
https://github.com/llvm/llvm-project/pull/209443
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
