[clang] [StaticAnalyzer] early return if sym is concrete on assuming (PR #115579)
via cfe-commits
cfe-commits at lists.llvm.org
Fri Nov 8 20:33:51 PST 2024
llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT-->
@llvm/pr-subscribers-clang
@llvm/pr-subscribers-clang-static-analyzer-1
Author: Ding Fei (danix800)
<details>
<summary>Changes</summary>
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
---
Full diff: https://github.com/llvm/llvm-project/pull/115579.diff
6 Files Affected:
- (modified) clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp (+2)
- (modified) clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp (+1-1)
- (modified) clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp (+8-1)
- (added) clang/test/Analysis/solver-sym-simplification-on-assumption.c (+31)
- (added) clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c (+33)
- (modified) clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp (+3-3)
``````````diff
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,
``````````
</details>
https://github.com/llvm/llvm-project/pull/115579
More information about the cfe-commits
mailing list