SMT решатели для битовой векторной арифметики

Я планирую несколько экспериментов по символическому исполнению кода на языке C, используя готовый SMT-решатель, и задаюсь вопросом, какой решатель использовать; например, рассматривая участников конкурса SMT и принимая только системы с открытым исходным кодом, мы сужаем их до Beaver, Boolector, CVC3, OpenSMT, Sateen, Sonolar, STP, Verit; который все еще длинный список.

Пытаясь сузить это немного дальше, я замечаю, что некоторые системы рекламируют способность обрабатывать битовую векторную арифметику, тогда как другие рекламируют только способность обрабатывать общую целочисленную арифметику. В принципе, первое верно для C, где переменные являются машинными словами, а не неограниченными целыми числами. Насколько это важно на практике? Что произойдет, если вы попытаетесь использовать общую целочисленную систему для такого рода работы? Применяется ли один из следующих сценариев?

  1. Битовая векторная система немного более эффективна, но вы можете использовать любую, без проблем.

  2. Вы можете использовать общую целочисленную систему с небольшой настройкой.

  3. Обычная целочисленная система хороша для подписанного типа int (поскольку результат переполнения не определен), но даст неправильный ответ для неподписанного.

  4. Обычная целочисленная система просто не подходит для арифметики машинных слов, и я могу сократить свой короткий список только до тех систем, которые предоставляют битовую векторную арифметику.

  5. Что-то другое...?

Я пытался задать как можно более конкретный вопрос, но если кто-нибудь может предложить какие-либо другие критерии для сужения списка, это было бы здорово!

Источник

2 ответа

Решение

У меня был хороший опыт использования STP для символического исполнения. STP был разработан именно для этой задачи. Кроме того, было несколько символических инструментов выполнения, которые успешно использовали STP для этой цели, поэтому есть основания полагать, что STP не сосет. Я определенно рекомендую STP другим в качестве выбора по умолчанию для такого рода экспериментов.

Однако я не пробовал другие системы, поэтому я не знаю, как STP сравнивается с ними.

Лично я вижу STP в качестве базовой линии и выбора по умолчанию для такого рода приложений. Так что, если у вас есть время, чтобы попробовать один решатель, попробовать STP кажется вполне разумным выбором.

Если бы мне пришлось угадывать, я бы предположил, что важно поддерживать арифметику битовых векторов, потому что любой большой системный код будет содержать нетривиальный объем кода, который выполняет побитовые операции. Кроме того, я подозреваю, что некоторые системные коды могут полагаться на поведение беззнаковой арифметики для переноса по модулю 2n, и если вы попытаетесь смоделировать его целыми числами, вы не получите правильную семантику C (потому что, как вы говорите,, целые числа просто не верны для машинной арифметики), и, следовательно, если вы попытаетесь использовать решатель только для целых чисел, у вас могут возникнуть некоторые трудности. Однако у меня нет веских доказательств ни для одного из этих подозрений.

PS Z3 также может быть претендентом на добавление в ваш список для рассмотрения. (Вам действительно нужен ваш решатель с открытым исходным кодом, если он бесплатный? Я бы ожидал, что символический инструмент выполнения будет использовать его только как черный ящик, без изменений.)

Источник

Согласно SMT-Wikipedia на 2011-08, у нас есть:

Исходя из этих мер, представляется, что наиболее яркими, хорошо организованными проектами являются OpenSMT, STP и CVC4.

Я просто проверяю этот материал - пока что все три, кажется разумным, плюс старый CVC -> CVC3.

Источник
Другие вопросы по тегам