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

王小兵 等:面向 MSVL 的智能合约形式化验证 1857

3.4 语义分析与程序转换模块
语义分析是编译过程中的一个逻辑阶段,其功能为对源程序进行上下文有关性质的分析,审查是否存在语
义错误,最终将源程序翻译为机器能够读懂的语言.本文对语法分析之后得到的 Solidity 源程序进行语义分析,
根据每条语句的实际含义制定出 Solidity 与 MSVL 之间的等价转换规则,并在语义分析的过程中实现程序转换.
通过分析和对比 Solidity 语言与 MSVL 语言,制定了两者之间的转换规则.下面从合约以及基本语句的转换
规则两方面进行介绍,部分转换规则见表 4.
Table 4 Conversion rules from Solidity to MSVL
表 4 Solidity 到 MSVL 的转换规则
类型 Solidity 程序 MSVL 程序
struct Candidate{ struct Candidate {
bytes8 name; char name and
结构体
uint voteCount; int voteCount
} };
uint public a=0; int a and a<=0 and skip;
声明语句
uint[⋅] public arr; int arr[MAX] and skip;
function vote(int id){
function vote(uint id) public{ frame(a) and (
函数 uint a=id; int a and a<=id and skip
} )
};
throw; skip;
block;
function fun(int return_value) {
转向语句 function fun(⋅) { frame(return_flag)(
return 0; int return_flag<=0 and skip;
} return_flag:=1 and return_value:=0)
};
if (expression){ if (expression) then {
block block
条件语句 }else{ }else{
block block
} }
while (e1) {
for (statedef;e1;e2){ block
循环语句 block e2;
}
}
e1[+,−,*,/,%]e2 e1[+,−,*,/,%]e2
含算术运算符的表达式
e1[++,−−] e1:=e1[+,−]1
e1=e2 e1:=e2
含赋值运算符的表达式
e1[+,−,*,/,%]=e2 e1:=e1[+,−,*,/,%]e2
e1&&e2 e1 AND e2
含逻辑运算符的表达式
e1||e2 e1 OR e2
智能合约主要由状态变量、结构体和函数构成.Solidity 中的 int8,uint256 等声明整型变量转换为 MSVL 程
序后均使用 int.同理,Solidity 中的 bytes 转换为 MSVL 的 char 类型,地址变量 address 转换为 char 类型.在 Solidity
中,结构体的声明与 MSVL 的用法相同,只需要在结构体内部加入相应的时序操作即可.Solidity 与 MSVL 中函
数声明的用法也相同,但函数中需要加入 frame 框架操作来保证变量值的遗传.
基本语句包括声明语句、表达式语句、条件判断语句、循环语句、转向语句、复合语句以及空语句.若
MSVL 当中存在 Solidity 某个语句的近似语句时,可以直接替换,例如 while 语句和 if 语句等;若 MSVL 中不存
在近似语句,则需要对该语句进行抽象表达,例如 throw 语句.当抛出异常时后面的语句不再执行,由于在 MSVL
中不存在抛出异常的语句,转换时将 throw 语句与将要执行的语句一并转换为 skip,其区间长度为 1,并在下一状
态执行空语句 empty.
根据 JavaCC 的特性,本文采用在语法分析过程中进行语义分析的方法来实现程序转换,根据制定的转换规
则在每个语法分析函数中预定义了转换的语义动作.程序转换的基本流程如图 10 所示:SOL2M 转换器首先读
取 Solidity 源程序文件(solidity.sol);然后进入语法分析阶段,提取 Solidity 程序语法单元的语义信息,并根据制定