|
From: Lok K. Y. <lo...@sy...> - 2012-08-02 01:07:14
|
In our case, we use SMT2 and bitvectors to model the v-bit calculation behavior and then verify the model. Since the bitvector operations are very similar to VEX IR operations, it should not take long to convert the IR implementation into SMT2 or similar. ________________________________________ From: Florian Krohm [br...@ac...] Sent: Wednesday, August 01, 2012 8:26 PM To: Julian Seward Cc: val...@li... Subject: Re: [Valgrind-developers] V-Bit Verification 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 ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ Valgrind-developers mailing list Val...@li... https://lists.sourceforge.net/lists/listinfo/valgrind-developers |