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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ accepted this revision.
NoQ added inline comments.
This revision is now accepted and ready to land.


================
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:
> > > > 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.
> `a` is indeed `[11, UINT_MAX]`.
> Current implementation checks a constant (i.e. `1`) and intersects the range for LHS `[11, UINT_MAX]` with `[UINT_MIN, 1]`, which produces empty range set (aka infeasible).
> 
> This is why I'm saying that intersection is a bad choice, it's even plain wrong.
> Before this patch we ignored constraints for `a` and considered it to be `[UINT_MIN, UINT_MAX]`. In that setting, intersection does indeed work (which doesn't make it correct).
> 
> Yes, it is a regression. I'm changing this implementation in the child revisions.
> 
> 
> Yes, it is a regression. I'm changing this implementation in the child revisions.

Oh, right, got it :D

Ok, let's land 'em together then!


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D79232