README.md

示例:FixedStack —— CBMC 有界模型检验的真实闭环

对应 Rust 那边的 examples/rust-kani/,换成 C++ + CBMC,验证 ../../references/cpp-cbmc.md 里的结论和命令是否准确。

文件

• stack_buggy.cpp —— 有 bug 的版本
• stack_fixed.cpp —— 修复后的版本

代码(buggy)

template <typename T, int N>
class FixedStack {
    T data[N];
    int size = 0;
public:
    void push(T v) {
        data[size] = v;
        size++;
    }
    T pop() {
        size--;
        return data[size];
    }
    bool empty() const { return size == 0; }
};

int main() {
    FixedStack<int, 3> s;
    s.push(1);
    s.push(2);
    s.push(3);
    s.push(4);   // 容量只有 3,这里越界写入
    return 0;
}

push 从不检查 size 是否已经达到容量 N,第 4 次调用会写到 data[3],超出固定大小数组 data[3] 的合法范围(下标 0~2)。

第一步:CBMC 实测(有 bug 的版本)

cbmc stack_buggy.cpp

实测输出(节选):

[push.array_bounds.1] line 7 array.FixedStack<signed_int,3>::data dynamic object upper bound in this->data[(signed long int)this->size]: FAILURE

** 2 of 20 failed (2 iterations)
VERIFICATION FAILED

array_bounds 检查直接失败,精确定位到 push 函数里写数组的那一行。

第二步:修复

void push(T v) {
    if (size < N) {
        data[size] = v;
        size++;
    }
}

第三步:CBMC 确认修复(实测)

cbmc stack_fixed.cpp

实测输出:

** 0 of 20 failed (1 iterations)
VERIFICATION SUCCESSFUL

全部 20 项检查通过,包括数组越界、指针解引用、算术溢出等。因为这段代码(固定 4 次 push 调用、无循环)是直线执行,这里的 VERIFICATION SUCCESSFUL 是穷尽式的,不是抽样意义上的"大概率没问题"。

真实踩过的坑:CI 里旧版 CBMC 的假阳性

.github/workflows/verify.yml 最初写的是 sudo apt-get install -y cbmc,Ubuntu 22.04 的 apt 源装出来是 CBMC 5.12(远旧于本文档实测用的 6.10.0)。CI 实际跑出来是:

CBMC version 5.12 (cbmc-5.12) 64-bit x86_64 linux
...
Generated 0 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL

stack_buggy.cpp 明明有 bug,却报 VERIFICATION SUCCESSFUL——原因是 Generated 0 VCC(s):5.12 这个版本根本没能对带模板的 FixedStack<T, N> 生成任何验证条件,相当于什么都没检查,而不是真的证明通过。这正是 references/cpp-cbmc.md 里强调"看到 VERIFICATION SUCCESSFUL 先看 VCC 数量是不是 0"的来源。修复方式是把 CI 和文档都换成从 GitHub release 下载固定版本(6.10.0),不依赖 apt 装到的不确定版本。