C* 的扩展

上一页介绍了 C* 原样继承自 HOL Light 的语法。本页列出 C* 在此基础上新增的内容：用于在逻辑中表达分离逻辑与 C 类型的类型常量、由此构建的常量与记号，以及逻辑变量与待验证 C 程序之间的命名约定。

这里列出的内容都用于反引号内的逻辑表达式。这是一份语法与类型层面的清单，说明各个名字、它们的类型以及如何解读。分离逻辑常量的含义见内存模型与断言，内存谓词的详细讨论见带类型的内存谓词。

C* 向 HOL Light 的类型语言中引入了四个类型常量。它们遵循上一页介绍的类型语法，可以出现在任何允许使用类型的位置，包括 (x:addr)(x:addr) 这样的类型标注，以及 (hprop)list(hprop)list 这样的后缀构造子应用。

struct_namestruct_name 与 fieldfield 被声明为不带任何构造子的 0 元类型常量：在程序引入自己的结构体名常量与字段名常量之前，这两个类型中没有任何元素，具体做法见下文的结构体与字段一节。 ctypectype 则是归纳类型，其构造子列在下文的“逻辑中的 C 类型”一节中。 hprophprop 是断言的类型；在 C* 的浅嵌入中，它展开为内存上的谓词，在语法层面则是一个不透明的类型常量。

下面两个类型缩写用于区分整数在内存模型中的不同用途：

addr = :int
byte = :int

addr = :int
byte = :int

类型缩写是透明的：addraddr 与 intint 是同一个类型，类型检查器不会区分二者。这些缩写只起说明作用：签名 addr->ctype->int->hpropaddr->ctype->int->hprop 能让读者分清哪个参数是地址、哪个是存储的值，而 int->ctype->int->hpropint->ctype->int->hprop 无法体现这种区别。

不带后缀的数字是自然数；C* 扩展了词法分析器，使带 ii 后缀的数字成为整数。

C* 对 C 程序建模时统一使用整数，地址、存储的值、大小与偏移的类型都是 intint，因此 C* 断言中的数字几乎都带 ii 后缀。漏掉它是编写断言时最常见的类型错误：

data_at p Tint 42data_at p Tint 42

无法通过类型检查，因为 data_atdata_at 需要的是 intint，而 4242 是 numnum。

对字面量取负时，用前缀 ---- 而非 --：1i1i 的加法逆元写作 --(1i)--(1i)，因为 -- 保留给二元减法。

下面这些常量构成分离逻辑的词汇表。第一组用于构建断言，结果类型为 hprophprop；最后一组陈述断言之间的关系，结果类型为 boolbool。也就是说，p |-- qp |-- q 是关于两个断言的命题，本身并非断言。

existsexists 与 forallforall 是绑定子（binder），写作

exists x. pexists x. p

与

forall x y. pforall x y. p

；这些写法是将常量应用于 lambda 抽象的语法糖。它们签名中的类型变量 AA 不受约束，可以对 intint、addraddr、列表或任何其他类型量化。

其中六个名字是重载的：truetrue、falsefalse、existsexists、forallforall、&&&&、|||| 除了用于 hprophprop，也各有一个布尔版本，类型推断会根据上下文选择相应的版本。

fact(x > 0i && y > 0i)fact(x > 0i && y > 0i)

里的 &&&& 是布尔合取（HOL Light 的 /\/\）；

fact(x > 0i) && empfact(x > 0i) && emp

里的 &&&& 则是堆合取。相比之下，|--|--、-|--|-、-||--||-、-*-*、-->-->、****、empemp、purepure、factfact 是 C* 专有的名字，没有布尔层面的解读。 C* 的约定还在记号上把两层量词分开：boolbool 层用符号 !! 与 ??，hprophprop 层用单词 forallforall 与 existsexists。

这三个关系记号之间的区别需要说明清楚。 -|--|- 就是 HOL Light 在 hprophprop 类型上的相等，即 (=):hprop->hprop->bool(=):hprop->hprop->bool 的另一个名字。打印关于断言的定理时会显示这个记号，所以表示谓词的定义在书写时用 ==，打印时却用 -|--|-。 -||--||- 是另行定义的常量 logic_equivlogic_equiv，含义是双向蕴含。两者在外延上一致，但仍是不同的项：用其中一个陈述的规则无法匹配用另一个写成的目标；证明库中的规则用的是 -|--|-。

