This article discusses various issues rebuilding a demonstrator intended for the BBC micro:bit (version 1.3b) after an interval of several years.
The demonstrator is part of the ColdFrame project. The underlying model is of a set of buttons and LEDs; each button controls one or more LEDs, and each LED is controlled by one or more buttons. Each button responds to a short push by remaining set for a short period; to a long push by remaining set until it’s pushed again. This implementation consists of a single button and a single LED (fortuitously part of the micro:bit already).
The compiler and runtime must support the ARM architecture (switches
Internal Compiler Error
The current compiler (GCC 12.2.0) failed to compile ColdFrame’s event dispatcher with an internal compiler error. I don’t think this has been reported on the GCC Bugzilla, and it’s hard to tell from the Changelog; however, it’s been fixed in GCC 13.0.1 of 20230129.
New compiler infrastructure
The last time this demonstrator was built was in 2019, using GCC 9. The new compiler (13.0.1) needed
System.Return_Stack.Rs_Pool), which was missing from Cortex GNAT RTS but easy to add. I don’t recall which unit required this change.
The build (at
-O0) wouldn’t fit in the micro:bit’s Flash (256K). In the past I’ve worked round this by compiling everything with
-O2. However, on looking into the map file, I noticed that in spite of compiling with the standard
-fdata-sections, and linking with
-gc-sections, a lot of Container code was included in spite of not being used (ColdFrame for Ravenscar uses
After some headscratching, and testing with the macOS equivalent linker switch
-dead_strip, I realised that - for a tagged type - all the primitive subprograms can be reached via the dispatch table! This will include controlled types, but they are far less likely than general container libraries to provide more primitives than an individual program uses; and they’re unlikely to be part of frequently-instantiated generics.
The standard containers have always been general-purpose tools, and it’s been (quietly) expected that projects will use alternatives if necessary, so I looked around for possibilities.
- must be generic
- must not be tagged
- only need to support definite elements
- must support maps - hashed maps greatly preferred
- must support vectors
- must not require finalization (the
Ada.Containersversions in Cortex GNAT RTS have had the finalization-related parts removed since the RTS doesn’t support finalization; they’re only used to support tampering checks in the presence of exceptions, and the RTS doesn’t support exceptions either - off to the Last Chance
- should support iterators,
for ... of ...preferred.
- The Ada 95 Booch Components are tagged.
- The Original Booch Components are somewhat unsupported (e.g. the test code is 404’d); besides, they seem much less usable and potentially slow. Iteration over lists is quite LISP-y).
- Stephe’s Ada Library:
SAL.Gen_Unbounded_Definite_Red_Black_Treeswould probably provide equivalent functionality to Maps, though generating an ordering function would be tricky in the ColdFrame context. Being unbounded explains why it uses finalization.
- The PragmAda Reusable Components don’t support Maps.
- The Simple Components: the maps are ordered (and use finalization). There are no vector equivalents.
- AdaCore’s Formal Containers aren’t tagged, don’t use finalization, and have an interface very similar to the corresponding standard versions.
The two containers considered are
.Formal_Hashed_Maps. The necessary source is in GCC 12.2, though not in GCC 13 (well, the specs are there, but using them will result in a compile time error telling you to go look in a SPARK release; the current Alire
gnatprove contains the same versions as in GCC 12.2).
It was straightforward though tiresome to convert ColdFrame’s code generator to use these containers when generating code for Ravenscar. The way that iterating over maps returns keys rather than elements was the only serious difference.
On building with them, the demonstrator ran just fine, but the executable was quite a bit larger than expected. This turned out to be because my application was built with
-gnata (assertions enabled), and that meant that the large amount of ghost code in the formal containers was built (and, presumably, executed when called for by pre- and post-conditions and other SPARK constructs).
I had thought that the lines
pragma Assertion_Policy (Pre => Ignore); pragma Assertion_Policy (Post => Ignore); pragma Assertion_Policy (Contract_Cases => Ignore);
would result in no code being generated …
Anyway, the results are more than acceptable for the moment: the sizes are
In the table, Button is a standard class with a state machine, LED is a standard class, and A1 is an association class which implements the many-to-many relationship between Button and LED.
‘standard’ means that the translation uses standard containers.
With the standard containers, suppressing assertions doesn’t make a lot of difference.
With the formal containers, suppressing assertions results in a factor of about 5 in size reduction from the standard.
Using the formal containers like this results in warnings,
simple_buttons-a1.ads:17:06: warning: "Ada.Containers.Formal_Hashed_Maps" is an internal GNAT unit [-gnatwi] simple_buttons-a1.ads:17:06: warning: use of this unit is non-portable and version-dependent [-gnatwi] simple_buttons-a1.ads:18:06: warning: "Ada.Containers.Formal_Vectors" is an internal GNAT unit [-gnatwi] simple_buttons-a1.ads:18:06: warning: use of this unit is non-portable and version-dependent [-gnatwi]
It should be fairly straightforward to build a simple pair of containers with just the required set of properties!