SPARK and integer arithmetic

SPARK and integer arithmetic

[Florian Weimer]

I'm trying to find out the capabilities of the SPARK when it comes to
verifying the correctness of integer arithmetic (and absence of
constraint errors).

The Barnes book (in the 2006 edition) is not really that helpful.  I'm
not even using the current SPARK tools, but the SPARK 2012 GPL
edition, but the command line options still are different from those
described in the book.

The warm-up exercise goes like this:

   package Sum is
      
      function Add (A, B : Integer) return Integer;
      --# pre 0 <= A and A <= 10 and 0 <= B and B <= 10;
      --# return A + B;
      
   end Sum;
   
   package body Sum is
      
      function Add (A, B : Integer) return Integer is
      begin
         return A + B;
      end Add;
      
   end Sum;

The SPARK configuration file contains:

   package Standard is
      type Integer is range -2147483648 .. 2147483647;
   end Standard;
   
I found the -vcg option, which causes spark the generate a sum/add.vcg
file, which shows that there is something to prove.  The sum/add.rls
contains the type range information from the configuration file.

Running sparksimp outputs:

   /home/fw/tmp/ada/arith/sum/add.vcg
      *** ERROR - The Simplifier failed.

The exit status is still zero, but I assume that this means that the
required proofs could not be performed.  Is this because the built-in
prover is not sufficiently powerful, or is there something else I can
do here (such as using an external prover)?

Re: SPARK and integer arithmetic

[Simon Wright]

Florian Weimer <fw@deneb.enyo.de> writes:

> I'm trying to find out the capabilities of the SPARK when it comes to
> verifying the correctness of integer arithmetic (and absence of
> constraint errors).
>
> The Barnes book (in the 2006 edition) is not really that helpful.  I'm
> not even using the current SPARK tools, but the SPARK 2012 GPL
> edition, but the command line options still are different from those
> described in the book.

With SPARK 2016 GPL, which of course uses different syntax, the
correctness of this piece of arithmetic is indeed verified.

package Sum
with SPARK_Mode
is

   function Add (A, B : Integer) return Integer
   with
     Pre => (A in 0 .. 10) and (B in 0 .. 10),
     Post => Add'Result = A + B;

end Sum;

package body Sum
with SPARK_Mode
is

   function Add (A, B : Integer) return Integer is
   begin
      return A - B;                              -- note the error!
   end Add;

end Sum;

$ 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)