这些中缀运算符的优先级与结合性见 HOL Light 语法中的运算符表；它们的定义以及所满足的定律见内存模型与断言。

这些常量用于构建描述 C 内存的断言。每个常量都接受一个地址、一个 ctypectype 以及对内存内容的描述，其中 ctypectype 说明该处内存应如何读取。

分段形式的参数依次是地址、C 类型、各个下标，最后是内容列表（仅用于已初始化的一族）。 missing_imissing_i 形式将被去掉的下标放在所有下标的最前面，如 array_at_missing_i_rec x ty i lo hi larray_at_missing_i_rec x ty i lo hi l。 undef_undef_ 一族不带内容列表，因为无法描述未初始化内存中的值；其下标参数与已初始化的一族一一对应，只是末尾用长度参数代替了内容列表。

以 xx 为基址的数组，第 ii 个元素位于地址 x + i * sizeof(ty)x + i * sizeof(ty)，这正是 C* 展开 C 下标表达式 a[i]a[i] 时产生的地址。这些谓词的拆分、合并与换基规则见带类型的内存谓词。

ctypectype 类型的值表示逻辑中的 C 类型，让 data_atdata_at 能够确定一处存储占多少字节、可以存放哪些值。九个构造子覆盖了 C* 所建模的标量类型；复合 C 类型也各有构造子，其中 TaliasTalias 按其内层类型解释，其余在逻辑中都视为不透明的类型。

TptrTptr 统一表示所有指针类型。逻辑不记录指针所指对象的类型，因此 int *int * 与 struct list *struct list * 都表示为 TptrTptr。

复合 C 类型也有对应的表示，但其语义没有建模：

Tstruct string | Tenum string | Tunion string |
Talias string ctype | Tarray int ctype |
Tfun (string)list (ctype)list ctype

Tstruct string | Tenum string | Tunion string |
Talias string ctype | Tarray int ctype |
Tfun (string)list (ctype)list ctype

TstructTstruct、TenumTenum 与 TunionTunion 只携带标签名；Talias name tyTalias name ty 表示一个 typedeftypedef，下面的函数会使用它的内层类型；Tarray n tyTarray n ty 表示含 nn 个元素的数组；TfunTfun 记录函数签名（参数名、参数类型、结果类型），只出现在带类型的内存谓词所述的函数指针规约 fnspecfnspec 与 fnspec_wfnspec_w 之内。手写断言只用九个标量常量，并通过 field_addrfield_addr 访问结构体内存。

三个函数用于从 ctypectype 中读取信息：

结构体名与字段名在逻辑中表示为常量，分别具有专用的 struct_namestruct_name 与 fieldfield 类型。证明库不预先声明这两个类型的任何元素，由程序按需引入，通常在全局证明声明中使用 new_constnew_const。命名约定是：结构体名常量在 C 结构体名前加 TT，字段名常量在 C 字段名前加 FF。这样，struct liststruct list 成为 TlistTlist，它的字段 headhead 与 tailtail 成为 FheadFhead 与 FtailFtail。 C* 根据这些名字将 C 程序与逻辑对应起来，因此这些前缀有实际作用，并非装饰。

字段地址由两个常量计算：

field_offset : struct_name->field->int
field_addr   : addr->struct_name->field->addr

field_offset : struct_name->field->int
field_addr   : addr->struct_name->field->addr

field_offsetfield_offset 是原始常量，声明时不带定义：结构体的实际字节偏移保持未解释，由各程序分别提供给验证器。 field_addrfield_addr 则是有定义的，它的定义定理以 field_addr_propfield_addr_prop 之名注册在定理数据库中：

field_addr x s f = x + field_offset s f

field_addr x s f = x + field_offset s f

因此，field_addr pt Tlist Ftailfield_addr pt Tlist Ftail 表示位于 ptpt 的 struct liststruct list 中 tailtail 字段的地址。嵌套访问也可以通过复合来表示：C 表达式 &it->node.next&it->node.next 对应 field_addr (field_addr it Titem Fnode) Tlink Fnextfield_addr (field_addr it Titem Fnode) Tlink Fnext。

C 的位运算符在逻辑中不是原始概念。 C* 在 intint 上定义了四族位运算，分别处理有符号与无符号的 32 位与 64 位整数，含义由 HOL Light 机器字库的机器字语义给出。

