ColdFrame and the micro:bit revisited

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 -mlittle-endian, -msoft-float, -mcpu=cortex-m0, -mthumb).

Issues

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 s-retsta.ads (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.

Tagged Containers considered fattening

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 -ffunction-sections and -fdata-sections, and linking with -gc-sections, a lot of Container code was included in spite of not being used (ColdFrame for Ravenscar uses Ada.Containers.Bounded_Vectors and .Bounded_Hashed_maps).

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.

Requirements:

• 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.Containers versions 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 SaloonHandler).
• should support iterators, for ... of ... preferred.

Candidates considered:

• 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_Trees would 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.

Formal Containers

The two containers considered are Ada.Containers.Formal_Vectors and .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

	Button	LED	A1
standard, -O2, -gnata	10888	9780	19408
standard, -O2	10848	9740	18240
formal, -O0, -gnata	13104	11040	10404
formal, -O2	2068	885	4436

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.

An observation:

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!