One of us got hooked on the promise of a credit-card-size programmable pocket game under the name of Arduboy and participated in its kickstarter in 2015. The kickstarter was successful (but late) and delivered  the expected working board in mid 2016. Of course, the idea from the start was to program it in Ada , but this is an 8-bits AVR microcontroller (the ATmega32u4 by Atmel) not supported anymore by GNAT Pro. One solution would have been to rebuild our own GNAT compiler for 8-bit AVR from the GNAT FSF repository and use the AVR-Ada project. Another solution, which we explore in this blog post, is to use the SPARK-to-C compiler that we developed at AdaCore to turn our Ada code into C and then use the Arduino toolchain to compile for the Arduboy board.

This is in fact a solution we are now proposing to those who need to compile their code for a target where we do not propose an Ada compiler, in particular small microcontrollers used in industrial automation and automotive industries. Thanks to SPARK-to-C, you can now develop your code in SPARK, compile it to C, and finally compile the generated C code to your target. We have built the universal SPARK compiler! This product will be available to AdaCore customers in the coming months.

We started from the version of Tetris in SPARK that we already ported to the Atmel SAM4S, Pebble-Time smartwatch and Unity game engine. For the details on what is proved on Tetris, see the recording of a talk at FOSDEM 2017 conference. The goal was to make this program run on the Arduboy.

SPARK-to-C Compiler

What we call the SPARK-to-C compiler in fact accepts both less and more than SPARK language as input. It allows pointers (which are not allowed in SPARK) but rejects tagged types and tasking (which are allowed in SPARK). The reason this is the case is that it’s easy to compile Ada pointers into C pointers but much harder to support object oriented or concurrent programming.

SPARK-to-C supports, in particular, all of Ada’s scalar types (enumerations, integers, floating-point, fixed-point, and access) as well as records and arrays and subtypes of these. More importantly, it can generate all the run-time checks to detect violations of type constraints such as integer and float range checks and checks for array accesses out of bounds and access to a null pointer or invalid pointer. Therefore, you can program in Ada and get the guarantee that the executable compiled from the C code generated by SPARK-to-C preserves the integrity of the program, as if you had compiled it directly from Ada with GNAT.

Compiling Ada into C poses interesting challenges. Some of them are resolved by following the same strategy used by GNAT during compilation to binary code. For example, bounds of unconstrained arrays are bundled with the data for the array in so-called "fat pointers", so that both code that directly references Array'First and Array'Last as well as runtime checks for array accesses can access the array bounds in C. This is also how exceptions, both explicit in the code and generated for runtime checks, are handled. Raising an exception is translated into a call to the so-called "last chance handler", a function provided by the user that can perform some logging before terminating the program. This is exactly how exceptions are handled in Ada for targets that don’t have runtime support. In general, SPARK-to-C provides very little runtime support, mostly for numerical computations (sin, cosine, etc.), accessing a real time clock, and outputting characters and strings. Other features require specific source-to-source transformations of Ada programs. For example, functions that return arrays in Ada are transformed into procedures with an additional output parameter (a pointer to some preallocated space in the caller) in C.

The most complex part of SPARK-to-C deals with unnesting nested subprograms because, while GCC supports nested functions as an extension, this is not part of standard C. Hence C compilers cannot be expected to deal with nested functions. Unnesting in SPARK-to-C relies on a tight integration of a source-to-source transformation of Ada code in the GNAT frontend, with special handling of nested subprograms in the C-generation backend. Essentially, the GNAT frontend creates an 'activation record' that contains a pointer field for each uplevel variable referenced in the nested subprogram. The nested subprogram is then transformed to reference uplevel variables through the pointers in the activation record passed as additional parameters. A further difficulty is making this work for indirect references to uplevel variables and through references to uplevel types based on these variables (for example the bound of an array type). SPARK-to-C deals also with these cases: you can find all details in the comments of the compiler file exp_unst.ads

Compiling Tetris from SPARK to C

Once SPARK-to-C is installed, the code of Tetris can be compiled into C with the version of GPRbuild that ships i SPARK-to-C:

For example, the SPARK expression function Is_Empty from Tetris code:

is compiled into the C function tetris_functional__is_empty, with explicit checking of array bounds before accessing the board:

or into the following simpler C function when using compilation switch -gnatp to avoid runtime checking:

Running on Arduboy

To interface the SPARK Tetris implementation with the C API of the Arduboy, we use the standard language interfacing method of SPARK/Ada:

A procedure Arduboy_Set_Screen_Pixel is declared in Ada but not implemented. The pragma Import tells the compiler that this procedure is implemented in C with the name “set_screen_pixel”.

SPARK-to-C will translate calls to the procedure “Arduboy_Set_Screen_Pixel” to calls to the C function “set_screen_pixel”. We use the same technique for all the subprograms that are required for the game (button_right_pressed, clear_screen, game_over, etc.).

The program entry point is in the Arduino sketch file SPARK_Tetris_Arduboy.ino (link). In this file, we define and export the C functions (set_screen_pixel() for instance) and call the SPARK/Ada code with _ada_main_tetris().

It’s that simple :)

If you have an Arduboy, you can try this demo by first following the quick start guide, downloading the project from GitHub, loading the Arduino sketch SPARK_Tetris_Arduboy/SPARK_Tetris_Arduboy.ino, and then clicking the upload button.