处理 SMT-LIB/Z3 中的溢出

Question

我正在尝试使用 SMT a + b - c - d 对以下表达式进行建模，所有常量 a,b,c,d 都是相同大小的 bitvecs，具有以下断言 a + b >= c + d 的约束。我想以不会发生上溢/下溢的方式对其进行建模。

这是我迄今为止尝试过的：

(declare-const a (_ BitVec 4))
(declare-const b (_ BitVec 4))
(declare-const c (_ BitVec 4))
(declare-const d (_ BitVec 4))

(assert (bvuge (bvadd a b) (bvadd c d)))

; this is an inaccurate, only checks the last operation for underflow
; (a+b-c-d) >= d
; (assert (bvuge (bvsub (bvsub (bvadd a b) c) d) d))
;
; this should model that either both sides overflow, neither,
; or only the expression to the left of the inequality
; (
;     (a + b <= a and c + d <= c and a + b >= c + d) or
;     (a + b >= a and c + d <= c) or
;     (a + b >= a and c + d >= c and a + b >= c + d)
; )
;(assert (or
;        (and (bvule (bvadd a b) a)
;             (bvule (bvadd c d) c)
;             (bvuge (bvadd a b) (bvadd c d)))
;        (and (bvuge (bvadd a b) a)
;             (bvule (bvadd c d) c))
;        (and (bvuge (bvadd a b) a)
;             (bvuge (bvadd c d) c)
;             (bvuge (bvadd a b) (bvadd c d)))))

(assert (bvuge (bvsub (bvsub (bvadd a b) c) d) #x0))

(check-sat)
(get-model)

但我不确定约束是否足够。

Answer 1

更好的策略是“扩展”到更大的位向量，并检查结果是否符合您想要的位向量大小。请注意，对位向量进行正确的下溢/上溢检查可能会非常棘手，尤其是在存在乘法的情况下。

幸运的是，有一篇出色的论文描述了如何正确执行此操作：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf

（这篇论文有一些小问题：这里和那里有一些拼写错误，有符号乘法上溢/下溢公式已经过时。但这是一个很好的开始资源！）

此外，Z3 还提供了开箱即用的检查器谓词，用于乘法欠/溢出。

阅读完论文后，如果您仍有问题，请随时就其内容提出更多问题！