[analyzer][Solver] Teach SymbolicRangeInferrer about commutativity (2/2) #112887
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This patch should not introduce much overhead as it only does one more constraint map lookup, which is really quick.
llvmbot
added
clang
|
@llvm/pr-subscribers-clang Author: Balazs Benics (steakhal) ChangesThis patch should not introduce much overhead as it only does one more constraint map lookup, which is really quick. Depends on #112583 Full diff: https://github.com/llvm/llvm-project/pull/112887.diff 2 Files Affected:
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index ecf7974c838650..f0311b7028f56d 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1249,6 +1249,8 @@ class SymbolicRangeInferrer
// calculate the effective range set by intersecting the range set
// for A - B and the negated range set of B - A.
getRangeForNegatedSymSym(SSE),
+ // If commutative, we may have constaints for the commuted variant.
+ getRangeCommutativeSymSym(SSE),
// If Sym is a comparison expression (except <=>),
// find any other comparisons with the same operands.
// See function description.
@@ -1485,6 +1487,21 @@ class SymbolicRangeInferrer
Sym->getType());
}
+ std::optional<RangeSet> getRangeCommutativeSymSym(const SymSymExpr *SSE) {
+ auto Op = SSE->getOpcode();
+ bool IsCommutative = llvm::is_contained(
+ // ==, !=, |, &, +, *, ^
+ {BO_EQ, BO_NE, BO_Or, BO_And, BO_Add, BO_Mul, BO_Xor}, Op);
+ if (!IsCommutative)
+ return std::nullopt;
+
+ SymbolRef Commuted = State->getSymbolManager().getSymSymExpr(
+ SSE->getRHS(), Op, SSE->getLHS(), SSE->getType());
+ if (const RangeSet *Range = getConstraint(State, Commuted))
+ return *Range;
+ return std::nullopt;
+ }
+
// Returns ranges only for binary comparison operators (except <=>)
// when left and right operands are symbolic values.
// Finds any other comparisons with the same operands.
diff --git a/clang/test/Analysis/unary-sym-expr.c b/clang/test/Analysis/unary-sym-expr.c
index 7c4774f3cca82f..92e11b295bee7c 100644
--- a/clang/test/Analysis/unary-sym-expr.c
+++ b/clang/test/Analysis/unary-sym-expr.c
@@ -29,12 +29,39 @@ int test(int x, int y) {
return 42;
}
-void test_svalbuilder_simplification(int x, int y) {
+void test_svalbuilder_simplification_add(int x, int y) {
if (x + y != 3)
return;
clang_analyzer_eval(-(x + y) == -3); // expected-warning{{TRUE}}
- // FIXME Commutativity is not supported yet.
- clang_analyzer_eval(-(y + x) == -3); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(-(y + x) == -3); // expected-warning{{TRUE}}
+}
+
+void test_svalbuilder_simplification_mul(int x, int y) {
+ if (x * y != 3)
+ return;
+ clang_analyzer_eval(-(x * y) == -3); // expected-warning{{TRUE}}
+ clang_analyzer_eval(-(y * x) == -3); // expected-warning{{TRUE}}
+}
+
+void test_svalbuilder_simplification_and(int x, int y) {
+ if ((x & y) != 3)
+ return;
+ clang_analyzer_eval(-(x & y) == -3); // expected-warning{{TRUE}}
+ clang_analyzer_eval(-(y & x) == -3); // expected-warning{{TRUE}}
+}
+
+void test_svalbuilder_simplification_or(int x, int y) {
+ if ((x | y) != 3)
+ return;
+ clang_analyzer_eval(-(x | y) == -3); // expected-warning{{TRUE}}
+ clang_analyzer_eval(-(y | x) == -3); // expected-warning{{TRUE}}
+}
+
+void test_svalbuilder_simplification_xor(int x, int y) {
+ if ((x ^ y) != 3)
+ return;
+ clang_analyzer_eval(-(x ^ y) == -3); // expected-warning{{TRUE}}
+ clang_analyzer_eval(-(y ^ x) == -3); // expected-warning{{TRUE}}
}
int test_fp(int flag) {
|
|
@llvm/pr-subscribers-clang-static-analyzer-1 Author: Balazs Benics (steakhal) ChangesThis patch should not introduce much overhead as it only does one more constraint map lookup, which is really quick. Depends on #112583 Full diff: https://github.com/llvm/llvm-project/pull/112887.diff 2 Files Affected:
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index ecf7974c838650..f0311b7028f56d 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1249,6 +1249,8 @@ class SymbolicRangeInferrer
// calculate the effective range set by intersecting the range set
// for A - B and the negated range set of B - A.
getRangeForNegatedSymSym(SSE),
+ // If commutative, we may have constaints for the commuted variant.
+ getRangeCommutativeSymSym(SSE),
// If Sym is a comparison expression (except <=>),
// find any other comparisons with the same operands.
// See function description.
@@ -1485,6 +1487,21 @@ class SymbolicRangeInferrer
Sym->getType());
}
+ std::optional<RangeSet> getRangeCommutativeSymSym(const SymSymExpr *SSE) {
+ auto Op = SSE->getOpcode();
+ bool IsCommutative = llvm::is_contained(
+ // ==, !=, |, &, +, *, ^
+ {BO_EQ, BO_NE, BO_Or, BO_And, BO_Add, BO_Mul, BO_Xor}, Op);
+ if (!IsCommutative)
+ return std::nullopt;
+
+ SymbolRef Commuted = State->getSymbolManager().getSymSymExpr(
+ SSE->getRHS(), Op, SSE->getLHS(), SSE->getType());
+ if (const RangeSet *Range = getConstraint(State, Commuted))
+ return *Range;
+ return std::nullopt;
+ }
+
// Returns ranges only for binary comparison operators (except <=>)
// when left and right operands are symbolic values.
// Finds any other comparisons with the same operands.
diff --git a/clang/test/Analysis/unary-sym-expr.c b/clang/test/Analysis/unary-sym-expr.c
index 7c4774f3cca82f..92e11b295bee7c 100644
--- a/clang/test/Analysis/unary-sym-expr.c
+++ b/clang/test/Analysis/unary-sym-expr.c
@@ -29,12 +29,39 @@ int test(int x, int y) {
return 42;
}
-void test_svalbuilder_simplification(int x, int y) {
+void test_svalbuilder_simplification_add(int x, int y) {
if (x + y != 3)
return;
clang_analyzer_eval(-(x + y) == -3); // expected-warning{{TRUE}}
- // FIXME Commutativity is not supported yet.
- clang_analyzer_eval(-(y + x) == -3); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(-(y + x) == -3); // expected-warning{{TRUE}}
+}
+
+void test_svalbuilder_simplification_mul(int x, int y) {
+ if (x * y != 3)
+ return;
+ clang_analyzer_eval(-(x * y) == -3); // expected-warning{{TRUE}}
+ clang_analyzer_eval(-(y * x) == -3); // expected-warning{{TRUE}}
+}
+
+void test_svalbuilder_simplification_and(int x, int y) {
+ if ((x & y) != 3)
+ return;
+ clang_analyzer_eval(-(x & y) == -3); // expected-warning{{TRUE}}
+ clang_analyzer_eval(-(y & x) == -3); // expected-warning{{TRUE}}
+}
+
+void test_svalbuilder_simplification_or(int x, int y) {
+ if ((x | y) != 3)
+ return;
+ clang_analyzer_eval(-(x | y) == -3); // expected-warning{{TRUE}}
+ clang_analyzer_eval(-(y | x) == -3); // expected-warning{{TRUE}}
+}
+
+void test_svalbuilder_simplification_xor(int x, int y) {
+ if ((x ^ y) != 3)
+ return;
+ clang_analyzer_eval(-(x ^ y) == -3); // expected-warning{{TRUE}}
+ clang_analyzer_eval(-(y ^ x) == -3); // expected-warning{{TRUE}}
}
int test_fp(int flag) {
|
|
This was already reviewed in the linked PR. I just need a separate PR to merge multiple commits, as rebase-merges are not allowed on llvm. |
NagyDonat
approved these changes
Oct 18, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This patch should not introduce much overhead as it only does one more constraint map lookup, which is really quick.
Depends on #112583