[clang] [StaticAnalyzer] early return if sym is concrete on assuming (PR #115579)
Ding Fei via cfe-commits
cfe-commits at lists.llvm.org
Fri Nov 8 20:33:18 PST 2024
https://github.com/danix800 created https://github.com/llvm/llvm-project/pull/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 need to solve equivalent: https://godbolt.org/z/ed8WqsbTh
>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] [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,
More information about the cfe-commits
mailing list