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

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

句进行抽象,最后采用人工分析进行抽象转换,这其中或引入执行语义的损失.
• NullStatement
空语句不执行任何操作但也符合 C 语言的语法规范,我们将其等价转换为 Pi 演算中的空过程 0.
3.3.3 表达式约简
表达式是 C 语言语句中的核心组件,对表达式的抽象逻辑处于整个抽象方案的最底层环节.变量和常量是
最基本的表达式:对于变量,我们直接在抽象逻辑中将其作为相应抽象类型的变量;常量将其视为不解义符号.
对于由变量和代数运算符等构成的表达式,先按照代数运算规则对其进行相应的计算约简,再将约简后的表达
式中的代数运算符抽象为 Pi 演算中的构建操作(constructor).
所谓约简,即在当前函数中,对表达式根据表达式的求值运算规则进行求值运算.
基于函数上下文关系的表达式约简算法见算法 2.
算法 2. 基于函数上下文关系的表达式约简算法.
输入:单个函数定义中的表达式序列 E;
输出:约简后的表达式序列 E′.
1. Context=[⋅];
2. E′=[⋅];
3. Foreach e in E then
4. Context.append{e};
5. e′=Simplify(Context,e); //据表达式上下文 Context 对表达式 e 进行化简
6. E′.append(e′);
7. EndFor
8. Return E′
在一个函数的上下文中,维护一个表达式的上下文内容,根据表达式的上下文内容逐行对当前的表达式进
行约简.最后,函数中出现的局部变量都会被函数的参数变量、全局变量以及常量的代数表达式所替代.经过约
简后的表达式,基本的代数运算和逻辑运算已经完成,无法根据当前信息进一步对表达式进行运算.无法进一步
运算的表达式中的代数运算符视为透明操作,用 Pi 演算中的 Constructor 来表示.以最基本的二元运算符+为例
进行说明.对于二元操作符+,抽象为 constructor add: fun add(num,num):num.其他操作符类似,n 元操作符抽象为
n 元函数即可.
基于函数表达式上下文关系代码约简示例如图 6.

... ...
x=a+1; x=a+1;
y=x+2*x+3+5; y=3*a+11;
result=x+y; result=4*a+12;
... ...

Fig.6 Sample code for expression reduction
图 6 表达式约简示例

4 C2P 实现与评估

4.1 实 现
本节介绍关于依照上文方案开发的 C2P 工具的实现.
C2P 工具以人工预处理后的源码为输入,将其依照上文所述的抽象方法转换为对应的 Pi 演算模型.在实现
时,我们利用 C 编译器前端开源项目 clang 及 llvm 库,采用 C++编程语言开发了 C2P 工具代码,约 1.5KLoC.