[2021][spark_unbound] Unbound data structures in Ada-Spark

[mhatzl]

spark_unbound

My goal for this crate is to provide generic unbound data structures for the Spark subset of Ada.

In embedded or highly critical systems, the need for dynamic allocations is probably not that high or even not possible by the underlying plattform, but I would like to expand the use of Spark also more in higher level programs that are facing a lot of human interaction either directly or indirectly. Being bound to a fixed size of requests or file lenghts that can be handled, seemed too restrictive to me (Note: At least to my knowledge most current programs in Spark are bound to some size).

With the introduction of pointers in Spark, unbound data structures seemed achievable. So I went through the ARM trying to find out how to make the usage of new safe, since Storage_Error can not be handled by Spark, but the abscene of it can also not be proven. This lead me to create my first question on StackOverflow on "How to check for Storage_Error" and then to create the issue at AdaCore/ada-spark-rfcs, where @Fabien-Chouteau provided an elegant solution.

spark_unbound is my take on unbound data structures in Spark that builts upon the safe heap allocation mentioned by @Fabien-Chouteau.

Purpose and current state

As mentioned, my goal for this crate is to provide generic unbound data structures for the Spark subset of Ada.

Currently, I have implemented a basic unbound array-like data structure in the package Spark_Unbound.Arrays. This should become a safe replacement for Ada.Containers.Vector. In Addition, I want to add some convinient functionalities like slicing and sorted contains.

For now, it is more of a 'fancy' stack, since I have not found the time to implement insert, prepend or indexed deletion.

Note: I am currently studying computer science, having quite some other projects to do, so I might not be able to add more functionality in the upcoming months.

Usage

spark_unbound is a library crate. To use it inside other projects, "with"-it using alire. An instance of an unbound array can then be created with the function To_Unbound_Array located in Spark_Unbound.Arrays.

Here is an example using Append taken from unit tests located in the tests subfolder:

type Test_Fixture is new AUnit.Test_Fixtures.Test_Fixture with record
      V1 : Integer;
      V2 : Integer;
      V3 : Integer;
      V4 : Integer; 
end record;

procedure Set_Up (T : in out Test_Fixture)
is
begin
      T.V1 := 1;
      T.V2 := 2;
      T.V3 := 3;
      T.V4 := 4;
end;

procedure TestAppend_WithSmallCapacity_ResultAppended(T : in out Test_Fixture)
is
      package UA_Integer is new Spark_Unbound.Arrays(Element_Type => Integer, Index_Type => Positive);
      Test_UA : UA_Integer.Unbound_Array := UA_Integer.To_Unbound_Array(Initial_Capacity => 3); -- Note the low capacity
      Success : Boolean;
begin      
      UA_Integer.Append(Test_UA, T.V1, Success);
      UA_Integer.Append(Test_UA, T.V2, Success);     
      UA_Integer.Append(Test_UA, T.V3, Success);     

      -- Now Append needs to resize
      UA_Integer.Append(Test_UA, T.V4, Success); 

      UA_Integer.Clear(Test_UA); -- deallocates the unbound array
end;

Note: The full example and some more can be found under /tests/src/Unbound_Array.

Design

For Spark_Unbound.Arrays, I am allocating an array with fixed size and compare the number of added elements ("Length") with the length of the underlying array ("Capacity"). If every index of the underlying array is set (Length = Capacity), the next append tries to allocate an array with twice the capacity and then copies all elements into the new array, freeing the old one at the end.

The reference to the allocated array and the number of added elements is stored in the Unbound_Array record. This record is the main type for the Spark_Unbound.Arrays package.

Note: I was not able to make the fields (more precise: the types of those fields) of the Unbound_Array record private, as this created a lot of problems while proving.

Prove and test state

The packages Spark_Unbound.Safe_Alloc and Spark_Unbound.Arrays are fully proven by Spark with one exception being the Alloc function inside the two nested packages of Spark_Unbound.Safe_Alloc handling the Storage_Error. Those functions are tested using AUnit. The tests can be found at /tests/src/Safe_Alloc.

I setup two workflows for the GitHub repo that prove and test spark_unbound on push or pull request to main. The results of the latest commit to main can be seen in the README at GitHub.

Note: Currently, I am getting "memory accessed through objects of access type" might not be initialized after elaboration of main program from GNATprove. This only affects the crate if you directly access Unbound_Array, but I would still prefer to resolve this. As mentioned in the issue [General] Add default initialization for heap allocated types, I do not have a solution so far.

Documentation

The API documentation for spark_unbound is automatically generated using GNATdoc and can be found at mhatzl.github.io/spark_unbound/.

Authors

For now, I am the only contributor to spark_unbound, but the idea for safe heap allocation originates from a discussion in AdaCore/ada-spark-rfcs where @Fabien-Chouteau posted a solution that I took and slightly updated for arrays. So I will not take any credit for safe heap allocation.

License

MIT Licensed