Reliability of 'Base

General
1

Hi, I’ve been wondering, how much is SomeScalar’Base a hack ?
Here is a routine to populate a 2-dimensional array (Square) from a list. I’m implementing the quadratic sort.

    for I in 1..NBCompletelines loop
      for J in 1..Side loop
        Square (I,J) := List (List'First +        Indextype'Base((I - 1) * Side + J - 1));
      end loop;
    end loop;

Indextype is Positive, the statement seems equivalent to

Square (I,J) := List (Indextype(Integer(List’First) + (I - 1) * Side + J - 1));

The rm states

The base range of a scalar type is the range of finite values of the type that can be represented in every unconstrained object of the type; it is also the range supported at a minimum for intermediate values during the evaluation of expressions involving predefined operators of the type.

But that seems so unpredictable, I don’t what kind of trust I should put in an expression like subtype ExtendedIndex is indextype'Base range 0..Indextype'Last; even though it litters the standard libraries.

I’m even surprised this is part of the language.

2

It’s not a hack.
Remember this as a working definition of type: A type is a set of values and operations upon those values.

Ok, so what you’re misunderstanding is that this has to be a bit more broad than if it were just integers. (Esp. because of floating-point and fixed-point.) But it’s essentially saying S'Base is the type, but “without the constraints” — consider a floating-point type backed by IEEE754: there’s all the non-numeric values like NaN and +Inf, the way to utilize floating-point within your general processing is to do something like Subtype Real is Interfaces.IEEE_Float32'Range; to strip out the non-numeric values at the earliest point (read from a sensor, read from a file, etc).

The question then becomes, if we have Real, how can we refer to the [underlying] type with all values? And the answer there is Real'Base.

