Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] integer overflow

> The compiler is not being smart,
> it is being a wiseass.

I agree-- full exploitation of C's undefined behavior makes the compiler 
essentially become evil.

A few more details:

For some benchmarks -- involving tight integer loops no doubt -- 
exploiting the undefinedness of overflow gives several tens of percent 
speedup.  In a benchmark-dominated industry, this opportunity is too 
tempting to pass up.

There exist codes where undefined overflow for unsigned math gives 
similar speedups, and so there exist compilers (I can't recall which) 
that optionally provide this non-standard behavior.

Java compiler people claim that the 2's complement behavior is a serious 
obstacle to optimization of numerical Java code.

I have talked to the LLVM people and to people at ARM, and both of them 
say (informally!) that for their C compiler, signed overflow leads to 
2's complement behavior.  I believe that Frama-C's integer strategy (as 
you outlined it) is sound for these compilers.  However, both the ARM 
and LLVM people are careful to say that they reserve the right to alter 
this behavior in the future-- so it is probably a mistake to depend on it.

Other compilers, such as GCC and Intel CC, explicitly exploit the 
undefinedness of signed overflow.  As my earlier mail tried to show, 
this makes Frama-C unsound in practical situations.

Finally, note that GCC supports a "-fwrapv" command line option that 
gives 2's complement behavior for signed overflow.  Of course this ties 
the optimizer's hands a bit, but I doubt it makes much different for 
most codes.

John Regehr