Generic formals and Aspects

Generic formals and Aspects

[Simon Wright]

Recently on StackOverflow there was a question[1] about clamping a value
to a range.

The answer, so far, suggests a generic:

   generic
      type Source_Type is range <>;
      type Destination_Type is range <>;
   function Saturate (X : Source_Type) return Destination_Type;

with discussion about what happens if Destination_Type'Range is not a
subset of Source_Type'Range.

I see in AARM 13.1.1(4.b)[2] that a formal_type_declaration is allowed to
include an aspect specification, so tried

   generic
      type Source_Type is range <>
        with Static_Predicate =>
          Long_Long_Integer (Destination_Type'First)
            >= Long_Long_Integer (Source_Type'First)
          and Long_Long_Integer (Destination_Type'Last)
            <= Long_Long_Integer (Source_Type'Last);
      type Destination_Type is range <>;
   function Saturate (X : Source_Type) return Destination_Type;

but GNAT (4.9.1, GPL 2014) said that Static_Predicate wasn't allowed
(nor was Dynamic_Predicate).

Predicate (GNAT-special?) was allowed, but had no effect: I was able to
instantiate with

   type Source is new Integer range 10 .. 20;
   type Destination is new Integer range 30 .. 40;


(a) what aspects are/should be allowed in a formal_type_declaration?

(b) how to write the generic to prevent this sort of mistake at compile
    time? (easy enough to get a runtime CE).

[1] http://stackoverflow.com/questions/26390135/can-i-clamp-a-value-into-a-range-in-ada
[2] http://www.ada-auth.org/standards/12aarm/html/AA-13-1-1.html#p4.b

Re: Generic formals and Aspects

[Shark8]

On 10/17/2014 7:17 AM, Simon Wright wrote:
> Predicate (GNAT-special?) was allowed, but had no effect

Hm, is your assertion-policy turned on?

Re: Generic formals and Aspects

[Simon Wright]

Shark8 <OneWingedShark@gmail.com> writes:

> On 10/17/2014 7:17 AM, Simon Wright wrote:
>> Predicate (GNAT-special?) was allowed, but had no effect
>
> Hm, is your assertion-policy turned on?

No; I think that (at the moment) -gnata enables all assertions.

But I tried it anyway: no difference.

Re: Generic formals and Aspects

[Shark8]

The following does work, though it doesn't catch it at compile-time:

    generic
       type Source_Type is range <>;
       type Destination_Type is range <>;

       S_First : Long_Long_Integer:= Long_Long_Integer(Source_Type'First);
       S_Last  : Long_Long_Integer:= Long_Long_Integer(Source_Type'Last);
       D_First : Long_Long_Integer:= 
Long_Long_Integer(Destination_Type'First);
       D_Last  : Long_Long_Integer:= 
Long_Long_Integer(Destination_Type'Last);
    function Saturate (X : Source_Type) return Destination_Type
      with Pre =>
               D_First >= S_First
           and D_Last  <= S_Last
      ;

Maybe this would be a good thing to suggest for the corrigenda -- 
addition of SUBTYPE to generic formals; the purpose thereof would be to 
"hang" Predicates on and [I think] Static_Predicate could be checked at 
compile-time.

Re: Generic formals and Aspects

[olivermkellogg]

On Friday, October 17, 2014 at 3:17:36 PM UTC+2, Simon Wright wrote:
> Recently on StackOverflow there was a question[1] about clamping a value
> to a range.
> 
> The answer, so far, suggests a generic:
> 
>    generic
>       type Source_Type is range <>;
>       type Destination_Type is range <>;
>    function Saturate (X : Source_Type) return Destination_Type;
> 
> with discussion about what happens if Destination_Type'Range is not a
> subset of Source_Type'Range.
> 
> I see in AARM 13.1.1(4.b)[2] that a formal_type_declaration is allowed to
> include an aspect specification, so tried
> 
>    generic
>       type Source_Type is range <>
>         with Static_Predicate =>
>           Long_Long_Integer (Destination_Type'First)
>             >= Long_Long_Integer (Source_Type'First)
>           and Long_Long_Integer (Destination_Type'Last)
>             <= Long_Long_Integer (Source_Type'Last);
>       type Destination_Type is range <>;
>    function Saturate (X : Source_Type) return Destination_Type;
> 
> but GNAT (4.9.1, GPL 2014) said that Static_Predicate wasn't allowed
> (nor was Dynamic_Predicate).
> 
> Predicate (GNAT-special?) was allowed, but had no effect: I was able to
> instantiate with
> 
>    type Source is new Integer range 10 .. 20;
>    type Destination is new Integer range 30 .. 40;
> 
> 
> (a) what aspects are/should be allowed in a formal_type_declaration?
> 
> (b) how to write the generic to prevent this sort of mistake at compile
>     time? (easy enough to get a runtime CE).
> 
> [1] http://stackoverflow.com/questions/26390135/can-i-clamp-a-value-into-a-range-in-ada
> [2] http://www.ada-auth.org/standards/12aarm/html/AA-13-1-1.html#p4.b

I share the sentiment.
Here is my use case:

-- File: big_endian_integer_buffer.ads
with Interfaces;

generic
   type Discrete_Type_16_or_32_or_64 is (<>);  -- CANDIDATE

package Big_Endian_Integer_Buffer is

   function Get return Discrete_Type_16_or_32_or_64;
   procedure Set (Value : Discrete_Type_16_or_32_or_64);

   Size_In_Bytes : constant Positive := Discrete_Type_16_or_32_or_64'Size / 8;

   type Buffer_Type is array (1 .. Size_In_Bytes) of Interfaces.Unsigned_8;
   for Buffer_Type'Component_Size use 8;

   Buffer : aliased Buffer_Type := (others => 0);

end Big_Endian_Integer_Buffer;


At the line marked CANDIDATE, I would have liked to write something like

type Discrete_Type_16_or_32_or_64 is (<>)
   with Static_Predicate => Discrete_Type_16_or_32_or_64'Size in 16 | 32 | 64;

Re: Generic formals and Aspects

[J-P. Rosen]

Le 19/07/2016 à 17:49, olivermkellogg@gmail.com a écrit :
>    generic
>>       type Source_Type is range <>
>>         with Static_Predicate =>
>>           Long_Long_Integer (Destination_Type'First)
>>             >= Long_Long_Integer (Source_Type'First)
>>           and Long_Long_Integer (Destination_Type'Last)
>>             <= Long_Long_Integer (Source_Type'Last);
>>       type Destination_Type is range <>;
>>    function Saturate (X : Source_Type) return Destination_Type;
>> 
Tip: you don't need to convert to Long_Long_Integer here (non portable,
etc...). Use:
          Destination_Type'Pos (Destination_Type'First)
            >= Source_Type'Pos (Source_Type'First)
          and Destination_Type'Pos (Destination_Type'Last)
            <= Source_Type'Pos (Source_Type'Last);

Since 'Pos returns Universal_Integer, you can compare values of
different types.

FWIW...
-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Generic formals and Aspects

[Shark8]

Try the following:


------ SPEC ------
    generic
	type Discrete_Type is (<>);  -- CANDIDATE

    package Big_Endian_Integer_Buffer is
	
	function Get return Discrete_Type;
	procedure Set (Value : Discrete_Type);
	
    Private
	type Internal is new Discrete_Type
	  with Static_Predicate => Internal'Size in 16 | 32 | 64;
	
	Size_In_Bytes : constant Positive := Internal'Size / 8;

	type Buffer_Type is array (1 .. Size_In_Bytes) of Interfaces.Unsigned_8
	  with Component_Size => 8;

	Buffer : Buffer_Type := (others => 0);
    end Big_Endian_Integer_Buffer;
    

------ BODY ------
    package body Big_Endian_Integer_Buffer is
	
	function Get return Discrete_Type is
	    Result : Discrete_Type
	      with Import, Address => Buffer'Address;
	begin
	    Return Discrete_Type(Result);
	End Get;
	
	procedure Set (Value : Discrete_Type) is
	    Temp : Internal
	      with Import, Address => Buffer'Address;
	begin
	    Temp := Internal(Value);
	End Set;
	
    end Big_Endian_Integer_Buffer;

Re: Generic formals and Aspects

[olivermkellogg]

On Tuesday, July 19, 2016 at 6:05:12 PM UTC+2, Shark8 wrote:
> Try the following:
> 
> 
> ------ SPEC ------
>     generic
> 	type Discrete_Type is (<>);  -- CANDIDATE
> 
>     package Big_Endian_Integer_Buffer is
> 	
> 	function Get return Discrete_Type;
> 	procedure Set (Value : Discrete_Type);
> 	
>     Private
> 	type Internal is new Discrete_Type
> 	  with Static_Predicate => Internal'Size in 16 | 32 | 64;
> 	
> 	Size_In_Bytes : constant Positive := Internal'Size / 8;
> 
> 	type Buffer_Type is array (1 .. Size_In_Bytes) of Interfaces.Unsigned_8
> 	  with Component_Size => 8;
> 
> 	Buffer : Buffer_Type := (others => 0);
>     end Big_Endian_Integer_Buffer;
>     
> 
> ------ BODY ------
>     package body Big_Endian_Integer_Buffer is
> 	
> 	function Get return Discrete_Type is
> 	    Result : Discrete_Type
> 	      with Import, Address => Buffer'Address;
> 	begin
> 	    Return Discrete_Type(Result);
> 	End Get;
> 	
> 	procedure Set (Value : Discrete_Type) is
> 	    Temp : Internal
> 	      with Import, Address => Buffer'Address;
> 	begin
> 	    Temp := Internal(Value);
> 	End Set;
> 	
>     end Big_Endian_Integer_Buffer;

Interesting.

Using your modified spec with the following test program:

-- File: beib_test.adb
with Interfaces;
with Big_Endian_Integer_Buffer;

procedure BEIB_Test is

   package Pass is new Big_Endian_Integer_Buffer (Interfaces.Unsigned_64);

   type RGB_T is mod 2 ** 24 with Size => 24;

   package Fail is new Big_Endian_Integer_Buffer (RGB_T);

   P : Interfaces.Unsigned_64;
   F : RGB_T;

begin
   P := Pass.Get;
   F := Fail.Get;
end BEIB_Test;

I get the following message from GNAT:

beib_test.ads:6:04: instantiation error at big_endian_integer_buffer.ads:16
beib_test.ads:6:04: expression is not predicate-static (RM 3.2.4(16-22))
[...]

Line 6 is at the Pass instantiation. (The same error happens at the Fail instantiation.)

Hmm, too bad... I would have preferred getting a compile time error.

That said, after changing Static_Predicate to Dynamic_Predicate in the spec, the test program builds okay.
However, it runs without failure. (I would have expected a failure on the Fail instantiation.)

For completeness, here is the generic body that I am using:

-- File:  big_endian_integer_buffer.adb
with System, Ada.Unchecked_Conversion;

package body Big_Endian_Integer_Buffer is

   use type System.Bit_Order;

   function Get return Discrete_Type is
      function To_Discrete is new Ada.Unchecked_Conversion
        (Buffer_Type, Discrete_Type);
   begin
      if System.Default_Bit_Order = System.High_Order_First then
         return To_Discrete (Buffer);
      end if;
      declare
         Native_Buf : Buffer_Type;
      begin
         for I in 1 .. Size_In_Bytes loop
            Native_Buf (I) := Buffer (Size_In_Bytes - I + 1);
         end loop;
         return To_Discrete (Native_Buf);
      end;
   end Get;

   procedure Set (Value : Discrete_Type) is
      function To_Buffer is new Ada.Unchecked_Conversion
        (Discrete_Type, Buffer_Type);
   begin
      if System.Default_Bit_Order = System.High_Order_First then
         Buffer := To_Buffer (Value);
         return;
      end if;
      declare
         Native_Buf : constant Buffer_Type := To_Buffer (Value);
      begin
         for I in 1 .. Size_In_Bytes loop
            Buffer (I) := Native_Buf (Size_In_Bytes - I + 1);
         end loop;
      end;
   end Set;

end Big_Endian_Integer_Buffer;

Re: Generic formals and Aspects

[Randy Brukardt]

<olivermkellogg@gmail.com> wrote in message 
news:18aedafc-c66d-4bba-81ce-76dce495f59e@googlegroups.com...
> On Tuesday, July 19, 2016 at 6:05:12 PM UTC+2, Shark8 wrote:
>> Try the following:
>>
>>
>> ------ SPEC ------
>>     generic
>> type Discrete_Type is (<>);  -- CANDIDATE
>>
>>     package Big_Endian_Integer_Buffer is
>>
>> function Get return Discrete_Type;
>> procedure Set (Value : Discrete_Type);
>>
>>     Private
>> type Internal is new Discrete_Type
>>   with Static_Predicate => Internal'Size in 16 | 32 | 64;

You could use a subtype here, if you don't want a new type:

  subtype Internal is Discrete_Type
      with Dynamic_Predicate => Internal'Size in 16 | 32 | 64;

BUT:

'Size shouldn't be allowed in either of these predicates, because "Internal" 
is a value (the value of the "current instance" of the subtype), while Size 
is the attribute of a subtype or object. (See AI12-0068-1.) This is 
necessary so that the properties of the object can't be queried in a 
predicate; that wasn't the purpose of predicates and it would allow some 
truly bizarre uses. (See "Zoofable" in the question of that AI.) 
Specifically, 8.6(17.1/4) says:

   Within an aspect_specification for a type or subtype, the current
   instance represents a value of the type; it is not an object. The
   nominal subtype of this value is given by the subtype itself (the
   first subtype in the case of a type_declaration), prior to applying
   any predicate specified directly on the type or subtype. If the type or
   subtype is by-reference, the associated object with the value is the
   object associated (see 6.2) with the execution of the usage name.

   AARM Ramification: For the purposes of Legality Rules, the current
   instance acts as a value within an aspect_specification. It might
   really be an object (and has to be for a by-reference type), but
   that isn't discoverable by direct use of the name of the current 
instance.

Looks like an ACATS test is needed.

>> Size_In_Bytes : constant Positive := Internal'Size / 8;
...
...
> That said, after changing Static_Predicate to Dynamic_Predicate in the 
> spec, the test program builds okay.
> However, it runs without failure. (I would have expected a failure on the 
> Fail instantiation.)

Did you remember to enable assertions? GNAT has the Assertion_Policy as 
Ignore by default. (This is implementation-defined in the Standard, mainly 
because we didn't have enough votes to make GNAT change.) If you're 
depending on assertions (like a predicate), you always need to appropriately 
place a Assertion_Policy pragma (or the equivalent command-line option, 
whatever it is).

                                       Randy.

Re: Generic formals and Aspects

[olivermkellogg]

On Tuesday, July 19, 2016 at 9:23:34 PM UTC+2, Randy Brukardt wrote:
> >> [...]
> >> type Internal is new Discrete_Type
> >>   with Static_Predicate => Internal'Size in 16 | 32 | 64;
> 
> You could use a subtype here, if you don't want a new type:
> 
>   subtype Internal is Discrete_Type
>       with Dynamic_Predicate => Internal'Size in 16 | 32 | 64;
> 
> BUT:
> 
> 'Size shouldn't be allowed in either of these predicates, because "Internal" 
> is a value (the value of the "current instance" of the subtype), while Size 
> is the attribute of a subtype or object. (See AI12-0068-1.) This is 
> necessary so that the properties of the object can't be queried in a 
> predicate; that wasn't the purpose of predicates and it would allow some 
> truly bizarre uses. (See "Zoofable" in the question of that AI.) 
> Specifically, 8.6(17.1/4) says:
> 
>    Within an aspect_specification for a type or subtype, the current
>    instance represents a value of the type; it is not an object. The
>    nominal subtype of this value is given by the subtype itself (the
>    first subtype in the case of a type_declaration), prior to applying
>    any predicate specified directly on the type or subtype. If the type or
>    subtype is by-reference, the associated object with the value is the
>    object associated (see 6.2) with the execution of the usage name.
> 
>    AARM Ramification: For the purposes of Legality Rules, the current
>    instance acts as a value within an aspect_specification. It might
>    really be an object (and has to be for a by-reference type), but
>    that isn't discoverable by direct use of the name of the current 
> instance.
> 
> Looks like an ACATS test is needed.
> 
> >> Size_In_Bytes : constant Positive := Internal'Size / 8;
> ...
> ...
> > That said, after changing Static_Predicate to Dynamic_Predicate in the 
> > spec, the test program builds okay.
> > However, it runs without failure. (I would have expected a failure on the 
> > Fail instantiation.)
> 
> Did you remember to enable assertions? GNAT has the Assertion_Policy as 
> Ignore by default. (This is implementation-defined in the Standard, mainly 
> because we didn't have enough votes to make GNAT change.) If you're 
> depending on assertions (like a predicate), you always need to appropriately 
> place a Assertion_Policy pragma (or the equivalent command-line option, 
> whatever it is).
> 

Yes, I added both
  pragma Assertion_Policy (Check);
on the package spec and "-gnata" on compiling; no change on execution.
Thanks for your insights.