Bit Vectors (1)

位向量(Bit Vectors)

1 位向量演算

计算机系统的设计是很容易出错的, 因此, 亟需验证此类系统的判定程序. 一个计算机系统通过位向量(bit vectors)来对信息进行编码, 比如说, 数字.

位向量演算的文法: \[ \begin{aligned} formula&:formula\land formula\ |\ \neg formula\ |\ (formula)\ |\ atom\\ atom&:term\ rel\ term\ |\ Boolean-Identifier\ |\ term[constant]\\ rel&:<\ |\ =\\ term&:term\ op\ term\ |\ identifier\ |\ ~term\ |\ constant\ |\ \\ &\ atom?term:term\ |\ term[constant:constant]\ |\ ext(term)\\ op&:+\ |\ -\ |\ \cdot\ |\ /\ |\ <<\ |\ >>\ |\ \&\ |\ |\ |\ \oplus\ |\ \circ \end{aligned} \]

通常来说, 其他运算符比如 \(\vee, \ne, \ge\) 可以通过文法中的布尔运算符组合得到. 其中一元运算符"~"表示按位取反(bitwise negation). ext函数代表符号扩展或者零扩展. 二元运算符"\(\circ\)"表示位向量的串联.

为什么要使用位向量演算?

首先考虑如下公式: \[ (x-y\gt 0)\Longleftrightarrow (x>y). \] 如果 \(x,y\) 是有限宽度的位向量, 该等价形式就不再成立了, 因为该减法操作可能存在溢出问题. 例如如下的的 C 程序片段:

unsigned char number = 200;
number = number + 100;
printf("Sum: %d\n", number);

上述结果输出的是 44, 因为是运算是无符号的字符类型, 所以: \[ \begin{aligned} 11001000=200\\ +01100100=100\\ \hline =00101100=44 \end{aligned} \] 在计算机中用 8 位二进制表示一个数的时候, 200 被存储为 11001000. 当执行加 100 的操作时, 会造成溢出, 因为第九位被舍去了.

因此, 运算符, 比如"+", 的含义是通过模运算定义的. 但是, 关于位向量的推理问题超出了溢出和模运算的范围. 出于效率原因, 程序员使用位级运算符(bit-level operators)将尽可能多的信息编码为可用的位数.

比如说, 命题 SAT 求解器的实现. 命题 SAT 求解器在 CNF 范式上的操作要存储大量的文字. 我们假定已经对出现在公式中的文字进行了标号, \(x_1, x_2,...\).

针对 CNF 的 DIMACS 标准用符号数对文字进行编码, 例如, 文字 \(\neg x_3\) 表示为 \(-3\). 治所用采用这种方式, 是因为避免了额外用一位来存储位向量的符号位. 从另一个方面说, 这种方法减少了变量数量可能增长至 \(2^{31}-1\) 这种情况, 而且对于实际应用还是能够满足的.

为了能够提取出变量的下标, 我们要对位向量的符号正负进行分析, 如下程序:

unsigned variable_index(int literal){
    if(literal < 0){
        return -literal;
    }else{
        return literal;
    }
}

由于很难为现代处理器的分支预测机制进行预测, 因此在上述程序中实现 \(if\) 语句所需的分支会减慢程序的执行速度. 因此, 大多数 SAT 求解器使用不同的编码形式: 位向量的最低有效位用于编码文字的符号, 其余位则用于编码变量. 然后可以通过位向量右移操作来提取变量的索引:

unsigned variable_index(unsigned literal){
    return literal >> 1;
}

类似地, 符号位可以通过按位与操作取得:

bool literal_sign(unsigned literal){
    return literal & 1;
}

上述的右移和按位与操作, 在大多数微处理器中都有实现, 而且执行效率较高. 这些位操作也高频地出现在硬件设计中. 对这些设计和构造进行推理证明需要用到位向量演算.

1.1 表示方法

我们使用 Church 的 \(\lambda\mbox{-}\rm notation\) 来定义向量. 一个有 \(l\) 个比特位的位向量用 lambda 表达式描述: \[ \lambda.i\in\{0,...,l-1\}.f(i), \] 其中 \(f(i)\) 是表示第 \(i\) 个比特的值的函数.

用一个例子说明 \(\lambda\mbox{-}\rm operator\) 是如何表示一个位向量的.

考虑如下表达式:

• \[ \lambda.i\in\{0,...,l-1\}.0 \]

  表示 \(l\) 长度的 0 向量.

• 一个 \(\lambda\) 表达式可以用另外一种方式来定义一个不具名的函数. 我们可以定义一个函数\(z\) \[ z(i)\doteq 0, \] 对于函数\(z\)也可以简单地写成 \(\lambda.i\in\{0,...,l-1\}.0\).

