SPARK Integer overflow check

Question

I have the following program:

procedure Main with SPARK_Mode is
   F : array (0 .. 10) of Integer := (0, 1, others => 0);
begin
   for I in 2 .. F'Last loop
      F (I) := F (I - 1) + F (I - 2);
   end loop;
end Main;

If I run gnatprove, I get the following result, pointing to the + sign:

medium: overflow check might fail

Does this mean that F (I - 1) could be equal to Integer'Last, and adding anything to that would overflow? If so, then is it not clear from the flow of the program that this is impossible? Or do I need to specify this with a contract? If not, then what does it mean?

A counterexample shows that indeed gnatprove in this case worries about the edges of Integer:

medium: overflow check might fail (e.g. when F = (1 => -1, others => -2147483648) and I = 2)

@JacobSparreAndersen, I think that would be true as long as `I <= 7`, and would be false otherwise. — rid, Nov 10 '17 at 20:54
Ahh. Yes. I can't remember the convergence limit for this series, but I'm sure it is possible to look it up somewhere. The trick is to convince your provers that it is correct. The easy solution would be to have `gnatprove` unroll the loop before passing it to the provers. — Jacob Sparre Andersen, Nov 11 '17 at 13:09
@JacobSparreAndersen, how can I do that? Also, wouldn't that present a problem if the upper limit of `F` would come from user input instead of being the constant `10`? — rid, Nov 11 '17 at 15:00
I think loop-unrolling is controlled by some command line parameter. And no, loop-unrolling wouldn't work if the range is dynamic. Then you have to know your math. — Jacob Sparre Andersen, Nov 11 '17 at 15:44

score 2 · Answer 1 · edited Nov 10 '17 at 21:02

2

Consider adding a loop invariant to your code. The following is an example from the book "Building High Integrity Applications with Spark".

procedure Copy_Into(Buffer : out Buffer_Type;
                    Source : in String) is
   Characters_To_Copy : Buffer.Count_Type := Maximum_Buffer_Size;
begin
   Buffer := (Others => ' '); -- Initialize to all blanks
   if Source'Length < Characters_To_Copy then
      Characters_To_Copy := Source'Length;
   end if;
   for Index in Buffer.Count_Type range 1..Characters_To_Copy loop
      pragma Loop_Invariant
        (Characters_To_Copy <= Source'Length and
         Characters_To_Copy = Characters_To_Copy'Loop_Entry);
      Buffer (Index) := Source(Source'First + (Index - 1));
   end loop;
end Copy_Into;

edited Nov 10 '17 at 21:02

rid

61,078
31
152
193

answered Nov 10 '17 at 17:37

Jim Rogers

4,822
1
11
24

I'm not sure I understand how I could use a `Loop_Invariant` for this. Can you please post an example? – rid Nov 10 '17 at 19:04
Every trip around the loop, you change the contents of `F`. You have to help the tools, but telling them something which doesn't change about `F` by taking one more trip around the loop. (Newer versions of the SPARK tools can be told to unroll short loops, thus avoiding having to think about loop invariants.) – Jacob Sparre Andersen Nov 10 '17 at 20:16
@JacobSparreAndersen, hmm, I'm thinking that the only thing that changes is the value of `F (I)`, everything else remains the same. Still, I'm not sure what I could express in a loop invariant to help the tool. – rid Nov 10 '17 at 20:59

score 2 · Answer 2 · edited Jul 28 '19 at 05:47

This is already an old question, but I would like to add an answer anyway (just for future reference).

With the advancement of provers, the example as stated in the question now proves out-the-box in GNAT CE 2019 (i.e. no loop invariant needed). A somewhat more advanced example can also be proven:

main.adb

procedure Main with SPARK_Mode is

   --  NOTE: The theoretical upper bound for N is 46 as
   --
   --              Fib (46)    <    2**31 - 1    <    Fib (47)
   --           1_836_311_903  <  2_147_483_647  <  2_971_215_073

   --  NOTE: Proved with Z3 only. Z3 is pretty good in arithmetic. Additional
   --        options for gnatprove:
   --
   --           --prover=Z3 --steps=0 --timeout=10 --report=all

   type Seq is array (Natural range <>) of Natural;

   function Fibonacci (N : Natural) return Seq with
     Pre  =>  (N in 2 .. 46),
     Post =>  (Fibonacci'Result (0) = 0)
     and then (Fibonacci'Result (1) = 1)
     and then (for all I in 2 .. N =>
                Fibonacci'Result (I) = Fibonacci'Result (I - 1) + Fibonacci'Result (I - 2));

   ---------------
   -- Fibonacci --
   ---------------

   function Fibonacci (N : Natural) return Seq is
      F : Seq (0 .. N) := (0, 1, others => 0);
   begin

      for I in 2 .. N loop

         F (I) := F (I - 1) + F (I - 2);

         pragma Loop_Invariant
           (for all J in 2 .. I =>
              F (J) = F (J - 1) + F (J - 2));

         --  NOTE: The loop invariant below helps the prover to proof the
         --        absence of overflow. It "reminds" the prover that all values
         --        from iteration 3 onwards are strictly monotonically increasing.
         --        Hence, if absence of overflow is proven in this iteration,
         --        then absence is proven for all previous iterations.

         pragma Loop_Invariant
           (for all J in 3 .. I =>
              F (J) > F (J - 1));

      end loop;

      return F;

   end Fibonacci;

begin
   null;
end Main;

score 1 · Answer 3 · edited Jul 28 '19 at 05:48

This loop invariant should work - since 2^(n-1) + 2^(n-2) < 2^n - but I can't convince the provers:

procedure Fibonacci with SPARK_Mode is
   F : array (0 .. 10) of Natural := (0      => 0,
                                      1      => 1,
                                      others => 0);
begin
   for I in 2 .. F'Last loop
      pragma Loop_Invariant
        (for all J in F'Range => F (J) < 2 ** J);

      F (I) := F (I - 1) + F (I - 2);
   end loop;
end Fibonacci;

You can probably convince the provers with a bit of manual assistance (showing how 2^(n-1) + 2^(n-2) = 2^(n-2) * (2 + 1) = 3/4 * 2^n < 2^n).

SPARK Integer overflow check

3 Answers3

Linked