「抽象解释与形式化验证」

// 一个随机测试很难发现的越界
int lookup(const int *table, int n, int idx) {
    if (idx < 0 || idx >= n) return -1;
    return table[idx];        // 若 n 为负数，两个条件同时为假
}

# 一个具体的小格：三值抽象 {负, 零, 正, 未知}
# 偏序：负 ⊑ 未知，零 ⊑ 未知，正 ⊑ 未知
JOIN = {
    ("neg", "neg"): "neg",  ("neg", "zero"): "top",
    ("neg", "pos"): "top",  ("zero", "zero"): "zero",
    ("zero", "pos"): "top", ("pos", "pos"): "pos",
}

def join(a, b):
    """控制流汇合：任一为 top 则结果 top"""
    if a == "top" or b == "top":
        return "top"
    return JOIN[(a, b)]

def transfer_sign(op, a, b):
    """抽象语义：在符号域上计算 x op y 的结果符号"""
    if a == "top" or b == "top":
        return "top"
    if op == "add":
        if a == "pos" and b == "pos": return "pos"
        if a == "neg" and b == "neg": return "neg"
        if a == "zero": return b
        return "top"
    if op == "mul":
        if a == "zero" or b == "zero": return "zero"
        return "pos" if a == b else "neg"
    return "top"

def solve_fixpoint(nodes, entry, succs, transfer, join, init_bottom):
    """Kildall 风格的工作表算法：迭代到所有节点状态稳定"""
    state = {n: init_bottom() for n in nodes}   # 初始全为 bottom
    state[entry] = transfer(entry, None)        # 入口状态
    worklist = list(nodes)
    while worklist:
        n = worklist.pop()
        in_state = init_bottom()
        for p in preds(n, succs):               # 汇合所有前驱
            in_state = join(in_state, state[p])
        out_state = transfer(n, in_state)
        if out_state != state[n]:               # 状态上升，需重新传播
            state[n] = out_state
            worklist.extend(succs[n])
    return state

// 不同抽象域能推出什么
void f(int x, int y) {
    if (x >= 0 && x <= 10 && y >= 0 && y <= 10) {
        int d = x - y;         // 区间域：d 在 [-10,10]，八边形域更紧
        if (x + y == 20) {
            // 多面体域能推出 x == 10 且 y == 10
            // 区间域只知道 x+y 在 [0,20]，无法利用等式约束
        }
    }
}

class Interval:
    def __init__(self, lo, hi):
        assert lo <= hi
        self.lo, self.hi = lo, hi

    def __add__(self, o):
        return Interval(self.lo + o.lo, self.hi + o.hi)

    def __mul__(self, o):
        cands = [self.lo * o.lo, self.lo * o.hi,   # 乘法取四端点极值
                 self.hi * o.lo, self.hi * o.hi]
        return Interval(min(cands), max(cands))

    def join(self, o):
        return Interval(min(self.lo, o.lo), max(self.hi, o.hi))
# 区间算术的精度损失：x - x 不一定是 [0,0]
x = Interval(0, 10)
print(x + Interval(1, 2))    # [1, 12]
print(x - x)                 # [-10, 10]  <- 丢失了相关性，实际恒为 0

void h(int n, int m) {
    if (n >= 0 && m >= 0 && n + m <= 100) {
        int a[100];
        a[n] = 1;      // 需要 n <= 100，区间域给出 n 在 [0,100]，勉强够用
        a[n + m] = 2;  // 需要 n+m <= 100，区间域给出 [0,200]，无法证明
    }
}

# 用多面体域描述程序状态（概念示意，实际用 PPL 或 Apron 库）
# 状态： x >= 0, y >= 0, x + y <= 100
# 细化： if (x + y == 50) -> 加等式约束；if (x > y) -> 加 x - y >= 1
# join 两条路径： A(0<=x<=10, y==0) 与 B(0<=x<=10, y==x)
#   join 后是两者的凸包：0 <= x <= 10, 0 <= y <= x

