Gem #151 : Specifying Mathematical Properties of Programs

by Yannick Moy —AdaCore

Let's get started...

Integer overflows are exotic and dangerous beasts, that most programmers do not encounter very often, and tend to forget about. An integer overflow occurs when the result of an arithmetic computation does not fit in the machine integer type that needs to hold the result. Of course, Ada requires run-time checks to protect against integer overflows, which are enabled by the switch -gnato in GNAT. But it is common to compile without this switch for production binaries, in which case an integer overflow will result in what the Ada Reference Manual calls "erroneous behavior", which means that anything could happen (see Gems #132 to #135).

Let's consider a function Max_Payload computing the maximum payload less than a capacity Capacity that can be constructed with two items It1 and It2:

package Pack is

   type Payload is new Natural;

   function Max_Payload
     (It1, It2 : Payload;
      Capacity : Payload) return Payload;

end Pack;

The implementation of Max_Payload tries to fit the biggest payload first, and then the smallest one:

package body Pack is

   function Max_Payload
     (It1, It2 : Payload;
      Capacity : Payload) return Payload
   is
      Result : Payload := 0;
      Small  : Payload := Payload'Min (It1, It2);
      Big    : Payload := Payload'Max (It1, It2);
   begin
      if Big <= Capacity then
         Result := Big;
      end if;

      if Small <= Capacity - Result then
         Result := Result + Small;
      end if;

      return Result;
   end Max_Payload;

end Pack;

Note that the test:

      if Small <= Capacity - Result then

is written this way to avoid integer overflows, while the more natural way of writing this test:

      if Small + Result <= Capacity then  --  incorrect

is vulnerable to integer overflows, if Small + Result is larger than the maximum integer.

While it is expected to write such unnatural expressions in code in order to avoid integer overflows, we would like to write specifications (like subprogram contracts) in a more mathematical way. For example, a natural way to express the postcondition for the function Max_Payload is:

   function Max_Payload
     (It1, It2 : Payload;
      Capacity : Payload) return Payload;
     with Post =>
       Max_Payload'Result =
         (if It1 + It2 <= Capacity then It1 + It2
          elsif It1 <= Capacity and (It1 >= It2 or It2 > Capacity) then It1
          elsif It2 <= Capacity then It2
          else 0);

As contracts are executable in Ada, one can compile them as run-time assertions when passing the switch -gnata to GNAT. (For finer-grain control over execution of assertions, see Gem #149.)

Let's test the above implementation:

with Pack; use Pack;

procedure Test_Pack is
begin
   pragma Assert (Max_Payload (1, Payload'Last, 10) = 1);
end Test_Pack;

Compiling and running leads to a run-time error, because It1 + It2 does not fit in an integer:

$ gnatmake -gnata -gnato test_pack.adb
$ ./test_pack

raised CONSTRAINT_ERROR : pack.ads:10 overflow check failed

Does that mean we cannot write specifications in the most natural way? With GNAT, the answer is no, by using an alternative overflow-checking mechanism for assertions (including subprogram contracts, pragma Assert, etc.)

The idea is to use 64-bit integers (Long_Long_Integer) for arithmetic computations in assertions, to eliminate the possibility of overflow in most cases. This can be achieved either by compiling with the switch -gnato12 or by adding the following pragma in pack.adb or in a configuration file:

pragma Overflow_Mode (General => Strict, Assertions => Minimized);

Compiling and running now results in no errors:

$ gnatmake -gnata -gnato12 -s test_pack.adb
$ ./test_pack

Note that GNAT uses 64-bit integers only when they are needed, based on the knowledge of static type bounds. Another mode (Eliminated, also triggered with switch -gnato13) directs the compiler to completely remove the possibility of overflows by using a run-time library of infinite-precision integers. Finally, the alternative overflow modes can also be used for code, as well as assertions, if the user wishes. For more details on overflow modes see the GNAT User's Guide.

PS: Still not sure that the body of Max_Payload implements its contract? As the code above is in SPARK 2014, just use the tool GNATprove to prove it! That's what I did.

About the Author