GNATProve fails to catch invalid Unchecked_Conversion?

General
1

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?

2

There are several “unsafe” and “unprovable” things that GNATProve cannot detect and which would greatly hinder SPARK usability; Unchecked_Conversion is one of these. — The compiler already warns you about size mismatches in the types, and that’s about all it can do.

That said, there is the 'Valid attribute that you can look into. (Its purpose is exactly for cases like Unchecked_Conversion, streams, and memory-mapped IO where you can get a value but it might violate some constraint.)

3

Thank you for your response, I’ll have a look at the 'Valid attribute.

I was under the impression that GNATProve should be able to issue both size and bit pattern checks for all types, but upon rereading this source 's section 5.1.2 it seems that a Size aspect is indeed required to trigger any warning at all. That explains why my initial record with no size aspect completely passed GNATProve with no message about size mismatches.

I also went back and reverted the indexes for the record while keeping the Size aspect, and it seems that it does trigger in this case.

Edit: I just realized another reason why I didn’t receive any warnings from GNATProve in the first place. I had SPARK_Mode => On in the function declaration, but not in the function body…oops