Hi,
I recently used Unchecked_Conversion to convert arbitrary data (i.e. an array of bytes) into a record type for a toy ELF header parser. To my knowledge, Unchecked_Conversion can be verified by gnatprove to not result in any runtime errors, by proving that the end result type does not have any invalid arrangement of bits. My code managed to pass gnatprove, but still managed to execute with erroneous behavior, corrupting the stack.
My original code is as follows. Note that the implementation of the record is wrong, since the index is incorrectly in bits instead of bytes. In addition, there are no bounds on the record (no size aspect on the record) and it doesn’t manage endian differences.
.ads:
type Elf64_Ehdr is record
e_ident : E_Ident_Array;
e_type : Elf64_Half;
e_machine : Elf64_Half;
e_version : Elf64_Word;
e_entry : Elf64_Addr;
e_phoff : Elf64_Off;
e_shoff : Elf64_Off;
e_flags : Elf64_Word;
e_ehsize : Elf64_Half;
e_phentsize : Elf64_Half;
e_phnum : Elf64_Half;
e_shentsize : Elf64_Half;
e_shnum : Elf64_Half;
e_shstrndx : Elf64_Half;
end record
with Convention => C, Alignment => 8;
-- C-compatible layout for Elf64_Ehdr.
-- Note: 'at' and 'range' are in bits.
for Elf64_Ehdr use record
e_ident at 0 range 0 .. 127; -- 0 .. 15 bytes
e_type at 128 range 0 .. 15; -- 16 .. 17 bytes
e_machine at 144 range 0 .. 15; -- 18 .. 19 bytes
e_version at 160 range 0 .. 31; -- 20 .. 23 bytes
e_entry at 192 range 0 .. 63; -- 24 .. 31 bytes
e_phoff at 256 range 0 .. 63; -- 32 .. 39 bytes
e_shoff at 320 range 0 .. 63; -- 40 .. 47 bytes
e_flags at 384 range 0 .. 31; -- 48 .. 51 bytes
e_ehsize at 416 range 0 .. 15; -- 52 .. 53 bytes
e_phentsize at 432 range 0 .. 15; -- 54 .. 55 bytes
e_phnum at 448 range 0 .. 15; -- 56 .. 57 bytes
e_shentsize at 464 range 0 .. 15; -- 58 .. 59 bytes
e_shnum at 480 range 0 .. 15; -- 60 .. 61 bytes
e_shstrndx at 496 range 0 .. 15; -- 62 .. 63 bytes
end record;
type ByteArray is array (size_t range <>) of unsigned_char;
.adb:
function GetELFHeader64 (fPath : in chars_ptr) return Elf64_Ehdr
is
bArray : constant ByteArray (1 .. 64) := ReadChunkFromMmap(fPath, 64, 0);
elfHeader64 : Elf64_Ehdr;
function ByteArrayToElf64_Ehdr_Bytes is
new Ada.Unchecked_Conversion(Source => ByteArray, Target => Elf64_Ehdr);
begin
pragma assert (bArray'First = 1);
elfHeader64 := ByteArrayToElf64_Ehdr_Bytes(bArray);
return elfHeader64;
end;
I managed to fix the bug causing UB by fixing the indices of the record, and enforce a strict size with Aspect Size => 512.
Is gnatprove intended to deal with situations like this?