Embedded Ada/SPARK, There's a Shortcut

by Fabien Chouteau – Aug 25, 2022

For years in this blog my colleagues and I have published examples, demos, and how-to’s on Ada/SPARK embedded (as in bare-metal) development.

Most of the time, if not always, we focused on one way of doing things: to start from scratch and write everything in Ada/SPARK, from the low level drivers to the application.

There are good reasons for that. First, we are passionate about the Ada language and we truly believe that it is the best solution for embedded systems, from low level drivers to high level functional code. Second, this is a common situation for our customers in the safety critical domain where the entire software stack has to be reliable, trusted, and certified.

That being said, while this way of doing Ada/SPARK embedded will yield the best results in terms of software quality, it might not be the most efficient in all cases. In this blog post I want to present an alternative method to introduce Ada/SPARK into your embedded development projects.

Low level vendor drivers

The alternative is to introduce Ada/SPARK on the high level functional part of the application first, and rely on the drivers provided by the hardware vendors to quickly get the project rolling.

Virtually every piece of hardware you can get your hands on comes with a Software Development Kit (SDK) of low level drivers written in C. The quality of the SDK may vary from vendor to vendor. It’s not uncommon even for C projects to re-write those drivers from scratch, but most of the time SDKs will get you started easily and quickly.

Establish a good Hardware Abstraction Layer (HAL)

The most important thing here is to define the delineation between the low level drivers from the SDK and application code in Ada/SPARK. This is usually called the Hardware Abstraction Layer (HAL). Doing so is actually a good practice in general, whether or not you are mixing Ada and C. Having a good hardware abstraction will also allow you to limit the cost of migrating your project onto a different hardware platform.

This task is not trivial at all, let’s take an example. If I want my application to log data on an SD card, where to put the abstraction:

A subprogram that takes a piece of data and the HAL will do all the work of opening, writing, and closing the file?
A posix-like file system API that the application will use to open, write, and close the file?
An API to read/write the SD card memory blocks and use an Ada/SPARK file system implementation?

There is no right or wrong answer here, but since we are exploring the combination of vendor SDK and Ada I would recommend starting by using as many features as possible from the SDK. It’s always possible to “lower” the abstraction level later, and replace SDK features with Ada/SPARK implementations. So for the example above I would say either option 1 if there is only one kind of access to the SD card file system, or option 2 if there are more uses of the file system throughout the application.

Who is in charge here?

Another important design choice is to decide which part of the system will be the main unit.

You can have a main application loop in C that calls Ada/SPARK code from time to time to provide specific features. Or the other way around, Ada/SPARK main loop that calls the C SDK from time to time.

If you want to use an RTOS written in C, it might be easier to have the cyclic tasks implemented in C and call Ada/SPARK functions from those tasks. Again there is no right or wrong, the answer will depend on your application and the features available in the SDK or RTOS.

Note that in case of a multitask/multithreaded application you have to be careful with the handling of the GNAT secondary stack. You will have to provide an implementation of the __gnat_get_secondary_stack function that returns a different stack pointer for each thread.

Integrating Ada/SPARK and C

In this part I will not go over the details of interfacing Ada/SPARK and C. I recommend having a look at the learn.adacore.com section on this topic: Interfacing With C.

Instead we will look at the integration on the toolchain/compilation side of things. The easiest way to go here is to bundle all the Ada/SPARK code into one or several static libraries that will then be linked to the C application built with the SDK. The Ada run-time has to be linked as well.

To make an Ada/SPARK static library only a couple of attributes are required in the GPR file.

First we specify the library name and kind:

for Library_Name use "my_library";
for Library_Kind use "static";

Then a library interface:

for Library_Interface use ("ada_code");

This attribute is very important as the binder will use it to work the elaboration and produce a function to run the elaboration code. The value “ada_code” is the name of an Ada package, discussed below.

The elaboration function will be called “<Library_Name>init” and it is required that the C code execute this function before calling any Ada/SPARK code.

Finally, linking the Ada/SPARK static library with the C application will of course depend on the build system used in the SDK, whether it’s Makefiles, CMake, or anything else. The SDK documentation likely provides instructions for how to do this.

A Concrete Example

If you are a regular reader of our blog you know that we like to show examples of the solutions we present. So far this blog has been very theoretical, so let’s dive into actual code.

For this example we will use an ESP32-C3 dev-kit. The ESP32-C3 is a 32-bit RISC-V microcontroller with a Wi-Fi and Bluetooth 5 controller. The application will connect to Wi-Fi and run an https server. When a page is requested, the Ada code will provide the HTML content and call a C function to change the color of the on-board LED.

Ada Project Setup

We will use Alire to set up the Ada project, it is not the only way but the tool will generate a few files for us. We first run the init command with the –lib switch to create a library project:

$ alr init –lib ada_code

There is a GPR scenario variable to control the kind of library this will produce, the default is set to static so we don’t have to touch anything here.

We do have to set the Target, Runtime, and Library_Interface attributes:

