使用符号高和低的 Z3 BitVec 提取

Question

我一直在尝试使用 Z3 证明某些 SIMD 矢量化，但我运行遇到了一个问题，试图对有条件地绕位或通道移动的 SIMD 操作建模（例如英特尔 _mm_shuffle_epi8 例如）

当我尝试将符号 high 和 low 与似乎不受支持的 Extract 一起使用时出现问题：

assert a.sort() == BitVecSort(128)
assert b.sort() == BitVecSort(128)
Extract( Extract(i+3,i,b)*8+7, Extract(i+3,i,b)*8, a)

结果

z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.

问题似乎有两个方面：

Z3 似乎不支持符号大小的 BitVecs

>>> a = Int('a')
>>> b = BitVec('b', a)
ctypes.ArgumentError: argument 2: <class 'TypeError'>: wrong type

会很整洁，但可惜。因此，Extract 需要能够知道其 return 值的精确 BitVec 类型，并要求 high 和 low 都是具体的，尽管看起来唯一真正的要求应该是 simplify(high - low) 产生一个具体的值。

正确的做法是什么？

Answer 1

是的，high/low 需要保持不变，以便静态知道结果类型。您可以使用 shifts and/or 掩码来执行您想要的操作，但您需要确定输出的最大大小。

Answer 2

SMTLib 位向量逻辑仅为具体的位大小定义。这不仅仅是一个疏忽：它是逻辑的一个基本限制：没有决策程序可以决定可能涉及符号大小的位向量公式的正确性，因为位向量公式的真实性会根据大小而改变。经典的例子是：

x <= 7

如果 x 是大小 <= 3 的位向量，则以上为真，否则为真。如果这看起来做作，请考虑以下内容：

x*x <= x+x+x

同样，如果 x 是 2 位宽，这是正确的，但如果是 3 位宽，则不是。因此，SMTLib 要求所有位向量大小在规范时都是具体的。请注意，您可以编写适用于任意位大小的高级程序，但是一旦它们被渲染并发送到求解器，所有位向量大小都必须是已知的具体常量。

关于您关于 Extract 的问题。你是对的，严格来说，最终长度的具体性就足够了。但是 z3py 是 SMTLib 之上的一个薄层，它不做这样的简化。 "concreteness" 要求来自对相应 SMTLib 函数的类似限制：

All function symbols with declaration of the form

  ((_ extract i j) (_ BitVec m) (_ BitVec n))

where
- i, j, m, n are numerals
- m > i ≥ j ≥ 0,
- n = i - j + 1  "

参见此处：http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml 请注意，出于这个原因，甚至逻辑本身也被称为 "FixedSizeBitVectors"，而不仅仅是 "BitVectors"。

然而，提取固定大小的块并不难，只需右移 lo，然后 mask/extract 所需的位数：

 ((_ extract 7 0) (bvlshr x lo))

如果您的块大小不是恒定的，那么您将再次陷入符号位向量大小的世界，而 SMTLib 出于我上面提到的原因避免了这种情况。（这也是为什么 extract 将具体整数作为参数并用有趣的 SMTLib 符号编写以指示参数是具体值的原因。）

如果您确实必须使用 "symbolic" 字长，最好的办法是编写程序并分别证明每个 "symbolic" 感兴趣的字长，方法是确保字长在每个案例。（本质上是针对您感兴趣的所有尺寸的案例拆分。）

使用符号高和低的 Z3 BitVec 提取

Z3 BitVec extraction using symbolic high and low

python

z3

z3py