证明溢出检查表达式是正确的

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 的注释

distinct 谓词定义在 SMTLib 文档的第 37 页：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

如果你正好传递两个参数，它本质上等同于取反等价。但是，对于 > 2 个参数，行为是不同的：如果传递更多参数，它会确保成对不等式。（也就是说，它们必须彼此不同。）它在很多问题中都派上用场。

向 = 传递 > 2 个参数也是可能的，它确保所有参数都相等。但是请注意，当您有 > 2 个参数时，取反的相等和不同会变得不同：例如，2 2 3 并不完全相等，但它们也不等于 distinct。我希望这能说明问题。

关于Overflow/Underflow检查的说明

Patrick 提出了溢出检查和机器整数使用的问题，他认为人们应该担心这些情况是正确的。我认为 Nikita 已经通过确保明确的界限来处理这里的特定用例。但是，一个人不能太小心！出于这些目的，z3 实际上内置了溢出检查原语。有关详细信息，请参阅 Nikolaj 的这篇精彩论文：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf

z3 提供的原语是：

bvsmul_noovfl: 有符号乘法无溢出
bvsmul_noudfl: 有符号乘法无下溢
bvumul_noovfl: 无符号乘法无溢出

但请参阅有关可用于检测其他操作溢出的逻辑公式的论文。（以上三种比较复杂，所以支持比较原始，其他情况用户可以直接检查）

证明溢出检查表达式是正确的

Prove overflow checking expression is right

smt

z3

关于 distinct 的注释

关于Overflow/Underflow检查的说明