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