Re: SPARK and integer arithmetic

[Florian Weimer <fw@deneb.enyo.de>]

* Simon Wright:

> $ gnatprove -P sum
> Phase 1 of 2: generation of Global contracts ...
> Phase 2 of 2: flow analysis and proof ...
> sum.ads:8:14: medium: postcondition might fail, cannot prove Add'Result = A + B (e.g. when A = 0 and Add'Result = -1 and B = 1)

Nice, that certainly looks more polished.

If I drop the pre-condition, I get a report about a failed overflow
check, which is what I expect:

sum.adb:8:16: medium: overflow check might fail (e.g. when A = -2147483648 and B = -1)

I've tried to model some of the things I'm actually dealing with (this
comes from the glibc dynamic linker).

package Sum
with SPARK_Mode
is
   
   type Address is mod 2**32;
   
   --  Used to model non-wrapping arithmetic.
   type Address_Integer is range 0 .. Address'Last;
   
   --  Approximation of struct link_map.
   type Link_Map is record
      L_Addr : Address;

      --  In the original, these fields are actually nested in an
      --  array.
      P_Vaddr : Address;
      P_Memsz : Address;
   end record
     with Dynamic_Predicate =>
       Address_Integer (L_Addr) + Address_Integer (P_Vaddr)
         + Address_Integer (P_Memsz) <= Address_Integer'Last + 1;

   function Address_Inside_Object (L : Link_Map; Addr : Address)
				  return Boolean
     with Post => Address_Inside_Object'Result 
       = ((L.L_Addr <= Addr)
          and (Address_Integer (Addr)
                 < (Address_Integer (L.L_Addr) + Address_Integer (L.P_Vaddr)
	            + Address_Integer (L.P_Memsz))));
   
end Sum;

package body Sum
with SPARK_Mode
is
   
   --  Ada translation of _dl_addr_inside_object (without the loop
   --  over l_phnum).
   function Address_Inside_Object (L : Link_Map; Addr : Address) return Boolean
   is
      Reladdr : constant Address := Addr - L.L_Addr;
   begin
      --  reladdr - l->l_phdr[n].p_vaddr < l->l_phdr[n].p_memsz
      return Reladdr - L.P_Vaddr < L.P_Memsz;
   end Address_Inside_Object;

end Sum;

I use this project file in an attempt to activate a configuration
pragma file, also shown below.

project Sum is
   for Source_Dirs use (".");
   package Compiler is
     for Local_Configuration_Pragmas use "gnat.adc";
   end Compiler;
end Sum;

--  gnat.adc
pragma Overflow_Mode (General => Strict, Assertions => Eliminated);


The intent is that I can write unbounded integer arithmetic in
predicates and post-conditions.

Not too surprisingly, gnatprove can't deal with this (I've already
been told it's beyond alt-ergo, and Z3 can only brute-force it).  But
perhaps there is a way to express the unbounded arithmetic so that
there is less work left for the prover?

The intent is to show that the transformation found in the original
sources is right.  It is related to the usual technique to eliminate
one comparison from an interval check.  More background is here:

  <https://sourceware.org/ml/libc-alpha/2016-08/msg00413.html>