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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.



In D102696#2766337 <https://reviews.llvm.org/D102696#2766337>, @NoQ wrote:

> Ok so the state has enough constraints. It's enough to know that `$x + $y == 0` and `$y == 0` in order to deduce that `$x + 0 == 0`. But you're saying that we don't know how to infer it so instead of making us able to infer it let's make us ask the solver easier questions. That's a terrible hack but at this point i think we might as well take it. @vsavchenko WDYT, what would it take to fix the solver instead?

Actually, the problem is more subtle than that. The solver is already capable of solving such equations, the below test passes on the main branch:

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

However, we can generalize the original problem, by using 3 variables. In this case no solver is capable of solving b/c we simply don't have enough equations:

  int test(int x, int y, int z) {
    if (x + y + z != 0)
      return 0;
    if (z != 0)
      return 0;
    clang_analyzer_eval(x + y + z == 0);  // UNKNOWN !
    clang_analyzer_eval(z == 0);          // OK.
    return 0;
  }

The crux of the problem is that we don't ask the right question from the solver because we are literally unable to ask the right question (as of main). The solver takes an SVal (more precisely a symbolic expression) and can give back the related ranges or a concrete value.
We can see that the constraints are there, and they are correct:

  "constraints": [
     { "symbol": "reg_$1<int z>", "range": "{ [0, 0] }" },
     { "symbol": "(reg_$0<int x>) + (reg_$1<int y>) + (reg_$1<int z>)", "range": "{ [0, 0] }" }
   ],

However, we never try to query "(reg_$0<int x>) + (reg_$1<int y>) + (reg_$1<int z>)", instead we ask the solver separately with "(reg_$0<int x>)", "(reg_$0<int y>)" and with ""(reg_$0<int z>)". This is because of how we bind the SVals to the expressions and because of the "constant folding" like mechanism encoded in `getKnownValue` and in `simplifySVal`. And, we had bound the ConcreteInt 0 to the ImplicitCastExpr of 'z', previously and this fuels the "constant folding" mechanism (which is very useful in most cases but causes this logical error).


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D102696/new/

https://reviews.llvm.org/D102696