Абстрактная интерпретация в LLVM
Мне нужно использовать абстрактную интерпретацию, чтобы провести некоторый анализ с использованием LLVM. Это возможно? или мне нужно проще использовать инструменты анализа. Если бы я мог сделать это с помощью LLVM, какие классы помогли бы мне сформулировать операторы из исходного исходного кода, чтобы получить отношения между переменными (и возможные диапазоны значений для каждой переменной)
3 ответа
Вы можете взглянуть на KLEE, который является символическим интерпретатором для битового кода LLVM: https://github.com/klee
Если вы используете для анализа область интервалов, вы можете использовать класс Constant Range для представления интервалов. Это позволит вам абстрагироваться от арифметических операций над диапазонами. С помощью метаданных отладки и некоторой дополнительной бухгалтерии вы можете получить отношения между переменными. Смотрите этот ответ.
Вы можете взглянуть на статический анализатор Pagai, который вычисляет инварианты для битового кода LLVM с использованием самых современных методов интерпретации абстрактных данных и может создать файл.bc с полученными инвариантами для использования вашим инструментом. http://pagai.forge.imag.fr/