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)

Alibi

Could one claim that F (I) <= 2 * I for all I? – Predecessor

@JacobSparreAndersen, I think that would be true as long as I <= 7, and would be false otherwise. – Alibi

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. – Predecessor

@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? – Alibi

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. – Predecessor

Answer 1

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;

Cazares

I'm not sure I understand how I could use a Loop_Invariant for this. Can you please post an example? – Alibi

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.) – Predecessor

@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. – Alibi

Answer 2

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;

Bioenergetics

Answer 3

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

Predecessor