From c489922e9d51326ea3415c6970418e6c6aceb3b6 Mon Sep 17 00:00:00 2001 From: Johannes Kliemann Date: Wed, 23 Nov 2022 17:20:07 +0100 Subject: [PATCH 1/3] Add RFC for constrained indefinite arrays --- considered/constrained_indefinite_arrays.md | 90 +++++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 considered/constrained_indefinite_arrays.md diff --git a/considered/constrained_indefinite_arrays.md b/considered/constrained_indefinite_arrays.md new file mode 100644 index 00000000..c0a8aae2 --- /dev/null +++ b/considered/constrained_indefinite_arrays.md @@ -0,0 +1,90 @@ +# Constrained Indefinite Arrays RFC + +## Summary + +This RFC proposes an addition to array types that allows to define them +with a static maximum size but still use them as if they were unconstrained. + +An array defined with +```Ada +type Index is range 0 .. 32; + +type Static_Array is array (Index range <>) of Element with + Constrained; +``` + +Adding the aspect `Constrained` will force the compiler to always reserve +enough space to fit every possible range of an object of this type without +changing the high level behaviour of the type. + +## Motivation + +Arrays in Ada can be declared either with a specific range or with a `<>` to +allow any value in the range of the index type. While the former variant +has a static size and is constrained it can only be used with values of the +same length. Assigning shorter values will fail. The second variant is more +flexible in that regard. It can take values of any range as long as the range +can be expressed by the index type. However these arrays require more specific +language features for some operations, in particular the secondary stack. + +In many projects, especially in the embedded or high integrity domain stack +boundedness is an important property. If stack boundedness needs to be +statically proven the secondary stack cannot be used as its boundedness cannot +be shown. Yet the ability to store values of an unknown length is still useful. +To provide this functionality without a secondary stack many projects use +the following workaround: + +```Ada +subtype Static_String is String (1 .. 32); + +type Sized_String is record + Length : Natural; + Value : Static_String; +end record; +``` + +This construct allows to store a value of unknown length with a statically +known maximum size of 36 byte. It is however cumbersome to use as these objects +cannot use the `&` operator and slices easily. + +## Reference Level Explanation + +A new aspect `Constrained` is added. + +## Syntax + +No custom Syntax. + +## Static Legality Rules + +`Constrained` can only be added to array declarations that would create an +indefinite array. It can be used on both types and subtypes. + +A subtype of a constrained array has the same behaviour as a subtype to a +regular array. If defined as indefinite, it will keep the `Constrained` +modifier but with a reduced static size. If defined with a specific constrained +range it will behave the same way it does without that aspect. + +## Operational Semantics + +Objects of an array type declared with `Constrained` will always be stored in a +memory zone that has the maximum size of that array type. +When returned from a function they behave as constrained types and do not +require the secondary stack. +Operations on that array such appending and slices will trigger the same checks +as they do for indefinite arrays. + +## Unresolved Questions + +* Whether there is a hard limit on the size of these arrays. Theoretically + an array with that aspect and the index type `Long_Integer` would be + 2 ***** 64 * element size bytes large. +* Whether `Constrained` is a good name for that aspect. + +## Alternatives + +One could argue that the same behaviour can also be achieved by creating a +record type as described above and implement the correct operators. However +this would not solve the problem with slicing. Also while such an +implementation could be generic, the type itself likely cannot as generic +formal parameters are never considered static. From 9907edb0539cde82c61e0de01823daf6b03184aa Mon Sep 17 00:00:00 2001 From: Johannes Kliemann Date: Tue, 17 Jan 2023 17:39:48 +0100 Subject: [PATCH 2/3] Add unresolved question about array semantics --- considered/constrained_indefinite_arrays.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/considered/constrained_indefinite_arrays.md b/considered/constrained_indefinite_arrays.md index c0a8aae2..1fad2c1d 100644 --- a/considered/constrained_indefinite_arrays.md +++ b/considered/constrained_indefinite_arrays.md @@ -80,6 +80,12 @@ as they do for indefinite arrays. an array with that aspect and the index type `Long_Integer` would be 2 ***** 64 * element size bytes large. * Whether `Constrained` is a good name for that aspect. +* Whether the behaviour of arrays with this aspect is different from regular arrays. + Assignments to regular arrays must have the same size as the current contents + of that array. As contrained arrays have their maximum possible size allocated + in memory it is possible to assign them values of different lengths or append + additional elements with the `&` operator. Both operations must not exceed the + maximum size of the array type. ## Alternatives From a2c998f2562ab74fcf6faed201c99f698a9da703 Mon Sep 17 00:00:00 2001 From: Johannes Kliemann Date: Mon, 13 Feb 2023 13:25:44 +0100 Subject: [PATCH 3/3] Rename to definite constrained arrays, improve example, clarify behavior --- ...ys.md => definite_unconstrained_arrays.md} | 54 ++++++++++++------- 1 file changed, 35 insertions(+), 19 deletions(-) rename considered/{constrained_indefinite_arrays.md => definite_unconstrained_arrays.md} (66%) diff --git a/considered/constrained_indefinite_arrays.md b/considered/definite_unconstrained_arrays.md similarity index 66% rename from considered/constrained_indefinite_arrays.md rename to considered/definite_unconstrained_arrays.md index 1fad2c1d..c60cb146 100644 --- a/considered/constrained_indefinite_arrays.md +++ b/considered/definite_unconstrained_arrays.md @@ -1,4 +1,4 @@ -# Constrained Indefinite Arrays RFC +# Definite Unconstrained Arrays RFC ## Summary @@ -7,15 +7,32 @@ with a static maximum size but still use them as if they were unconstrained. An array defined with ```Ada -type Index is range 0 .. 32; +type Index is range 0 .. 7; -type Static_Array is array (Index range <>) of Element with - Constrained; +type Static_Array is array (Index range <>) of Natural with + Definite; ``` -Adding the aspect `Constrained` will force the compiler to always reserve -enough space to fit every possible range of an object of this type without -changing the high level behaviour of the type. +Adding the aspect `Definite` will force the compiler to always reserve +enough space to fit every possible range of an object of this type. As the +possible range for this array is preallocated objects of that type can be +resized. + +```Ada +declare + subtype Static_Subtype is Static_Array (1 .. 3); + A : Static_Array := (1, 2, 3, 4); + B : Static_Array := (2, 3); + S : Static_Subtype := (1, 2, 3); +begin + A := B; + A := A & S; + A := A & (8, 9); + pragma Assert (A'Capcity = 8); + A := (0, 1, 2, 3, 4, 5, 6, 7, 8); -- forbidden as it exceeds the array capacity + S := (1, 2); -- forbidden as Static_Subtype is a constrained array +end; +``` ## Motivation @@ -49,7 +66,12 @@ cannot use the `&` operator and slices easily. ## Reference Level Explanation -A new aspect `Constrained` is added. +A new aspect `Definite` is added. An array declared with this aspect is +resizable within its index type boundaries. Assignments of slices that do not +fit the original length of that array are allowed. + +Additionally objects of that type have the `'Capacity` attribute that returns +the maximum number of elements the object can hold. ## Syntax @@ -57,17 +79,17 @@ No custom Syntax. ## Static Legality Rules -`Constrained` can only be added to array declarations that would create an -indefinite array. It can be used on both types and subtypes. +`Definite` can only be added to array declarations that would create an +unconstrained array. It can be used on both types and subtypes. A subtype of a constrained array has the same behaviour as a subtype to a -regular array. If defined as indefinite, it will keep the `Constrained` +regular array. If defined as unconstrained, it will keep the `Definite` modifier but with a reduced static size. If defined with a specific constrained range it will behave the same way it does without that aspect. ## Operational Semantics -Objects of an array type declared with `Constrained` will always be stored in a +Objects of an array type declared with `Definite` will always be stored in a memory zone that has the maximum size of that array type. When returned from a function they behave as constrained types and do not require the secondary stack. @@ -79,13 +101,7 @@ as they do for indefinite arrays. * Whether there is a hard limit on the size of these arrays. Theoretically an array with that aspect and the index type `Long_Integer` would be 2 ***** 64 * element size bytes large. -* Whether `Constrained` is a good name for that aspect. -* Whether the behaviour of arrays with this aspect is different from regular arrays. - Assignments to regular arrays must have the same size as the current contents - of that array. As contrained arrays have their maximum possible size allocated - in memory it is possible to assign them values of different lengths or append - additional elements with the `&` operator. Both operations must not exceed the - maximum size of the array type. +* Whether `Definite` is a good name for that aspect. ## Alternatives