Совмещение ACSL спецификаций с машинным кодом

Аннотация

При разработке программ на языках высокого уровня, разработчикам приходится делать предположение о корректности компилятора. Однако это может быть неприемлемо для критически важных систем. Поскольку на данный момент не существует полноценных компиляторов, для которых корректность доказана, автор предлагает решать эту проблему путём доказательства корректности сгенерированного машинного кода методами дедуктивной верификации. Для достижения данной цели необходимо решить ряд задач, одной из которых является слияние модели спецификаций пред- и постусловий с моделью поведения машинного кода. В данной статье представлен подход к проведению слияния спецификаций для случая Си функций без циклов. Суть подхода заключается построении моделей как машинного кода, так и его спецификации на едином логическом языке, и использовании ABI целевого процессора для связывания машинных регистров с параметрами функции высокого уровня. Для успешной реализации такого подхода необходимо предпринять ряд мер по обеспечению совместимости высокоуровневых спецификаций с моделью поведения машинного кода. К таким мерам, в частности, относятся использование типа регистра в высокоуровневых спецификациях, трансляция пред- и постусловий в абстрактные предикаты. Также в статье производится и обосновывается выбор логического языка для построения моделей, выбираются наиболее подходящие инструменты для реализации подхода слияния спецификаций и производится оценка работы системы дедуктивной верификации машинного кода, построенной на основе предложенного подхода, с использованием тестовых примеров полученных путём компиляции Си программ без циклов.