Skip to content

Commit 67e8421

Browse files
authored
[analyzer][Solver] Teach SymbolicRangeInferrer about commutativity (2/2) (llvm#112887)
This patch should not introduce much overhead as it only does one more constraint map lookup, which is really quick. Depends on llvm#112583
1 parent 90bc60c commit 67e8421

File tree

2 files changed

+47
-3
lines changed

2 files changed

+47
-3
lines changed

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

Lines changed: 17 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,21 @@ class SymbolicRangeInferrer
14851487
Sym->getType());
14861488
}
14871489

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

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

Lines changed: 30 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,12 +29,39 @@ int test(int x, int y) {
2929
return 42;
3030
}
3131

32-
void test_svalbuilder_simplification(int x, int y) {
32+
void test_svalbuilder_simplification_add(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}}
37+
}
38+
39+
void test_svalbuilder_simplification_mul(int x, int y) {
40+
if (x * y != 3)
41+
return;
42+
clang_analyzer_eval(-(x * y) == -3); // expected-warning{{TRUE}}
43+
clang_analyzer_eval(-(y * x) == -3); // expected-warning{{TRUE}}
44+
}
45+
46+
void test_svalbuilder_simplification_and(int x, int y) {
47+
if ((x & y) != 3)
48+
return;
49+
clang_analyzer_eval(-(x & y) == -3); // expected-warning{{TRUE}}
50+
clang_analyzer_eval(-(y & x) == -3); // expected-warning{{TRUE}}
51+
}
52+
53+
void test_svalbuilder_simplification_or(int x, int y) {
54+
if ((x | y) != 3)
55+
return;
56+
clang_analyzer_eval(-(x | y) == -3); // expected-warning{{TRUE}}
57+
clang_analyzer_eval(-(y | x) == -3); // expected-warning{{TRUE}}
58+
}
59+
60+
void test_svalbuilder_simplification_xor(int x, int y) {
61+
if ((x ^ y) != 3)
62+
return;
63+
clang_analyzer_eval(-(x ^ y) == -3); // expected-warning{{TRUE}}
64+
clang_analyzer_eval(-(y ^ x) == -3); // expected-warning{{TRUE}}
3865
}
3966

4067
int test_fp(int flag) {

0 commit comments

Comments
 (0)