113. Ada и SPARK: Alire, GNAT для Cortex-M, доказательство

В Ada диапазон — часть типа, и выход за него не проходит молча: его ловит доказатель до сборки или проверка во время работы. SPARK — подмножество Ada, для которого инструмент gnatprove доказывает, что ошибок времени выполнения в коде нет — если вызывающие соблюдают его предусловия. Alire — менеджер пакетов и тулчейнов Ada, как Cargo у Rust: проект описан в alire.toml, а компилятор и зависимости Alire ставит сам. Раздел собирает на Ada ту же CRC-32 из раздела 105 и то же мигание на регистрах — для F103 и F407, в образе stm-ada:1 — и доказывает функцию целиком.

Rust — раздел 114, PlatformIO и CMake — раздел 115, карта памяти и стартовый код — раздел 11.

Как это называется в документации

Оригинал	Перевод
crate	пакет Alire: исходники и манифест
manifest, alire.toml	описание пакета и его зависимостей
toolchain	компилятор со всеми инструментами
solver	подбор версий зависимостей
GPR project file	файл проекта для gprbuild
runtime: light, light-tasking, embedded	среда исполнения: без задач, с задачами, полная
range type	тип с диапазоном
contract, precondition (Pre)	договор подпрограммы, предусловие
SPARK_Mode	код, который берётся доказывать gnatprove
proof, counterexample	доказательство, контрпример
run-time check, Constraint_Error	проверка во время работы, её исключение
last chance handler	последний обработчик ошибки без ОС
aspect Address, Volatile	адрес объекта, запрет оптимизировать доступ

113.1 Alire: пакет и тулчейн

Пакет Alire — каталог с манифестом. Компилятор для Cortex-M — тоже пакет, gnat_arm_elf, и его версию закрепляют, как любую зависимость:

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

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

alr toolchain --select gnat_arm_elf gprbuild ставит кросс-компилятор и сборщик, а alr build -- -XMCU=f103 решает зависимости и зовёт gprbuild с нужным окружением. В опыте Alire 2.1.1 подобрал gnat_arm_elf 16.1.0 и gprbuild 26.0.1; граф зависимостей — одна строка: blink113=0.1.0 --> gnat_arm_elf=16.1.0.

113.2 Проект GPR и среда light

Что и как собирать, описывает файл проекта. Для голого Cortex-M берут среду light: без задач и без кучи, зато с проверками и последним обработчиком ошибок:

   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;

Готовой среды под F103 нет. Под F407 она есть прямо в тулчейне gnat_arm_elf 16.1.0 — light-stm32f4 (и light-tasking-stm32f4, embedded-stm32f4) с картой памяти F407: 1 МБ Flash, 128 КБ ОЗУ и 64 КБ CCM. Опыт собирает оба камня одинаково, на общих средах. Общая среда light-cortex-m4f не знает карты памяти камня, и без неё компоновщик ругается на отсутствие _start и кладёт образ на 0x8000, где у STM32 ничего нет. Поэтому стартовый код и карта памяти свои: crt0.S — таблица векторов, копирование .data, нули в .bss, включение FPU у F407 — и link.ld с флеш-памятью от 0x08000000.

113.3 Регистры: адрес и Volatile

Регистр в Ada — обычная переменная с адресом и запретом оптимизировать доступ:

   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);

Адреса — в пакете Board, свой для каждого камня; gprbuild берёт каталог src/f103 или src/f407 по переменной MCU:

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

Это те же адреса, что в C-варианте _verify/lang113.c, и там они сверены с заголовками CMSIS через _Static_assert.

113.4 Типы с диапазоном и проверки

   type Deci_Celsius is range -400 .. 1250;

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

Температура в десятых долях градуса не может быть 1500 — такого значения у типа просто нет. Опыт на компьютере, родным GNAT: To_Deci (100) — 250, To_Deci (-3) — −7, а To_Deci (600) вместо молчаливого переполнения поднимает Constraint_Error. На приборе исключению деваться некуда, и оно уходит в последний обработчик — компилятор честно предупреждает об этом у каждой проверки. Ключ -gnatp выключает проверки совсем; для кода, ради которого выбирают Ada, он противопоказан.

113.5 SPARK: доказательство вместо проверки

Пакет помечен SPARK_Mode, и gnatprove берётся доказать, что проверки в нём никогда не сработают:

package Crc113 with SPARK_Mode is

gnatprove 16.1.0 из Alire доказал все 5 проверок: деление, диапазон результата и завершение обеих функций. Без предусловия он нашёл две дыры и к каждой — контрпример. Raw_Q4 = -214748365: умножение на 10 не влезает в 32 бита. Raw_Q4 = -161: −161 · 10 / 4 = −402, ниже −400. К обеим он сам предложил предусловие. Доказанный код можно собирать без проверок, если предусловие соблюдают все вызывающие: они тоже доказаны или аргумент проверен на границе, куда приходят внешние данные, — вызов из C, байты из UART. Само Pre во время работы проверяется, только если сборка включила утверждения ключом -gnata: без него To_Deci (600) ловит лишь проверка диапазона результата. Переполнение стека и сбои железа доказательство не покрывает — стек оценивают отдельно, по кадрам функций (раздел 4б.9).

113.6 Что легло в память

Таблица векторов — 4 слова, остальное — CRC, мигание, проверки диапазона и код среды. Сравнение с C и Rust — в разделе 114.

113.7 Грабли

Компоновщик: «cannot find entry symbol _start», образ на 0x8000. Общая среда без карты памяти камня. Свой crt0.S и link.ld или среда под плату.

Сборка падает на предупреждениях о Last_Chance_Handler. -gnatwe превращает их в ошибки. Проверки оставить, а эти предупреждения погасить ключом -gnatw.X.

Alire отказывается читать манифест. Описание длиннее 72 символов.

Генератор стартового кода не собирается. В опыте startup_gen 26.0.0 не собрался родным GNAT 16.1: не компилируется его библиотека libgpr.

Светодиод не мигает, а код верный. Порт не тактируется: сначала бит в RCC, потом режим вывода.

113.8 Итоги

• Alire ставит компилятор и зависимости сам; версии закрепляют в alire.toml.
• Для F103 и F407 — общая среда light плюс свои crt0.S и link.ld.
• Регистр — переменная с Address и Volatile.
• Диапазон — часть типа: To_Deci (600) — Constraint_Error, а не 1500.
• SPARK: gnatprove доказал 5 проверок; без предусловия — две дыры с контрпримерами −214748365 и −161.

Полные исходники

alire.toml — описание пакета Alire.

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"

Дальше: раздел 114 «Rust: Cargo, no_std, cortex-m-rt, embedded-hal» — та же прошивка на Rust и сравнение трёх языков по байтам.