[clang] 4163136 - [analyzer][Solver] Early return if sym is concrete on assuming (#115579)
via cfe-commits
cfe-commits at lists.llvm.org
Fri Nov 15 00:43:36 PST 2024
Author: Ding Fei
Date: 2024-11-15T16:43:32+08:00
New Revision: 4163136e2ee121a5d7b86cb1262a524dde4a5ec4
URL: https://github.com/llvm/llvm-project/commit/4163136e2ee121a5d7b86cb1262a524dde4a5ec4
DIFF: https://github.com/llvm/llvm-project/commit/4163136e2ee121a5d7b86cb1262a524dde4a5ec4.diff
LOG: [analyzer][Solver] Early return if sym is concrete on assuming (#115579)
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.
1. The crash: https://godbolt.org/z/8KKWeKb86
2. The solver needs to solve equivalent: https://godbolt.org/z/ed8WqsbTh
Added:
clang/test/Analysis/solver-sym-simplification-on-assumption.c
clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
Modified:
clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
Removed:
################################################################################
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..171b4c6392d2f8 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;
+ 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..c2db144b8a7244
--- /dev/null
+++ b/clang/test/Analysis/solver-sym-simplification-on-assumption.c
@@ -0,0 +1,37 @@
+// RUN: %clang_analyze_cc1 -triple=x86_64-unknown-linux-gnu %s \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// 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)
+ return;
+
+ if (elem-- == 0)
+ return;
+
+ if (s0 < 1)
+ return;
+ clang_analyzer_value(s0); // expected-warning{{[1, 2147483647]}}
+
+ if (s1 < 1)
+ 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_eval(s0 == 1); // expected-warning{{TRUE}}
+
+ if (s1 > 1)
+ return;
+ clang_analyzer_eval(s1 == 1); // expected-warning{{TRUE}}
+
+ 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..595b8b30ee1dff
--- /dev/null
+++ b/clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
@@ -0,0 +1,43 @@
+// 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
+
+#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--)
+ 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
+ int iterations = 0;
+ while (elements--) {
+ iterations++;
+ _add_one_to_index_C(indices, shape);
+ 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}}
+ }
+}
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,
More information about the cfe-commits
mailing list