Proof of array initialization in SPARK 2014

Proof of array initialization in SPARK 2014

[Dmitrij Novikov]

Hi,

I don't know how to cope with complex array initializations in SPARK.

When I write:

  type My_Array is array ( Positive range <> ) of Boolean;

  function Initialize return My_Array
  is
    A : My_Array(1..8); 
  begin

    A(A'Last) := False;

    for I in A'First .. A'Last - 1 loop
      A(I) := True;
    end loop;

    return A;
  end Initialize;

The SPARK Examiner gives the warning that 'A' might not be initialized.
So I tried:

  type Extended_Boolean is (Uninitialized, False, True);
  type My_Array is array ( Positive range <> ) of Extended_Boolean;
  
  function Initialize return My_Array
  is
    A : My_Array(1..8) := (others => Uninitialized);
  begin

    A(A'Last) := False;

    for I in A'First .. A'Last - 1 loop
      A(I) := True;
      pragma Loop_Invariant (for all X in A'First .. I => A(X) = True);
      pragma Loop_Invariant (A(A'Last) = False);
    end loop;

    pragma Assert( for all X in A'Range => A(X) /= Uninitialized );
    
    return A;
  end Initialize;

The initialization can be proven by the theorem prover. But I have a 
state of my type and an assignment which are only useful for proof and
useless in the executable. 
So I can go back to my first version and add:
 
  pragma Annotate (GNATprove, False_Positive,
                     " might not be initialized",
                    "Initialization proven in separate file");
                    
When there would be something like ghost states for variables and ghost 
assignments I could take the second version and write:

  type Boolean is (False, True) with Ghost_State => Uninitialized;
  
and then:
  
  A : My_Array(1..8) := (others => Uninitialized)
   with Ghost_Assignment => True;

Are there similar constructs in SPARK 2014 ?
Or is there a better way to cope with array initialization?

Re: Proof of array initialization in SPARK 2014

[ake.ragnar.dahlgren]

SPARK has problems with arrays. I would say it's a well known issue. Maybe this will change in SPARK GPL 2016? However, I suggest you do not introduce a third state but use Boolean as originally intended and initialize

    A : My_Array(1..8) := (others => False); 

Put a post condition on the Initialize function of what the expected values of  the Array should be.

Re: Proof of array initialization in SPARK 2014

[Dmitrij Novikov]

Using the aggregate the array would be initialized twice without being read between the assignments. 
I would prefer to use the Annotate pragma or is it considered bad style?

The second problem is that in some cases there might be no suitable post condition. For example when an array is initialized with values from different temperature sensors. So the array elements might have any allowed value. The only thing to prove would be that all elements of the array are covered by the assignment.

Re: Proof of array initialization in SPARK 2014

[Phil Thornley]

On Thursday, May 12, 2016 at 1:01:19 PM UTC+1, Dmitrij Novikov wrote:
> Hi,
> 
> I don't know how to cope with complex array initializations in SPARK.
> 
> When I write:
> 
>   type My_Array is array ( Positive range <> ) of Boolean;
> 
>   function Initialize return My_Array
>   is
>     A : My_Array(1..8); 
>   begin
> 
>     A(A'Last) := False;
> 
>     for I in A'First .. A'Last - 1 loop
>       A(I) := True;
>     end loop;
> 
>     return A;
>   end Initialize;
> 
> The SPARK Examiner gives the warning that 'A' might not be initialized.
> So I tried:
> 
>   type Extended_Boolean is (Uninitialized, False, True);
>   type My_Array is array ( Positive range <> ) of Extended_Boolean;
>   
>   function Initialize return My_Array
>   is
>     A : My_Array(1..8) := (others => Uninitialized);
>   begin
> 
>     A(A'Last) := False;
> 
>     for I in A'First .. A'Last - 1 loop
>       A(I) := True;
>       pragma Loop_Invariant (for all X in A'First .. I => A(X) = True);
>       pragma Loop_Invariant (A(A'Last) = False);
>     end loop;
> 
>     pragma Assert( for all X in A'Range => A(X) /= Uninitialized );
>     
>     return A;
>   end Initialize;
> 
> The initialization can be proven by the theorem prover. But I have a 
> state of my type and an assignment which are only useful for proof and
> useless in the executable. 
> So I can go back to my first version and add:
>  
>   pragma Annotate (GNATprove, False_Positive,
>                      " might not be initialized",
>                     "Initialization proven in separate file");
>                     
> When there would be something like ghost states for variables and ghost 
> assignments I could take the second version and write:
> 
>   type Boolean is (False, True) with Ghost_State => Uninitialized;
>   
> and then:
>   
>   A : My_Array(1..8) := (others => Uninitialized)
>    with Ghost_Assignment => True;
> 
> Are there similar constructs in SPARK 2014 ?
> Or is there a better way to cope with array initialization?

You could use a parallel Ghost array recording the initializations:

   function Initialize return My_Array
   is
      A : My_Array(1..8); 
      A_Is_Init : My_Array(1..8) := (others => False) with Ghost;
   begin

      A(A'Last) := False;
      A_Is_Init(A'Last) := True;

      for I in A'First .. A'Last - 1 loop
         A(I) := True;
         A_Is_Init(I) := True;
         pragma Loop_Invariant (for all J in A'First .. I => A_Is_Init(J));
         pragma Loop_Invariant (A_Is_Init(A'Last));
      end loop;

      pragma Assert (for all J in A'First .. A'Last => A_Is_Init(J));
      
      return A;
   end Initialize;

Re: Proof of array initialization in SPARK 2014

[Dmitrij Novikov]

This is a good solution. Thank you.

Re: Proof of array initialization in SPARK 2014

[rieachus]

On Thursday, May 12, 2016 at 1:01:19 PM UTC+1, Dmitrij Novikov wrote:

> I don't know how to cope with complex array initializations in SPARK.

What is wrong with?

   function Initialize return My_Array
   is
     A : My_Array(1..8) := (others => True); 
   begin 
     A(A'Last) := False; 
     return A;
   end Initialize;

This code should be faster (if that matters), but has the advantage that A is initialized before beginning the loop (that went away).

You could also assign a constant array to A.  You don't want A to be a constant, so you do need an assignment.  Or you could initialize to True, True, True, True, True, True, True, False.  But I assume that this example is a simplified version of a more complex problem.

Will the compiler generate a loop to initialize A, or build a constant into the code?  Depends on a lot of things, so what you get is what you get. ;-)  In particular, if A fits in a register and is returned on the stack you will probably get fast initialization.  It is often worth defining a bit array type:

         subtype Index is Integer range 0 .. 31;
         type Bit_Array is array (Index range <>) of Boolean;

Especially when working with hardware registers.  (Change 31 to 15 for some older hardware, and maybe 63 for some newest hardware.)

It may seem that I worry more about speed than correctness, but in hard real time (like radar) when you are bit twiddling registers inside interrupts, you want code that eliminates non-stack memory references.

Re: Proof of array initialization in SPARK 2014

[Dmitrij Novikov]

> It may seem that I worry more about speed than correctness, but in hard real time (like radar) when you are bit twiddling registers inside interrupts, you want code that eliminates non-stack memory references.

Are CPUs fast enough for hard real time applications or is it necessary to use FPGAs or ASICs? 

Re: Proof of array initialization in SPARK 2014

[Simon Wright]

Dmitrij Novikov <drr73@gmx.de> writes:

>> It may seem that I worry more about speed than correctness, but in
>> hard real time (like radar) when you are bit twiddling registers
>> inside interrupts, you want code that eliminates non-stack memory
>> references.
>
> Are CPUs fast enough for hard real time applications or is it
> necessary to use FPGAs or ASICs?

Normally hard real time systems are also fast real time systems, but
they need not be; the differentiation is that a hard real time system
*must* meet all its deadlines, according to Wikipedia[1].

Myself, I would have thought it possible for only some of the deadlines
to be hard, while others could slip (but then, maybe they wouldn't count
as *dead*lines).

[1] https://en.wikipedia.org/wiki/Real-time_computing#Criteria_for_real-time_computing

Re: Proof of array initialization in SPARK 2014

[rieachus]

On Thursday, May 19, 2016 at 2:12:49 PM UTC-4, Simon Wright wrote:
> Dmitrij Novikov writes:
> 
> >> It may seem that I worry more about speed than correctness, but in
> >> hard real time (like radar) when you are bit twiddling registers
> >> inside interrupts, you want code that eliminates non-stack memory
> >> references.
> >
> > Are CPUs fast enough for hard real time applications or is it
> > necessary to use FPGAs or ASICs?
> 
> Normally hard real time systems are also fast real time systems, but
> they need not be; the differentiation is that a hard real time system
> *must* meet all its deadlines, according to Wikipedia[1].

Correct, I prefer the definition that results that don't arrive before the deadline are wrong. It amounts to the same thing.  As for using commercial CPU chips, you very much don't want to work in virtual memory mode.  Caches if implemented nicely can be used in real-time systems, but they make measuring times very difficult.  If you can meet your deadlines with the caches disabled, and enabling the caches speeds everything up, you are good to go.  There are also some processors designed for the HRT business that have a page of addressable static RAM instead of a cache.  Extra work to figure out what goes in the fast SRAM, but much easier to prove deadlines are met.  (It's nice when you can put all of the real-time operational code and data in SRAM, and use DRAM for initialization and low-priority processes.)  

> Myself, I would have thought it possible for only some of the deadlines
> to be hard, while others could slip (but then, maybe they wouldn't count
> as *dead*lines).

It is fairly common for say an aircraft flight controller to have a number of different deadlines, with preemption used to serve the earliest deadline first.  There will also be a priority level for tasks without explicit deadlines.  It sounds simple, but for real systems you spend way more time proving you can meet the deadlines than actually writing code.

The issues involved in assigning priorities also get pretty messy during the requirements stage.  Everyone thinks their data is important but, do they really need it in 1 ms?  How about 20 ms?  Also let's say that the radar can track N hostile missiles or aircraft.  However, dealing with that data makes the controls laggy, or pushes software for the ejection seat down.  You may be better off limiting the system to N-1 or even N-2 bogies.  (Hmmm, to help you understand this:  All aspect, zero-zero ejection seats are nice.  But they need a go-no go from the flight software so that the pilot doesn't get ejected into the ground.  There may be an delay, and then the seat ejects anyway, or more likely the flight software tells the seat in advance when not to activate.  Either way, very little extra processing, but very time critical.)