NoQ added inline comments.
================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:340-345
+ // TODO #2: We didn't go into the nested expressions before, so it
+ // might cause us spending much more time doing the inference.
+ // This can be a problem for deeply nested expressions that are
+ // involved in conditions and get tested continuously. We definitely
+ // need to address this issue and introduce some sort of caching
+ // in here.
----------------
xazax.hun wrote:
> NoQ wrote:
> > vsavchenko wrote:
> > > NoQ wrote:
> > > > I think this is a must-have, at least in some form. We've been
> > > > exploding like this before on real-world code, well, probably not with
> > > > bitwise ops but i'm still worried.
> > > It will be pretty easy to introduce a limit on how deep we go into a tree
> > > of the given symbolic expression. That can also be a solution.
> > I mean, doing something super trivial, like defining a map from symexprs to
> > ranges in `SymbolicRangeInferrer` itself and find-or-inserting into it,
> > will probably not be harder than counting depth(?)
> I am a bit ignorant of this topic, but I wonder what a good caching mechanism
> would look like.
> A simple `symexpr -> range` mapping does not feel right as the same symexpr
> might have a different range in a different program state (e.g., we might
> learn new ranges for our symbols). But having a separate map for each state
> state might do relatively little caching?
Even a simple `symexpr -> range` mapping with lifetime of
`SymbolicRangeInferrer` should be able to improve algorithmic complexity
dramatically. And it doesn't need to consider different states because it only
lives for the duration of a single `assume()` operation.
================
Comment at: clang/test/Analysis/constant-folding.c:127-128
+ if (a > 10) {
+ clang_analyzer_eval((a & 1) <= 1); // expected-warning{{FALSE}}
+ clang_analyzer_eval((a & 1) > 1); // expected-warning{{FALSE}}
+ }
----------------
vsavchenko wrote:
> NoQ wrote:
> > vsavchenko wrote:
> > > NoQ wrote:
> > > > How can both of these be false? o.o
> > > Yeah :) I realized how weird it is.
> > > Anything is possible in the land of infeasible ranges.
> > >
> > > I changed a comment there to address this
> > I mean, this pretty much never happened before. How are you not tripping on
> > [[
> > https://github.com/llvm/llvm-project/blob/1a4421a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h#L100
> > | this assert ]]? (probably it's simply been disabled in normal debug
> > builds now that it's under "expensive checks")
> >
> > The correct thing to do is to detect the paradox earlier and mark the path
> > as infeasible. What prevents us from doing it right away here?
> Before we didn't really care about constraints on the operands and I changed
> it :)
> So, now `Intersect` (which is logically not a correct way to do what is
> meant) can cause this type of behaviour
[visible confusion]
Could you elaborate? I see that only constraint so far is `$a: [11; UINT_MAX]`.
I don't see any infeasible ranges here. `(a & 1) <= 1` is clearly true. If we
were previously thinking that it's unknown and now we think that it's false,
then it's a regression.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D79232/new/
https://reviews.llvm.org/D79232
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
