pragma Import with 'Address clause

pragma Import with 'Address clause

[Lutz Donnerhacke]

A common technique to reinterpret data is:
  a : AT;
  [...]
  b : BT;
  for b'Address use a'Address;
  pragma Import(Ada, b);

Is the "pragma Import" really necessary? Of course, the ARM says, that
elaboration and definition of the imported object is externally defined. So
they are omitted from the Ada code itself.

Assume BT is a record without any default expressions. Does this mean, the
pragma can be omitted from the source code?

Background: Spark prohibits the use of Pragma Import on objects.
  

Re: pragma Import with 'Address clause

[B0966864]

The Pragma Import should not be needed. I have used the overlays and do
not have the Import statements for any of them in this case. You can
also use the syntax of
 
for b use at a'Address 

I have seen both used in ada95

Jerico

Lutz Donnerhacke wrote:
> 
> A common technique to reinterpret data is:
>   a : AT;
>   [...]
>   b : BT;
>   for b'Address use a'Address;
>   pragma Import(Ada, b);
> 
> Is the "pragma Import" really necessary? Of course, the ARM says, that
> elaboration and definition of the imported object is externally defined. So
> they are omitted from the Ada code itself.
> 
> Assume BT is a record without any default expressions. Does this mean, the
> pragma can be omitted from the source code?
> 
> Background: Spark prohibits the use of Pragma Import on objects.
>

Re: pragma Import with 'Address clause

[Stephen Leake]

Lutz Donnerhacke <lutz@iks-jena.de> writes:

> A common technique to reinterpret data is:
>   a : AT;
>   [...]
>   b : BT;
>   for b'Address use a'Address;
>   pragma Import(Ada, b);
> 
> Is the "pragma Import" really necessary? Of course, the ARM says, that
> elaboration and definition of the imported object is externally defined. So
> they are omitted from the Ada code itself.
> 
> Assume BT is a record without any default expressions. Does this mean, the
> pragma can be omitted from the source code?
> 
> Background: Spark prohibits the use of Pragma Import on objects.

I would hope Spark would prohibit the address clause as well! you are
totally defeating the Ada type system!

-- 
-- Stephe

RE: pragma Import with 'Address clause

[Beard, Frank Randolph CIV]

> The Pragma Import should not be needed.

Shouldn't be needed but isn't guaranteed.  The Pragma Import is
there to ensure the compiler doesn't initialize the data.  There
is no guarantee that the compiler won't initialize it to
something, despite the fact the data structure doesn't have a
default expression.

When we were on VAX Ada, it seemed to initialize everything within
the range of the type.  The Alsys Ada, and I think the early versions
of Aonix, we used initialized integers to zero, booleans to FALSE,
etc.  The current version of Aonix does not do the initialization.
We ran into a problem once when upgrading the Aonix compiler.  Code
that used to work began raising CONSTRAINT_ERROR on uninitialized
variables in various places.  I always initialize everything, but
we were working with a team that was new to Ada and weren't 
experienced enough to value the practice.

So, it is better to use the pragma to guarantee the result rather
than hope it always works.  Your compiler vendor may change 
something some day and then your code will suddenly cease to run
properly.

Frank

Re: pragma Import with 'Address clause

[Lutz Donnerhacke]

* Stephen Leake wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> writes:
>> A common technique to reinterpret data is:
>>   a : AT;
>>   [...]
>>   b : BT;
>>   for b'Address use a'Address;
>>   pragma Import(Ada, b);
>>
>> Is the "pragma Import" really necessary? Of course, the ARM says, that
>> elaboration and definition of the imported object is externally defined. So
>> they are omitted from the Ada code itself.
>>
>> Assume BT is a record without any default expressions. Does this mean, the
>> pragma can be omitted from the source code?
>>
>> Background: Spark prohibits the use of Pragma Import on objects.
>
> I would hope Spark would prohibit the address clause as well!

Spark does handle the 'Address clause much more carefully than Ada95.
The following function is problematic in Spark for two reasons:
  - Calculating with external variables is undeterministic.
  - Imported variables might not conform the type restrictions.

function get_b return BT is
  b : BT;
  for b'Address use xxx;
begin
  return b+b;
end get_b;


> you are totally defeating the Ada type system!

No.

Re: pragma Import with 'Address clause

[Rod Chapman]

Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb7guml.nt.lutz@taranis.iks-jena.de>...
> A common technique to reinterpret data is:
>   a : AT;
>   [...]
>   b : BT;
>   for b'Address use a'Address;
>   pragma Import(Ada, b);

This is really bad style, especially in SPARK.  You are deliberately
creating an aliasing that the Examiner can't detect, so this will
cause great confusion for the information-flow analysis of your program.

A better way might be to use a hidden, in-lined instantiation of
Unchecked_Conversion, thus:

   function AT_To_BT (A : in AT) return BT
   is
      --# hide AT_To_BT;
      function C is new Unchecked_Conversion (AT, BT);
   begin
      return C(A);
   end AT_To_BT;
   pragma Inline (AT_To_BT);

