SPARK 2014 and protected objects

SPARK 2014 and protected objects

[Simon Wright]

I'm struggling with a package whose spec has subprograms whose bodies
call a PO declared in the package body, which governs access to volatile
data (an SPI-connected device). gnatprove (2016) wants me to use
Abstract_State and (sometimes) Part_Of, but I can't get the syntax
right. Does anyone have any worked examples?

What I have so far is at http://pastebin.com/HGpH4xL4; the error I get
is

     1. package body PO
     2. with Refined_State => (State => (Protected_Value,
                               |
        >>> non-external state "State" cannot contain external constituents in refinement

     3.                                  Impl))
     4. is
     5.
     6.    Protected_Value : Integer := 0
     7.      with Volatile;
     8.
     9.    protected Impl is
    10.       procedure Set (Value : Integer);
    11.       procedure Get (Value : out Integer);
    12.    end Impl;

If I don't include Impl in the refined state then I get

     1. package body PO
                     |
        >>> body of package "PO" has unused hidden states
        >>> variable "Impl" defined at line 8

     2. with Refined_State => (State => (Protected_Value))
                               |
        >>> non-external state "State" cannot contain external constituents in refinement

     3. is
     4.
     5.    Protected_Value : Integer := 0
     6.      with Volatile;
     7.

