vsavchenko marked an inline comment as done.
vsavchenko added inline comments.
================
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}}
+ }
----------------
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.
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