for Target use "riscv64-elf";
for Runtime ("Ada") use "zfp-rv32imac";
for Library_Interface use ("ada_code");

C Project Setup

For the C side we just follow the getting started instructions from ESP32-C3 documentation.

Instead of using the hello_world example, we copy the https_server one: $IDF_PATH/examples/protocols/https_server

The Hardware Abstraction Layer

For this example we define the HAL as such:

The Ada code provides a function that fills a memory buffer with the content of an HTML page.
The C code provides a function to set the color of the on-board LED.

Here are the specifications for the Ada side:

with System;
with Interfaces;

package Ada_Code is

   -- API exported to the C code --

   function Generate_Page (Buffer     : System.Address;
                           Buffer_Len : Interfaces.Unsigned_32)
                           return Interfaces.Unsigned_32;
   pragma Export (C, Generate_Page, "generate_page");

   -- API imported from C code --

   type LED_Color is (Off, Red, Green, Blue);
   for LED_Color use (Off => 0, Red => 1, Green => 2, Blue => 3);

   procedure Set_LED_Color (Color : LED_Color);
   pragma Import (C, Set_LED_Color, "set_led_color");

end Ada_Code;

And for the C side:

#ifndef _HARDWARE_ABSTRACTION_H_
#define _HARDWARE_ABSTRACTION_H_

/* API exported to Ada/SPARK */

enum LEDColor {OFF = 0, RED = 1, GREEN = 2, BLUE = 3};

void set_led_color(enum LEDColor color);

void __gnat_last_chance_handler(void);

/* API imported from Ada/SPARK */

extern uint32_t generate_page(void *page_buffer, uint32_t buffer_size);

extern void Ada_Codeinit(void);

#endif /* ! _HARDWARE_ABSTRACTION_H_ */

There are a couple things I need to explain here:

__gnat_last_chance_handler: a function that will be called when an (unhandled) Ada exception is raised. It is implemented in C to use the event logging features of the ESP SDK.
Ada_Codeinit: the Ada elaboration function I mentioned above. It is provided in the Ada static library and must be called from the C code.
Set_led_color: Here I could have made a reusable binding for the ESP SDK LED strip library. But I really only care about setting the color of one LED. So as I explained above I keep the HAL as simple as possible.

Who is in charge here?

The application is relatively simple; we just want to serve one HTML page. The C code will be mostly in charge and just sporadically call the Ada code to fill a buffer with the content of the page.

Integrating Ada/SPARK and C

The ESP SDK is based on CMake which is fairly flexible if you put in the time to learn how things work. I will just show you the code that we have to add to the CMakeLists.txt file in the root directory.

What is going on here is:

Call Alire to build the Ada code
Link the Ada code static library
Find the location of the Ada run-time library
Link the Ada run-time library

# Build the Ada code using Alire
execute_process(COMMAND alr -n build
                WORKING_DIRECTORY "${PROJECT_SOURCE_DIR}/../ada_code/")

# Add the Ada code static library
add_library(ada_code STATIC IMPORTED GLOBAL)
set_property(TARGET ada_code PROPERTY IMPORTED_LOCATION "${CMAKE_SOURCE_DIR}/../ada_code/lib/libAda_Code.a")
target_link_libraries(https_server.elf PUBLIC ada_code)

# Get path of Ada run-time library (libgnat.a)
execute_process(COMMAND bash -c "alr exec -- riscv64-elf-gnatls --RTS=zfp-rv32imac -v 2>&1 | grep adalib"
                WORKING_DIRECTORY "${PROJECT_SOURCE_DIR}/../ada_code/"
                RESULT_VARIABLE gnatls_result
                OUTPUT_VARIABLE gnatls_output)

string(STRIP "${gnatls_output}" ada_runtime_dir)

# Add the Ada run-time static library
message(STATUS "Link Ada run-time ${ada_runtime_dir}/libgnat.a")
add_library(libgnat STATIC IMPORTED GLOBAL)
set_property(TARGET libgnat PROPERTY IMPORTED_LOCATION "${ada_runtime_dir}/libgnat.a")
target_link_libraries(https_server.elf PUBLIC libgnat)

I am sure there are better ways to do this with CMake, don’t hesitate to comment below if you have some suggestions.

Filling the blanks

The only thing left to do is to implement the HAL functions on both sides and call the Ada function to generate HTML from the root_get_handler function. All the code is available in this repository if you want to see the full picture: https://github.com/Fabien-Chou...

Blinky!

Once the application is built and flashed to the ESP32-C3, we have our little device serving HTML pages generated from Ada code over https.

Conclusion

With this simple example we can see how easily one can integrate Ada/SPARK code into an embedded project. The most difficult part really was to figure out the right way to link static libraries with CMake.

Posted in #Embedded

About Fabien Chouteau

Fabien joined AdaCore in 2010 after his engineering degree at the EPITA (Paris). He is involved in real-time, embedded and hardware simulation technology. Maker/DIYer in his spare time, his projects include electronics, music and woodworking.