113. Ada and SPARK: Alire, GNAT for Cortex-M, proof

In Ada a range is part of the type, and going outside it never passes silently: it is caught either by the prover before the build or by a check at run time. SPARK is a subset of Ada for which the gnatprove tool proves that the code has no run-time errors — provided the callers respect its preconditions. Alire is the package and toolchain manager for Ada, like Cargo for Rust: the project is described in alire.toml, and Alire installs the compiler and dependencies by itself. This section builds in Ada the same CRC-32 from section 105 and the same register-level blink — for F103 and F407, in the stm-ada:1 image — and proves a function in full.

Rust is section 114, PlatformIO and CMake are section 115, the memory map and startup code are section 11.

Terms used in the documentation

Term	Meaning
crate	an Alire package: sources and a manifest
manifest, alire.toml	the description of a package and its dependencies
toolchain	the compiler with all its tools
solver	picking the versions of dependencies
GPR project file	the project file for gprbuild
runtime: light, light-tasking, embedded	run-time environment: no tasks, with tasks, full
range type	a type with a range
contract, precondition (Pre)	the contract of a subprogram, a precondition
SPARK_Mode	code that gnatprove undertakes to prove
proof, counterexample	a proof, a counterexample
run-time check, Constraint_Error	a check at run time, its exception
last chance handler	the final error handler when there is no OS
aspect Address, Volatile	the address of an object, no optimizing of accesses

113.1 Alire: the package and the toolchain

An Alire package is a directory with a manifest. The compiler for Cortex-M is also a package, gnat_arm_elf, and its version is pinned like any other dependency:

[[depends-on]]
gnat_arm_elf = "=16.1.0"                    # версия закреплена: размеры образа не поплывут

# камень выбирают при сборке: alr build -- -XMCU=f103
[gpr-set-externals]
MCU = "f407"

alr toolchain --select gnat_arm_elf gprbuild installs the cross-compiler and the builder, and alr build -- -XMCU=f103 resolves the dependencies and calls gprbuild with the right environment. In the experiment Alire 2.1.1 picked gnat_arm_elf 16.1.0 and gprbuild 26.0.1; the dependency graph is one line: blink113=0.1.0 --> gnat_arm_elf=16.1.0.

113.2 The GPR project and the light runtime

What to build and how is described by the project file. For bare Cortex-M you take the light runtime: no tasks and no heap, but with checks and a last chance handler:

   for Languages use ("Ada", "Asm_Cpp");
   for Target use "arm-eabi";
   case MCU is
      when "f103" => for Runtime ("Ada") use "light-cortex-m3";
      when "f407" => for Runtime ("Ada") use "light-cortex-m4f";
   end case;

There is no ready-made runtime for F103. For F407 there is one right in the toolchain gnat_arm_elf 16.1.0 — light-stm32f4 (plus light-tasking-stm32f4 and embedded-stm32f4) with the F407 memory map: 1 MB Flash, 128 KB RAM and 64 KB CCM. The experiment builds both chips the same way, on the generic runtimes. The generic runtime light-cortex-m4f does not know the memory map of the chip, and without it the linker complains that _start is missing and places the image at 0x8000, where an STM32 has nothing. So the startup code and the memory map are our own: crt0.S — the vector table, copying .data, zeroing .bss, enabling the FPU on F407 — and link.ld with Flash starting at 0x08000000.

113.3 Registers: address and Volatile

A register in Ada is an ordinary variable with an address and a ban on optimizing accesses to it:

   Enable : Unsigned_32 with Volatile, Import, Address => To_Address (Board.RCC_Enable);
   Mode   : Unsigned_32 with Volatile, Import, Address => To_Address (Board.Mode_Address);
   ODR    : Unsigned_32 with Volatile, Import, Address => To_Address (Board.ODR_Address);

The addresses live in the Board package, one per chip; gprbuild takes the directory src/f103 or src/f407 according to the MCU variable:

