Page 109 - 《软件学报》2025年第9期

4020 软件学报 2025 年第 36 卷第 9 期

C 集合判断外部调用的智能合约是否存在于区块链之上, 若不存在, 调用失败, 参考规则 (S-18), 若存在,
其中, 使用
通过 G 函数获取该合约的全局环境. 之后通过 fundef 函数判断外部调用的函数是否被定义, 若已定义, 则获取其函
数定义, 执行函数并得到其返回值, 参考规则 (S-19). 若不存在其函数定义, 则调用失败, 执行结果为 Fail, 参考规
则 (S-20).
当内部函数或外部函数成功获取到函数定义时, func(vs) 为函数定义, v re 为函数 func 的返回值, 函数内部语
句执行结果 out、返回值类型与返回值之间的关系如下:

Normal|Return,void # ∅ Return v|Return vs,τ # v re 当τ , void时.
对于内部函数调用 func(vs) 有:

func = [τ|void]id f (par){stmt} alloc_mem(M,lpar) = (M 1 ,loc)
(S-21)
store_mem(M 1 ,loc,l, par,vs) = M 2 p,g,l, f ⊢ stmt,µ 2 ⇒ out,µ 3 out,τ # v re
p,g,l, f ⊢ func(vs),µ ⇒ v re , free_mem(µ 3 ,loc)
其中, par 表示函数的形参, alloc_mem(M,l, par) 为形参分配其在内存 memory 中所需的内存, 并返回新的内存状
态 M 1 和分配的内存位置 loc. 函数 store_mem(M 1 ,loc,l, par,vs) 使用传入的参数值 vs 为形参 par 进行赋值. free_mem
(µ 3 ,loc) 表示在退出函数时, 当前 Solidity 状态为 µ 3 , 且在退出时会释放当前函数为保存形参所分配的内存.
对于外部函数调用 id c .func(vs) 有:

func = extern[τ|void]id f (par){stmt} v re = id f (par)
(S-22)
p,g,l, f ⊢ id c .func(vs),µ ⇒ v re ,µ
其中, v re = id f (par) 获取外部函数调用 id f (par) 返回的结果, 外部函数执行时并不会对当前合约的状态造成影响,
因此外部函数调用执行前后状态 µ 未发生改变.

3 Solidity 与 MSVL 操作语义等价性证明

SOL2M 转换器 [12,13] 的功能是将 Solidity 程序转换为功能等价的 MSVL 程序, 为保证转换前后的程序在操作
语义上等价, 本文定义了 Solidity 语言子集的操作语义, 并在本节中给出 Solidity 子集操作语义与 MSVL 操作语义
之间的等价性证明.

3.1 Solidity 到 MSVL 的转换规则
在过去的研究中, 通过 JavaCC 对 Solidity 进行了词法和语法分析, 实现了 Solidity 到 MSVL 的自动转换工具
SOL2M 转换器, 完成了对 Solidity 程序的自动化建模, 并通过实例进行了 Solidity 程序的形式化验证, 说明了方法
的可行性. 本节主要介绍 SOL2M 转换器的转换规则, 为下文的等价性证明奠定基础.
表 9 为 Solidity 到 MVSL 的基本类型转换规则, 将 Solidity 类型 τ s 与 MSVL 类型 τ m 一一对应, 是后续内存注
入函数 α 定义及 α 等价性证明的基础. 其中使用形式化方法的抽象解释, 简化了字节和地址类型的变量声明, 其长
度限定为 1, 因此均转换为 MSVL 的 char 类型. 此外, 由于 MSVL 中没有映射类型, 因此使用结构体对其进行抽象
描述, 其中一个成员变量对应映射类型中的键, 另一个对应映射类型中的值. 每一组 mapping 键值对在 MSVL 中
都有一个相对应的结构体实例表示, 整个 mapping 类型由结构体数组抽象表示. 表 10 为 Solidity 到 MSVL 的核心
转换规则, block s 表示 Solidity 程序块, 转换后的 MSVL 程序块使用 block m 表示.

表 9 Solidity 到 MSVL 的基本类型转换规则

Solidity数据类型 MSVL数据类型
int, int8, int16, …, int256 int
uint, uint8, uint16, …, uint256 int
bytes, bytes1, bytes2, …, bytes32 char
bool bool
address char