[PATCH] D104844: [Analyzer][solver] Fix crashes during symbol simplification

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

In D104844#2838674 <https://reviews.llvm.org/D104844#2838674>, @martong wrote:

>> I don't really get why we get not simplified symbol to begin with.
>
> This is because of the Environment bindings. I.e.` b1` is bound to `$a0 - $b0 + $c` when we evaluate `int b1 = (unsigned)a1 + c;`. This binding is not changed/updated, so when we evaluate the division then we query the DeclRefExpr for `b1` from the Environment and that gives still `$a0 - $b0 + $c`. We either do the simplification in the ConstraintManager (as we do now with this and the parent patch) or perhaps we could try to simplify the Environment bindings as an alternative solution.

Yeah, I remember now, thanks!



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2314-2315
 
+  if (SymbolRef SimplifiedSym = simplify(St, Sym))
+    Sym = SimplifiedSym;
+
----------------
martong wrote:
> vsavchenko wrote:
> > I don't like the idea of duplicating it into every `assume` method.  This way we drastically increase our chances to forget it (like you did with `assumeSymGE` and `assumeSymLE`).
> > I think the better place for it is in `RangedConstraintManager::assumeSymRel` and neighboring methods, though still not perfect.
> > I don't really get why we get not simplified symbol to begin with.
> > 
> `assumeSymRel` is not enough, because e.g. `assumeSymGE` is called also e.g. from `assumeSymUnsupported`. Perhaps we could change the signature of `assumeSymEQ/NE/GT/GE/LT/LE` to take an auxiliary `Simplifier` wrapper object instead of `SymbolRef`?
> 
> ```
>   ProgramStateRef assumeSymNE(ProgramStateRef State, Simplifier S,
>                                       const llvm::APSInt &V,
>                                       const llvm::APSInt &Adjustment);
> 
> ```
> And for the Simplifier something like:
> ```
> struct Simplifier {
>   SymbolRef SimplifiedSym = nullptr;
>   Simplifier(SymbolRef Sym) : SimplifiedSym(simplify(Sym)) {}
>   
> };
> ```
> 
> assumeSymRel is not enough, because e.g. assumeSymGE is called also e.g. from assumeSymUnsupported. 
Yep, that's why I suggested `assumeSymRel` and its neighbors.  I actually think that three top-level public methods from `RangedConstraintManager` will do: `assumeSym`, `assumeSymInclusiveRange`, and `assumeSymUnsupported`.


We can't really change the signatures of those methods because we'll be introducing this functionality into solvers that didn't sign up for this (and don't need it).

Also we can least put this `if` statement inside of `simplify`, so we can use it like this: `Sym = simplify(St, Sym);`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D104844