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