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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