package Board is
   RCC_Enable   : constant Integer_Address := 16#4002_1018#;   --  RCC_APB2ENR
   Enable_Bit   : constant Unsigned_32 := 16#10#;              --  IOPCEN
   Mode_Address : constant Integer_Address := 16#4001_1004#;   --  GPIOC_CRH

These are the same addresses as in the C version _verify/lang113.c, and there they are checked against the CMSIS headers with _Static_assert.

113.4 Range types and checks

   type Deci_Celsius is range -400 .. 1250;

   function To_Deci (Raw_Q4 : Integer) return Deci_Celsius
     with Pre => Raw_Q4 in -160 .. 500;

A temperature in tenths of a degree cannot be 1500 — the type simply has no such value. An experiment on a PC with native GNAT: To_Deci (100) gives 250, To_Deci (-3) gives −7, and To_Deci (600), instead of silently overflowing, raises Constraint_Error. On the device the exception has nowhere to go, and it ends up in the last chance handler — the compiler honestly warns about this at every check. The -gnatp switch turns the checks off completely; for the code you choose Ada for, it is contraindicated.

113.5 SPARK: proof instead of checks

The package is marked SPARK_Mode, and gnatprove undertakes to prove that the checks in it will never fire:

package Crc113 with SPARK_Mode is

gnatprove 16.1.0 from Alire proved all 5 checks: the division, the range of the result and the termination of both functions. Without the precondition it found two holes and a counterexample for each. Raw_Q4 = -214748365: the multiplication by 10 does not fit in 32 bits. Raw_Q4 = -161: −161 · 10 / 4 = −402, below −400. For both it proposed a precondition by itself. Proven code can be built without checks if every caller respects the precondition: the callers are proven too, or the argument is checked at the boundary where external data comes in — a call from C, bytes from a UART. The Pre itself is checked at run time only if the build enabled assertions with the -gnata switch: without it To_Deci (600) is caught only by the range check on the result. Stack overflow and hardware faults are not covered by the proof — the stack is estimated separately, from the function frames (section 4б.9).

113.6 What ended up in memory

The vector table is 4 words; the rest is the CRC, the blink, the range checks and runtime code. The comparison with C and Rust is in section 114.

113.7 Pitfalls

Linker: "cannot find entry symbol _start", image at 0x8000. A generic runtime without the chip's memory map. Use your own crt0.S and link.ld, or a runtime for the board.

The build fails on warnings about Last_Chance_Handler. -gnatwe turns them into errors. Keep the checks, and silence these warnings with the -gnatw.X switch.

Alire refuses to read the manifest. The description is longer than 72 characters.

The startup code generator does not build. In the experiment startup_gen 26.0.0 did not build with native GNAT 16.1: its libgpr library does not compile.

The LED does not blink, yet the code is correct. The port is not clocked: first the bit in RCC, then the pin mode.

113.8 Summary

• Alire installs the compiler and dependencies by itself; versions are pinned in alire.toml.
• For F103 and F407 — the generic light runtime plus your own crt0.S and link.ld.
• A register is a variable with Address and Volatile.
• A range is part of the type: To_Deci (600) gives Constraint_Error, not 1500.
• SPARK: gnatprove proved 5 checks; without the precondition — two holes with counterexamples −214748365 and −161.

Full sources

alire.toml — the Alire package description.

name = "blink113"
description = "Blink and CRC-32 on STM32F103/F407 registers (handbook 113)"
version = "0.1.0"
authors = ["STM32 Handbook"]
maintainers = ["STM32 Handbook <stm32@example.com>"]
maintainers-logins = ["stm32"]
licenses = "MIT"
project-files = ["blink.gpr"]
executables = ["blink"]

# кросс-компилятор для Cortex-M: Alire поставит его сам и сделает PATH для gprbuild
[[depends-on]]
gnat_arm_elf = "=16.1.0"                    # версия закреплена: размеры образа не поплывут

# камень выбирают при сборке: alr build -- -XMCU=f103
[gpr-set-externals]
MCU = "f407"

Next: section 114 "Rust: Cargo, no_std, cortex-m-rt, embedded-hal" — the same firmware in Rust and a byte-by-byte comparison of the three languages.