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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to