# 用 Frama-C 的 Eva 插件做抽象解释分析
frama-c -eva -eva-precision 5 -eva-domains octagon,equality array_bounds.c
# 输出形如：
#   [eva] test.c:12: assertion 'i < 100' got status valid
#   [eva] test.c:15: accessing 'a[i]' with i in [0, 99]  <- 证明安全

def widen(a, b):
    """加宽算子：b 是本轮迭代结果，a 是上一轮
    上界增长则跳到 +inf，下界减小则跳到 -inf"""
    lo = float("-inf") if b.lo < a.lo else a.lo
    hi = float("inf") if b.hi > a.hi else a.hi
    return Interval(lo, hi)

def narrow(a, b):
    """收窄算子：不动点之后用更精确的 b 收缩 a，仍保持健全"""
    lo = b.lo if b.lo > a.lo else a.lo
    hi = b.hi if b.hi < a.hi else a.hi
    return Interval(lo, hi)

# 迭代过程（n 已知为 [0, 100]）：i = [0,0] -> [0,1]
#   上界增长 -> 加宽到 [0, +inf) -> 与 n 的上界取交 -> [0, 100]，收敛
# 收窄：用循环体语义重新计算 -> [0, 99]（因为 i < n 且 n <= 100）

// 断言注入：把分析器的猜测变成用户的承诺
void process(int *buf, int len) {
    __ESBMC_assume(len > 0 && len <= 4096);   // 告诉分析器
    __ESBMC_assert(buf != NULL, "buffer must be valid");
    for (int i = 0; i < len; i++) buf[i] = 0; // 有了假设，越界可证安全
}

# 符号执行的简化骨架
from z3 import BitVec, Solver, sat, Not

def sym_exec(branches, target_line):
    """沿路径累积约束，求解出触发目标的具体输入"""
    x = BitVec("x", 32)
    pc, results = [], []                 # pc 为路径条件
    for stmt in branches:
        s = Solver(); s.add(pc); s.add(stmt.cond)
        if s.check() == sat:
            if stmt.line == target_line:
                results.append(s.model())    # 找到触发输入
            pc = pc + [stmt.cond]            # 真分支可行，继续
        else:
            s2 = Solver(); s2.add(pc); s2.add(Not(stmt.cond))
            if s2.check() != sat: break      # 两条分支都不可行
            pc = pc + [Not(stmt.cond)]       # 只能走假分支
    return results

# CBMC：有界模型检验的典型工具
cbmc --unwind 10 --bounds-check --pointer-check target.c
# 输出形如：
#   [main.assertion.1] line 12 assertion i < 100: SUCCESS
#   [main.pointer_dereference.3] line 15: SUCCESS
#   VERIFICATION SUCCESSFUL

# 用 Z3 求解数组越界的反例
from z3 import Int, Solver, sat
idx, n = Int("idx"), Int("n")
s = Solver()
s.add(n > 0, n < 100, idx >= 0, idx < n)   # 循环不变式
s.add(idx >= 100)                          # 断言越界成立的条件
print(s.check())                           # unsat -> 越界不可能发生

// ACSL 规格（Frama-C 使用的契约语言）
/*@ requires n >= 0 && \valid(a + (0 .. n-1));
    ensures \result == \sum(a, n);
    assigns \nothing;
*/
int sum(const int *a, int n) {
    int s = 0;
    /*@ loop invariant 0 <= i <= n && s == \sum(a, i);
        loop variant n - i;
    */
    for (int i = 0; i < n; i++) s += a[i];
    return s;
}

# 用 Frama-C 的 WP 插件做演绎验证
frama-c -wp -wp-rte -wp-prover alt-ergo,z3 sum.c
# 输出：每个 goal 的证明状态（Valid / Unknown / Timeout）
infer -- clang -c target.c      # Infer 自动推断，无需写规格

// 别名带来的精度崩塌
void copy(int *dst, const int *src, int n) {
    for (int i = 0; i < n; i++) dst[i] = src[i];
    // 若 dst 与 src 可能重叠，分析器必须考虑所有别名组合
}
void copy_fast(int *restrict dst, const int *restrict src, int n) {
    for (int i = 0; i < n; i++) dst[i] = src[i];
    // 加上 restrict 限定后，分析精度立刻提升
}