(I've looked at AdaCore's Certyflie[1], but it looks as though all the
POs are in packages that they don't prove)

[1] https://github.com/AdaCore/Certyflie

Re: SPARK 2014 and protected objects

[Shark8]

On Tuesday, August 30, 2016 at 4:33:59 AM UTC-6, Simon Wright wrote:
> I'm struggling with a package whose spec has subprograms whose bodies
> call a PO declared in the package body, which governs access to volatile
> data (an SPI-connected device). gnatprove (2016) wants me to use
> Abstract_State and (sometimes) Part_Of, but I can't get the syntax
> right. Does anyone have any worked examples?
> 
> What I have so far is at http://pastebin.com/HGpH4xL4; the error I get
> is
> 
>      1. package body PO
>      2. with Refined_State => (State => (Protected_Value,
>                                |
>         >>> non-external state "State" cannot contain external constituents in refinement
> 
>      3.                                  Impl))
>      4. is
>      5.
>      6.    Protected_Value : Integer := 0
>      7.      with Volatile;
>      8.
>      9.    protected Impl is
>     10.       procedure Set (Value : Integer);
>     11.       procedure Get (Value : out Integer);
>     12.    end Impl;
> 
> If I don't include Impl in the refined state then I get
> 
>      1. package body PO
>                      |
>         >>> body of package "PO" has unused hidden states
>         >>> variable "Impl" defined at line 8
> 
>      2. with Refined_State => (State => (Protected_Value))
>                                |
>         >>> non-external state "State" cannot contain external constituents in refinement
> 
>      3. is
>      4.
>      5.    Protected_Value : Integer := 0
>      6.      with Volatile;
>      7.
> 
> (I've looked at AdaCore's Certyflie[1], but it looks as though all the
> POs are in packages that they don't prove)
> 
> [1] https://github.com/AdaCore/Certyflie

Have you tried moving "Protected_Value : Integer := 0 with Volatile;" into the protected object's private section (inside the specification)?

Re: SPARK 2014 and protected objects

[Simon Wright]

Shark8 <onewingedshark@gmail.com> writes:

> Have you tried moving "Protected_Value : Integer := 0 with Volatile;"
> into the protected object's private section (inside the
> specification)?

Like this ...

   private

      Protected_Value : Integer := 0
        with Volatile,
        Part_Of => State;

   end PO;

but I still get the problem with Impl ... so I put its spec in po.ads
similarly ... State still needs refinement, but it can't be done ...

     1. package body PO
     2. with Refined_State => (State => (Protected_Value,
                               |
        >>> non-external state "State" cannot contain external constituents in refinement

     3.                                  Impl))
     4. is

What is a non-external state?

(by the way, this is the compiler complaining, not gnatprove)

Re: SPARK 2014 and protected objects

[Simon Wright]

Simon Wright <simon@pushface.org> writes:

> What is a non-external state?

This version proves OK. Note the (State with External). I _think_ that
Protected_Value and Impl's spec, being Part_Of State, have to be in the
same declarative region (i.e. not the body).

package PO
with Spark_Mode => On,
  Abstract_State => (State with External),
  Initializes => State
is

   procedure Set (Value : Integer)
     with Depends => (State =>+ Value);

   procedure Get (Value : out Integer)
     with Depends => (State => State,
                      Value => State);

private

   Protected_Value : Integer := 0
     with Volatile,
     Part_Of => State;

   protected Impl
     with Part_Of => State
   is
      procedure Set (Value : Integer)
        with Depends => (Impl => Impl,
                         Protected_Value => Value);
      procedure Get (Value : out Integer)
        with Depends => (Impl => Impl,
                         Protected_Value => Protected_Value,
                         Value => Protected_Value);
   end Impl;

end PO;

package body PO
with Spark_Mode => On,
  Refined_State => (State => (Protected_Value,
                              Impl))
is

   procedure Set (Value : Integer) is
   begin
      Impl.Set (Value);
   end Set;

   procedure Get (Value : out Integer) is
   begin
      Impl.Get (Value);
   end Get;

   protected body Impl is
      procedure Set (Value : Integer) is
      begin
         Protected_Value := Value;
      end Set;

      procedure Get (Value : out Integer) is
      begin
         Value := Protected_Value;
      end Get;
   end Impl;

end PO;

Re: SPARK 2014 and protected objects

[Simon Wright]

Simon Wright <simon@pushface.org> writes:

> What is a non-external state?

There is a lot of Good Stuff in the SPARK Users Guide, e.g. section
5.9.5.

http://docs.adacore.com/spark2014-docs/html/ug/source/concurrency.html

Re: SPARK 2014 and protected objects

[Shark8]

Pragma Ada_2012;
Pragma Profile(Ravenscar);
Pragma Partition_Elaboration_Policy(Sequential);

package PO
with
  Spark_Mode     =>  On,
  Abstract_State => (State with External),
  Initializes    =>  State
is

   procedure Set (Value : Integer)
     with Depends => ((State =>+ Value));

   procedure Get (Value : out Integer)
     with Depends => ((Value => State, State => State));

private

   protected Impl
     with Part_Of => State
   is
      procedure Set (Value : Integer)
        with Depends => ((Impl =>+ Value));
      procedure Get (Value : out Integer)
        with Depends => (Impl => Impl, Value => Impl);

   private
	Protected_Value : Integer := 0;
   end Impl;
    
    -- GNAT doesn't allow Volatile on the protected object's with.
    Pragma Volatile(Impl);
    
end PO;

-----------------

package body PO
with Spark_Mode => On, Refined_State  => (State => Impl) is

   procedure Set (Value : Integer) is
   begin
      Impl.Set (Value);
   end Set;

   procedure Get (Value : out Integer) is
   begin
      Impl.Get (Value);
   end Get;
    
   protected body Impl is
      procedure Set (Value : Integer) is
      begin
         Protected_Value := Value;
      end Set;

      procedure Get (Value : out Integer) is
      begin
         Value := Protected_Value;
      end Get;
   end Impl;

end PO;

Re: SPARK 2014 and protected objects

[Simon Wright]

Shark8 <onewingedshark@gmail.com> writes:

>    protected Impl
>      with Part_Of => State
>    is
>       procedure Set (Value : Integer)
>         with Depends => ((Impl =>+ Value));
>       procedure Get (Value : out Integer)
>         with Depends => (Impl => Impl, Value => Impl);
>
>    private
> 	Protected_Value : Integer := 0;
>    end Impl;
>     
>     -- GNAT doesn't allow Volatile on the protected object's with.
>     Pragma Volatile(Impl);

We seem to have come up with (almost) the same solution, which gives me
confidence it's the right one. Thanks.

I had Protected_Value outside the PO because it's standing in for a
number of I/O registers communicating with devices on a shared SPI bus
via their /Chip Select lines. Not sure how to deal with the concept of
"a number of machine registers"!

Re: SPARK 2014 and protected objects

[Shark8]

On Wednesday, August 31, 2016 at 1:42:51 AM UTC-6, Simon Wright wrote:
> 
> We seem to have come up with (almost) the same solution, which gives me
> confidence it's the right one. Thanks.

You're quite welcome.
 
> I had Protected_Value outside the PO because it's standing in for a
> number of I/O registers communicating with devices on a shared SPI bus
> via their /Chip Select lines. Not sure how to deal with the concept of
> "a number of machine registers"!

Well, if they're memory-mapped registers you could use something like:
Regester_A : Word with Address => Location;

If they aren't, you may have to be a bit more complex. Perhaps something like:
Type Register is (AX, BX, CX, PC, Flags);
Subtype GP_Register is Register range AX..Register'Pred(PC);

-- Implemented w/ Machine_Code.
Procedure Read ( Item : GP_Register; Value : out Value_Type );
Procedure Write( Item : GP_Register; Value :  in Value_Type );

Re: SPARK 2014 and protected objects

[Simon Wright]

Shark8 <onewingedshark@gmail.com> writes:

>> I had Protected_Value outside the PO because it's standing in for a
>> number of I/O registers communicating with devices on a shared SPI
>> bus via their /Chip Select lines. Not sure how to deal with the
>> concept of "a number of machine registers"!
>
> Well, if they're memory-mapped registers you could use something like:
> Regester_A : Word with Address => Location;

I meant rather how I was to get SPARK to handle them. I suppose one
could detail each individual register or even bit field, but as far as I
can see most folk just turn SPARK_Mode off.

Re: SPARK 2014 and protected objects

[Shark8]

On Wednesday, August 31, 2016 at 2:55:42 PM UTC-6, Simon Wright wrote:
> Shark8 writes:
> 
> >> I had Protected_Value outside the PO because it's standing in for a
> >> number of I/O registers communicating with devices on a shared SPI
> >> bus via their /Chip Select lines. Not sure how to deal with the
> >> concept of "a number of machine registers"!
> >
> > Well, if they're memory-mapped registers you could use something like:
> > Regester_A : Word with Address => Location;
> 
> I meant rather how I was to get SPARK to handle them. I suppose one
> could detail each individual register or even bit field, but as far as I
> can see most folk just turn SPARK_Mode off.

Well, Randy just pointed out that specifying the address was/is meant for registers -- https://groups.google.com/forum/#!topic/comp.lang.ada/gPJh0r2XxcA -- so I guess it just depends on how far you want to use SPARK on them.