有没有办法在使用数组定义变量时指定变量的域？

Question

我的程序从一个 smt2 文件中读取约束，所有的变量都定义为一个数组。例如

(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun y () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (bvslt  (concat  (select  x (_ bv3 32) ) (concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) ) (select  x (_ bv0 32) ) ) ) ) (concat  (select  y (_ bv3 32) ) (concat  (select  y (_ bv2 32) ) (concat  (select  y (_ bv1 32) ) (select  y (_ bv0 32) ) ) ) ) ) )
(check-sat)
(exit)

省略了其他一些约束。有时求解器会给出 x 的值：

(store (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #xfe)
                     #x00000002
                     #x00)
              #x00000001
              #xff)
       #x00000003
       #x80)

根据定义，数组的每个元素都是一个十六进制值，所以值应该是0x8000fffe。此值超出 C++ 中整数的上限。当我将它转换回 int 时，它是一个负值。所以我猜Z3将数组定义的所有变量都视为无符号整数。 例如，如果约束是 x > y，求解器可能会给出 x = 0x8000ffe 和 y = 0x00000001。这些值满足无符号比较的约束，但是在进行有符号比较时，x为负，y为正，因此是错误的。我想知道是否有办法告诉求解器在将数字定义为数组时对它们进行签名？

已于 2019 年 9 月 14 日 22:26:43 添加 我有两个 smt2 文件，一个是

(set-logic QF_AUFBV )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun y () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (bvslt  (concat  (select  x (_ bv3 32) ) (concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) ) (select  x (_ bv0 32) ) ) ) ) (concat  (select  y (_ bv3 32) ) (concat  (select  y (_ bv2 32) ) (concat  (select  y (_ bv1 32) ) (select  y (_ bv0 32) ) ) ) ) ) )
(check-sat)
(exit)

约束就是 x

(set-logic QF_AUFBV )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun y () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (let ( (?B1 (concat  (select  y (_ bv3 32) ) (concat  (select  y (_ bv2 32) ) (concat  (select  y (_ bv1 32) ) (select  y (_ bv0 32) ) ) ) ) ) (?B2 (concat  (select  x (_ bv3 32) ) (concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) ) (select  x (_ bv0 32) ) ) ) ) ) ) (let ( (?B3 (bvsub  ?B1 ?B2 ) ) ) (and  (and  (and  (and  (and  (=  false (=  (_ bv0 32) ?B2 ) ) (=  false (=  (_ bv0 32) ?B1 ) ) ) (=  false (bvslt  ?B1 ?B2 ) ) ) (=  false (=  (_ bv0 32) ?B3 ) ) ) (=  false (bvslt  ?B3 ?B2 ) ) ) (=  (_ bv0 32) (bvsub  ?B3 ?B2 ) ) ) ) ) )
(check-sat)
(exit)

这是

 [(! (0 == x)), 
   (! (0 == y)), 
   (! ( y < x)),
   (! (0 ==( y - x))), 
   (! (( y - x) < x)), 
   (0 ==(( y - x) - x)) ]

这些smt2文件是Klee生成的。求解器给出

x = (store (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #xfe)
                     #x00000002
                     #x00)
              #x00000001
              #xff)
       #x00000003
       #x80)
y = before minimize: (store (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #xfc)
                     #x00000002
                     #x01)
              #x00000001
              #xff)
       #x00000003
       #x00)

所以 x=0x8000fffe，y=0x0001fffc。转换为十进制，我们有 x=2147549180，y=131068。所以 y-x-x 是-4294967296，而不是十进制的 0。求解器认为它是满意的，因为 4294967296 是

1 00000000 00000000 00000000 00000000

二进制，其中“1”是第 33 位，将被删除。所以 -4294967296 在内存中被认为是 0x00。这就是我问这个问题的原因。 X 和 y 应该是整数，所以 0x8000fffe 是 -0x0000fffe，也就是 -65534。 y 是 131068。y-x-x 显然不是 0。所以就整数而言，这些值不满足约束。表达式 y - x - x 似乎是在无符号规则中计算的。

Answer 1

位向量没有符号

SMTLib 中没有带符号或无符号位向量的概念。位向量只是一个位序列，没有附加任何关于如何将其视为数字的语义。

然而，区分符号性的是操作。这就是为什么你有bvslt 和bvult；例如，用于有符号和无符号小于比较。您可能想在这里阅读逻辑描述：http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

长话短说，求解器告诉您的只是结果包含这些位；您如何将其解释为无符号字或有符号 2 的补码完全取决于您。请注意，这与硬件中机器算术的完成方式完美匹配，您只需拥有包含位序列的寄存器。它是根据他们可能选择的任何约定来处理值的说明。

我希望这很清楚；随时询问具体案例；发布完整的程序也总是有帮助的，只要它们从细节中抽象出来并描述您正在尝试做的事情。

另请参阅更详细的早期问题：How to model signed integer with BitVector?

避免上溢/下溢

您可以要求 z3 在位向量算术期间避免上溢/下溢。但是，这将需要为您要执行的每个操作添加额外的断言，因此它会变得相当混乱。 （另外，看起来你想使用 Klee；我不确定 Klee 是否允许你一开始就这样做。）本文详细解释了该技术：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf

您特别想通读第 5.1 节：作者描述了如何“注释”每个算术运算并断言它不会显式溢出。例如，如果你想确保加法不会溢出；您首先将您的位向量从 32 位零扩展为 33 位；做加法，并检查结果的 33 位是否为1。为避免溢出，您只需编写一个断言，说明该位不能为1。这是一个例子：

; Two 32-bit variables
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))

; Zero-Extend them to 33-bits
(define-fun x33 () (_ BitVec 33) (concat #b0 x))
(define-fun y33 () (_ BitVec 33) (concat #b0 y))

; Add them
(define-fun  extendedAdd () (_ BitVec 33) (bvadd x33 y33))

; Get the sign bit
(define-fun signBit () (_ BitVec 1) ((_ extract 32 32) extendedAdd))

; Assert that the addition won't overflow:
(assert (= signBit #b0))

; Regular addition result:
(define-fun addResult () (_ BitVec 32) ((_ extract 31 0) extendedAdd))

; Now you can use addResult as the result of x+y; and you'll
; be assured that this addition will never overflow

(check-sat)
(get-model)

您还必须在每个操作中检查下溢。进一步增加了复杂性。

如您所见，这可能会变得非常棘手，并且乘法规则实际上非常棘手。为了简化这个 z3 实际上提供了用于乘法溢出检查的内置原语，称为：

• bvsmul_noovfl: 仅当有符号乘法不溢出时才为真
• bvsmul_noudfl：只有当有符号乘法没有下溢时才为真
• bvumul_noovfl: 仅当无符号乘法不溢出时才为真

没有用于检查无符号乘法是否会下溢的谓词，因为这种情况不会发生。但重点仍然存在：您必须注释每个操作并明确断言相关条件。这最好在代码生成期间由更高级别的 API 完成，并且一些 z3 绑定确实支持此类操作。 （例如，请参阅http://hackage.haskell.org/package/sbv-8.4/docs/Data-SBV-Tools-Overflow.html 了解 SMT 求解器之上的 Haskell 层如何处理此问题。）如果您要大规模执行此操作，您可能希望构建一些自动生成的机制，就像手动执行一样极易出错。

或者你可以切换并使用Int 类型，它永远不会溢出！但是，当然，您不再对实际运行的程序进行建模，而是对实际整数值进行推理；根据您的问题领域，这可能是可以接受的。