The other thing that might be in play is mapping to machine-types —now I’d have to re-read is so consider this as more on the conceptual level— consider the abstracted type-system: there’s Universal_Integer which doesn’t map to hardware, there’s a subset, Integer, which maps to the integer-range covering the “standard” word-size for that machine, and there’s things like Subtype Natural is Integer range 0..Integer'Last/Subtype Positive is Natural range Natural'Succ(Natural'First)..Natural'Last; — Positive'Base then refers to Integer, the unconstrained (“full type”) that was mapped from Universal_Integer into something that you can have an object of.

3

It’s equivalent to

Square (I, J) := List (List’First + (I - 1) * Side + J - 1);

As you quoted, 'Base is “the range supported at a minimum for intermediate values during the evaluation of expressions involving predefined operators of the type”, so the index expression will be evaluated using 'Base for the index subtype (or a larger integer type), with the result checked for membership in the subtype. You never have to do conversions to obtain this behavior.

When you declare

type T is range 1 .. 10;

you get the predefined operators, such as

function "+" (Left : in T'Base; Right : in T'Base) return T'Base;

where T’Base will probably be equivalent to Interfaces.Integer_8. So expressions like

(T'First - T'Last) + 2 * ( (T'First + T'Last) / 2)

give the correct result.

It’s still possible for intermediate results to not fit in the type used to evaluate an expression. With GNAT, using -gnato3 uses unbounded integers to evaluate all integer expressions, so they should always give the correct result.

4

It must be said that Ada has a reasonable compromise between fully defined semantics and system determined behaviour. Either end would be unusable. E.g. if you require

type S is range 1..2;

were fully defined as 1 and 2, you would lose all arithmetic. If you make it machine dependent like C’s int you would have C’s mess. Ada is somewhere in between.

As an OO proponent I must say that having a class could allow the user to define the semantics precisely by expressing promotion rules alike C’s double and Ada’s base type in terms of two related integer types. One for computations, another for storing. They could have completely different representations like C’s promotion rules allow. E.g. you could use one byte for storing and Big Integer for computations…

5

Square (I, J) := List (List’First + (I - 1) * Side + J - 1);

Indextype is its own formal type, so I get

quadratic_sort_generic.adb:23:42: error: invalid operand types for operator “+”
quadratic_sort_generic.adb:23:42: error: left operand has type “IndexType” defined at quadratic_sort_generic.ads:5

My point was that 'Base could fail to provide a given value if we force the appropriate representation upon the actual, restraining the byte size. I’ve never used that so I can’t try. So using 'Base in generics to extend an actual should be a hazard because it doesn’t ensure anything.
Does that respond to my question plainly :rofl: ? Not I don’t also enjoy the indepth exposition though :slightly_smiling_face:

6

You can be certain that 'Base on a signed integer subtype extends the range to be a symmetric range around zero, possibly with an extra negative value, thanks to RM 3.5.4(9):

A signed_integer_type_definition defines an integer type whose base range includes at least the values of the simple_expressions and is symmetric about zero, excepting possibly an extra negative value.

You can also presume on essentially all modern computers that the range is extended up to the signed range provided by the nearest power of 256 (2**8). In the language-defined library, we generally are just trying to get it to include zero, and possibly -1. There isn’t much more than that needed, and so it should not be introducing a portability problem.

2 Likes
7

This was not clear from the original post, which only said that it “is Positive”.

As Taft said, 'Base for a signed integer subtype is roughly symmetric around zero. It will also be equivalent to one of the Interfaces.Integer_* types. Whether or not the base type is big enough for what you want to do must be ascertained separately. For example

generic -- Example
   type T is range <>;
package Example is
   pragma Assert (T'First > T'Base'First); -- We need to be able to do T'First - 1

   subtype Extended_T is T'Base range T'First - 1 .. T'Last;
end Example;
8

Positive but it is but as the actual… sorry.
Screw aspect specifications, your Assert made me find the solution ! pragma Compile_Time_Error.

This pragma can be used to generate additional compile time error messages. It is particularly useful in generics, where errors can be issued for specific problematic instantiations

Gnat-specific but perfect. Extraordinary useful. I just added in the body:

procedure decimal_radix_sort (List: IN OUT ListType) is
pragma Compile_Time_Error (Indextype’Last = Indextype’Base’Last, “indextype too narrow”);

But it forces the user to provide an actual explicitly excluding its base type last element. Neither gnat or spark can prove anything that considers List’s actual range instead of Indextype. Anything like pragma Compile_Time_Error (List'Last = Indextype'Base'Last, "indextype too narrow"); produces “condition is not known at compile time” and the corresponding assertion can not be proved.
Yet in all those cases List’s value is static. It’s bothersome to need to make an index subtype that excludes indextype’Base’Last. There is a loop that increment an index that exceeds List’Last at the end of last iteration. I know I can simply add an exception handler but it’s not fun.

But why can’t Spark see the value of List ? I would have supposed the following could be proved

spark code

procedure main with SPARK_Mode is
generic
type Indextype is (<>);
type ListType IS array (Indextype range <>) of Integer;
procedure decimal_radix_sort (List: ListType);
procedure decimal_radix_sort (List: ListType) is
pragma Assert (List’Last < Indextype’Base’Last);
begin
null;
end decimal_radix_sort;
type PosArray is array (Positive range <>) of Integer;
procedure sort is new decimal_radix_sort (Positive,PosArray);
List: PosArray := (4,87,557,9,0,1);
begin
sort (List);
end main;

Lastly, I would like to suppress Range_Check pr Overflow_check locally with

pragma Suppress (Range_Check);
PlaceInResult := Indextype’Succ (@);
pragma Unsuppress (Range_Check);

… But it has this damn limitation:

A checking pragma is allowed only immediately within a declarative_part, immediately within a package_specification, or as a configuration pragma.

Why ? I don’t want to suppress it everywhere, but just locally !

9

Probably the implementation has a set of configurations for optimizations and suppressions as a parameter to the codegen that operates on the package-level.

The solution I use, when I need things that SPARK can’t verify is this templating:

Package Example with SPARK_Mode => On is
  Type Blah is private;
  Procedure Some_Operation( Object : in out Blah );
Private
   Type Blah is null record;

   Package Internals with SPARK_Mode => Off is
      Procedure Operation( Object : in out Blah );
   End Internals;

  Procedure Some_Operation( Object : in out Blah )
    renames Internals.Operation;
End Example;

Depending on the details, the definition of the publicly visible type might need to be after Internals, such as when the type itself is not SPARK friendly.

10

Yeah I thought that I would need to make Increment its own compilation unit. No matter. But I can’t either ?
Should the following be legal ?

procedure Increment_integer (I: in out nteger) is
	A: Integer := Integer'Last; 
	pragma suppress (Overflow_Check, A);
	pragma suppress (Range_Check, A);
begin
	A := Integer'Succ (A);
end Increment_integer;

But it gets me a gcc bug. Do I misunderstand pragma Suppress ? The report is here, as I suppose I’m not the first to have this issue.
While the array’s last index is unlikely to be Integer’last, on the other hand if it could be instanciated with Boolean, and so will cause overflow at the second loop iteration.
This is normal and should be suppressed here.

11

Good if the index is Positive. But it could be Boolean.

12

Please, state the original problem. It is relatively simple to ensure that indices do not overflow. You can always check the border cases for no overflow (indices are ascending).

No, you do not need that. Nor you can ensure it as T’First could be Integer’First.

The correct formula is. Given

for I in Row'Range loop
   for J in Column'Range loop

   List'First
+  (I - Row'First) * Columns_Number
+  (J - Column'First)
13

IIRC, if it is its own compilation unit, then yes.
NOTE: GNAT has the implementation limitation that a compilation-unit must be in its own file.

Somehow, I think you’ve “wandered off the reservation” — that could be a minimal example of the pragmas, but it also is pretty trivial to SPARK prove —see AdaCore’s docs/tutorial here— but increment w/ wraparound would be:

Procedure Inc( X : in out Some_Int )
  with Post    => X = (if X'Old = Some_Int'Last
                       then Some_Int'First
                       else Some_Int'Succ(X'Old)),
       Global  => null,
       Depends => (X => X);
-- …
Procedure Inc( X : in out Some_Int ) is
Begin
  Return (if X = Some_Int'Last then Some_Int'First 
          else Some_Int'Succ(X'Old));
End Inc;

I think you’ve failed to use your attributes. —(if Value = Discrete'Last then Discrete'First else Discrete'Succ(Value))— works in all cases to do an standard wrap-around increment. If you’re doing something where you need to reserve the first value then “use a zero”:

Generic
   Type Element is (<>);
   Zero : Element:= Element'First; 
Package Example is

  Subtype Natural  is Element range Zero..Element'Last;
  Subtype Positive is Natural range Natural'Succ(Natural'First)..Natural'Last;

  Procedure Natural_Inc ( X : in out Element ); -- all the SPARK annotation…
  Procedure Positive_Inc( X : in out Element ); -- all the SPARK annotation…
Private
   Generic
      type Derived is new Element;
   Procedure Generic_Increment( X : in out Element );
End Example;

Package Body Example is
  Procedure Generic_Increment( X : in out Element ) is
   (if X not in Derived then Derived'First
    elsif X = Derived'Last then Derived'First
    else Derived'Inc( X )
   );

  Procedure Natural_Inc_Instance  is new Generic_Increment( Natural  );
  Procedure Positive_Inc_Instance is new Generic_Increment( Positive );

  Procedure Positive_Inc( X : in out Element )
     renames Positive_Inc_Instance;
  Procedure Natural_Inc ( X : in out Element )
     renames Natural_Inc_Instance;
End Example;
14

As for the need well it is the radix sort. Each key of a list is not compared to another as usual, but sorted digit after digit, starting from the unit, or power 0 of the base. It works with any scalar type.
Keys are sorted in n number of bins/subarray, each corresponding to a digit. Then the keys/elements are put back in the original list. Then rinse and repeat for the successive ranks / powers.

My need in this loop:

for D in Bins'Range when Lasts (D) > 0 loop
	for E of Bins(D) (BinType'First..Lasts(D)) loop
		List (PlaceInResult) := E;
        PlaceInResult := Indextype'Succ (@);
	end loop;
end loop;

It refills the list in order after a sorting for a given position. Starting at List’First att the end of the last iteration PlaceInResult overflows when List’Last equals the last value of the index base type.
I don’t think I can substitute with the two loops with an aggregate and so do away with a separate index variable, because some Bins can be empty (no key having that digit in that position) and filters don’t work in container or array aggregates.

I know I can always wrap around, but either that or an additional check would introduce overhead. This chapter in particular is about performance so I take it to heart. It would be more efficient to let it overflow and not care, since the index is reinitialized after each loop.

15

Run the inner loop one iteration less followed by assignment of the last element. You can also convert loop into

loop
   --- Do stuff
   exit when Condition;
   -- Increment destination index
end loop;

And final note, avoid containers, use arrays. You can simply assign array slice instead of running a loop. Which is also far faster and easier for compiler to optimize and validate.

16

Then why not use a “helper” index:

Generic
  Type Index is (<>);
Package Whatever_Sort is
  Type Aux is mod Index'Pos(Index'Last)-Index'Pos(Index'First);
  Procedure Inc( X : in out Index );
Private
  --…
End Whatever_Sort;

Package Body Whatever_Sort is
  Procedure Inc( X : in out Index ) is
    -- Remember to offset from Index'First:
    Aux_Index : Aux renames "+"(Index'Pos(X), 1+Index'Pos(Index'First));
  Begin
    X:= Index'Val( Aux_Index );
  End Inc;  
End Whatever_Sort;

There, done.

17

OneWingedShark: Nope :laughing: I tried something similar already. Do compile your snippet and see what you get :wink: (RM 4.9(7,8))

I replaced the inner loop, but I encountered a weird phenomena : the range of an iterated component association of a proper length would not slide to coincide with ListType, until I qualified it. Weird.