Докажите, что выражение проверки переполнения верно - PullRequest
Новая
       8

Докажите, что выражение проверки переполнения верно

0 голосов
/ 10 февраля 2019

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

Функция C ++: 

template <typename T>
bool add(int radix, int digit, T& n)
{
    assert(radix > 2);
    assert(radix <= 36);
    assert(digit >= 0);
    assert(digit < radix);

    T max = std::numeric_limits<T>::max();
    assert(max >= radix);

    // the overflows check
    if ((n > (max / radix)) || ((n * radix) > (max - digit)))
        return false;

    n = n * radix + digit;
    return true;
}

Я хочу доказать (деления целые, вещественной части нет):

(n > (max / radix)) || ((n * radix) > (max - digit)) <=> n > ((max - digit) / radix)

или в более общем случае, если эти выражения всегда истинны, когда (n * radix) > max или (n * radix + digit) > max

Z3-код, который у меня есть: 

(declare-const radix Int)
(assert (>= radix 2))
(assert (<= radix 36)) ; this is the upper bound we officially support

(declare-const digit Int)
(assert (>= digit 0))
(assert (< digit radix))

(declare-const max Int)
(assert (> max 0))
(assert (>= max radix)) ; this is a reasonable requirement
;(assert (>= max 256)) ; the smallest upper bound for C++ fundamentals, but UDTs can have it lower

(declare-const n Int)
(assert (<= n max))
;(assert (>= n 0)) ; not really, but usually

; our current check
;(assert (not (or
;  (> n (div max radix))
;  (> (* n radix) (- max digit))
;)))
; our optimized check
(assert (not
  (> n (div (- max digit) radix))
))

(assert (or
  (> (* n radix) max)           ; check no mul overflow
  (> (+ n digit) max)           ; check no add overflow
  (> (+ (* n radix) digit) max) ; check no muladd overflow
))

(check-sat)
(get-model)
(exit)

https://rise4fun.com/Z3/po1h

1 Ответ

0 голосов
/ 10 февраля 2019

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

(define-fun oldCheck () Bool
  (or (> n (div max radix)) 
      (> (* n radix) (- max digit))))

(define-fun newCheck () Bool
      (> n (div (- max digit) radix)))

(assert (distinct oldCheck newCheck))

, который четко показывает, что вы проверяете.Вы можете быть уверены, что ваша оптимизация хороша!

Примечание к отдельному

Предикату distinct определено на странице 37 документа SMTLib: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

Это по существу эквивалентно отрицательной эквивалентности, если вы передадите ей точно два аргумента.Однако поведение отличается для> 2 аргументов: если вы передадите больше аргументов, это обеспечит парное неравенство.(То есть все они должны отличаться друг от друга.) Это очень удобно во многих задачах.

Передача> 2 аргументов в = также возможна, и это гарантирует, что все аргументыравны.Но обратите внимание, что когда у вас есть> 2 аргумента, отрицательное равенство и отличное становятся различными: например, 2 2 3, не все равны, но они также не distinct.Надеюсь, это проясняет ситуацию.

Замечание по проверке переполнения / переполнения

Патрик поднял вопрос проверки переполнения и использования целых чисел машины, и он прав, что следует беспокоиться об этих случаях.,Я думаю, что Никита уже обрабатывает конкретный случай использования, обеспечивая четкие границы.Однако нельзя быть слишком осторожным!Для этих целей в z3 встроены примитивы проверки переполнения. См. Этот замечательный документ Николая о деталях: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf

Примитивы, которые предоставляет z3:

  • bvsmul_noovfl: Умножение со знаком без переполнения
  • bvsmul_noudfl: Умножение со знаком без недостатка
  • bvumul_noovfl: Умножение без знака без переполнения

Но см. Статью о логических формулахВы можете использовать для обнаружения переполнения для других операций.(Выше три довольно сложны, поэтому они поддерживаются примитивно. Для других условий проверки могут выполняться непосредственно пользователем.)

...