Re: pragma Import with 'Address clause

[Lutz Donnerhacke <lutz@iks-jena.de>]

* 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  |       |       |       |       | 
----------------------------------------------------------------------------