SPARK 2014 Abstract_State visibility rules with generic packages

SPARK 2014 Abstract_State visibility rules with generic packages

[daniel.dmk]

Hi All,

I'm having trouble with visibility rules in GNAT with Abstract_State in a generic package. Specifically, this package is used as a argument to another generic package.

I've cut down my code into a small example that demonstrates my problem. Here's my problem in a nutshell:

I have the following generic package G1 which defines some abstract external state, as in SPARK 2014 LRM 7.1.3 and 7.1.4, and defines a procedure that uses this abstract state in Globals and Depends aspects:

   generic
      Base_Address : Natural;
   package G1
     with Abstract_State => (Register with External => Async_Writers)
   is
      
      procedure Read_Register(Value : out Natural)
        with Global => (Input => Register),
        Depends => (Value => Register);
      
   end G1;

Next, I use this package as a generic package parameter in another package as follows:

   with G1;

   generic
      with package Regs is new G1(<>);
   package G2
   is
      procedure Foo(Value : out Natural);
   end G2;
   
However, the "with package" clause in G2 generates an error in GNAT, complaining that "Register" in G1 is not visible when the package is instantiated in G2. Specifically, the error messages are:

   g2.ads:4:04: instantiation error at g1.ads:8
   g2.ads:4:04: "Register" is not visible (more references follow)
   g2.ads:4:04: instantiation error at g1.ads:8
   g2.ads:4:04: non-visible declaration at g1.ads:4
   
Can anyone provide some insight as to why the "Register" abstract state in G1 is not visible in the generic part of G2?
   
Being fairly new to Ada and SPARK, I don't fully understand the visibility rules so I guess I'm doing something illegal here but I don't quite understand what. I've been reading the Ada 2012 LRM and SPARK 2014 LRM to try and understand what is going on here. Section 7.1.4 of the SPARK 2014 LRM states:

   "State abstraction provides a mechanism for naming, in a package's visible part, state (typically a collection of variables) that will be declared within the package's body (its hidden state)."
   
So the abstract state "Register" should be in the package's visible part as far as I can tell. And indeed, I can instantiate G1 as normal and then call Read_Register:

   declare
      package X is new G1(16#4000_0000#); --  OK
      Value : Natural;
   begin
      X.Read_Register(Value); --  OK
   end
   

   
I'll provide some more insight as to what I am doing (perhaps there is a better way to do what I am trying to do).

Essentially, I am writing some code in SPARK 2014 to interface with memory-mapped peripheral registers on a microcontroller (STM32 F4 series). For some peripherals, there are several instances of the peripheral, for example, there are up to 11 GPIO peripherals (GPIO A .. K), each with the same register layout. In this case, I want to be able to define the layout of the registers, and then use this "template" to define each peripheral. 

A key point here is that I wish to use the "external state" features of SPARK 2014 (LRM 7.1.2) with the Async_Writers, Async_Readers, Effective_Writes, and Effective_Reads aspects in order to aid flow analysis. Each register in the peripheral can have different combinations of these aspects, and these aspects can only be applied to volatile *objects*. Hence, I cannot simply define a record containing all these registers (with the relevant aspects) because I would be unable to assign these aspects to each register inside the record. They can only be applied to the global volatile objects.

For this reason, I am using a generic package (like my example package G1 above) to define registers (which are hidden in the package body) along with accessor procedures to ensure that those registers are accessed correctly. I can then assign the external state aspects to each of the registers (i.e. global objects), and simply instantiate the generic package for each of the peripherals at their address. For example, using my package G1 from above:

   with G1;
   package Registers
   is
      -- Instantiate some registers
      package R1 is new G1(16#3000_0000#);
      package R2 is new G1(16#4000_0000#);
      package R3 is new G1(16#5000_0000#);
      package R4 is new G1(16#6000_0000#);
      package R5 is new G1(16#7000_0000#);
   end Registers;
   
Next, I would like to create a package containing some higher-level functionality. For example, to configure a GPIO. I would like for these procedures to be able to operate on any of the GPIOs, so I have defined the package as a generic package (like my example in G2, above) so that I can instantiate it like so:

   package R1_Functions is new G2(Registers.R1);
   package R2_Functions is new G2(Registers.R2);
   --  etc
   
However, I'm running into the problem with the visibility.

Perhaps there is a better way to achieve what I'm after?

Regards,
Daniel