[all-commits] [llvm/llvm-project] 416313: [analyzer][Solver] Early return if sym is concrete...

[Ding Fei via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 4163136e2ee121a5d7b86cb1262a524dde4a5ec4
      https://github.com/llvm/llvm-project/commit/4163136e2ee121a5d7b86cb1262a524dde4a5ec4
  Author: Ding Fei <fding at feysh.com>
  Date:   2024-11-15 (Fri, 15 Nov 2024)

  Changed paths:
    M clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp
    M clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
    M clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
    A clang/test/Analysis/solver-sym-simplification-on-assumption.c
    A clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c
    M clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp

  Log Message:
  -----------
  [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



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications