SPARK internal error?

SPARK internal error?

[Maciej Sobczak]

As a continuation of my previous post, here is the complete package with the array sorting exercise (not sure if it's correct):

Package spec:

pragma SPARK_Mode;

package My_Package is

    type Index is range 1 .. 10;
    type My_Array is array (Index range <>) of Integer;
    
    procedure Find_Min (A : in My_Array; I : out Index)
        with Pre => A'First <= A'Last,
             Post =>
             (I in A'Range and
                (for all J in A'Range =>
                    A (I) <= A (J)));

    procedure Min_To_Left (A : in out My_Array)
        with Pre => A'First <= A'Last,
             Post =>
             (for all I in A'Range => A (A'First) <= A (I));
        
    procedure Sort (A : in out My_Array)
        with Pre => A'First <= A'Last,
             Post =>
             (for all I in A'Range =>
                (for all J in I .. A'Last =>
                   A (I) <= A (J)));

end My_Package;


Package body:

pragma SPARK_Mode;

package body My_Package is

    procedure Find_Min (A : in My_Array; I : out Index) is
        Last_Min : Integer;
    begin
        I := A'First;
        Last_Min := A (A'First);
        
        for J in A'First + 1 .. A'Last loop

            if A (J) < Last_Min then
                I := J;
                Last_Min := A (J);
            end if;

            pragma Loop_Invariant
                (for all K in A'First .. J =>
                    I in A'First .. J and Last_Min = A (I) and Last_Min <= A (K));
        end loop;
    end Find_Min;
    
    procedure Min_To_Left (A : in out My_Array) is
        I : Index;
        Tmp : Integer;
    begin
        Find_Min (A, I);
        
        Tmp := A (A'First);
        A (A'First) := A (I);
        A (I) := Tmp;
    end Min_To_Left;
    
    procedure Sort (A : in out My_Array) is
    begin
        for I in A'Range loop
            Min_To_Left (A (I .. A'Last));
            
            pragma Loop_Invariant
                (for all J in I .. A'Last =>
                        A (I) <= A (J));
        end loop;
    end Sort;

end My_Package;

GNATprove says:

C:\maciej\temp\spark>gnatprove -Ptest -q
Internal error:
File "C:\maciej\temp\spark\gnatprove\my_package\..\my_package.mlw", line 2094, characters 208-235:
This term has type tindexB, but is expected to have type int.
 Aborting.
gprbuild: *** compilation phase failed
gnatprove: error during generation and proof of VCs, aborting.


The my_package.mlw file has explicit content and is unappropriate for Usenet publication. ;-)

Can you reproduce it? Is it a bug in the toolset?
How can I work around it?

-- 
Maciej Sobczak * http://www.inspirel.com/

Re: SPARK internal error?

[G.B.]

On 03.03.15 10:54, Maciej Sobczak wrote:
> Can you reproduce it? Is it a bug in the toolset?

Same here, on a Mac with GNAT GPL 2014.

(Looking at context in the .mlw file, the line indicated
by gnatprove (showing a VC_RANGE_CHECK of I for  A (I .. A'Last)?)
does not have the .to_int parts present on lines nearby.
I vaguely remember original SPARK conditions referring
to integer supersets. Not that this helps, I guess.)

Re: SPARK internal error?

[G.B.]

On 03.03.15 10:54, Maciej Sobczak wrote:
>      procedure Sort (A : in out My_Array) is
>      begin
>          for I in A'Range loop
>              Min_To_Left (A (I .. A'Last));
>
>              pragma Loop_Invariant
>                  (for all J in I .. A'Last =>
>                          A (I) <= A (J));
>          end loop;
>      end Sort;

The following passes and makes gnatprove produce
warning addressing range/pre/post/loop_invariant:

     procedure Sort (A : in out My_Array) is
     begin
         for I in A'Range loop
             declare
                 X : My_Array (I .. A'Last) := (others => 0);
             begin
                 for K in I .. A'Last loop
                     X (K) := A (K);
                 end loop;
                 Min_To_Left (X);
                 for K in I .. A'Last loop
                     A (K) := X (K);
                 end loop;
             end;

             pragma Loop_Invariant
                 ((for all J in I .. A'Last =>
                         A (I) <= A (J)));
         end loop;
     end Sort;

Re: SPARK internal error?

[Maciej Sobczak]

> The following passes and makes gnatprove produce
> warning addressing range/pre/post/loop_invariant:
> 
>      procedure Sort (A : in out My_Array) is
>      begin
>          for I in A'Range loop
>              declare
>                  X : My_Array (I .. A'Last) := (others => 0);

Yes, in the line above. But why? We have a precondition that guarantees there are no empty slices here - and even without it, the fact that we are within the for loop over A'Range should already guarantee that both I and A'Last have safe values. Something is wrong here.

And of course, partially sorting a temporary array does not help in the proof that the main array becomes sorted as well...

-- 
Maciej Sobczak * http://www.inspirel.com/

Re: SPARK internal error?

[Georg Bauhaus]

On 03.03.15 16:33, Maciej Sobczak wrote:
>>               declare
>> >                  X : My_Array (I .. A'Last) := (others => 0);
> Yes, in the line above.  But why?

Looking back, as SPARK originally did not permit dynamic (array) bounds,
maybe there is new circuitry in GNATprove so that, whatever is to be
diagnosed isn't properly diagnosed by the currently available implementation?

Re: SPARK internal error?

[joakim.strandberg]

On Tuesday, March 3, 2015 at 10:54:08 AM UTC+1, Maciej Sobczak wrote:
> As a continuation of my previous post, here is the complete package with the array sorting exercise (not sure if it's correct):
> 
> Package spec:
> 
> pragma SPARK_Mode;
> 
> package My_Package is
> 
>     type Index is range 1 .. 10;
>     type My_Array is array (Index range <>) of Integer;
>     
>     procedure Find_Min (A : in My_Array; I : out Index)
>         with Pre => A'First <= A'Last,
>              Post =>
>              (I in A'Range and
>                 (for all J in A'Range =>
>                     A (I) <= A (J)));
> 
>     procedure Min_To_Left (A : in out My_Array)
>         with Pre => A'First <= A'Last,
>              Post =>
>              (for all I in A'Range => A (A'First) <= A (I));
>         
>     procedure Sort (A : in out My_Array)
>         with Pre => A'First <= A'Last,
>              Post =>
>              (for all I in A'Range =>
>                 (for all J in I .. A'Last =>
>                    A (I) <= A (J)));
> 
> end My_Package;
> 
> 
> Package body:
> 
> pragma SPARK_Mode;
> 
> package body My_Package is
> 
>     procedure Find_Min (A : in My_Array; I : out Index) is
>         Last_Min : Integer;
>     begin
>         I := A'First;
>         Last_Min := A (A'First);
>         
>         for J in A'First + 1 .. A'Last loop
> 
>             if A (J) < Last_Min then
>                 I := J;
>                 Last_Min := A (J);
>             end if;
> 
>             pragma Loop_Invariant
>                 (for all K in A'First .. J =>
>                     I in A'First .. J and Last_Min = A (I) and Last_Min <= A (K));
>         end loop;
>     end Find_Min;
>     
>     procedure Min_To_Left (A : in out My_Array) is
>         I : Index;
>         Tmp : Integer;
>     begin
>         Find_Min (A, I);
>         
>         Tmp := A (A'First);
>         A (A'First) := A (I);
>         A (I) := Tmp;
>     end Min_To_Left;
>     
>     procedure Sort (A : in out My_Array) is
>     begin
>         for I in A'Range loop
>             Min_To_Left (A (I .. A'Last));
>             
>             pragma Loop_Invariant
>                 (for all J in I .. A'Last =>
>                         A (I) <= A (J));
>         end loop;
>     end Sort;
> 
> end My_Package;
> 
> GNATprove says:
> 
> C:\maciej\temp\spark>gnatprove -Ptest -q
> Internal error:
> File "C:\maciej\temp\spark\gnatprove\my_package\..\my_package.mlw", line 2094, characters 208-235:
> This term has type tindexB, but is expected to have type int.
>  Aborting.
> gprbuild: *** compilation phase failed
> gnatprove: error during generation and proof of VCs, aborting.
> 
> 
> The my_package.mlw file has explicit content and is unappropriate for Usenet publication. ;-)
> 
> Can you reproduce it? Is it a bug in the toolset?
> How can I work around it?
> 
> -- 
> Maciej Sobczak * http://www.inspirel.com/

Dear Maciej,

Your probably already know this but I have found that the SPARK mailing list is a great place to ask SPARK questions:

http://lists.forge.open-do.org/pipermail/spark2014-discuss/

It is moderated but all questions I've posted so far have been accepted and answered shockingly fast by Yannick Moy (although there are other active users there too).

Best regards,
Joakim Strandberg

Re: SPARK internal error?

[Peter Chapin]

On Tue, 3 Mar 2015, Maciej Sobczak wrote:

> As a continuation of my previous post, here is the complete package with 
> the array sorting exercise (not sure if it's correct):
>
> Package spec:
>
> [...]
>
> Package body:
>
> [...]
>
> GNATprove says:
>
> C:\maciej\temp\spark>gnatprove -Ptest -q
> Internal error:
> File "C:\maciej\temp\spark\gnatprove\my_package\..\my_package.mlw", line 2094, characters 208-235:
> This term has type tindexB, but is expected to have type int.
> Aborting.
> gprbuild: *** compilation phase failed
> gnatprove: error during generation and proof of VCs, aborting.
>
> Can you reproduce it? Is it a bug in the toolset?

Apparently. I executed gnatprove successfully on your sample code. I'm 
using version

     16.0.0w (20141212)

This is a wavefront version. As far as I know its capabilities should be 
available in SPARK GPL 2015 (I'm not an AdaCore employee so I don't know 
anything for sure about their release schedule).

BTW, I get the following message from gnatprove:

sandbox.ads:25:20: medium: postcondition might fail, requires A (I) <= A 
(J)

So it's having problems with the postcondition of Sort.

Peter