C*：开发与证明一体化

第一个 C* 程序

EN | 中文

本节中，我们会编写并验证第一个 C* 程序：求绝对值。这个例子虽然简单，却能说明：C 语义中的细微之处很容易导致代码出现未定义行为（UB）。确保代码没有未定义行为，是 C 程序验证的一个基本目标。后面的教程还会讨论如何确保内存安全和功能正确。本节最后，我们会下载并配置 C* 提供的证明标准库。它支持常见的规约与证明，后续示例也会用到这个库。

初始化 C* 项目

  1. 创建一个新文件夹：mkdir cstar_verification ; cd cstar_verificationmkdir cstar_verification ; cd cstar_verification。
  2. 初始化项目：cstarc initcstarc init。这一步会创建 cstar.tomlcstar.toml 与 compile_flags.txtcompile_flags.txt。
  3. 创建 .vscode/settings.json.vscode/settings.json 文件，内容如下：
{
  "clangd.path": "cst_clangd"
}
{
  "clangd.path": "cst_clangd"
}
  1. 在 VSCode 中打开项目。
  2. 使用快捷键 ctrl+shift+pctrl+shift+p（macOS 上为 shift+cmd+pshift+cmd+p）打开命令面板，输入并选择 CStar IDE: Start HOL Light ServerCStar IDE: Start HOL Light Server。
  1. HOL Light Server 面板显示以下内容时，就说明启动成功了：
...
[INFO] Use Ctrl-\ to quit the server!
[INFO] RPC server listening on 127.0.0.1:7000 ..
...
[INFO] Use Ctrl-\ to quit the server!
[INFO] RPC server listening on 127.0.0.1:7000 ..

编写求绝对值函数

在刚创建的 C* 项目中添加文件 abs.cabs.c，内容如下：

#cst_include "cstar.h"
int myabs(int x)
{
  int r;
  if (x >= 0) {
    r = x;
  } else {
    r = -x;
  }
  return r;
}
#cst_include "cstar.h"
int myabs(int x)
{
  int r;
  if (x >= 0) {
    r = x;
  } else {
    r = -x;
  }
  return r;
}

第一行的 #cst_include#cst_include 导入一个验证时（Verification Time）使用的头文件。其中定义的符号，比如定理证明中用到的证明函数，只能用于程序验证，不能用于实现代码。 cstar.hcstar.h 是 C* 提供的核心头文件，主要提供与上述 HOL Light Server 交互的接口。我们暂时可以忽略这一行，等到需要编写证明代码时，再解释它的机制。现在只需记住：所有 C* 程序都需要以 #cst_include "cstar.h"#cst_include "cstar.h" 开头。

在 VSCode 中，右键单击代码的第 4 行，选择 Show Symbolic StateShow Symbolic State。这是 C* 提供的验证功能，用于显示该行对应的符号状态（稍后解释）。此时却会报错，VSCode 会在对应行上标出以下诊断信息：

