Constraint_Error from arithmetic operations

Constraint_Error from arithmetic operations

[Florian Weimer]

This is somewhat related to the recent discussion on exception
contracts, but I'm more interested in what can be right now (with
current tools).

I recently browsed through Barnes' 2006 SPARK book and noticed that
SPARK has a rather drastic approach to arithmetic operations which
overflow and fail to deliver the mathematically correct result
(program termination).  The SPARK tools do not seem to be able to
statically show that arithmetic operators do not overflow, which is
obviously difficult in the general case, but should be doable with
help from the programmer.

Eventually, I hope to be able to show that protocol decoders do not
trigger arithmetic overflow due to sufficient manual checking.  (It
does not matter if this checking is actually dead code, or if the
checks are somewhat conservative, they just need to be there.)
Checking for the absence of Constraint_Error from indexed components
would be a bonus.

Re: Constraint_Error from arithmetic operations

[Phil Thornley]

In article <87r4mbrgl8.fsf@mid.deneb.enyo.de>, fw@deneb.enyo.de says...
> 
> This is somewhat related to the recent discussion on exception
> contracts, but I'm more interested in what can be right now (with
> current tools).
> 
> I recently browsed through Barnes' 2006 SPARK book and noticed that
> SPARK has a rather drastic approach to arithmetic operations which
> overflow and fail to deliver the mathematically correct result
> (program termination).  The SPARK tools do not seem to be able to
> statically show that arithmetic operators do not overflow, which is
> obviously difficult in the general case, but should be doable with
> help from the programmer.
> 
(The publication dates of the three SPARK books are 1997, 2003, and 2012 
so I'm not sure which one you mean).

I don't know how you read the any of books to get that understanding, 
but SPARK has always included the option to generate overflow checks 
(and they are now always included whenever VCs are generated).

With this code:

======================================
package P
is

   type My_Int is new Short_Integer range -20_000 .. 20_000;
   --  Short_Integer is -32768 .. 32767.

   function Op (A, B : My_Int) return My_Int;

end P;


package body P
is

   function Op (A, B : My_Int) return My_Int
   is
   begin
      return (A + B) / 2;
   end Op;

end P;
======================================

There is an unprovable VC remaining after simplification:

function_op_1.
H1:    a >= - 20000 .
H2:    a <= 20000 .
H3:    b >= - 20000 .
H4:    b <= 20000 .
H5:    my_int__size >= 0 .
       ->
C1:    a + b >= - 32768 .
C2:    a + b <= 32767 .

which comes from the overflow check on the plus operation in the return 
expression.

(You have to specify the ranges for Short_Integer of course - this is in 
the configuration file for the particular compiler you are using).

Originally the base range had to be specified using a 'base type 
assertion' but the recent versions of the language have included the use 
of derived types, as above.

Cheers,

Phil

Re: Constraint_Error from arithmetic operations

[Brian Drummond]

On Thu, 27 Dec 2012 10:33:00 +0000, Phil Thornley wrote:

> In article <87r4mbrgl8.fsf@mid.deneb.enyo.de>, fw@deneb.enyo.de says...
>> 
>> This is somewhat related to the recent discussion on exception
>> contracts, but I'm more interested in what can be right now (with
>> current tools).
>> 
>> I recently browsed through Barnes' 2006 SPARK book 

> (The publication dates of the three SPARK books are 1997, 2003, and 2012
> so I'm not sure which one you mean).

The 2003 one was reprinted (twice) in 2006 and again in 2008...
so, probably that one.

I'm curious how large the differences are for the 2012 version - at the 
moment I would have to think twice about buying it again!

- Brian

Re: Constraint_Error from arithmetic operations

[Florian Weimer]

* Phil Thornley:

> (The publication dates of the three SPARK books are 1997, 2003, and 2012 
> so I'm not sure which one you mean).

My copy says (C) 2003, 2006, it doesn't say which edition.

> I don't know how you read the any of books to get that understanding, 
> but SPARK has always included the option to generate overflow checks 
> (and they are now always included whenever VCs are generated).

I see, thanks.  The book deals with this mainly in section 11.3
("Run-time checks"), which I had not come across yet.

> Originally the base range had to be specified using a 'base type 
> assertion' but the recent versions of the language have included the use 
> of derived types, as above.

Okay, The SPARK 2011 GPL edition in Debian wheezy does not seem to
support this yet.

Anyway, I got to the point where I've got useful .siv files, but I've
hit an obstacle: I've got an array

   type Byte is mod 256;
   type Data_Array_Index is range 0 .. 2**16 - 1;
   type Data_Array is array (Data_Array_Index) of Byte;

and Data is of type Data_Array_Index, but the Examiner cannot tell
that

    element(data, [offset + 1]) >= 0

This comes from an assignment

	    Content_Length := Data_Array_Index (Data (Offset + 1));

where Content_Length has type Data_Array_Index.

Should I just avoid modular types?

Re: Constraint_Error from arithmetic operations

[Phil Thornley]

In article <87wqw3pr8e.fsf@mid.deneb.enyo.de>, fw@deneb.enyo.de says...

> Anyway, I got to the point where I've got useful .siv files, but I've
> hit an obstacle: I've got an array
> 
>    type Byte is mod 256;
>    type Data_Array_Index is range 0 .. 2**16 - 1;
>    type Data_Array is array (Data_Array_Index) of Byte;
> 
> and Data is of type Data_Array_Index, but the Examiner cannot tell
> that
> 
>     element(data, [offset + 1]) >= 0
> 
> This comes from an assignment
> 
> 	    Content_Length := Data_Array_Index (Data (Offset + 1));
> 
> where Content_Length has type Data_Array_Index.
> 
> Should I just avoid modular types?

An imported modular value will be assumed to be in range, but because 
the data are array elements, the hypothesis will be a quantified formula 
- something like:

H1:    for_all(i___1 : integer, 0 <= i___1 and i___1 <= 65535 -> 0 <= 
          element(data, [i___1]) and element(data, [i___1]) <= 255) .

The Simplifier will only be able to use this to prove
     element(data, [offset + 1]) >= 0
if it can first prove that offset + 1 is in [0, 65535].  Perhaps this is 
the problem.

Depending on the complexity of the code, it is possible that the 
conclusion is provable, but not proved by the Simplifier. (If you have 
Victor and Alt-Ergo included in the distribution then you can try using 
them to deal with provable VCs that the Simplifier doesn't prove.)

If you post SPARKable code then we can give more precise answers.

Cheers,

Phil