https://github.com/steakhal created
https://github.com/llvm/llvm-project/pull/112887
This patch should not introduce much overhead as it only does one more
constraint map lookup, which is really quick.
Depends on #112583
>From e380dd4572c8914fbd87a812e74addba1f24304d Mon Sep 17 00:00:00 2001
From: Balazs Benics <benicsbal...@gmail.com>
Date: Wed, 16 Oct 2024 15:53:20 +0200
Subject: [PATCH] [analyzer][Solver] Teach SymbolicRangeInferrer about
commutativity (2/2)
This patch should not introduce much overhead as it only does one more
constraint map lookup, which is really quick.
---
.../Core/RangeConstraintManager.cpp | 17 ++++++++++
clang/test/Analysis/unary-sym-expr.c | 33 +++++++++++++++++--
2 files changed, 47 insertions(+), 3 deletions(-)
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) {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
