[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

[Gabor Marton via Phabricator via cfe-commits]

martong created this revision.
martong added reviewers: NoQ, steakhal, ASDenysPetrov, Szelethus, xazax.hun.
Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware.
Herald added a project: All.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

In some cases a parent State is already infeasible, but we recognize
this only if an additonal constraint is added. This patch is the first
of a series to address this issue. In this patch `assumeDual` is changed
to clone the parent State but with an `Infeasible` flag set, and this
infeasible-parent is returned both for the true and false case. Then
when we add a new transition in the exploded graph and the destination
is marked as infeasible, the node will be a sink node.

Related bug:
https://github.com/llvm/llvm-project/issues/50883
Actually, this patch does not solve that bug in the solver, rather with
this patch we can handle the general parent-infeasible cases.

Next step would be to change the State API and require all checkers to
use the `assume*Dual` API and deprecate the simple `assume` calls.

Hopefully, the next patch will introduce `assumeInBoundDual` and will
solve the CRASH we have here:
https://github.com/llvm/llvm-project/issues/54272


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D124674

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/ProgramState.cpp
  clang/test/Analysis/sink-infeasible.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D124674.426061.patch
Type: text/x-patch
Size: 7252 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220429/91308f55/attachment.bin>