Re: [Valgrind-developers] V-Bit Verification

[Julian S. <js...@ac...>]

On Thursday, August 02, 2012, John Reiser wrote:

> I consider that memcheck often generates incorrect V bits.

Yes.  This is by design.  There's a tradeoff between accuracy of V bit
tracking and performance.  Memcheck is designed to be accurate enough to
give a low false positive rate in real use scenarios whilst not being 
excessively slow.  It is also designed to err on the side of false
positives rather than false negatives.

If there's one single thing that Loyan's crew could usefully do, it is
to show that if a bit is marked as defined then it really is defined --
that is, demonstrate that there are no false negatives.

False positives are inconvenient and we try to minimise them, but
fundamentally are not a hindrance to using Memcheck to making software
more reliable, since they can be worked around by over-initialising
data.

False negatives are dangerous -- they cause program flaws to be missed
and there is no way to recover from that.


> Memcheck does not understand word-wide binary integer inequality.
>     !!((a ^ b) & Va & Vb) ==> (a != b)

True.  Is this a problem in practice?  I don't remember many bug reports
about this.


> Memcheck does not understand binary integer addition.  [...]

Yeah.  We know.  It leads to bug 242137.  There is a mode in which addition
is done exactly.  The problem is it is slow and is not necessary 99.9% of the
time.  It would be nice to have an intermediate-cost version which is 
accurate enough to correctly handle the underlying LLVM optimisation whilst
not being as expensive as the full version, but I'm not sure this is possible.


> Memcheck gives up if it encounters Undef bits in floating point arithmetic.

Yes.  Show me the bug reports where this causes users problems in practice.


>     (a ^ a)  ==> 0  regardless of Undef in 'a'; but memcheck ignores this

xor-with-self cases are transformed out by iropt upstream of instrumentation,
which gets rid of all such cases resulting from xoring a register with itself.


>     (x & ~x) ==> 0  regardless of Undef in 'x'; but memcheck ignores this

Mmhmh, is this really a problem in practice?

J