[PATCH] D102696: [Analyzer] Find constraints that are directly attached to a BinOp

[Gabor Marton via Phabricator via cfe-commits]

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

Currently, if we have a constraint on a binary operand and then we add
another constraint to any of the binop's sub-expression then the first
constraint is not considered by the engine:

  int foo() {
    if (x + y != 0)
      return 0;
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} OK.
    if (y != 0)
      return 0;
    clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}} OK.
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} FAILS!
  }

Interestingly, if we constrain first y and then (x + y) then the
behaviour is what we'd normally expect:

  int foo() {
    if (y != 0)
      return 0;
    if (x + y != 0)
      return 0;
    clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}} OK.
    clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}} OK.
  }

The discrepancy stems from the underlying implementation of the engine:
In the latter case, the Environment of the current ExplodedNode has a
(x + y) -> [0, 0] binding. However, in the first case we have a [y] -> 0
binding in the current ExplodedNode, and when we build the SVal for the
(x + y) expression we simply build up the [x + 0] SVal, i.e. we never
try to find the constraint for (x + y).

In this patch, I add a StmtVisitor that builds up an SVal that
constitutes only from LValue SVals. This SVal then can be used to query
the constraint manager, this way we can find the desired constraint.

Alternative implementation could have been to traverse back in the
Exploded Graph to the Node where we can find the original binding of the
x + y expression. This seemed to be a far from ideal approach as we may
not know how far should we traverse back.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D102696

Files:
  clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
  clang/test/Analysis/find-binop-constraints.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D102696.346189.patch
Type: text/x-patch
Size: 5949 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210518/feee5132/attachment.bin>