[PATCH] D110913: [analyzer][solver] Handle simplification to ConcreteInt

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.


================
Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h:390-396
 /// Try to simplify a given symbolic expression's associated value based on the
 /// constraints in State. This is needed because the Environment bindings are
 /// not getting updated when a new constraint is added to the State.
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);
+/// If the symbol is simplified to a constant then it returns the original
+/// symbol.
 SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
----------------
steakhal wrote:
> I'm confused about which comment corresponds to which function.
> You should also signify the difference between the two APIs.
> 
> Shouldn't be one of them an implementation detail? If so, why do we have the same visibility?
> Shouldn't be one of them an implementation detail? If so, why do we have the same visibility?

No, we use both of them. `simplify` that always returns a symbol is used e.g. in `RangedConstraintManager::assumeSym`.

And we use `simplifyToSVal` directly in `EquivalenceClass::simplify`.


================
Comment at: clang/test/Analysis/solver-sym-simplification-concreteint.c:22
+  // c == 0 --> 0 + 1 == 0 contradiction
+  clang_analyzer_eval(c == 0);    // expected-warning{{FALSE}}
+
----------------
steakhal wrote:
> Could we have an `eval(c == -1) // TRUE`?
> Also, please disable eager bifurcation to prevent state-splits in the eval arguments.
Actually,  it is `eval(c == -1) // FALSE` that holds. 

This is because after the simplification with `b==1` we have a constraint `c+1==0` but we do not reorder this equality to `c==-1`. Besides we have another constraint that we inherited from a previous State, this is `c: [0, 1]`. Now, when you query `c==-1` then the latter constraint is found, thus resulting in an infeasible state, so you'll receive `FALSE` in the warning. Actually, these are the constraints after line 19:
```
  "constraints": [
    { "symbol": "(reg_$1<int c>) + (reg_$0<int b>)", "range": "{ [0, 0] }" },
    { "symbol": "(reg_$1<int c>) + 1", "range": "{ [0, 0] }" },
    { "symbol": "reg_$0<int b>", "range": "{ [1, 1] }" },
    { "symbol": "reg_$1<int c>", "range": "{ [0, 1] }" }
  ],
```

I am considering to create a follow-up patch, where the reordering of `c+1==0` to `c==-1` is done (perhaps by reusing `RangedConstraintManager::assumeSymRel`).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D110913