这些运算符都由普通的 HOL 定义给出，并非公理；每条定义定理都可以用 <op>_def<op>_def 这个名字从定理数据库中取回。定义采用以下方式：先用 iwordiword 将两个操作数转换为 N 位机器字，再执行对应的机器字运算，最后将结果转换为整数。其中，i32_i32_/i64_i64_ 一族使用 ivalival（有符号解释），u32_u32_/u64_u64_ 一族使用 &(val ...)&(val ...)（无符号解释）。

i32_and x y = ival (word_and ((iword x):(32)word) ((iword y):(32)word))
u32_and x y = &(val (word_and ((iword x):(32)word) ((iword y):(32)word)))
i64_shr x y = ival (word_ishr ((iword x):(64)word) (num_of_int y))
u64_shr x y = &(val (word_ushr ((iword x):(64)word) (num_of_int y)))

i32_and x y = ival (word_and ((iword x):(32)word) ((iword y):(32)word))
u32_and x y = &(val (word_and ((iword x):(32)word) ((iword y):(32)word)))
i64_shr x y = ival (word_ishr ((iword x):(64)word) (num_of_int y))
u64_shr x y = &(val (word_ushr ((iword x):(64)word) (num_of_int y)))

对这些运算符进行推理时，需要注意这套编码的两点细节。

• 值操作数的回绕对所有整数都有定义。 iwordiword 对每个整数都有定义，包括负数，因此即使 b > ab > a，u32_and (a - b) cu32_and (a - b) c 也是良定的。这是有意的设计：本模型将无符号 C 算术的中间结果保留为数学整数，没有 u32_subu32_sub 这样的运算；若采用部分定义的编码，这类项将无法化简。
• 移位计数则没有这样的保证。 shlshl 与 shrshr 的第二个操作数要经过 num_of_intnum_of_int，而该函数对负数输入的结果未作规定。负的移位计数在 C 中属于未定义行为，因此这样处理并无损失；但如果证明需要对移位求值，就必须先证明计数非负。

右移在机器字层面也区分有符号与无符号的情况：有符号一族使用算术移位 word_ishrword_ishr，无符号一族使用逻辑移位 word_ushrword_ushr。

另有两个运算符用于刻画 C 中将值转换为给定位宽的操作：

signed_last_nbits   x y = cast_signed y x
unsigned_last_nbits x y = cast_unsigned y x

signed_last_nbits   x y = cast_signed y x
unsigned_last_nbits x y = cast_unsigned y x

两者的类型都是 int->int->intint->int->int，其中 xx 是值，yy 是以位计的目标宽度。注意，参数顺序与 C 语义层中的底层运算 cast_signedcast_signed、cast_unsignedcast_unsigned 恰好相反。 cast_unsigned n zcast_unsigned n z 就是 z rem exp_2 nz rem exp_2 n（HOL 的 remrem 是欧几里得余数，因此结果不会为负），cast_signedcast_signed 则调整这个余数，使其落在有符号的取值范围内。两者都是全函数，且不限于某个位宽：对于负的 xx 以及 64 位及更大的宽度，都能正确处理。

以下三条关于这两个运算符的事实已得到证明，可从定理数据库中取得：

两条 _range_range 引理给出结果的取值范围，可用于卸除转换后的 data_atdata_at 取值范围义务。 unsigned_last_nbits_idunsigned_last_nbits_id 则说明：如果值已在范围内，转换就保持该值不变。这恰好对应 C* 前端从验证条件中移除一次转换所需的条件。 cast_signedcast_signed 与 cast_unsignedcast_unsigned 的定义本身也以 cast_signed_defcast_signed_def 与 cast_unsigned_defcast_unsigned_def 这两个名字导出，证明块在必要时可以逐层展开到最底层。

C* 的内存模型把存储并入堆：断言中没有程序变量这个概念，因此 C 变量必须以普通逻辑变量的形式出现在逻辑中。符号执行引擎按固定的命名规则生成这些变量，契约与不变式中的断言也使用这些名字。

分隔符是两个下划线。对词法分析器来说，这些名字都是普通标识符：HOL Light 将 __ 视为字母数字字符，因此 x__addrx__addr 是单个词法单元。程序仍可自行声明同名变量，没有机制阻止它与这套命名约定发生冲突。

