[27947] in Kerberos
Re: NULL ptr dereferences found with Calysto static checker
daemon@ATHENA.MIT.EDU (Domagoj Babic)
Sat Jun 16 01:25:43 2007
Message-ID: <e3684ba30706152023y5f9d9011i8540f1f1ace4dd69@mail.gmail.com>
Date: Fri, 15 Jun 2007 20:23:39 -0700
From: "Domagoj Babic" <babic.domagoj@gmail.com>
To: "Ken Raeburn" <raeburn@mit.edu>
In-Reply-To: <8DC6861C-5D7D-4D89-B648-9BD93914BFA8@mit.edu>
MIME-Version: 1.0
Content-Disposition: inline
Cc: kerberos@mit.edu
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Errors-To: kerberos-bounces@mit.edu
Hi Ken
On 6/15/07, Ken Raeburn <raeburn@mit.edu> wrote:
> On Jun 15, 2007, at 04:38, Domagoj Babic wrote:
> >> > int f(int a, int b) {
> >> > int a1;
> >> > if (a%2) { a1 = a + 1; }
> >> > else { a1 = a; }
> >> > int c = a1 * a1;
> >> > assert(c % 4 == 0);
> >> > }
> >>
> >> If I felt like being picky, I'd point out that overflow in signed
> >> integer arithmetic in C produces undefined results according to the
> >> standard, so the assertion may not be met. :-)
> >
> > If it addition overflows, a1+1=0, hence 0*0%4=0. The assertion is
> > always true. Calysto and Spear preserve the properties of 2's
> > complement
> > (bit-vector | modular arithmetic).
>
> Actually, in two's complement with wrapping signed arithmetic, the
> overflow case would be a=INT_MAX and a1=a+1=INT_MIN, which would
> still be even.
Right. For 'unsigned' you would need to use unsigned remainder, for
'signed int' signed remainder. In the first case, UINT_MAX+1=0, in the
second case INT_MAX+1=INT_MIN. Anyways, in both cases, the assertion
holds.
I made a slight mistake, saying a1+1=0, because the example obviously
requires signed remainder, while my explanation was based on unsigned
numbers. Anyways, Spear/Calysto combination handle them exactly as in
the compiled code, supporting both signed and unsigned operators (for
those operators where it actually matters).
> From what I've read, modern versions of GCC have optimizations that
> take advantage of this undefined behavior to make transformations
> that speed up the code but don't give the wrap-on-signed-overflow
> result. So, actually, proving whether or not signed arithmetic can
> overflow may also be useful...
Right. Having the correct overflow behaviour was the reason why Spear
theorem prover was designed to handle modulear arithmetic precisely.
Recent JPEG bug was probably the most famous instance of such an
overflow bug (see my MSR tech report with Madan).
I'll reply to the rest later...
Regards,
--
Domagoj Babic
http://www.domagoj.info/
________________________________________________
Kerberos mailing list Kerberos@mit.edu
https://mailman.mit.edu/mailman/listinfo/kerberos
