Monday, September 26, 2011

Overflow and correctness

Eiffel is a programming language that strives for correctness.
In C instead most of the times speed is regarded as more important than correctness (paraphrasing a comment of Eric Sosman ).
Most Eiffel compilers use C as an intermediate language (Liberty/SmartEiffel, ISE), so a programming language striving for correctness relies on one that trade correctness for speed.
I've been thinkering about
I think we cannot blame C as this is a issue that has no "solution"; let's see a little panoramic of the efforts poured into something "as simple" as correctness in integer calculations:
Sadly there is no magic wand for this issue.
An answer may be saturation arithmetic; digging my fading knowledge of assembler, mainly from my days on 6502 I was wondering why no one seems to use the overflow flag present in almost all CPU: it seems there is no portable way to do it access it. Oh it would be so nice to write in INTEGER_GENERAL 
«infix "+" (another: like Current): like Current is external "built_in" ensure has_overflowed=False end»
I naively thought that an arithmetic overflow would have triggered a SIGFPE signal in POSIX systems. It seems I'm wrong:
    -- Test integer overflow
creation make
feature make is
        local i,j: INTEGER
            i := Maximum_integer
            j := i+1 -- SIGFPE expected
            ("i:=#(1), j=i+1=#(2)%N"# (&i) # (&j) ).print_on(std_output)
When compiled with "compile  overflow.e" Liberty Eiffel correctly says:
*** Error at Run Time ***: Require Assertion Violated.
*** Error at Run Time ***: no_overflow
3 frames in current stack.
=====  Bottom of run-time stack  =====
<system root>
Current = OVERFLOW#0x925b038
line 5 column 9 file /media/Liberty/tybor-liberty/work/tybor-sandbox/overflow.e
Current = OVERFLOW#0x925b038
i = 2147483647
j = 0
line 9 column 4 file /media/Liberty/tybor-liberty/work/tybor-sandbox/overflow.e
infix + (infix + INTEGER_32)
Current = 2147483647
other = 1
Result = 0
line 21 column 80 file /home/paolo/current-liberty/src/lib/numeric/integral.e
=====   Top of run-time stack    =====
*** Error at Run Time ***: Require Assertion Violated.
*** Error at Run Time ***: no_overflow
but when we compile it with "compile --boost overflow.e" it happily says: "i:=2147483647, j=i+1=-2147483648" which is obviously wrong. You have to compile it with "compile --boost overflow.e --cc gcc -ftrapv" to laconically receive the answer
"Received signal 6.
Eiffel program crash at run time.
No trace when using option "-boost"
Which is not what I would expect, since signal 6 is ABRT on my system.

1 comment:

  1. Well, SmartEiffel's philosophy has always been, use -boost only on a program proven correct (otherwise the behaviour is not specified).

    As you correctly noted, there are assertions in the library to protect overflows.