因此，在函数入口处，intint 参数 xx 对应符号状态中的资源 data_at x__addr Tint x__predata_at x__addr Tint x__pre，而未初始化的局部变量 int rint r 对应 undef_data_at r__addr Tintundef_data_at r__addr Tint。 x__prex__pre 的取值范围包含在 data_atdata_at 资源之中，在该状态中并非一条独立的纯事实；证明需要这条事实时，可以用取值范围规则提取。

int abs_diff(int a, int b)
    [[cst::require(`emp`)]]
    [[cst::ensure(`fact(__return == a__pre - b__pre || __return == b__pre - a__pre) **
                   fact(__return >= 0i)`)]];

int abs_diff(int a, int b)
    [[cst::require(`emp`)]]
    [[cst::ensure(`fact(__return == a__pre - b__pre || __return == b__pre - a__pre) **
                   fact(__return >= 0i)`)]];

如何用这些名字书写契约与不变式，见函数契约、循环不变式与断言；它们如何出现在引擎产生的验证条件中，见验证条件生成。

逻辑表达式通过 cst::cst:: 命名空间下的 C23 属性进入 C* 程序。函数属性紧跟在原型或定义的参数列表之后；语句属性放在所修饰的语句之前（不变式放在循环之前，wherewhere 放在调用之前），或者自成一条语句。下表中的每个实参都是一段反引号引用，按本组页面的规则解析。

另有三种写法由工具链产生，无需手写：[[cst::include("cstar.h")]];[[cst::include("cstar.h")]]; 是 #cst_include#cst_include 指令经预处理后的形式；[[cst::module("dep.c")]];[[cst::module("dep.c")]]; 是模块依赖指令 #require "dep.c"#require "dep.c" 经预处理后的形式（采用这个名字是为了避免与前置条件属性 requirerequire 冲突）；[[cst::lsp]][[cst::lsp]] 则由编辑器集成注入，用于标记需要转储哪一行的符号状态。教程页函数契约、循环不变式与断言与第一个 C* 程序展示了这些属性的用法。

• C* 向 HOL Light 的类型语言中添加了类型常量 hprophprop、ctypectype、struct_namestruct_name、fieldfield，以及透明的类型缩写 addr = :intaddr = :int 与 byte = :intbyte = :int。
• 数字默认是 numnum，带 ii 后缀才成为 intint；证明库中的定理表述改用与之等价的 &n&n 注入记号。
• 堆命题常量——****、&&&&、||||、-*-*、-->-->、empemp、purepure、factfact、truetrue、falsefalse、existsexists、forallforall——用于构建断言；|--|--、-|--|-、-||--||- 陈述断言之间的关系，结果类型为 boolbool。其中六个名字与布尔版本重载。
• data_atdata_at/undef_data_atundef_data_at 与 array_atarray_at/undef_array_atundef_array_at 两族描述 C 内存；每个签名都带一个 ctypectype 参数，数组的第 ii 个元素位于 x + i * sizeof(ty)x + i * sizeof(ty)。
• 九个 ctypectype 构造子覆盖 C 的标量类型，TaliasTalias 则按其内层类型解释；TstructTstruct、TenumTenum、TunionTunion、TarrayTarray 与 TfunTfun 是不透明的；sizeofsizeof、min_ofmin_of、max_ofmax_of 从标量类型中读取信息；结构体通过带 TT 前缀与 FF 前缀的常量，以及 field_addr x s f = x + field_offset s ffield_addr x s f = x + field_offset s f 进入逻辑。
• 位运算与位宽转换运算符基于 HOL 的机器字定义，并非公理化：值操作数经 iwordiword 回绕，这一操作对所有整数都有定义；移位计数经过 num_of_intnum_of_int（负计数属于 C 的未定义行为）；signed_last_nbitssigned_last_nbits 与 unsigned_last_nbitsunsigned_last_nbits 的取值范围引理均已证明。
• 程序变量以 x__addrx__addr、x__prex__pre 与 __return__return 的形式进入逻辑。
• 引用通过 cst::cst:: 属性进入程序：函数上的 paramparam、requirerequire、ensureensure；语句上的 invariantinvariant、partial_invariantpartial_invariant、assertassert、partial_assertpartial_assert、wherewhere、where_typewhere_type、givengiven；证明块与幽灵声明用 proofproof。