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

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

(functions)、事件(events)、结构体(struct)等.状态变量能够描述系统状态,类似于整个代码中的全局变量;函数是
指包含一系列操作的可执行单元,能够完成特定的功能,由关键字 function 声明;结构体是指包含任意成员变量
的自定义类型,由关键字 struct 声明,与高级程序设计语言中的结构体类似;事件是调用以太坊虚拟机 EVM 日志
功能的接口,使用关键字 event 声明.
以下通过一个 Solidity 实例进行简单介绍(如图 2 所示).
1 Contract Demo {
2 uint v;

3 function set(uint x) {
4 v=x;
5 }

6 function get(⋅) returns (uint r) {
7 return v
8 }
9 }

Fig.2 Solidity example
图 2 Solidity 实例
合约 Demo 包含变量声明和函数两部分,声明了一个类型为无符号整数 uint 的状态变量 v,声明了一个 set
函数用于修改变量 v 的值,声明了一个 get 函数用于查询变量 v 的值.

3 SOL2M 转换器的研究与实现

本文使用 MSVL 对智能合约 Solidity 程序进行建模,为减少建模过程中大量的人工操作,开发了一种能够实
现 Solidity 语言到 MSVL 语言的等价转换工具 SOL2M,实现了建模过程的自动化,其具体结构以及工作流程如
图 3 所示.

Solidity
词法规则 语法规则 MSVL转换规则
实
现
过 JavaCC
程

词法分析器 语法分析器 转换实现

工
作 预处理
流 Solidity 词法 语法 程序 MSVL
程 程序 分析 分析 转换 程序
Fig.3 Architecture of SOL2M converter
图 3 SOL2M 转换器架构
SOL2M 转换器主要分为 4 个部分.
(1) 预处理:处理 Solidity 源程序中的版本标识语句和导入其他源文件语句;
(2) 词法分析:通过 JavaCC 工具生成词法分析器,对 Solidity 程序进行词法分析,将源程序识别为特定的单
词流;
(3) 语法分析:通过 JavaCC 工具生成语法分析器,对 Solidity 程序进行语法分析,把词法分析生成的单词流
识别为程序语句;
(4) 程序转换:通过分析 Solidity 和 MSVL 的词法以及语法的异同,制定出 Solidity 到 MSVL 的转换规则,
并将转换代码嵌套在语法分析的 BNF 范式中,实现 Solidity 程序到 MSVL 程序的动态转换.