PLComp

Forwarded from Covalue

Bertot, [2008] "Structural abstract interpretation, A formal study using Coq"

+ порт на Агду

В статье обсуждается кодирование внутри теории типов подхода к статическому анализу программ, известного как абстрактная интерпретация (АИ). Для анализа взят простой императивный язык с целочисленными значениями (можно ограничить до натуральных) со сложением и булевым сравнением, мутабельными переменными, последовательной композицией и while-циклами. Корректность полученного абстрактного интерпретатора доказана относительно аксиоматической (Хоаровой) семантики языка, а гарантия завершимости получается по построению.

Идея абстрактной интерпретации заключается в вычислении приближенных значений для некоторых аспектов поведения программы - обычно анализ делается по графу потока управления программы, но в статье анализируется напрямую синтаксическое дерево. Такую аппроксимацию, как правило, можно получить значительно быстрее, нежели исполнять саму программу, при этом на её основании можно проводить компиляторные оптимизации и делать выводы о корректности. Стандартным примером приближенного анализа является огрубление точных значений числовых переменных до бита четности или интервала значений. Классически при этом выводится аппроксимация "сверху" (overapproximation), т.е. мы хотим гарантировать отсутствие ложноотрицательных результатов за счет возможных ложноположительных (стандартный компромисс статического анализа). Формально отношения между точными (конкретными) и приближенными (абстрактными) множествами значений описываются в теории АИ через соответствия Галуа (пара функции абстракции α и функции конкретизации γ, необходимы для транспорта отношений порядка), в статье используется ad-hoc форма этой конструкции. Также требуется, чтобы домен абстрактных значений имел структуры полугруппы (т.к. моделируются числовые значения) и ограниченной (полу)решетки.

Для задания семантики анализируемого языка используется исчисление предусловий, состоящее из (1) бескванторных логических формул (предусловий/assertions) и аннотированных ими программ, (2) функции вычисления наислабейшего предусловия (формулы, которой должны удовлетворять переменные в начале исполнения) по аннотированной программе и (3) функции для генерации условий проверки (набор импликаций, которые, будучи валидными, гарантируют что любое исполнение программы, стартующее из удовлетворяющего предусловию состояния, будет удовлетворять всем последующим формулам). Для while-циклов также добавляются явные инварианты. Нужно заметить, что в самой статье полноценная аксиоматическая семантика c пред- и постусловиями не вводится, но это проделано в предыдущей статье автора, откуда я взял соответствующий кусок с доказательствами корректности аксиоматической семантики относительно операционной и корректности генератора условий. Ключевым же свойством генератора условий для корректности абстрактного интерпретатора является монотонность, т.е. валидность условий, построенных из некой формулы влечет валидность условий, построенных из её ослабления. Задача абстрактного интерпретатора - по исходной программе и абстрактному начальному состоянию одновременно вывести аннотированную программу и абстрактное конечное состояние.

В статье демонстрируется построение двух вариантов абстрактного интерпретатора, причем во втором, более продвинутом, сделана попытка обнаруживать незавершимость и мёртвые ветки кода. В качестве базовой инфраструктуры для обоих вариантов вводится таблица поиска (lookup table) для абстрактных состояний переменных (пары из имени переменной и абстрактного значения; отсутствующие переменные имеют по умолчанию значение верхнего элемента полурешетки) и набор функций для отображения этих состояний в логические формулы, каковые функции должны иметь ряд свойств (включающие, например, требования параметричности отображения и перевода верхнего элемента в тривиальную истину). Для верификации интерпретатора также нужна функция построения предиката внутри метатеории (теории типов) по его сигнатуре.

www.tg-me.com/us/PLComp/com.plcomp/108

1.2K viewsAlex Gryzlov, Jul 23, 2024 at 12:18

Bertot, [2008] "Structural abstract interpretation, A formal study using Coq"

+ порт на Агду

В статье обсуждается кодирование внутри теории типов подхода к статическому анализу программ, известного как абстрактная интерпретация (АИ). Для анализа взят простой императивный язык с целочисленными значениями (можно ограничить до натуральных) со сложением и булевым сравнением, мутабельными переменными, последовательной композицией и while-циклами. Корректность полученного абстрактного интерпретатора доказана относительно аксиоматической (Хоаровой) семантики языка, а гарантия завершимости получается по построению.

Идея абстрактной интерпретации заключается в вычислении приближенных значений для некоторых аспектов поведения программы - обычно анализ делается по графу потока управления программы, но в статье анализируется напрямую синтаксическое дерево. Такую аппроксимацию, как правило, можно получить значительно быстрее, нежели исполнять саму программу, при этом на её основании можно проводить компиляторные оптимизации и делать выводы о корректности. Стандартным примером приближенного анализа является огрубление точных значений числовых переменных до бита четности или интервала значений. Классически при этом выводится аппроксимация "сверху" (overapproximation), т.е. мы хотим гарантировать отсутствие ложноотрицательных результатов за счет возможных ложноположительных (стандартный компромисс статического анализа). Формально отношения между точными (конкретными) и приближенными (абстрактными) множествами значений описываются в теории АИ через соответствия Галуа (пара функции абстракции α и функции конкретизации γ, необходимы для транспорта отношений порядка), в статье используется ad-hoc форма этой конструкции. Также требуется, чтобы домен абстрактных значений имел структуры полугруппы (т.к. моделируются числовые значения) и ограниченной (полу)решетки.

Для задания семантики анализируемого языка используется исчисление предусловий, состоящее из (1) бескванторных логических формул (предусловий/assertions) и аннотированных ими программ, (2) функции вычисления наислабейшего предусловия (формулы, которой должны удовлетворять переменные в начале исполнения) по аннотированной программе и (3) функции для генерации условий проверки (набор импликаций, которые, будучи валидными, гарантируют что любое исполнение программы, стартующее из удовлетворяющего предусловию состояния, будет удовлетворять всем последующим формулам). Для while-циклов также добавляются явные инварианты. Нужно заметить, что в самой статье полноценная аксиоматическая семантика c пред- и постусловиями не вводится, но это проделано в предыдущей статье автора, откуда я взял соответствующий кусок с доказательствами корректности аксиоматической семантики относительно операционной и корректности генератора условий. Ключевым же свойством генератора условий для корректности абстрактного интерпретатора является монотонность, т.е. валидность условий, построенных из некой формулы влечет валидность условий, построенных из её ослабления. Задача абстрактного интерпретатора - по исходной программе и абстрактному начальному состоянию одновременно вывести аннотированную программу и абстрактное конечное состояние.

В статье демонстрируется построение двух вариантов абстрактного интерпретатора, причем во втором, более продвинутом, сделана попытка обнаруживать незавершимость и мёртвые ветки кода. В качестве базовой инфраструктуры для обоих вариантов вводится таблица поиска (lookup table) для абстрактных состояний переменных (пары из имени переменной и абстрактного значения; отсутствующие переменные имеют по умолчанию значение верхнего элемента полурешетки) и набор функций для отображения этих состояний в логические формулы, каковые функции должны иметь ряд свойств (включающие, например, требования параметричности отображения и перевода верхнего элемента в тривиальную истину). Для верификации интерпретатора также нужна функция построения предиката внутри метатеории (теории типов) по его сигнатуре.

BY PLComp