Xenolith Engine 

Для экспериментов с формальной верификацией кода (для встраиваемых приложений в первую очередь) у нас появился форк знаменитого инструмента CBMC.

CBMC это инструмент, позволяющий на основе формальной логики доказать отсутствие определённых классов ошибок в коде. Не "проверить, что работает", как инструменты тестирования, а выстроить полную цепочку математического доказательства отсутствия ошибки. Не любой, а строго конкретного вида (проблему останова никто не отменял). К счастью, самые распространённые ошибки известны заранее.

Без нейросетей, на такую работу просто не остаётся времени: научный код слишком сложный для интеграции в него своих концепций, только на поиск места для расширения могут уйти недели. При том, что сам код достаточно просто подтверждается на целевых задачах. Математика - штука строгая, и нарушения в решателе будут заметны сразу. Но даже с нейросетями, нужно сперва знать, а что вообще нужно и имеет смысл делать.

В первую очередь, добавлена полноценная поддержка хорновских дизъюнктов в качестве вывода символьного исчисления. Решаются через Z3 и Golem. Это серьёзно расширяет поддерживаемые классы кодовых выражений, которые покрываются верификатором. В частности, это индукция по рекурсии и сворачивание циклов в одно выражение. То есть, больше кода может стать верифицируемым.

Был вариант использовать SeaHorn и CBMC одновременно, но, во-первых, SeaHorn не настолько зрелый инструмент, и, во-вторых, они работают над разной базой: CBMC покрывает код непосредственно, а SeaHorn - байткод LLVM после конвертации. Потому, корректнее расширить CBMC для покрытия обоих классов.

Во вторую, добавлено четыре новых инструмента для профилирования результата работы верификатора:

--symex-merge-report показывает слияния путей, на которых значение перестаёт быть константой.

--equation-report показывает состав уравнения после среза по месту в коде.

--equation-trace показывает, где именно значение перестаёт быть константой.

Исправление ошибок предыдущего

- В набор на Linux не попали нужные библиотеки spir-v

- В iOS не попала libtiff

- Наборы Windows собрались без вложенных лицензий

- Убрана некорректная ссылка на lib/clang/include для wasm

- Перед релизом пакеты теперь проверяются на некомплект

И, в некоторой степени вынужденно, в этом же релизе добавлена экспериментальная поддержка loongarch64 для Linux в качестве host и target.

Долго мы шли к тому, чтобы действительно показать что-то интересное, кроме кода и картинок. Наконец, пришли.

Playground - сборка с использованием нашего SDK всякого разного прямо в браузере. Без сервера, без CI, прямо на странице. Там есть Doom и HoMM2. И наши примеры. Код можно менять, перекомпилировать и собирать себе на настольную систему. Сборка работает даже на мобильных устройствах. На сами мобильные устройства сборки нет. Но. кто знает, может и появится.

https://github.com/XenolithEngine/xenolith-engine/releases/tag/sdk-v0rc0
 
SDK потихоньку двигается к релизу. С этого момента оно торжественно назначается release candidate, а значит, существенных изменений до версии v1 не ожидается.
 
Ключевые изменения:
- Поддержка wasm64 как target
- Патчи LLVM для wasm как host
- Убрана поддержка mbedtls - это второй по кошмарности поддержки проект после libzip, и поддержка этого бэка для криптографии тянулась скорее по памяти со времён, когда openssl не имела стабильной версии на Android.
 
Чего нет:
- Wasm host. Раз уж это называется RC, самой экспериментальной из наших фич тут точно не место. Патчи, однако, проверены, потому включены.
- embox и nulltx бинарными релизами не собираются - они зависят от конкретной сборки ОС
- экспериментальный режим embox+user (работа рантайма на уровне пользователя EL0, а не уровне ядра EL1) - шаблон для него в коде есть, реализации пока нет.
 
MacOS+open и Windows хосты собраны самим SDK, как и раньше, MacOS без +open - на базе MacOS SDK (без него в AppStore не пустит), linux под glibc 2.33 (запустится через обратную совместимость).