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@-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, _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
