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:
class OVERFLOW
    -- Test integer overflow
insert PLATFORM
creation make
feature make is
        local i,j: INTEGER
        do
            i := Maximum_integer
            j := i+1 -- SIGFPE expected
            ("i:=#(1), j=i+1=#(2)%N"# (&i) # (&j) ).print_on(std_output)
        end
    end
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
======================================
make OVERFLOW
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.


infix "#": Eiffel's printf

It's really nice to be able to write in Liberty/SmartEiffel:

("i:=#(1), j=i+1=#(2)%N"# (&i) # (&j) ).print_on(std_output)
("obviously foo := #(2), bar := #(1)%N" # &42 # &17).print_on(std_output)

which may look cryptic to most Eiffel programmers, but may look familiar when translated into C:
printf("i:=%d, j=i+1=%d\n", i,j)
printf("obviously foo := %d, bar := %d\n", 17,42)
Beside looking a little more convoluted it actually has quite a few advantages:
  • like QString::arg of Qt fame it allows positional arguments,
  • it does not rely on variable argument function calls,
  • it does not allocate an unnecessary array to hold the arguments; each call to # actually return a ROPE which does is an ABSTRACT_STRING holding references to two substrings; the prefix "&" operator returns a LAZY_STRING (praises to Adrian for good idea) which will not be converted to a string until it gets iterated over, usually printing or copying it.
  • it allows to write things like:
    local s,t,u: STRING
    do
    s := "Eiffel"; t:= "beautiful"
    u := s | " is a " |t| " language"
    assert (u.is_equal("Eiffel is a beautiful language")
    t.prepend("really ")
    assert (u.is_equal("Eiffel is a really beautiful language")
    -- which may also obtained with
    u := "#(1) is a #(2) language" # s # t
    end
  • it does retain type-safety (AFAIK)