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

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

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

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

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

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

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

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

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


verification smt theorem-proving
person rwallace    schedule 07.06.2011    source источник

Ответы (2)


arrow_upward
7
arrow_downward

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

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

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

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

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

person D.W.    schedule 30.06.2011

arrow_upward
2
arrow_downward

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

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

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

person Grzegorz Wierzowiecki    schedule 01.09.2011