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 AuthorYannick Moy’s work focuses on software source code analysis, mostly to detect bugs or verify safety/security properties. Yannick previously worked for PolySpace (now The MathWorks) where he started the project C++ Verifier. He then joined INRIA Research Labs/Orange Labs in France to carry out a PhD on automatic modular static safety checking for C programs. Yannick joined AdaCore in 2009, after a short internship at Microsoft Research.
Yannick holds an engineering degree from the Ecole Polytechnique, an MSc from Stanford University and a PhD from Université Paris-Sud. He is a Siebel Scholar.