证明溢出检查表达是右

Question

我有一个包含其是简单地用手可证明的表达式（溢流检查）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

Answer 1

对我来说看上去很好。风格上，我会写它像下面这样：

(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谓词定义SMTLib文件第37页：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

如果你通过它恰恰两个参数这基本上等同于否定等价。然而，该行为是> 2个ARGS不同：如果传递的参数可以确保成对的不平等。 （也就是说，所有的人都必须互不相同。），它有很方便的诸多问题。

传递> 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：无符号乘法没有溢出

但是看到你可以用它来检测溢出进行其它操作的逻辑公式的纸。 （以上三种是相当复杂的，所以它们原始地支持。对于其他情况，该检查可以直接由用户来完成。）