Почему это символическое выполнение с Z3 приводит к ошибке?

Question

Я пытаюсь создать тестовые примеры, используя символьную логику выполнения на основе SMT Solver Z3.

У меня есть следующий код.

      void foo(int a, int b, int c){
    int x = 0, y = 0, z = 0;
    if(a){
        x = -2;
    }

    if (b < 5){
        if (!a && c) { y = 1; }
        z = 2;
    }

    assert(x + y + z != 3);
}

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

      (set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-option :produce-proofs true)
(define-sort bot () Int)

(declare-const sv_1 Int)
(declare-const sv_5 Int)
(define-fun strcmp ((a String) (b String)) Int (ite (= a b) 0 1))

(assert (! (not (= sv_1 0)) :named __a0))
(assert (! (< sv_5 5) :named __a1))
(assert (! (not (not (= sv_1 0))) :named __a2))
(assert (! (not (not (= (+ (+ (bvneg 2) 0) 2) 3))) :named __a3))
(check-sat)
(get-unsat-core)
(get-model)

Я провел некоторое тестирование с этим кодом.

Если я не использую x, y, z в функции assert, ошибки нет.

Если первый оператор if - истина (т. Е. A! = 0), то программа никогда не будет вводить оператор if (! A && c). Если я удалю один из этих операторов if, ошибки не будет. Но я не понимаю, почему возникает эта ошибка. Может ли кто-нибудь объяснить мне, почему Z3 не может решить эту проблему? Спасибо.

Answer 1

Вы не сказали нам, какую именно ошибку вы получаете, поэтому я предполагаю, что она исходит от z3, а не от какой-то другой части вашей инструментальной цепочки. Давайте запустим программу SMTLib, которую вы разместили через z3. Когда я это делаю, z3 сообщает мне, что есть «несоответствие сортировки»:

      (error "line 13 column 38: operator is applied to arguments of the wrong sort")

И это потому, что у вас есть строка:

      (assert (! (not (not (= (+ (+ (bvneg 2) 0) 2) 3))) :named __a3))

и, в частности, выражение (bvneg 2). Функция является отрицанием битового вектора, но 2является целым числом, а не значением битового вектора. Вместо этого вы хотите использовать обычное отрицание. Итак, измените эту строку на:

      (assert (! (not (not (= (+ (+ (- 0 2) 0) 2) 3))) :named __a3))

После этого изменения z3 говорит:

      unsat
(__a3)
(error "line 16 column 10: model is not available")

Большой; так что теперь у вас есть, а unsat-core есть. Ошибку в последней строке можно проигнорировать, она возникает из-за того, что вы позвонили get-model но проблема неудовлетворительна, и поэтому нет модели для отображения.

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

Это сводится к этим двум строкам, созданным вашим инструментом:

      (assert (! (not (= sv_1 0)) :named __a0))
(assert (! (not (not (= sv_1 0))) :named __a2))

Давайте упростим их, отбросив аннотации, и для ясности я переименую sv_1к, поскольку, похоже, это источник переменной. Это дает нам:

      (assert (not (= a 0)))
(assert (not (not (= a 0))))

Давайте немного упростим:

      (assert (distinct a 0))
(assert (not (distinct a 0)))

(В SMTLib, (distinct x y) средства (not (= x y)).)

И теперь мы видим проблему; у вас есть два утверждения, первое говорит, что нет , а второе говорит, что это не так, a не является 0. Ясно, что эти два утверждения противоречат друг другу, и именно об этом вам сообщает z3.

На самом деле есть еще один источник конфликта. Другое утверждение упрощает:

      (assert (not (not (= (+ (+ (- 0 2) 0) 2) 3)

что, если вы выполните арифметику, говорит:

      (assert (= 0 3))

что явно не так. (Вот почему z3 сообщает вам ваш unsat ядро __a3; что является основной причиной невыполнимости всего набора предположений. Обратите внимание, что неподходящие ядра не уникальны, и z3 не гарантирует, что предоставит вам минимальный набор. Так он мог бы сказать вам (__a0 __a2)а также unsat-core; но это отдельное обсуждение.)

Итак, z3 поступает правильно, учитывая вашу сгенерированную библиотеку SMTLib (после исправления, упомянутого выше).

Почему ваш инструмент генерирует эту SMTLib для C-программы, мы не сможем вам помочь, если вы не расскажете нам больше о том, как вы сгенерировали этот вывод или что на самом деле делает этот промежуточный инструмент. Мое приблизительное предположение состоит в том, что на самом деле он генерирует кучу тестовых примеров, и в конечном итоге доходит до того, что он говорит: «У меня больше нет тестовых примеров для генерации», так что на самом деле все в порядке; но, похоже, есть некоторая проблема с тем, почему он генерирует (get-model)вызов; или почему это сделало бы bvnegвызов, который неверен. Но в противном случае вам придется проконсультироваться с разработчиками инструмента, который генерирует для вас эту SMTLib для дальнейшей отладки.