Of course, a good compiler will generate absolutely no code for this
at all, which is good news.  You can then create a BT-typed "view" onto
A where and when required without having to introduce aliasing.


If A and B are both library level objects, and the address of A is static,
then you can create two views onto the same area of memory, and use SPARK's
data refinement mechanism to pretend to the outside world that it's
only 1 object really.  Something like:

 package ROM
 --# own Contents;
 --# initializes Contents; -- probably...
 is
    ...
 end ROM;

 package body ROM
 --# own Contents is Raw_View, Typed_View;
 is
   Typed_View : AT;
   for A'Address use Wibble;

   Raw_View   : BT;
   for B'Address use Wibble;

   ...

 end ROM;

You still have to think hard here about which object gets
initialized and when.

This kind of trick is just about justifiable when you want two views of
something like a ROM - one "raw" (Array-of-words or something) view for
checksumming, and one strongly-typed view for strucured access.

Oh - there's one other case where we've done this trick - for I/O
devices that overload a single address port with both a write-only control
register and a read-only status register.  For those things, we simply
declare 2 library level variables which have an identical address
clause, since in this case, we really would prefer to treat them
as distinct objects anyway... :-)

 - Rod, SPARK Team.

Re: pragma Import with 'Address clause

[Randy Brukardt]

Beard, Frank Randolph CIV wrote in message ...
>> The Pragma Import should not be needed.

>Shouldn't be needed but isn't guaranteed.  The Pragma Import is
>there to ensure the compiler doesn't initialize the data.  There
>is no guarantee that the compiler won't initialize it to
>something, despite the fact the data structure doesn't have a
>default expression.


Absolutely right. Also recall that Ada requires implicit initialization
of discriminants and access objects, so you need to insure that there is
nothing that requires implicit initialization as well as default
expressions.

>When we were on VAX Ada, it seemed to initialize everything within
>the range of the type.

I'm told that Rational Apex does this (I haven't checked it myself).

Conclusion: if you need your code to be portable enough to compile with
another Ada compiler (including a new version of the one you are using),
you'll use the pragma Import.

            Randy.

Re: pragma Import with 'Address clause

[Rod Chapman]

Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb7h93l.nt.lutz@taranis.iks-jena.de>...

> function get_b return BT is
>   b : BT;
>   for b'Address use xxx;
> begin
>   return b+b;
> end get_b;
> 

Again, this is really bad style.  Giving Address clauses to local
variable is dubious at best and also defeats SPARK's information flow
model in various ways.  Try something like this:

package Simple_Port
--# own in B; -- volatile "in" mode external variable
is
   function Get_B return BT;
   --# global in B;
end Simple_Port;

package body Simple_Port
is
   B : BT;
   for B'Address use ...; -- external variable with Address clause;
   pragma Volatile (B);   -- probably needed, so better safe than sorry...

   function Get_B return BT
   is
      Raw_B, Result : BT;
   begin
      Raw_B := B; -- simple assignment OK.
      if Raw_B'Valid then
         Result := Raw_B + Raw_B; -- or whatever...
      else
         Result := BT'First; -- or some other safe value
      end if;
      return Result;
   end Get_B;
end Simple_Port;

This is 100% SPARK and freedom from exceptions and invalid values
can be proven.  Note that 

1) The Examiner DOESN'T assert that "Local_B in BT" directly following
the first assignment, since the Examiner is clever enough to know
that something coming from a memory-mapped location might not have a
valid representation.

2) 'Valid can be used to re-establish validity.

3) In this context, an assignment such as

    Raw_B := B + B;

is illegal in SPARK, since B is known to be Volatile, and therefore
such expressions are susceptible to undesirable evaluation
order dependencies.

We thought about these issues very hard indeed when designing the
external-variable and volatility model in SPARK! :-)

 - Rod, SPARK Team.

Re: pragma Import with 'Address clause

[Lutz Donnerhacke]

* Rod Chapman wrote:
> We thought about these issues very hard indeed when designing the
> external-variable and volatility model in SPARK! :-)

I know. That's why I provided the example.

Re: pragma Import with 'Address clause

[Lutz Donnerhacke]

* Rod Chapman wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb7guml.nt.lutz@taranis.iks-jena.de>...
>> A common technique to reinterpret data is:
>>   a : AT;
>>   [...]
>>   b : BT;
>>   for b'Address use a'Address;
>>   pragma Import(Ada, b);
>
> This is really bad style, especially in SPARK.

It's efficient.

> You are deliberately creating an aliasing that the Examiner can't detect,
> so this will cause great confusion for the information-flow analysis of
> your program.

That's why I hide it.

> A better way might be to use a hidden, in-lined instantiation of
> Unchecked_Conversion, thus:
> 
>    function AT_To_BT (A : in AT) return BT
>    is
>       --# hide AT_To_BT;
>       function C is new Unchecked_Conversion (AT, BT);
>    begin
>       return C(A);
>    end AT_To_BT;
>    pragma Inline (AT_To_BT);