(I'm surprised gnatprove is so tentative!)

The proof succeeds with the proper operator.

Re: SPARK and integer arithmetic

[Florian Weimer]

* 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>

Re: SPARK and integer arithmetic

[Paul Rubin]

Florian Weimer <fw@deneb.enyo.de> writes:
> 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?

I think there is some way for Spark to use Coq, which can deal with
things like that easily.  The Wikipedia article on Presburger arithmetic
also cites http://ieeexplore.ieee.org/document/6987606/?arnumber=6987606
about using (adapting?) the CVC4 SMT solver on quantifier-free
arithmetic expressions.

Re: SPARK and integer arithmetic

[Florian Weimer]

* Paul Rubin:

> Florian Weimer <fw@deneb.enyo.de> writes:
>> 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?
>
> I think there is some way for Spark to use Coq, which can deal with
> things like that easily.  The Wikipedia article on Presburger arithmetic
> also cites http://ieeexplore.ieee.org/document/6987606/?arnumber=6987606
> about using (adapting?) the CVC4 SMT solver on quantifier-free
> arithmetic expressions.

The actual formula in the program uses modular arithmetic, so I don't
think this can be represented efficiently in Presburger arithmetic.
Or am I missing something?

Re: SPARK and integer arithmetic

[Paul Rubin]

Florian Weimer <fw@deneb.enyo.de> writes:
>>> perhaps there is a way to express the unbounded arithmetic ...
> The actual formula in the program uses modular arithmetic, so I don't
> think this can be represented efficiently in Presburger arithmetic.

Oh I didn't understand, I saw the modular arithmetic in your post but
thought you wanted to change it to unbounded arithmetic.  Still though,
if the modulus is a known constant, then a=b(mod m) means a+mx=b+my for
some x and y, and multiplication by the constant m can be converted to
repeated additions with depth log2(m).  So it's still in Presburger
arithmetic, with even that seeming like overkill.

Re: SPARK and integer arithmetic

[Mark Lorenzen]

On Sunday, September 18, 2016 at 12:10:36 PM UTC+2, Florian Weimer wrote:
> I'm trying to find out the capabilities of the SPARK when it comes to
> verifying the correctness of integer arithmetic (and absence of
> constraint errors).
> 
> The Barnes book (in the 2006 edition) is not really that helpful.  I'm
> not even using the current SPARK tools, but the SPARK 2012 GPL
> edition, but the command line options still are different from those
> described in the book.

I would really like to advice you to use the latest SPARK GPL toolset and the SPARK book

https://www.amazon.co.uk/Building-High-Integrity-Applications-Spark/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1475489273&sr=8-1&keywords=high+integrity+applications

The new SPARK language and toolset are major improvements over the old ones.

Regards,

Mark L

Re: SPARK and integer arithmetic

[Florian Weimer]

* Mark Lorenzen:

> On Sunday, September 18, 2016 at 12:10:36 PM UTC+2, Florian Weimer wrote:
>> I'm trying to find out the capabilities of the SPARK when it comes to
>> verifying the correctness of integer arithmetic (and absence of
>> constraint errors).
>> 
>> The Barnes book (in the 2006 edition) is not really that helpful.  I'm
>> not even using the current SPARK tools, but the SPARK 2012 GPL
>> edition, but the command line options still are different from those
>> described in the book.
>
> I would really like to advice you to use the latest SPARK GPL toolset
> and the SPARK book
>
> https://www.amazon.co.uk/Building-High-Integrity-Applications-Spark/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1475489273&sr=8-1&keywords=high+integrity+applications
>
> The new SPARK language and toolset are major improvements over the old ones.

Indeed, but they do not cover this particular issue well (proving
correctness of wraparound arithmetic).

Re: SPARK and integer arithmetic

[moy]

Hi Florian,

Sorry for jumping in so late in the game, I just discovered your discussion yesterday. The problem you have with your specification is that it mixes modular integers with signed integers. These do not mix so easily with the provers we currently ship with GNATprove: with CVC4 and Z3, modular types are converted into bitvectors and signed integers into mathematical integers; with Alt-Ergo both are converted into mathematical integers, with modulo operations where needed. In both cases, provers have difficulties dealing with the mix. 

An easier solution here is to use 64 bits modular types as a proxy type for infinite precision integer type, given that you deal with operations that cannot exceed the bounds of a 64 bits modular integer. That way, the translation for CVC4 and Z3 is fully in bitvectors, so you have a chance to get fully automatic proof.

This is what I did, defining Address_Integer as follows:

   type Address_64 is mod 2**64;
   subtype Address_Integer is Address_64 range 0 .. Address_64(Address'Last);

Then, GNATprove produces an interesting counterexample for your postcondition:

sum.ads:26:19: medium: postcondition might fail, cannot prove Address_Inside_Object'Result = ((L.L_Addr <= Addr) and (Address_Integer (Addr) < (Address_Integer (L.L_Addr) + Address_Integer (L.P_Vaddr) + L.P_Memsz (e.g. when Addr = 1934972246 and Address_Inside_Object'Result = False and L = (L_Addr => 0, P_Vaddr => 3254779904, P_Memsz => 234881024))

You can copy-paste these values inside a test:

  with Sum; use Sum;

  procedure Test_Sum is
     Addr : Address := 1934972246;
     L : Link_Map := (L_Addr => 0, P_Vaddr => 3254779904, P_Memsz => 234881024);
     B : Boolean;
  begin
     B := Address_Inside_Object (L, Addr);
  end Test_Sum;

and check that indeed these values violate the postcondition:

  $ ./test_sum 
  raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed postcondition from sum.ads:26

The problem is that your first inequality is not the correct one, you're missing the addition of L.P_Vaddr (which you do correctly in the C version you point to in another thread). Here is a correct version of your postcondition:

     with Post => Address_Inside_Object'Result
       = ((Address_Integer (L.L_Addr) + Address_Integer (L.P_Vaddr) <= Address_Integer(Addr))
          and (Address_Integer (Addr)
                 < (Address_Integer (L.L_Addr) + Address_Integer (L.P_Vaddr)
                    + Address_Integer (L.P_Memsz))));

This version is proved automatically by GNATprove (although with a large timeout):

sum.ads:26:19: info: postcondition proved (CVC4: 2 VC in max 4.8 seconds and 6546 steps; Z3: 1 VC in max 76.5 seconds and 247567 steps)

I think we could also get GNATprove to prove your original specification, but this will require more effort to guide the proof through ghost code, possibly requiring combination of SMT solvers and static analysis, similar to what we did in this paper: http://www.spark-2014.org/entries/detail/research-corner-floating-point-computations-in-spark

Let us know if you do other similar experiments with SPARK!