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