Page 15 - 《软件学报》2021年第6期

张协力 等:C2P:基于 Pi 演算的协议 C 代码形式化抽象方法和工具 1589

现象,因为它们的处理方式和正常函数的处理类似.在对语句进行抽象处理时,将表达式 Expr 视为原子项,对于
表达式的处理将在第 3.3.3 节阐述.首先介绍 C 中的变量类型处理,再介绍各种类型语句的抽象方法.
A. 变量类型转换
方案将 C 语言中的变量基本类型简化为两种基本类型:数字型 num 和字符串类型 bitstring.其中,num 类型
包含了 C 语言中常见的 int,float,long,double 等.对于字符及数组等抽象为 bitstring 类型.为了支持条件分支语句
逻辑,还应该引入对 bool 类型的抽象.Pi 演算模型中,内建类型中支持 bool 类型以及与之相伴随的 true 和 false
两个 bool 型常量,这里直接将 C 语言中的 bool 类型及 true,false 与之对应抽象即可.
在此基础上增加指针类型 ptr,并通过引入 PTR 构建操作和对应的析构操作 VAR 来实现对 C 语言中基本类
型指针的支持.
• PTR_num(a:num):ptr 获取 num 类型变量 a 的内存地址;
• PTR_bitstring(s:bitstring):ptr 获取 bitstring 类型变量 s 的内存地址;
• VAR_num(p:ptr):num 获取地址 p 处的值,返回类型为 num;
• VAR_bitstring(p:ptr):bitstring 获取地址 p 处的值,返回类型为 bitstring.
用 Pi 演算中的重写规则来将这两种操作进行关联.
type num.
type bitstring.
type ptr.
fun PTR_num(num):ptr.
reduc forall a:num,p:ptr;VAR_num(PTR_(ptr))=a.
fun PTR_bitstring(bitstring):ptr.
reduc forall s:bitstring,p:ptr;VAR_bitstring(PTR_bitstring(ptr))=p.
本方案暂不支持函数指针以及指针的运算操作,当协议代码中涉及到这些语法时,自动化抽象程序仅将这
些语法部分标注出来,留作人工处理.
B. 语句抽象
对代码块的处理,我们以 C 语言中的语句(statement)作为基本的翻译单元.考虑协议的 C 代码中常见的语句
类型,主要有变量声明/定义语句、表达式语句、条件分支语句、函数调用语句、返回语句、循环结构语句等.
其中,函数调用语句和返回语句在上一小节中已经进行了抽象处理,本方案暂不支持 C 程序中的循环结构语句,
涉及到循环结构的部分需要依赖人工经验进行手工转换(见表 3).
Table 3 Common statements type in C language
表 3 C 中常见语句类型
语句类型 说明
VarDeclStatement 变量声明和定义
ExprStatement 表达式
IfStatement/SwitchStatement 条件分支
NullStatement 空
CallStatement 函数调用
ReturnStatement 函数返回
ForStatement/WhileStatement 循环
下面逐一给出这些语句到 Pi 演算逻辑的转换方法.
• VarDeclStatement
变量声明和定义语句在抽象转换时并无特殊区别,因为 C2P 并不关注协议 C 代码的语法正确性.这是编译
工具所做的事情.
全局变量与局部变量定义语句在具体的抽象细节上稍有不同,具体抽象规则描述如下:
VarDeclstatement::=〈Ctype〉〈varname〉[Initial],