I would like to use SPARK to prove that the underlying implementation uses IEEE754 for the Float type.
The approach for validation is to compare the data used by the float type with a reference byte array representation [1].
The trouble is that SPARK will not allow the address overlay for the byte array / float type.
Here’s the code:
[ platform_test.ads ]
package Platform_Test
with SPARK_Mode => On
is
function Float_Is_IEEE754 return Boolean
with Post => Float_Is_IEEE754'Result = True;
end Platform_Test;
[ platform_test.adb ]
package body Platform_Test is
function Float_Is_IEEE754 return Boolean
is
Sample : Float := 10.001;
Sample_u8 : u8_Array (1 .. 4) with Import, Address => Sample'Address;
begin
-- Validate: Reference conversion: 10.001 matches: 0x19042041 --
if Sample_u8 (1) /= 16#19# or
Sample_u8 (2) /= 16#04# or
Sample_u8 (3) /= 16#20# or
Sample_u8 (4) /= 16#41#
then
return False;
end if;
return True;
end Float_Is_IEEE754;
end Platform_Test;
gnatprove output:
platform_test.adb:4:61: high: object is unsuitable for aliasing via address clause
395 | Sample_u8 : u8_Array (1 .. 4) with Import, Address => Sample'Address;
| ^~~~~~~~~~~~~~
possible explanation: floating-point types have invalid bit patterns for SPARK
The standard does not specify endianness, so in general you cannot do it the way you described because there is no guarantee that machine endianness is same.
As I side note, I have no idea why want this, because in communication and automation we rather immediately convert IEEE 754 type to the problem space Ada type and back.
Also we never use IEEE 754 without killing non-numbers first. Like this:
type Safe_Float is new Float range Float'First..Float'Last
I have horror stories to tell about NaN slipping into the database ruining a week of mileage test (one hour of the dynamometer is about 10K EUR).
Returning to the question, the best method were to check the range since different floating-point formats have different ranges or else to check for non-numbers. Only IEEE 754 has them AFAIK.
That warning is happening because SPARK does not permit Float values to have invalid bit patterns such as NaN. Using an address clause to create a mutable alias could allow Sample to be set to an invalid bit pattern by writing certain values to Sample_u8.
If all you want to do is read the bit pattern (not write), then you can make Sample and Sample_u8constant to prevent this warning.
BTW, who said it is big or little endian? You know, some I/O terminals have bytes of IEEE 754 single precision float arranged in the most peculiar order.
Ok, so there are several things that are going to make this VERY hard to do: IIRC, the IEEE754 spec allows for either big- or little-endian implementation. So, regardless of your system architecture, you’ll have to implement for both (eg for file-reading).
I think this is referring to the problem above: proving the bit-pattern of a Float is implicitly depending on that particular implementation of IEEE754.
with Interfaces;
with Ada.Unchecked_Conversion;
package body Platform_Test is
function Float_Is_IEEE754 return Boolean is
subtype Byte is Interfaces.Unsigned_8;
use type Byte;
type Byte_List is array (1 .. 4) of Byte;
function To_Bytes is new Ada.Unchecked_Conversion (Source => Float, Target => Byte_List);
Sample : constant Float := 10.001;
List : constant Byte_List := To_Bytes (Sample);
begin -- Float_Is_IEEE754
return List = (16#19#, 16#04#, 16#20#, 16#41#);
end Float_Is_IEEE754;
end Platform_Test;
To avoid endianness issues you could use an Unsigned_32 instead of a byte array. IIUC Unsigned_32 and Float should have the same byte order on the same machine in practice.
I simplified the operation to reduce the complexity of the proof. It is interesting to note that the Unchecked_Conversion version is prove-able and the version that uses a memory overlay cannot be proved.
[ platform_test.ads ]
package Platform_Test
with SPARK_Mode => On
is
type u8 is mod 2**8;
type u8_Array is array (Natural range <>) of u8;
function Check_Representation_1 return Boolean
with Post => Check_Representation_1'Result = True;
function Check_Representation_2 return Boolean
with Post => Check_Representation_2'Result = True;
end Platform_Test;
[ platform_test.adb ]
with Ada.Unchecked_Conversion;
with Interfaces; use Interfaces;
package body Platform_Test
with SPARK_Mode => On
is
function Check_Representation_1 return Boolean
is
Sample : constant Unsigned_8 := 16#01#;
Sample_8 : constant u8_Array (1 .. 1)
with Import, Address => Sample'Address;
begin
-- Memory overlay version
if Sample_8 (1) /= 16#01# then
return False;
end if;
return True;
end Check_Representation_1;
function Check_Representation_2 return Boolean
is
type Byte is array (1 .. 1) of u8;
function To_Byte is new Ada.Unchecked_Conversion
(Source => Unsigned_8,
Target => Byte);
Sample : constant Unsigned_8 := 16#01#;
Sample_8 : constant Byte := To_Byte (Sample);
begin
-- Unchecked conversion version
if Sample_8 (1) /= 16#01# then
return False;
end if;
return True;
end Check_Representation_2;
end Platform_Test;
[ main.adb ]
with Ada.Text_IO; use Ada.Text_IO;
with Platform_Test;
procedure Main is
begin
-- Unit test
Put_Line("Check_1: " & Boolean'Image (Platform_Test.Check_Representation_1));
Put_Line("Check_2: " & Boolean'Image (Platform_Test.Check_Representation_2));
end Main;
gnatprove output:
alr exec gnatprove -P1 – gnatprove --counterexamples=on -j0 --level=4
…
platform_test.ads:8:20: high: postcondition might fail
8 | with Post => Check_Representation_1’Result = True;
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
e.g. when Check_Representation_1’Result = False
unit test output:
Check_1: TRUE
Check_2: TRUE
gnatprove version output:
alt-ergo: Alt-Ergo version 2.6.0
cvc5: This is cvc5 version 1.2.1 [git tag 1.2.1 branch HEAD]
compiled with GCC version 9.4.0
z3: Z3 version 4.13.4 - 64 bit
