[clang] [analyzer][Solver] Early return if sym is concrete on assuming (PR #115579)
Ding Fei via cfe-commits
cfe-commits at lists.llvm.org
Thu Nov 14 09:11:20 PST 2024
https://github.com/danix800 updated https://github.com/llvm/llvm-project/pull/115579
>From 19b47c6ad25453c6be74bfd4cbdb7bc7eeed401c Mon Sep 17 00:00:00 2001
From: dingfei <fding at feysh.com>
Date: Sat, 9 Nov 2024 10:28:59 +0800
Subject: [PATCH 1/4] [StaticAnalyzer] early return if sym is concrete on
assuming
This could deduce some complex syms derived from simple ones whose
values could be constrainted to be concrete during execution, thus
reducing some overconstrainted states.
This commit also fix 'unix.StdCLibraryFunctions' crash due to these
overconstrainted states being added to the graph, which is marked as
sink node (PosteriorlyOverconstrained). The 'assume' API is used in
non-dual style so the checker should protectively test whether these
newly added nodes are actually impossible.
---
.../Checkers/StdLibraryFunctionsChecker.cpp | 2 ++
.../StaticAnalyzer/Core/ConstraintManager.cpp | 2 +-
.../Core/RangedConstraintManager.cpp | 9 ++++-
.../solver-sym-simplification-on-assumption.c | 31 +++++++++++++++++
...ions-bufsize-nocrash-with-correct-solver.c | 33 +++++++++++++++++++
...simplification-fixpoint-two-iterations.cpp | 6 ++--
6 files changed, 78 insertions(+), 5 deletions(-)
create mode 100644 clang/test/Analysis/solver-sym-simplification-on-assumption.c
create mode 100644 clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
diff --git a/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
index 4f30b2a0e7e7da..5faaf9cf274531 100644
--- a/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
@@ -1354,6 +1354,8 @@ void StdLibraryFunctionsChecker::checkPreCall(const CallEvent &Call,
if (BR.isInteresting(ArgSVal))
OS << Msg;
}));
+ if (NewNode->isSink())
+ break;
}
}
}
diff --git a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
index c0b3f346b654df..2b77167fab86f2 100644
--- a/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -74,7 +74,7 @@ ConstraintManager::assumeDualImpl(ProgramStateRef &State,
// it might happen that a Checker uncoditionally uses one of them if the
// other is a nullptr. This may also happen with the non-dual and
// adjacent `assume(true)` and `assume(false)` calls. By implementing
- // assume in therms of assumeDual, we can keep our API contract there as
+ // assume in terms of assumeDual, we can keep our API contract there as
// well.
return ProgramStatePair(StInfeasible, StInfeasible);
}
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index 4bbe933be2129e..cc2280faa6f730 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -23,7 +23,14 @@ RangedConstraintManager::~RangedConstraintManager() {}
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
SymbolRef Sym,
bool Assumption) {
- Sym = simplify(State, Sym);
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
+ if (SimplifiedVal.isConstant()) {
+ bool Feasible = SimplifiedVal.isZeroConstant() ? !Assumption : Assumption;
+ return Feasible ? State : nullptr;
+ }
+
+ if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
+ Sym = SimplifiedSym;
// Handle SymbolData.
if (isa<SymbolData>(Sym))
diff --git a/clang/test/Analysis/solver-sym-simplification-on-assumption.c b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
new file mode 100644
index 00000000000000..941c584c598c52
--- /dev/null
+++ b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
@@ -0,0 +1,31 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -verify
+
+void clang_analyzer_eval(int);
+
+void test_derived_sym_simplification_on_assume(int s0, int s1) {
+ int elem = s0 + s1 + 1;
+ if (elem-- == 0) // elem = s0 + s1
+ return;
+
+ if (elem-- == 0) // elem = s0 + s1 - 1
+ return;
+
+ if (s0 < 1) // s0: [1, 2147483647]
+ return;
+ if (s1 < 1) // s0: [1, 2147483647]
+ return;
+
+ if (elem-- == 0) // elem = s0 + s1 - 2
+ return;
+
+ if (s0 > 1) // s0: [-2147483648, 0] U [1, 2147483647] => s0 = 0
+ return;
+
+ if (s1 > 1) // s1: [-2147483648, 0] U [1, 2147483647] => s1 = 0
+ return;
+
+ // elem = s0 + s1 - 2 should be 0
+ clang_analyzer_eval(elem); // expected-warning{{FALSE}}
+}
diff --git a/clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c b/clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
new file mode 100644
index 00000000000000..3b39bbe32dfc21
--- /dev/null
+++ b/clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
@@ -0,0 +1,33 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=unix.StdCLibraryFunctions \
+// RUN: -analyzer-config unix.StdCLibraryFunctions:ModelPOSIX=true \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -triple x86_64-unknown-linux-gnu \
+// RUN: -verify
+
+// expected-no-diagnostics
+
+#include "Inputs/std-c-library-functions-POSIX.h"
+
+void _add_one_to_index_C(int *indices, int *shape) {
+ int k = 1;
+ for (; k >= 0; k--)
+ if (indices[k] < shape[k])
+ indices[k]++;
+ else
+ indices[k] = 0;
+}
+
+void PyObject_CopyData_sptr(char *i, char *j, int *indices, int itemsize,
+ int *shape, struct sockaddr *restrict sa) {
+ int elements = 1;
+ for (int k = 0; k < 2; k++)
+ elements += shape[k];
+
+ // no contradiction after 3 iterations when 'elements' could be
+ // simplified to 0
+ while (elements--) {
+ _add_one_to_index_C(indices, shape);
+ getnameinfo(sa, 10, i, itemsize, i, itemsize, 0);
+ }
+}
diff --git a/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp b/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
index 679ed3fda7a7a7..3f34d9982e7c8a 100644
--- a/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
+++ b/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
@@ -28,13 +28,13 @@ void test(int a, int b, int c, int d) {
return;
clang_analyzer_printState();
// CHECK: "constraints": [
- // CHECK-NEXT: { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
+ // CHECK-NEXT: { "symbol": "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
// CHECK-NEXT: { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
// CHECK-NEXT: { "symbol": "reg_$2<int c>", "range": "{ [0, 0] }" }
// CHECK-NEXT: ],
// CHECK-NEXT: "equivalence_classes": [
- // CHECK-NEXT: [ "(reg_$0<int a>) != (reg_$3<int d>)" ],
- // CHECK-NEXT: [ "reg_$0<int a>", "reg_$3<int d>" ],
+ // CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)" ],
+ // CHECK-NEXT: [ "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$3<int d>" ],
// CHECK-NEXT: [ "reg_$2<int c>" ]
// CHECK-NEXT: ],
// CHECK-NEXT: "disequality_info": null,
>From 082e45aceae537d392f8dd815693df29f919271f Mon Sep 17 00:00:00 2001
From: dingfei <fding at feysh.com>
Date: Tue, 12 Nov 2024 10:48:31 +0800
Subject: [PATCH 2/4] dump more test details & simplify logic test expr
---
.../Core/RangedConstraintManager.cpp | 2 +-
.../solver-sym-simplification-on-assumption.c | 21 ++++++++++++-------
...ions-bufsize-nocrash-with-correct-solver.c | 16 +++++++++++---
3 files changed, 27 insertions(+), 12 deletions(-)
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index cc2280faa6f730..171b4c6392d2f8 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -25,7 +25,7 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
bool Assumption) {
SVal SimplifiedVal = simplifyToSVal(State, Sym);
if (SimplifiedVal.isConstant()) {
- bool Feasible = SimplifiedVal.isZeroConstant() ? !Assumption : Assumption;
+ bool Feasible = SimplifiedVal.isZeroConstant() != Assumption;
return Feasible ? State : nullptr;
}
diff --git a/clang/test/Analysis/solver-sym-simplification-on-assumption.c b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
index 941c584c598c52..a07edbad6ddf6c 100644
--- a/clang/test/Analysis/solver-sym-simplification-on-assumption.c
+++ b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
@@ -3,29 +3,34 @@
// RUN: -verify
void clang_analyzer_eval(int);
+void clang_analyzer_value(int);
void test_derived_sym_simplification_on_assume(int s0, int s1) {
int elem = s0 + s1 + 1;
- if (elem-- == 0) // elem = s0 + s1
+ if (elem-- == 0)
return;
- if (elem-- == 0) // elem = s0 + s1 - 1
+ if (elem-- == 0)
return;
- if (s0 < 1) // s0: [1, 2147483647]
+ if (s0 < 1)
return;
- if (s1 < 1) // s0: [1, 2147483647]
+ clang_analyzer_value(s0); // expected-warning{{[1, 2147483647]}}
+
+ if (s1 < 1)
return;
+ clang_analyzer_value(s1); // expected-warning{{[1, 2147483647]}}
- if (elem-- == 0) // elem = s0 + s1 - 2
+ if (elem-- == 0)
return;
- if (s0 > 1) // s0: [-2147483648, 0] U [1, 2147483647] => s0 = 0
+ if (s0 > 1)
return;
+ clang_analyzer_value(s0); // expected-warning{{1}}
- if (s1 > 1) // s1: [-2147483648, 0] U [1, 2147483647] => s1 = 0
+ if (s1 > 1)
return;
+ clang_analyzer_value(s1); // expected-warning{{1}}
- // elem = s0 + s1 - 2 should be 0
clang_analyzer_eval(elem); // expected-warning{{FALSE}}
}
diff --git a/clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c b/clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
index 3b39bbe32dfc21..595b8b30ee1dff 100644
--- a/clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
+++ b/clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
@@ -1,14 +1,17 @@
// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-max-loop 6 \
// RUN: -analyzer-checker=unix.StdCLibraryFunctions \
// RUN: -analyzer-config unix.StdCLibraryFunctions:ModelPOSIX=true \
// RUN: -analyzer-checker=debug.ExprInspection \
// RUN: -triple x86_64-unknown-linux-gnu \
// RUN: -verify
-// expected-no-diagnostics
-
#include "Inputs/std-c-library-functions-POSIX.h"
+void clang_analyzer_value(int);
+void clang_analyzer_warnIfReached();
+void clang_analyzer_printState();
+
void _add_one_to_index_C(int *indices, int *shape) {
int k = 1;
for (; k >= 0; k--)
@@ -26,8 +29,15 @@ void PyObject_CopyData_sptr(char *i, char *j, int *indices, int itemsize,
// no contradiction after 3 iterations when 'elements' could be
// simplified to 0
+ int iterations = 0;
while (elements--) {
+ iterations++;
_add_one_to_index_C(indices, shape);
- getnameinfo(sa, 10, i, itemsize, i, itemsize, 0);
+ getnameinfo(sa, 10, i, itemsize, i, itemsize, 0); // no crash here
+ }
+
+ if (shape[0] == 1 && shape[1] == 1 && indices[0] == 0 && indices[1] == 0) {
+ clang_analyzer_value(iterations == 3 && elements == -1);
+ // expected-warning at -1{{1}}
}
}
>From bae44da574d60830b4d73660bcdd99f7d10ad6ee Mon Sep 17 00:00:00 2001
From: dingfei <fding at feysh.com>
Date: Thu, 14 Nov 2024 08:51:15 +0800
Subject: [PATCH 3/4] fix insufficient test output matching
---
.../test/Analysis/solver-sym-simplification-on-assumption.c | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/clang/test/Analysis/solver-sym-simplification-on-assumption.c b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
index a07edbad6ddf6c..378fd407f4b768 100644
--- a/clang/test/Analysis/solver-sym-simplification-on-assumption.c
+++ b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
@@ -21,16 +21,17 @@ void test_derived_sym_simplification_on_assume(int s0, int s1) {
return;
clang_analyzer_value(s1); // expected-warning{{[1, 2147483647]}}
+ clang_analyzer_eval(elem); // expected-warning{{UNKNOWN}}
if (elem-- == 0)
return;
if (s0 > 1)
return;
- clang_analyzer_value(s0); // expected-warning{{1}}
+ clang_analyzer_eval(s0 == 1); // expected-warning{{TRUE}}
if (s1 > 1)
return;
- clang_analyzer_value(s1); // expected-warning{{1}}
+ clang_analyzer_eval(s1 == 1); // expected-warning{{TRUE}}
clang_analyzer_eval(elem); // expected-warning{{FALSE}}
}
>From 3ee424f03bb41b4d4f144e59d499418049bb46f5 Mon Sep 17 00:00:00 2001
From: dingfei <fding at feysh.com>
Date: Fri, 15 Nov 2024 01:10:41 +0800
Subject: [PATCH 4/4] pin target for fixed width of int
---
clang/test/Analysis/solver-sym-simplification-on-assumption.c | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/clang/test/Analysis/solver-sym-simplification-on-assumption.c b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
index 378fd407f4b768..c2db144b8a7244 100644
--- a/clang/test/Analysis/solver-sym-simplification-on-assumption.c
+++ b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
@@ -1,4 +1,4 @@
-// RUN: %clang_analyze_cc1 %s \
+// RUN: %clang_analyze_cc1 -triple=x86_64-unknown-linux-gnu %s \
// RUN: -analyzer-checker=debug.ExprInspection \
// RUN: -verify
More information about the cfe-commits
mailing list