Given that AT'Size is large (and possibly indetermined), the possible
temporary copy has to be avoided in any case.

> If A and B are both library level objects, and the address of A is static,
> then you can create two views onto the same area of memory, and use SPARK's
> data refinement mechanism to pretend to the outside world that it's
> only 1 object really.

Known, but not applicable here.

> You still have to think hard here about which object gets initialized and
> when.

That's the purpose of my question.

> Oh - there's one other case where we've done this trick - for I/O
> devices that overload a single address port with both a write-only control
> register and a read-only status register.  For those things, we simply
> declare 2 library level variables which have an identical address
> clause, since in this case, we really would prefer to treat them
> as distinct objects anyway... :-)

Known and already used.

Current code excerpt:
   procedure getdents_read(dents : in out Dir_State;
     node : out INode; name : out Filename; name_last : out Filename_Length;
     valid : out Boolean) is
      e_node   : long;
      e_reclen : ushort;
      new_offset : Positive;
      
      procedure Init
	--# global out name, e_node, e_reclen; in dents;
	--# derives name, e_node, e_reclen from dents;
	is
         --# hide Init;
	 type getdent is record
	    d_ino : long;
	    d_off : Offset_T;
	    d_reclen : ushort;
	    d_name : Filename;
	 end record;
	 pragma Convention(C, getdent);

	 e : getdent;
	 for e'Address use dents.buffer(dents.offset)'Address;
	 pragma Import(Ada, e);
      begin
	 e_node   := e.d_ino;
	 e_reclen := e.d_reclen;
	 name     := e.d_name;
      end Init;
      pragma Inline (Init);
   begin
      Init;
      new_offset := dents.offset + Natural(e_reclen);
      if e_node not in long(INode'First) .. long(INode'Last) or else
        new_offset > dents.length or else
        name(name'First) = ASCII.NUL then
	 valid     := false;
         node      := 0;
         name_last := name'First;
      else
	 valid := true;
	 node := INode(e_node);
	 dents.offset := new_offset;
	 name_last := name'First;
	 for i in Filename_Length range name'First + 1 .. name'Last
	   --# assert i in name'First + 1 .. name'Last;
	   loop
	    if name(i) = ASCII.NUL then
	       name_last := i - 1;
               exit;
	    end if;
	 end loop;
      end if;

      if node = 0 then
         dents.length := 0; --  signaling end of data
      end if;
   end getdents_read;
\f
File /var/home/lutz/work/ada/src/kernel/kernel_/io/getdents_read.vcg
procedure IO.getdents_read

VCs generated 21-MAR-2003 12:21:16

VCs simplified 21-MAR-2003 12:24:23

VCs for procedure_getdents_read :
----------------------------------------------------------------------------
      |       |                    |  ---------Proved In---------  |       |
 #    | From  | To                 |  vcg  |  siv  |  plg  |  prv  | TO DO |
----------------------------------------------------------------------------
 1    | start | rtc check @ 185    |       |  YES  |       |       |       | 
 2    | start | rtc check @ 186    |       |  YES  |       |       |       | 
 3    | start | rtc check @ 190    |       |  YES  |       |       |       | 
 4    | start | rtc check @ 191    |       |  YES  |       |       |       | 
 5    | start | rtc check @ 194    |       |  YES  |       |       |       | 
 6    | start | rtc check @ 195    |       |  YES  |       |       |       | 
 7    | start | rtc check @ 196    |       |  YES  |       |       |       | 
 8    | start | rtc check @ 197    |       |  YES  |       |       |       | 
 9    | start | rtc check @ 197    |       |  YES  |       |       |       | 
 10   | start |    assert @ 197    |       |  YES  |       |       |       | 
 11   | 197   |    assert @ 197    |       |  YES  |       |       |       | 
 12   | 197   | rtc check @ 200    |       |  YES  |       |       |       | 
 13   | 197   | rtc check @ 201    |       |  YES  |       |       |       | 
 14   | start | rtc check @ 208    |       |  YES  |       |       |       | 
 15   | start | rtc check @ 208    |       |  YES  |       |       |       | 
 16   | 197   | rtc check @ 208    |       |  YES  |       |       |       | 
 17   | 197   | rtc check @ 208    |       |  YES  |       |       |       | 
 18   | start |    assert @ finish |  YES  |       |       |       |       | 
 19   | start |    assert @ finish |  YES  |       |       |       |       | 
 20   | start |    assert @ finish |  YES  |       |       |       |       | 
 21   | start |    assert @ finish |  YES  |       |       |       |       | 
 22   | 197   |    assert @ finish |  YES  |       |       |       |       | 
 23   | 197   |    assert @ finish |  YES  |       |       |       |       | 
 24   | 197   |    assert @ finish |  YES  |       |       |       |       | 
 25   | 197   |    assert @ finish |  YES  |       |       |       |       | 
----------------------------------------------------------------------------