[all-commits] [llvm/llvm-project] f66f4d: [analyzer] Track assume call stack to detect fixpoint

[Gabor Marton via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: f66f4d3b07b2226cf14bd7a0f2056dfb2d26a89f
      https://github.com/llvm/llvm-project/commit/f66f4d3b07b2226cf14bd7a0f2056dfb2d26a89f
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2022-06-07 (Tue, 07 Jun 2022)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
    M clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
    M clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

  Log Message:
  -----------
  [analyzer] Track assume call stack to detect fixpoint

Assume functions might recurse (see `reAssume` or `tryRearrange`).
During the recursion, the State might not change anymore, that means we
reached a fixpoint. In this patch, we avoid infinite recursion of assume
calls by checking already visited States on the stack of assume function
calls. This patch renders the previous "workaround" solution (D47155)
unnecessary. Note that this is not an NFC patch. If we were to limit the
maximum stack depth of the assume calls to 1 then would it be equivalent
with the previous solution in D47155.

Additionally, in D113753, we simplify the symbols right at the beginning
of evalBinOpNN. So, a call to `simplifySVal` in `getKnownValue` (added
in D51252) is no longer needed.

Fixes https://github.com/llvm/llvm-project/issues/55851

Differential Revision: https://reviews.llvm.org/D126560