From 4163136e2ee121a5d7b86cb1262a524dde4a5ec4 Mon Sep 17 00:00:00 2001 From: Ding Fei Date: Fri, 15 Nov 2024 16:43:32 +0800 Subject: [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 --- clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp') diff --git a/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp index 4f30b2a..5faaf9c 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; } } } -- cgit v1.1