[PATCH] D79232: [analyzer] Refactor range inference for symbolic expressions

[Artem Dergachev via Phabricator via cfe-commits]

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