[llvm-dev] UB and known bits

[David Majnemer via llvm-dev]

We used to have a serious problem with isSafeToSpeculativelyExecute
utilizing computeKnownBits with division.  It'd try to prove the
denominator is non-zero to avoid division by zero but get tricked when it
was faced with a denominator whose value is produced by a lshr exact and
reason that the range of the operation must be constrained within some
bound.  However, the lshr could produce any value because it could have
been fed in undef or poison for either/both operands thus rendering the
constraint in computeKnownBits useless.  I fixed this not too long ago...

The only remaining "interesting" use is SimplifyDemandedUseBits.  It is not
far-fetched that we would remove an 'or' because we'd think it would be
redundant due to computeKnownBits reasoning that undefined behavior would
result otherwise.  However, the bit in question might actually be undef
with the 'or' being the only remaining operation keeping an undef value
from being replaced with zero.



On Tue, Sep 8, 2015 at 10:26 AM, John Regehr via llvm-dev <
llvm-dev at lists.llvm.org> wrote:

> On the subject of undefined behavior and known bits, as I'm sure some of
> you are aware, code in ValueTracking.cpp is exploiting poison value rules
> to get a bit of extra precision in the known bits. These rules fire on
> examples like the ones below.  Do we have a set of rules that clients of
> known bits need to follow to avoid unsoundness?  I remember Nuno and/or
> David Majnemer saying something about this but I don't have it handy.
>
> John
>
>
> %0:i32 = var
> %1:i32 = lshr %0, 1:i32
> %2:i32 = addnw 1:i32, %1
> infer %2
>
> known from Souper:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from compiler: 0xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> llvm is stronger
>
>
>
> %0:i32 = var (000000000000000xxxxxxxxxxxxxxxxx)
> %1:i32 = and 65535:i32, %0
> %2:i16 = var
> %3:i32 = zext %2
> %4:i32 = mulnw %1, %3
> infer %4
>
> known from Souper:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from compiler: 0xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> llvm is stronger
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20150908/3fe786ec/attachment.html>