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、列表或任何其他类型量化。

其中六个名字是重载的，并不专属于 hprophprop：truetrue、falsefalse、existsexists、forallforall、&&&&、|||| 各自还表示一个布尔版本，类型推断会根据上下文在二者之间选择。

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，以及一份对内容的描述。

分段形式的参数顺序是：地址、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* 所建模的标量类型。

TptrTptr 对所有指针类型一视同仁——逻辑不记录指针指向什么，因此 int *int * 与 struct list *struct list * 都是 TptrTptr。 （ctypectype 数据类型还带有一个构造子 TstructTstruct，用于证明库内部的字节级推导；手写断言只用上述九个标量常量，并改为通过 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 资源之中，证明需要时用取值范围规则提取出来。

[[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)`
int abs_diff(int a, int b);

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

• 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 的标量类型；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 的形式进入逻辑。