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

1590 Journal of Software 软件学报 Vol.32, No.6, June 2021

其中,
Ctype::=int|float|char|….
全局变量的抽象方式:
free〈varname〉:〈type〉.
局部变量的抽象方式:
new〈varname〉:〈type〉,
其中,type 是依照前文所述的变量类型转换方法进行替换:
〈type〉=abs(〈Ctype〉).
对于含有初始化部分〈Initial〉的变量定义语句,采用和 ExprStatement 中的赋值表达式相同抽象方法处理.
• ExprStatement
一个表达式作为独立的 C 语言语句,表达式语句是 C 语言中最基础的语句类型.严格意义上,函数调用语句
也属于表达式语句的一种,但这里的 ExprStatement 不包含函数调用的表达式语句,因为函数调用表达式语句的
抽象过程中已被处理过.在 C 语言中的表达式语句的作用是对表达式进行求值,然后丢弃求值结果,像 a+3.这种
表达式作为单独语句是没有意义的,有用的是执行表达式之后会对参与的变量(一个或多个)的值进行修改的表
达式语句,最常见是赋值语句和自增减语句.自增减其本质也是一种赋值操作,若作为单独语句,是可以和赋值
语句等价转换.
赋值语句的语法如下:
〈Lvarname〉=〈subExpr〉.
对应的 Pi 演算抽象:
let 〈Lvarname〉=abs(〈subExpr〉) in
对于〈subExpr〉抽象 abs(〈subExpr〉),我们会进行基于表达式上下文化简,具体参考第 3.3.3 节.
• IfStatement/SwitchStatement
C 语言语法中存在两类条件分支语句:If-Else 和 Switch-Case.Switch case 结构可以转化为 If-Else 结构,所以
我们重点讨论 IfStatement.SwitchStatement 的抽象可以先将其转换为 IfStatement,再对其进行抽象转换为 Pi 演算
模型.Pi 演算中支持 if-else 条件判断,因此仅需要将相应的部分条件表达式 condition,if 分支代码块 If_block,else
分支代码块 Else_block 等,利用本方案中的对应类型进行抽象即可.对于没有 else 的分支,自动补充 else 部分抽
象:else 0.具体的抽象规则描述如图 5 所示,abs(〈c_code〉)表示对〈c_code〉进行抽象后的结果.

Pi演算
C代码 IfStatement::=
If abs( condition ) then
IfStatement::= (
if ( condition )
abs( If_block)
If_block 抽 )
else 象
else
Else_block (
abs( Else_block )
)

Fig.5 IfStatement abstraction
图 5 条件语句抽象
• ForStatement/WhileStatement
考虑到循环控制结构在 Pi 演算抽象模型中无合适的模型对应,因此和现有的一些方案类似,本文方案对循
环结构无确定的自动化抽象转换规则.在自动化分析阶段采用保留循环,仅对其中代码块中的子表达式和子语