• 表达式 \[ \lambda i\in\{0,...,7\}. \begin{equation} \left\{\begin{array}{lr} 0:i\ \rm is\ even\\ 1:\rm otherwise \end{array} \right. \end{equation} \] 表示位向量是 10101010.

• 表达式 \[ \lambda i\in\{0,...,l-1\}.\neg x_i \] 表示对向量\(x\)进行按位取反操作.

1.2 语义

首先给出位向量的定义. 一个位向量 \(b\) 是一个给定长度 \(l\) 或者维度的比特向量: \[ b:\{0,...,l-1\}\longrightarrow\{0,1\}. \] 用 \(bvec_l\) 来表示长度为 \(l\) 的所有 \(2^l\) 个位向量的集合. 位向量 \(b\) 的第 \(i\) 个比特记为 \(b_i\).

一个位向量公式的含义依赖于位向量变量的宽度.即使不使用演算也是如此, 比如说, \[ x\neq y\land x\neq z\land y\neq z \] 对于其中三个如果只有一个比特的位向量来说是不可满足的, 但是对于位数更多的是可满足的.

有时可以用位向量对正数进行编码(无符号位向量), 也可以同时对正数和复数进行编码(有符号位向量). 因此, 每一种表达式都有与之对应的类型(type). 位向量的类型表述是

1. 表达式的宽度(以比特为单位),
2. 无论是否有符号.

我们将表示方式限制为具有固定长度的位向量, 因为一旦允许任意宽度的位向量, 位向量演算就无法判定. 宽度在实践中出现的大多数问题中都是已知的.

按位运算符

或运算符 "|". \(|_{[l]}: (bvec_l \times bvec_l)\longrightarrow bvec_l\).

使用 \(\lambda\) 表示符, 按位或操作可以表示为: \[ a\ |\ b \doteq \lambda i.(a_i \lor b_i). \] 其他的按位运算符的定义方式也是类似的.

算术运算符

具有算术运算符的位向量公式的含义取决于对其包含的位向量的解释. 有许多使用位向量对数字进行编码的方法. 最常用的整数编码是无符号整数的二进制编码(binary encoding)和带符号整数的二进制补码(two's complement).

二进制编码(binary encoding). 令 \(x\) 代表一个自然数, \(b\) 是属于 \(bvec_l\) 的一个位向量. 我们称 \(b\) 为 \(x\) 二进制编码, 当且仅当 \[ x = \langle b\rangle_U, \] 其中的 \(\langle b \rangle_U\) 有如下定义: \[ \langle \cdot \rangle_U: bvec_l \longrightarrow \{0,...,2^l-1\},\\ \langle b\rangle_U \doteq \Sigma_{i=0}^{l-1}b_i\cdot 2^i. \] \(b_0\) 称为最低有效位, \(b_{l-1}\) 称为最高有效位.

二进制编码只能用来表示非负整数. 同样地, 一种编码复数的方式是使用其中一个比特位作为符号位. 使用符号位的一种简单方法是在设置了指定位(例如最高有效位)的情况下简单地对数字进行取反. 比如说, 1001 会被解释成 \(-1\) 而不是 1. 这种编码方式很少应用于实践中. 大多数微处理器架构大多采用二进制补码进行编码.

二进制补码(two's complement). 令 \(x\) 代表一个自然数, \(b\) 是属于 \(bvec_l\) 的一个位向量. 我们称 \(b\) 为 \(x\) 的二进制补码, 当且仅当 \[ x=\langle b \rangle_S, \] 其中 \(\langle b \rangle\) 定义为: \[ \langle \cdot \rangle_S: bvec_l \longrightarrow \{-2^{l-1},...,2^{l-1}-1\},\\ \langle b\rangle_S := -2^{l-1}\cdot b_{l-1}+ \Sigma_{i=0}^{l-2}b_i\cdot 2^i. \] 下标为 \(l-1\) 的比特为位向量 \(b\) 的符号位.

比如说, 一些二进制整型和其对应的二进制补码编码 \[ \begin{aligned} &\langle 11001000\rangle_U = 20,\\ &\langle 11001000\rangle_U=-128+64+8=-56,\\ &\langle 01100100\rangle_S=100. \end{aligned} \] 如最开始的示例所描述的那样, 位向量的算术运算具有环绕效果: 如果表示结果所需的位数超过了可用位数, 则结果的其他比特位将被丢弃, 即结果被截断. 这对应于以 \(2^l\) 为底的取模运算. 写成 \(x=y\ mod\ b\) 代表 \(x\) 与 \(y\) 模 \(b\) 是相等的. 模运算的使用允许可以对所有的算数运算符进行直接定义:

• 加法和减法: \[ \begin{aligned} a_{[l]} +_U b_{[l]} = c_{[l]} &\Longleftrightarrow \langle a\rangle_U + \langle b\rangle_U = \langle c\rangle_U\ \rm mod\ 2^l,\\ a_{[l]} -_U b_{[l]} = c_{[l]} &\Longleftrightarrow \langle a\rangle_U - \langle b\rangle_U = \langle c\rangle_U\ \rm mod\ 2^l,\\ a_{[l]} +_S b_{[l]} = c_{[l]} &\Longleftrightarrow \langle a\rangle_S + \langle b\rangle_S = \langle c\rangle_S\ \rm mod\ 2^l,\\ a_{[l]} -_S b_{[l]} = c_{[l]} &\Longleftrightarrow \langle a\rangle_S - \langle b\rangle_S = \langle c\rangle_S\ \rm mod\ 2^l. \end{aligned} \]

• 取反(unary minus): \[ -a_{[l]}=b_{[l]}\Longleftrightarrow -\langle a\rangle_S = \langle b\rangle_S\ \rm mod\ 2^l. \]

• 关系运算符(relational operators): \[ \begin{aligned} a_{[l]U}\lt b_{[l]U} &\Longleftrightarrow \langle a\rangle_U \lt \langle b\rangle_U,\\ a_{[l]S}\lt b_{[l]S} &\Longleftrightarrow \langle a\rangle_S \lt \langle b\rangle_S,\\ a_{[l]U}\lt b_{[l]S} &\Longleftrightarrow \langle a\rangle_U \lt \langle b\rangle_S,\\ a_{[l]S}\lt b_{[l]U} &\Longleftrightarrow \langle a\rangle_S \lt \langle b\rangle_U. \end{aligned} \]

• 乘法与除法: \[ \begin{aligned} a_{[l]}\cdot_U b_{[l]}=c_{[l]} &\Longleftrightarrow \langle a\rangle_U\cdot \langle b\rangle_U = \langle c\rangle_U\ \rm mod\ 2^l,\\ a_{[l]}/_U b_{[l]}=c_{[l]} &\Longleftrightarrow \langle a\rangle_U/ \langle b\rangle_U = \langle c\rangle_U\ \rm mod\ 2^l,\\ a_{[l]}\cdot_S b_{[l]}=c_{[l]} &\Longleftrightarrow \langle a\rangle_U\cdot \langle b\rangle_S = \langle c\rangle_S\ \rm mod\ 2^l,\\ a_{[l]}/_S b_{[l]}=c_{[l]} &\Longleftrightarrow \langle a\rangle_U/ \langle b\rangle_S = \langle c\rangle_S\ \rm mod\ 2^l. \end{aligned} \] 乘法的语义无论参数是无符号数还是二进制补码形式都不受影响, 因此下标 \(U/S\) 可以省略. 但是除法不行.

• 扩展运算符(extension operator): 将原有的无符号位向量扩展为具有更多比特的无符号位向量称为零扩展(zero extension), 对于有符号的位向量来说是符号扩展(sign extension). 令 \(l\le m\). 以下的扩展形式对值无影响: \[ \begin{aligned} ext_{[m]U}(a_{[l]}) = b_{[m]U} &\Longleftrightarrow \langle a\rangle_U = \langle b\rangle_U,\\ ext_{[m]S}(a_{[l]}) = b_{[m]S} &\Longleftrightarrow \langle a\rangle_S = \langle b\rangle_S. \end{aligned} \]

• 移位(shifting): 左移位运算符"<<"取两个操作数, 并将第一个操作数向左移动第二个操作数相对应的位数. 左侧操作数的宽度称为移位宽度(width of the shift), 右侧操作数的宽度是移位距离的宽度(width of the shift distance), 向量从右边开始用进行零填充: \[ a_{[l]} << b_U = \lambda i\in\{0,...,l-1\}. \begin{equation} \left\{\begin{array}{lr} a_{i-\langle b\rangle_U}:i \ge \langle b\rangle_U\\ 0:\rm otherwise. \end{array} \right. \end{equation} \] 右移运算符的含义取决于第一个操作数的编码方式: 如果使用的是二进制编码(也就是针对无符号位向量的编码), 那就从左端开始填充0. 这称为逻辑右移(logical right shift): \[ a_{[l]U} >> b_U = \lambda i\in\{0,...,l-1\}. \begin{equation} \left\{\begin{array}{lr} a_{i+\langle b\rangle_U}:i \lt l - \langle b\rangle_U\\ 0:\rm otherwise. \end{array} \right. \end{equation} \] 如果第一个操作数采用的是二进制补码进行编码(也就是针对有符号位向量的编码), 那么\(a\) 的符号位就要被复制. 这称为算术右移(arithmetic right shift): \[ a_{[l]S} >> b_U = \lambda i\in\{0,...,l-1\}. \begin{equation} \left\{\begin{array}{lr} a_{i+\langle b\rangle_U}:i \lt l - \langle b\rangle_U\\ a_{l-1}:\rm otherwise. \end{array} \right. \end{equation} \]

2 用Flattening判定位向量的演算

最常用的针对位向量演算的判定程序称为 flattening. 如图所示的算法实现了这一技术. 给定一个位向量演算公式 \(\varphi\), 该算法计算出一个等价的命题公式 \(\mathcal{B}\), 并将命题公式传给一个SAT求解器. \[ \begin{aligned} &\mathbf{Algorithm\ 1.}\ \rm{BV\mbox{-}FLATTENING}\\ &\mathbf{Input:}\ \rm{A\ formula}\ \varphi\ {\rm in\ bit\mbox{-}vector\ arithmetic}\\ &\mathbf{Output:}\ \rm{An\ equisatisfiable\ Boolean\ formula\ } \mathcal{B}\\ &\\ &1.\hspace{2mm}\mathbf{function\ } {\rm BV\mbox{-}FLATTENING}\\ &2.\hspace{10mm}\mathcal{B}:=e(\varphi);\hspace{50mm}\triangleright\ {\rm the\ propositional\ skeleton\ of\ }\varphi\\ &3.\hspace{10mm} \mathbf{for\ } {\rm each}\ t_{[l]} \in T(\varphi)\ \mathbf{do}\\ &4.\hspace{18mm} \mathbf{for\ } {\rm each}\ i\in \{0,...,l-1\}\ \mathbf{do}\\ &5.\hspace{40mm} {\rm set}\ e(t)_i\ {\rm to\ a\ new\ Boolean\ variable};\\ &6.\hspace{10mm} \mathbf{for\ } {\rm each\ } a\in At(\varphi)\ \mathbf{do}\\ &7.\hspace{18mm} \mathcal{B}:=\mathcal{B}\wedge\ {\rm BV\mbox{-}CONSTRAINT}(e,a);\\ &8.\hspace{10mm} \mathbf{for\ } {\rm each\ } t_{[l]}\in T(\varphi)\ \mathbf{do}\\ &9.\hspace{18mm} \mathcal{B}:=\mathcal{B}\wedge\ {\rm BV\mbox{-}CONSTRAINT}(e,t);\\ &10.\hspace{8mm} \mathbf{return\ } \mathcal{B}; \end{aligned} \] 令 \(At(\varphi)\) 表示原公式 \(\varphi\) 中原子的集合. 第一步, 算法将 \(\varphi\) 中的原子用新的布尔变量进行替换. 用 \(e(a)\) 来表示替换之后的原子 \(a\), 并且 \(a\in At(\varphi)\), 这个过程称为 \(a\) 的命题编码器(propositional encoder). 所有的原子被布尔变量替换之后形成的公式记为 \(e(\varphi)\), 称之为公式 \(\varphi\) 的命题骨架(propositional skeleton). 命题骨架是初始赋值给 \(\mathcal{B}\) 的表达式. 令 \(T(\varphi)\) 代表原公式 \(\varphi\) 中项(terms)的集合. 算法对 \(T(\varphi)\) 中的每一个位向量的项都赋一个新的布尔变量的向量. 用 \(e(t)\) 表示对于给定 \(t\) 的变量向量, \(t \in T(\varphi)\), 用 \(e(t)_i\) 表示 \(t\) 中索引为 \(i\) 的 变量. \(e(t)\) 的宽度与项 \(t\) 的宽度一致. 然后, 该算法在公式 \(\varphi\) 上做迭代, 并计算相应的约束. 约束由函数 BV-CONSTRAINT 返回, 并添加到公式 \(\mathcal{B}\) 中.

特定原子 \(a\) 或项 \(t\) 所需的约束分别取决于原子或项. 如果是位向量或布尔变量, 则不需要约束, 并且 BV-CONSTRAINT 返回真. 如果 \(t\) 是一个位向量约束 \(C_{[l]}\), 那么会生成以下约束: \[ \bigwedge_{i=1}^{l-1}(C_i \Longleftrightarrow e(t)_i). \] 否则, 项 \(t\) 必须包含一个位向量运算符. 所需的约束依赖于这个运算符. 按位运算符的约束很简单. 比如说, 考虑按位或, 令 \(t = a|_{[l]}b\). 函数 BV-CONSTRAINT 返回的约束为 \[ \bigwedge_{i=0}^{l-1}((a_i\lor b_i)\Longleftrightarrow e(t)_i). \] 其他的按位运算符对应的约束与上述的形式一致.

上述算法其实就是对一个位向量演算公式进行布尔变量变量编码和添加相应的布尔约束条件, 进而传给SAT求解器, 并对公式进行可满足性的判定.