Skip to content

Commit be65bb0

Browse files
committed
[analyzer][Solver] Teach SymbolicRangeInferrer about commutativity
This patch should not introduce much overhead as it only does one more constraint map lookup, which is really quick.
1 parent 4bf74c7 commit be65bb0

File tree

2 files changed

+15
-2
lines changed

2 files changed

+15
-2
lines changed

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1249,6 +1249,8 @@ class SymbolicRangeInferrer
12491249
// calculate the effective range set by intersecting the range set
12501250
// for A - B and the negated range set of B - A.
12511251
getRangeForNegatedSymSym(SSE),
1252+
// If commutative, we may have constaints for the commuted variant.
1253+
getRangeCommutativeSymSym(SSE),
12521254
// If Sym is a comparison expression (except <=>),
12531255
// find any other comparisons with the same operands.
12541256
// See function description.
@@ -1485,6 +1487,18 @@ class SymbolicRangeInferrer
14851487
Sym->getType());
14861488
}
14871489

1490+
std::optional<RangeSet> getRangeCommutativeSymSym(const SymSymExpr *SSE) {
1491+
bool IsCommutative = llvm::is_contained({BO_Add, BO_Mul}, SSE->getOpcode());
1492+
if (!IsCommutative)
1493+
return std::nullopt;
1494+
1495+
SymbolRef Commuted = State->getSymbolManager().getSymSymExpr(
1496+
SSE->getRHS(), BO_Add, SSE->getLHS(), SSE->getType());
1497+
if (const RangeSet *Range = getConstraint(State, Commuted))
1498+
return *Range;
1499+
return std::nullopt;
1500+
}
1501+
14881502
// Returns ranges only for binary comparison operators (except <=>)
14891503
// when left and right operands are symbolic values.
14901504
// Finds any other comparisons with the same operands.

clang/test/Analysis/unary-sym-expr.c

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,7 @@ void test_svalbuilder_simplification(int x, int y) {
3333
if (x + y != 3)
3434
return;
3535
clang_analyzer_eval(-(x + y) == -3); // expected-warning{{TRUE}}
36-
// FIXME Commutativity is not supported yet.
37-
clang_analyzer_eval(-(y + x) == -3); // expected-warning{{UNKNOWN}}
36+
clang_analyzer_eval(-(y + x) == -3); // expected-warning{{TRUE}}
3837
}
3938

4039
int test_fp(int flag) {

0 commit comments

Comments
 (0)