416 Journal of Software软件学报Vol.21,No.3,March2010 术.应用类型系统ATs将程序状态引入类型系统，依靠ATS与Hoare逻辑的相似性，以ATS来编码Hoare逻辑， 从而可以在类型系统上模拟Hoare逻辑的推理」 对于第2个挑战，Necula作为先驱者实现了一个叫作Touchstone的出具证明编译器(certifying compiler)I, 它包含一个类型安全的C语言小子集的传统编译器，还有为该编译器生成的汇编代码自动产生类型安全证明 的证明器.Touchstone的主要限制是在指针类型和动态存储分配方面.随后，Colby等人实现了Special J例，这是 Java语言较大子集的一个出具证明编译器，它把Java字节代码编译成英特尔IA32体系结构的目标代码. 近年来，我们研究了将出具证明编译和携带证明代码的技术应用到有显式内存管理的编程语言.我们设计 了有动态内存分配和回收机制的类C小语言PointerCl1ol,其基本安全策略要求程序运行时不出现通过NULL 指针或悬空指针(dangling pointer))进行存取指向对象的操作、不把NULL指针或悬空指针作为free函数调用 的实在参数、不发生内存泄漏等.我们采用一种基于逻辑的和基于类型的技术相结合的方式来推导程序的性 质.为了使类型系统简单并保证语言的安全性，我们在定型规则(yping rule)中增加了约束语法表达式的值的副 条件.为了静态检查这些副条件，我们为PointerC语言设计了一种指针逻辑l,l,它是Hoare逻辑的一种拓展，新 颖之处是，将精确的指针分析应用于程序验证指针逻辑可用来从前向后收集各指针是NULL指针、悬空指针 还是有效指针(valid pointer,,有指向对象的指针)的信息，收集各有效指针之间相等与否的信息.所收集信息用来 证明指针程序是否满足定型规则的副条件，以支持对指针程序的安全性验证和其他性质的验证，我们完成了 PointerC语言安全性和指针逻辑可靠性的证明]，并实现了PointerC出具证明编译器的一个原型2,1 本文是对指针逻辑前期设计的改进和扩展，主要贡献如下： (1)提出了合法(l©gal)访问路径集合的概念，极大地简化了访问路径上基本运算的定义，并使得指针逻辑 推理规则变得直观和易理解： (2)增加了局部推理规则和函数构造的推理规则，使得指针逻辑可以方便地用于有函数调用的场合： (3)与广泛使用的分离逻辑进行了深入比较指针逻辑相当于高级语言层面的分离逻辑，其优于分离逻 辑之处是能够防止内存泄漏 本文全面介绍重新设计的指针逻辑：第1节介绍PointerC语言.第2节介绍指针逻辑的重新设计.第3节给 出采用指针逻辑的一个证明实例第4节比较指针逻辑和分离逻辑第5节是相关工作的比较第6节是总结， 1 PointerC语言 PointerC是一个强调指针类型的类C小语言，它略去函数声明部分的语法（如图1所示），其类型系统可见文 献[10]. (Program) program::=structdeclist vardeclist stmtlist (Structure Decl.List)structdeclist::=structdeclist structdeds (Structure Decl.) structdec::=struct id vardeclist; (Variable Decl.List) vardeclist::=vardeclist vardecs (Variable Decl.) vardec::=type idlist; (Identifier List) idlist::=idlist.idid (Type) type::=boolintstruct ids (Statement List) stmtlist:=stmtlist stmtstmt (Statement) stmt::=hval=exp,Ival=malloc(struct id);if boolexp)block else block while(boolexp)block free (al); (Block) block.:=stm叫{stmtlis (Expression) exp::=mumberlNULLVvall-explexp+explexp-explexpxexpl... (Bool Expression) boolexp::=truelfalselexp==explexp!=expl.. -boolexp boolexpAboolexp boolexpvboolexp (L-value) Ial::=idlval->id (Natual Number) number::=012... Fig.I Syntax of PointerC language 图1 PointerC语言语法 在PointerC中，指针类型的变量只能用于赋值、相等与否比较、存取指向对象等运算以及作为函数的参数： 指针算术和取地址运算(&)被禁止.malloc和free被看成是PointerC预定义的函数，并且满足安全程序的最基本 ©中国科学院软件研究所htp:wwv.c-s-a.org.cn416 Journal of Software 软件学报 Vol.21, No.3, March 2010 术.应用类型系统 ATS[7]将程序状态引入类型系统,依靠 ATS 与 Hoare 逻辑的相似性,以 ATS 来编码 Hoare 逻辑, 从而可以在类型系统上模拟 Hoare 逻辑的推理. 对于第 2 个挑战,Necula 作为先驱者实现了一个叫作 Touchstone 的出具证明编译器(certifying compiler)[8], 它包含一个类型安全的 C 语言小子集的传统编译器,还有为该编译器生成的汇编代码自动产生类型安全证明 的证明器.Touchstone 的主要限制是在指针类型和动态存储分配方面.随后,Colby 等人实现了 Special J[9],这是 Java 语言较大子集的一个出具证明编译器,它把 Java 字节代码编译成英特尔 IA32 体系结构的目标代码. 近年来,我们研究了将出具证明编译和携带证明代码的技术应用到有显式内存管理的编程语言.我们设计 了有动态内存分配和回收机制的类 C 小语言 PointerC[10],其基本安全策略要求程序运行时不出现通过 NULL 指针或悬空指针(dangling pointer)进行存取指向对象的操作、不把 NULL 指针或悬空指针作为 free 函数调用 的实在参数、不发生内存泄漏等.我们采用一种基于逻辑的和基于类型的技术相结合的方式来推导程序的性 质.为了使类型系统简单并保证语言的安全性,我们在定型规则(typing rule)中增加了约束语法表达式的值的副 条件.为了静态检查这些副条件,我们为 PointerC 语言设计了一种指针逻辑[11,12],它是 Hoare 逻辑的一种拓展,新 颖之处是,将精确的指针分析应用于程序验证.指针逻辑可用来从前向后收集各指针是 NULL 指针、悬空指针 还是有效指针(valid pointer,有指向对象的指针)的信息,收集各有效指针之间相等与否的信息.所收集信息用来 证明指针程序是否满足定型规则的副条件,以支持对指针程序的安全性验证和其他性质的验证.我们完成了 PointerC 语言安全性和指针逻辑可靠性的证明[13],并实现了 PointerC 出具证明编译器的一个原型[12,14]. 本文是对指针逻辑前期设计的改进和扩展,主要贡献如下: (1) 提出了合法(legal)访问路径集合的概念,极大地简化了访问路径上基本运算的定义,并使得指针逻辑 推理规则变得直观和易理解; (2) 增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合; (3) 与广泛使用的分离逻辑进行了深入比较.指针逻辑相当于高级语言层面的分离逻辑,其优于分离逻 辑之处是能够防止内存泄漏. 本文全面介绍重新设计的指针逻辑:第 1 节介绍 PointerC 语言.第 2 节介绍指针逻辑的重新设计.第 3 节给 出采用指针逻辑的一个证明实例.第 4 节比较指针逻辑和分离逻辑.第 5 节是相关工作的比较.第 6 节是总结. 1 PointerC 语言 PointerC 是一个强调指针类型的类 C 小语言,它略去函数声明部分的语法(如图 1 所示),其类型系统可见文 献[10]. Fig.1 Syntax of PointerC language 图 1 PointerC 语言语法 在 PointerC 中,指针类型的变量只能用于赋值、相等与否比较、存取指向对象等运算以及作为函数的参数; 指针算术和取地址运算(&)被禁止.malloc 和 free 被看成是 PointerC 预定义的函数,并且满足安全程序的最基本 (Program) program::=structdeclist vardeclist stmtlist (Structure Decl. List) structdeclist::=structdeclist structdec|ε (Structure Decl.) structdec::=struct id{vardeclist}; (Variable Decl. List) vardeclist::=vardeclist vardec|ε (Variable Decl.) vardec::=type idlist; (Identifier List) idlist::=idlist, id|id (Type) type::=bool|int|struct id∗ (Statement List) stmtlist::=stmtlist stmt|stmt (Statement) stmt::=lval=exp; |lval=malloc(struct id); |if (boolexp) block else block |while (boolexp) block |free (lval); (Block) block::=stmt|{stmtlist} (Expression) exp::=number|NULL|lval|−exp|exp+exp|exp–exp|exp×exp|… (Bool Expression) boolexp::=true|false|exp==exp|exp!=exp|… |¬boolexp|boolexp∧boolexp|boolexp∨boolexp (L-value) lval::=id|lval->id (Natual Number) number::=0|1|2|…