error: function without a specification
  near: int myabs(int x) ▸{
  at .../cstar_verification/abs.c:3:5  in myabs
  fed to the engine:
      int myabs(int x) {
error: function without a specification
  near: int myabs(int x) ▸{
  at .../cstar_verification/abs.c:3:5  in myabs
  fed to the engine:
      int myabs(int x) {

这提示我们，验证程序前，需要先编写它的规约（Specification）。 C* 采用广泛使用的契约式规约，以函数为单位给出：

  • 前置条件（Pre-condition）：函数的输入需要满足的条件。
  • 后置条件（Post-condition）：函数的输出应该满足的条件。

在 C* 中，我们通过标注 [[cst::require(...)]][[cst::require(...)]] 以及 [[cst::ensure(...)]][[cst::ensure(...)]] 来编写函数契约：

#cst_include "cstar.h"
int myabs(int x)
  [[cst::require(`emp`)]]
  [[cst::ensure(`
      fact(
        (x >= 0i && __return == x) ||
        (x <  0i && __return == --x)
      )
  `)]]
{
  int r;
  if (x >= 0) {
    r = x;
  } else {
    r = -x;
  }
  return r;
}
#cst_include "cstar.h"
int myabs(int x)
  [[cst::require(`emp`)]]
  [[cst::ensure(`
      fact(
        (x >= 0i && __return == x) ||
        (x <  0i && __return == --x)
      )
  `)]]
{
  int r;
  if (x >= 0) {
    r = x;
  } else {
    r = -x;
  }
  return r;
}

在上面的代码中，逻辑表达式写在反引号 `...``...` 中。 C* 使用分离逻辑（Separation Logic）作为规约逻辑，稍后会详细介绍。在这个例子中：

  • empemp 可以先理解为真值，即没有对程序状态施加任何约束。

  • fact()fact() 表示对程序状态施加 表达的约束。 myabsmyabs 的后置条件用它表达以下约束：

    • 要么参数 xx 非负并且函数返回值等于 xx；
    • 要么参数 xx 为负数并且函数返回值等于 xx 的相反数。

现在，右键单击代码的第 11 行（函数入口的大括号处），再次选择 Show Symbolic StateShow Symbolic State。VSCode 右侧的符号状态面板会显示：

这也是一个分离逻辑表达式：data_at data_at 表示在地址 处存储了一个 类型的值 。分离逻辑刻画的是资源（Resource）：要描述程序操作的某块内存，就需要显式描述这块内存资源。上面的符号状态表示，变量 xx 的地址处存储着一个 intint 类型的值，等于 xx 在函数入口处的初值。

接下来，右键单击代码的第 12 行，再次选择 Show Symbolic StateShow Symbolic State，得到以下符号状态：

其中的 undef_data_atundef_data_at 谓词与 data_atdata_at 含义类似，区别在于前者不指定内存中存储的值。如果接下来立即使用 rr 的值，也会报错，因为 rr 尚未初始化。这个符号状态中还出现了逻辑连接词 ****，即分离逻辑中十分重要的分离合取（Separating Conjunction）连接词。逻辑表达式 ** ** 所描述的内存空间可以分成两个不相交的部分，分别满足 和 。所以，上述符号状态明确表示，变量 xx 和 rr 占据的内存空间互不相交。后面我们还会看到，分离逻辑的这一能力可以用来精确、简洁地刻画别名关系。

如果在函数返回后（第 18 行）查看符号状态，得到的是：

目前，C* 不返回函数出口处的符号状态。这在一定程度上符合直觉：函数返回后，它所拥有的内存空间（参数和局部变量）都已回收。

验证求绝对值函数

查看符号状态的过程已经包含了一些验证：没有编写函数规约、访问的内存资源未被描述，或使用了未初始化变量的值，都会报错。符号状态的推理能够继续推进，本身就已在一定程度上说明了内存安全性。不过，程序验证还需要考虑功能正确性。如果在函数出口的大括号处（第 19 行）查看符号状态，面板显示的就是验证条件（Verification Condition）：

如果所有验证条件都成立，就能保证函数没有未定义行为、满足内存安全性，而且功能符合函数契约的描述。上面的验证条件对应第 16 行的赋值语句 r = -x;r = -x;。它要求 |--|--（分离逻辑中的蕴含连接词）前的符号状态蕴含其后的符号状态。具体来说，它要求证明：如果 xx 在函数入口处为负，那么它的值就不等于 -2147483648-2147483648（逻辑表达式中的 ~~ 表示逻辑非）。这个条件显然不成立：整型变量完全可以取值 -2147483648-2147483648。为什么要验证这个条件呢？原因在于 C 语义中的一个细节：有符号整型运算溢出属于未定义行为，对 -2147483648-2147483648 取相反数就会出现这种情况。验证条件中 |--|-- 后的部分，正是为了确保取相反数时不触发未定义行为。

为了让求绝对值函数通过验证，我们可以加强函数的前置条件，约束函数输入：

int myabs(int x)
  [[cst::require(`fact(x > --2147483648i)`)]]
  ...
int myabs(int x)
  [[cst::require(`fact(x > --2147483648i)`)]]
  ...

也就是说，我们限制了输入范围，使其绝对值能够在整型范围内正确计算。修改后，再次在函数结束后的位置查看符号状态，面板会显示：

至此，第一个 C* 程序就编写并验证完成了！接下来看看，如果实现代码写错了，会出现什么样的验证条件。比如，把第 16 行的 r = -x;r = -x; 改为 r = x;r = x;，再次在函数末尾查看符号状态，得到以下验证条件：

如果 xx 在函数入口处的初值为负，规约要求返回 xx 的相反数，代码却返回了 xx。这样就得到一个无法证明的验证条件 x == -xx == -x。由此可见，程序验证可以在开发过程中发现逻辑错误，确保实现代码的行为符合规约。

C* 的证明标准库

在继续学习之前，先在项目中配置 C* 的证明标准库。

  1. 进入项目根目录（cstar_verificationcstar_verification），执行 git initgit init，初始化 git 版本控制。
  2. 执行 git submodule add https://gitee.com/cstarlang/cstar_stdlib.git proofgit submodule add https://gitee.com/cstarlang/cstar_stdlib.git proof。不要修改 proofproof 文件夹名！
  3. 把 abs.cabs.c 的第一行从 #cst_include "cstar.h"#cst_include "cstar.h" 改为 #include "proof/proof.h"#include "proof/proof.h"。
  4. 在 abs.cabs.c 中再次尝试查看符号状态，确认仍然能够正常工作。

小结

  • 用 cstarc initcstarc init 初始化 C* 项目，在 VSCode 中启动 HOL Light Server；所有 C* 程序经过 C 预处理器处理后，都以 #cst_include "cstar.h"#cst_include "cstar.h" 开头。
  • 验证从规约开始：C* 采用契约式规约，用 [[cst::require(...)]][[cst::require(...)]] 与 [[cst::ensure(...)]][[cst::ensure(...)]] 标注前置与后置条件；契约中变量名表示其在函数入口处的值，__return__return 表示返回值。
  • 反引号 `...``...` 中是逻辑表达式，语法源自 HOL Light：整数常量带 ii 后缀，用 ---- 取相反数，用 ~~ 表示逻辑非。
  • Show Symbolic StateShow Symbolic State 显示某一行处的符号状态：data_atdata_at/undef_data_atundef_data_at 显式刻画每一块内存资源，**** 表示两部分内存不相交。
  • 验证条件形如“符号状态 |--|-- 符号状态”；若全部验证条件成立，函数就没有未定义行为、满足内存安全性，而且功能符合契约。myabsmyabs 的例子展示了验证条件如何揭示有符号整型溢出这类 UB，以及如何通过加强前置条件来修复。
  • 配置证明标准库后，用 #include "proof/proof.h"#include "proof/proof.h" 替代 #cst_include "cstar.h"#cst_include "cstar.h"；后续教程都基于该库。