You can subscribe to this list here.
| 2002 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
(1) |
Oct
(122) |
Nov
(152) |
Dec
(69) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2003 |
Jan
(6) |
Feb
(25) |
Mar
(73) |
Apr
(82) |
May
(24) |
Jun
(25) |
Jul
(10) |
Aug
(11) |
Sep
(10) |
Oct
(54) |
Nov
(203) |
Dec
(182) |
| 2004 |
Jan
(307) |
Feb
(305) |
Mar
(430) |
Apr
(312) |
May
(187) |
Jun
(342) |
Jul
(487) |
Aug
(637) |
Sep
(336) |
Oct
(373) |
Nov
(441) |
Dec
(210) |
| 2005 |
Jan
(385) |
Feb
(480) |
Mar
(636) |
Apr
(544) |
May
(679) |
Jun
(625) |
Jul
(810) |
Aug
(838) |
Sep
(634) |
Oct
(521) |
Nov
(965) |
Dec
(543) |
| 2006 |
Jan
(494) |
Feb
(431) |
Mar
(546) |
Apr
(411) |
May
(406) |
Jun
(322) |
Jul
(256) |
Aug
(401) |
Sep
(345) |
Oct
(542) |
Nov
(308) |
Dec
(481) |
| 2007 |
Jan
(427) |
Feb
(326) |
Mar
(367) |
Apr
(255) |
May
(244) |
Jun
(204) |
Jul
(223) |
Aug
(231) |
Sep
(354) |
Oct
(374) |
Nov
(497) |
Dec
(362) |
| 2008 |
Jan
(322) |
Feb
(482) |
Mar
(658) |
Apr
(422) |
May
(476) |
Jun
(396) |
Jul
(455) |
Aug
(267) |
Sep
(280) |
Oct
(253) |
Nov
(232) |
Dec
(304) |
| 2009 |
Jan
(486) |
Feb
(470) |
Mar
(458) |
Apr
(423) |
May
(696) |
Jun
(461) |
Jul
(551) |
Aug
(575) |
Sep
(134) |
Oct
(110) |
Nov
(157) |
Dec
(102) |
| 2010 |
Jan
(226) |
Feb
(86) |
Mar
(147) |
Apr
(117) |
May
(107) |
Jun
(203) |
Jul
(193) |
Aug
(238) |
Sep
(300) |
Oct
(246) |
Nov
(23) |
Dec
(75) |
| 2011 |
Jan
(133) |
Feb
(195) |
Mar
(315) |
Apr
(200) |
May
(267) |
Jun
(293) |
Jul
(353) |
Aug
(237) |
Sep
(278) |
Oct
(611) |
Nov
(274) |
Dec
(260) |
| 2012 |
Jan
(303) |
Feb
(391) |
Mar
(417) |
Apr
(441) |
May
(488) |
Jun
(655) |
Jul
(590) |
Aug
(610) |
Sep
(526) |
Oct
(478) |
Nov
(359) |
Dec
(372) |
| 2013 |
Jan
(467) |
Feb
(226) |
Mar
(391) |
Apr
(281) |
May
(299) |
Jun
(252) |
Jul
(311) |
Aug
(352) |
Sep
(481) |
Oct
(571) |
Nov
(222) |
Dec
(231) |
| 2014 |
Jan
(185) |
Feb
(329) |
Mar
(245) |
Apr
(238) |
May
(281) |
Jun
(399) |
Jul
(382) |
Aug
(500) |
Sep
(579) |
Oct
(435) |
Nov
(487) |
Dec
(256) |
| 2015 |
Jan
(338) |
Feb
(357) |
Mar
(330) |
Apr
(294) |
May
(191) |
Jun
(108) |
Jul
(142) |
Aug
(261) |
Sep
(190) |
Oct
(54) |
Nov
(83) |
Dec
(22) |
| 2016 |
Jan
(49) |
Feb
(89) |
Mar
(33) |
Apr
(50) |
May
(27) |
Jun
(34) |
Jul
(53) |
Aug
(53) |
Sep
(98) |
Oct
(206) |
Nov
(93) |
Dec
(53) |
| 2017 |
Jan
(65) |
Feb
(82) |
Mar
(102) |
Apr
(86) |
May
(187) |
Jun
(67) |
Jul
(23) |
Aug
(93) |
Sep
(65) |
Oct
(45) |
Nov
(35) |
Dec
(17) |
| 2018 |
Jan
(26) |
Feb
(35) |
Mar
(38) |
Apr
(32) |
May
(8) |
Jun
(43) |
Jul
(27) |
Aug
(30) |
Sep
(43) |
Oct
(42) |
Nov
(38) |
Dec
(67) |
| 2019 |
Jan
(32) |
Feb
(37) |
Mar
(53) |
Apr
(64) |
May
(49) |
Jun
(18) |
Jul
(14) |
Aug
(53) |
Sep
(25) |
Oct
(30) |
Nov
(49) |
Dec
(31) |
| 2020 |
Jan
(87) |
Feb
(45) |
Mar
(37) |
Apr
(51) |
May
(99) |
Jun
(36) |
Jul
(11) |
Aug
(14) |
Sep
(20) |
Oct
(24) |
Nov
(40) |
Dec
(23) |
| 2021 |
Jan
(14) |
Feb
(53) |
Mar
(85) |
Apr
(15) |
May
(19) |
Jun
(3) |
Jul
(14) |
Aug
(1) |
Sep
(57) |
Oct
(73) |
Nov
(56) |
Dec
(22) |
| 2022 |
Jan
(3) |
Feb
(22) |
Mar
(6) |
Apr
(55) |
May
(46) |
Jun
(39) |
Jul
(15) |
Aug
(9) |
Sep
(11) |
Oct
(34) |
Nov
(20) |
Dec
(36) |
| 2023 |
Jan
(79) |
Feb
(41) |
Mar
(99) |
Apr
(169) |
May
(48) |
Jun
(16) |
Jul
(16) |
Aug
(57) |
Sep
(32) |
Oct
|
Nov
|
Dec
|
| S | M | T | W | T | F | S |
|---|---|---|---|---|---|---|
|
|
|
|
1
(22) |
2
(32) |
3
(34) |
4
(27) |
|
5
(36) |
6
(30) |
7
(19) |
8
(30) |
9
(28) |
10
(13) |
11
(1) |
|
12
|
13
(1) |
14
(2) |
15
(14) |
16
(21) |
17
(16) |
18
(19) |
|
19
(2) |
20
(9) |
21
(19) |
22
(15) |
23
(30) |
24
(28) |
25
(22) |
|
26
(23) |
27
(18) |
28
(35) |
29
(24) |
30
(24) |
31
(16) |
|
|
From: Tom H. <to...@co...> - 2012-08-02 02:21:13
|
valgrind revision: 12810 VEX revision: 2454 C compiler: gcc (GCC) 4.6.3 20120306 (Red Hat 4.6.3-2) Assembler: GNU assembler version 2.21.53.0.1-6.fc16 20110716 C library: GNU C Library development release version 2.14.90 uname -mrs: Linux 3.4.0-1.fc17.x86_64 x86_64 Vendor version: Fedora release 16 (Verne) Nightly build on bristol ( x86_64, Fedora 16 ) Started at 2012-08-02 02:51:50 BST Ended at 2012-08-02 03:20:56 BST Results unchanged from 24 hours ago Checking out valgrind source tree ... done Configuring valgrind ... done Building valgrind ... done Running regression tests ... failed Regression test results follow == 624 tests, 3 stderr failures, 0 stdout failures, 1 stderrB failure, 2 stdoutB failures, 0 post failures == gdbserver_tests/mcinfcallWSRU (stderrB) gdbserver_tests/nlcontrolc (stdoutB) gdbserver_tests/nlpasssigalrm (stdoutB) memcheck/tests/origin5-bz2 (stderr) memcheck/tests/overlap (stderr) memcheck/tests/str_tester (stderr) |
|
From: Christian B. <bor...@de...> - 2012-08-02 02:11:59
|
valgrind revision: 12810 VEX revision: 2454 C compiler: gcc (SUSE Linux) 4.3.4 [gcc-4_3-branch revision 152973] Assembler: GNU assembler (GNU Binutils; SUSE Linux Enterprise 11) 2.20.0.20100122-0.7.9 C library: GNU C Library stable release version 2.11.1 (20100118) uname -mrs: Linux 2.6.32.59-0.7-default s390x Vendor version: Welcome to SUSE Linux Enterprise Server 11 SP1 (s390x) - Kernel %r (%t). Nightly build on sless390 ( SUSE Linux Enterprise Server 11 SP1 gcc 4.3.4 on z196 (s390x) ) Started at 2012-08-02 03:45:01 CEST Ended at 2012-08-02 04:11:49 CEST Results unchanged from 24 hours ago Checking out valgrind source tree ... done Configuring valgrind ... done Building valgrind ... done Running regression tests ... failed Regression test results follow == 555 tests, 2 stderr failures, 0 stdout failures, 0 stderrB failures, 0 stdoutB failures, 0 post failures == helgrind/tests/tc18_semabuse (stderr) helgrind/tests/tc20_verifywrap (stderr) |
|
From: Christian B. <bor...@de...> - 2012-08-02 02:04:10
|
valgrind revision: 12810 VEX revision: 2454 C compiler: gcc (GCC) 4.5.3 20110121 (Red Hat 4.5.3-5) Assembler: GNU assembler version 2.20.51.0.7-4bb6.fc13 20100318 C library: GNU C Library stable release version 2.12.1 uname -mrs: Linux 3.3.4-53.x.20120504-s390xperformance s390x Vendor version: unknown Nightly build on fedora390 ( Fedora 13/14/15 mix with gcc 3.5.3 on z196 (s390x) ) Started at 2012-08-02 03:45:01 CEST Ended at 2012-08-02 04:04:12 CEST Results unchanged from 24 hours ago Checking out valgrind source tree ... done Configuring valgrind ... done Building valgrind ... done Running regression tests ... failed Regression test results follow == 554 tests, 5 stderr failures, 0 stdout failures, 0 stderrB failures, 0 stdoutB failures, 0 post failures == helgrind/tests/tc18_semabuse (stderr) helgrind/tests/tc20_verifywrap (stderr) helgrind/tests/tc21_pthonce (stderr) helgrind/tests/tc22_exit_w_lock (stderr) drd/tests/tc21_pthonce (stderr) |
|
From: Tom H. <to...@co...> - 2012-08-02 01:54:54
|
valgrind revision: 12810 VEX revision: 2454 C compiler: gcc (GCC) 4.7.1 20120720 (Red Hat 4.7.1-5) Assembler: GNU assembler version 2.22.52.0.4-6.fc18 20120604 C library: GNU C Library stable release version 2.16 uname -mrs: Linux 3.4.0-1.fc17.x86_64 x86_64 Vendor version: Fedora release 18 (Rawhide) Nightly build on bristol ( x86_64, Fedora 18 ) Started at 2012-08-02 02:31:15 BST Ended at 2012-08-02 02:54:42 BST Results unchanged from 24 hours ago Checking out valgrind source tree ... done Configuring valgrind ... done Building valgrind ... done Running regression tests ... failed Regression test results follow == 624 tests, 6 stderr failures, 0 stdout failures, 0 stderrB failures, 0 stdoutB failures, 0 post failures == gdbserver_tests/mcinfcallRU (stderr) gdbserver_tests/mcinfcallWSRU (stderr) gdbserver_tests/mcmain_pic (stderr) memcheck/tests/origin5-bz2 (stderr) memcheck/tests/overlap (stderr) memcheck/tests/str_tester (stderr) |
|
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 |
|
From: Lok K. Y. <lo...@sy...> - 2012-08-02 00:58:07
|
Please let me preface my comments with some comments on what we have done: 1. Our formal model is for tainting, which is (should) be equivalent to "undefinedness" in memcheck. 2. Verification is also conducted for tainting. (Once again this should be equivalent to "undefinedness"). In particular, we have been successful in verifying or show that a bit that is marked as not-tainted is indeed not-tainted. We have not been successful (theorem prover times out) in verifying that something that is tainted CAN NOT be not-tainted - in all cases (e.g. this works for rotate left but not add). This means if a bit is marked as defined - then it is definitedly defined, whereas a bit that is marked as undefined can possible be defined. 3. It is important to keep in mind that there are limitations to tracking definedness (or tainting) through instructions. For example, the simple combo of a = a & ~a is very hard to capture if we are looking at undefindness per instruction. Basically the problem is that we don't know what the overall operation is until we have processed over multiple instructions. 4. We have NOT conducted any analysis on floating point units - the fundamental problem for us is we haven't found an IEEE 754 model yet. Maybe we can write our own definitions? 5. Because the V-Bit rules are generic - they might lead to false positives for some special cases. I think a good comparison is LEAKPOINT, http://www.eecis.udel.edu/~clause/research/papers/clause-orso-icse10.pdf. It is very interesting to me that their taint propagation rules (or definedness rules) are much simpler than the V-Bit rules, but for their tests they achieved the same detection rate. I am not saying that it will always remain true, but it is enlightening how simple rules can cover so many test cases. ________________________________________ From: John Reiser [jr...@bi...] Sent: Wednesday, August 01, 2012 6:33 PM To: val...@li... Subject: Re: [Valgrind-developers] V-Bit Verification On 08/01/2012 12:08 PM, Julian Seward wrote: > >> I am interested in the accuracy of the V-Bit calculations > > So am I. I consider that memcheck often generates incorrect V bits. Memcheck does not understand word-wide binary integer inequality. !!((a ^ b) & Va & Vb) ==> (a != b) [inequality at any position that has two Valid bits determines Valid inequality for the whole operation. http://bugs.kde.org/show_bug.cgi?id=117362 Summary: false positive uninit for bitfields or partial word. This bug is nearing 7 years old (filed 2005-11-30) and includes three suggested approaches for a fix.] LOK: *** From what I can see in the memcheck source code (mc_translate.c) it seems like there is already support for accurately calculating the CmpEQ and CmpNE. These rules seems correct - at least from my understanding of it, but I just need to verify that they are correct. Memcheck does not understand binary integer addition. If there is a place value [bit number] at which both operands have a Valid zero bit, then a CarryIn which propagates into that bit gets stopped (CarryOut is guaranteed to be zero), but memcheck will propagate an Undef Carry through that bit position anyway. Memcheck propagates Undef "all the way to the left" regardless of CarryStop. ----- #include <stdlib.h> #include <stdio.h> main(int argc, char *argv[]) { int *p = malloc(sizeof(int)); *p &= 0xff; /* top 24 bits of *p are Valid and zero */ int *q = malloc(sizeof(int)); *q &= 0xff; /* top 24 bits of *q are Valid and zero */ /* The top 23 bits of the sum are Valid and zero. */ if ((*p + *q) < 0) { printf("Impossible.\n"); } return 0; } ----- The complaint from memcheck [below] is incorrect. ==15496== Conditional jump or move depends on uninitialised value(s) ==15496== at 0x400585: main (memcheck-add.c:11) LOK: *** I am also a little bit confused about the carry problem since there expensiveAddSub (in mc_translate.c) seems to address the problem outlined above. The default LEFT operation does not though. Memcheck does not understand unsigned integer remainder by 2**n-1. (((a*256*256*256) + (b*256*256) + (c*256) + d) % 255) == ((a+b+c+d) % 255) >From that it can be seen that Undef "middle" bits in each of a,b,c,d do not affect the V bits for low bits of the remainder, as long as (a+b+c+d) < 255. But memcheck says that any Undef on input gives an Undef remainder. Memcheck gives up if it encounters Undef bits in floating point arithmetic. If either operand has any Undef bits, then all bits of all results are Undef. In practice for floating point compare, often this is the worst thing to do. It is very likely that the floating condition codes do not depend on a few Undef bits in either input. [Numerical analysis wouldn't exist if it did.] Almost the same can be said for floating point addition, subtraction, and multiplication: the sign, exponent and more-significant fraction bits of many particular results often do not depend on a few less-significant fraction bits. LOK: *** Floating point is hard Beyond individual operations, memcheck is blind with respect to "re-convergent fan-out". If there is any common history between the two operands, then memcheck does not care, even though the result may. (a ^ a) ==> 0 regardless of Undef in 'a'; but memcheck ignores this (x & ~x) ==> 0 regardless of Undef in 'x'; but memcheck ignores this Generally, memcheck often ignores any contribution that the actual values of Valid operand bits might make to the Valid bits of the result. That is, memcheck often believes that the V bits of the result depend only on the opcode and the V bits of the inputs, and not on the inputs themselves (in particular, the actual values of input bits that are Valid.) [If the actual shift count is all-Valid, then "shift by variable number of bits" is an exception. But if the shift count itself has any Undef bits, then memcheck says "all result bits are Undef" even though a detailed analysis might not give such a pessimistic result. Shifting by "either 2 or 3" (because of an Undef low bit in the count) need not totally destroy the output, although in this case memcheck says "every bit of the result is Undef, regardless of the actual bits and actual V bits of the other operand."] LOK: *** I agree that the pessimistic nature of the shift count being undefined means the whole result is undefined could cause problems. At the same time, it makes a lot of sense to make that tradeoff if performance is an issue. We might be able to come up with improved rules (like the ones that were defined for AND/OR/CMP/ADD/SUB) and if our model and methods turn out to be correct, then verification of these new rules is possible. -- ------------------------------------------------------------------------------ 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 |
|
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 |