在bitvector上模运算分析

摘要

你在 Java 或 C 中写 int x = 2147483647; x = x + 1; 时，结果会"溢出"变成负数。这是因为整数运算实际上是模 $ 2^{32} $ 的算术。大多数程序分析工具假设运算在有理数$ \mathbb{Q} $ 上进行（没有溢出），因此会漏掉或误判很多实际程序中才有的性质。
论文解决了：如何在模$2^{\omega}$算术下精确分析程序中的仿射关系？

这篇论文提出了一种在模$2^{\omega}$算术下既可靠又完备的程序分析方法——可靠意味着不会给出错误结论，完备意味着不会漏掉任何真实有效的仿射关系。这是之前基于$ \mathbb{Q} $或$ \mathbb{Z}_p $的方法做不到的。

在$\mathbb{Q}$上分析

$\mathbb{Q}$上的分析在数学上好处理，是一个域，线性代数简单，但是一旦程序运用了模运算的性质，他就会漏掉真实的不变式。

在$\mathbb{Z}_p$上分析

在$\mathbb{Z}_P$上分析，虽然已经涉及到模运算的性质，但是模$p$和模$2^w$有着完全不同的结构，会给出错误结论，因为模$2^w$的偶数不可逆，是零因子。

引言

过往的分析大多无法发现图 1 中 Java 程序终止时线性不变式 21·x − y = 1 成立。为什么？因为 Java 对整数类型执行模 m = 2ʷ 的算术运算（int 类型 w=32，long 类型 w=64）。21·x − y = 1 之所以有效，是因为 21 × 1,022,611,261 = 1 (mod 2³²)。

这是在$\mathbb{Q}$分析的缺陷，说明了基于有理数域对程序的分析是不完整的，而在$\mathbb{Z}_p$域进行分析的结果不但是不完整的，甚至可能是不可靠的。

幂的模环

对于环类$\mathbb{Z}_{2^\omega}$，可以将元素分为两类:($ m = 2^\omega $)
(1) 如果 a 是偶数，则 a 是零因子——存在 b ≠ 0 使得 a·b = 0 (mod m)。
(2) 如果 a 是奇数，则 a 可逆——存在 b 使得 a·b = 1 (mod m)。逆元可用牛顿法在 O(log w) 时间内计算。

这里的求解采用梯阵形式。

梯阵形式 (echelon form )：一组非零向量处于梯阵形式，当所有向量的首项指标(leading index)（第一个非零分量的位置）互不相同。梯阵形式中的集合最多有 N 个元素。梯阵集合的秩定义为所有向量首项的秩之和加上 (N−s)·w（s 是向量个数）。

将新向量加入梯阵形式的生成元集合的算法：
给定梯阵集合 G 和新向量 x（首项指标 i，首项 d·2ʳ）：
1. 如果 G 中没有向量的首项指标是 i → 直接加入
2. 如果 G 中有向量 y 首项指标也是 i（首项 d'·2ʳ'）：
  (a) 如果 r' ≤ r → 用 y 消去 x 的首项，继续处理
  (b) 如果 r' > r → 用 x 替换 y，然后消去 y 的首项
每一步都减小生成元集合的总秩，保证了终止。

算法

这个方法的算法主体如下:

1.把程序变成流图
2.将状态拓展成"扩展向量"
3.建立两个约束系统(S记录过程矩阵，R记录每个程序点的状态集)
4.抽象，将R状态记录为他自身的线性闭包(我们只需要永远成立的仿射关系，并不需要知道具体状态)
5.不动点迭代求解
6.从子模提取仿射关系，解得向量a组成不变关系

公式引入测试

行内公式：$ E = mc^2$

块级公式：363730\sum_{i=1}^n i^3 = \left( \frac{n(n+1)}{2} \right)^2363730