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。
  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
  at .../cstar_verification/abs.c:3:5  in myabs
error: function without a specification
  at .../cstar_verification/abs.c:3:5  in myabs

这提示我们，要验证一个程序，需要首先编写它的规约（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 的值也会报错，因为这是一个未初始化的变量。 在这个符号状态中还出现了一个逻辑连接词 ****，它是分离逻辑中非常重要的分离合取（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 版本控制（通过 git initgit init）。
  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"；后续教程都基于该库。