|
From: Florian K. <br...@ac...> - 2012-08-02 00:26:33
|
On 08/01/2012 03:08 PM, Julian Seward wrote: > Even better would be > to have a test suite, since a formal proof is a one-time thing > that becomes invalid as soon as the Memcheck code changes. > > Florian Krohm worked on tester which is at > https://bugs.kde.org/show_bug.cgi?id=300102 > Not sure of its current status though. > Dormant but not forgotten. > It would be nice to have a way to test Memcheck's V-bit > propagation through each IROp individually -- that would provide > a way to do the abovementioned regression test. This is what I do, essentially. The tester generates an asm program that tests propagation of undefinedness through a specific IROp. So you need an asm insn that maps to the IROp you want to test. If you don't have that you cannot test it. That's a limitation. It tests for each input bit of the IROp in isolation that its undefinedness propagates properly to the output bits. > This requires 2 > parts: first, a way to set and get V bits on arbitrary pieces of > memory. That is easy -- the VALGRIND_GET_VBITS and > VALGRIND_SET_VBITS client requests. > > The second thing that is required is a way to write an > instruction that passes its operands though an IROp that is > specified in a test program, and no others -- so they can be > tested individually. One way we could achieve this i to extend > the "Special" instruction mechanism (eg, see guest_amd64_toIR.c > and search for "Special") so that it will accept a > pseudo-instruction with a specified IR op in the middle of it. Interesting idea with the advantage that you don't have to retarget it. I'll keep it in mind. Florian |