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

王小兵 等: Solidity 到 MSVL 转换的等价性研究 4013

Solidity 基本语句定义为 stmt, 包含语句块 stmt , 表达式语句 e;, 变量声明语句 VarDe f , 返回语句 return, 条件
∗
判断语句 if-else, 循环语句, 转向语句 throw. 语法定义如下:

∗
stmt::= {stmt }|e;|VarDe f|return e;|return;|if (e) stmt 1 (else stmt 2 )?

|for(stmt 1 ;e; stmt 2 ) stmt|while(e) stmt|throw;

2.2 语义定义策略
本节在定义 Solidity 操作语义时, 首先借鉴了文献 [20] 中 Solidity 语义定义的基本形式, 其中给出的大步语义
形式的 Solidity 求值规则与核心动态语义为本文提供了基础结构, 并且对于以太坊状态和 Solidity 状态的形式化
定义也为本文定义语义元素提供了思路. 之后参考了文献 [21] 中对于 Solidity 内存模型的研究, 其中给出的对
Solidity 内存模型以及函数调用的形式化定义, 为本文定义语义元素中的内存模块提供了理论基础, 也为函数调用
的操作语义提供了值得借鉴的步骤. 然后参考文献 [18] 中证明 C 语言与 MSVL 操作语义等价性的方法, 确定了本
文的等价性证明思路. 针对将来 Solidity 快速迭代引入的新版本特性, 可根据语句变化完善现有的操作语义, 进而
将本文的等价性研究工作扩展到 Solidity 高阶版本.
本节所定义的 Solidity 操作语义覆盖了 Solidity 的主要语法, 并给出了更详尽的语义元素以及操作函数定义,
相较于文献 [20] 的 Solidity 操作语义更加完善. 本文采用大步语义的形式定义 Solidity 的操作语义, 这一方面是由
于文献 [18] 均采用大步语义的形式, 保持形式的一致有利于之后等价性的证明以及研究的扩展; 另一方面大步语
义在描述高级程序设计语言的操作语义上更有优势. 小步语义通常用于描述机器级语言的语义, 更注重于描述程
序每走一步的规则, 解释执行语句的每个步骤如何进行, 即将父结构不断拆分为子结构, 最终递归得到结果; 而大
步语义则更关注程序的开始与结束的状态变化, 描述如何得到语句执行终止的最终状态, 预设了语句可终止, 所给
出的操作语义更加高效, 易于调试和扩展 [22] .
大步语义的求值规则有如下基本形式 [23] :

ρ ⊢ e ⇒ v (1)

(2)
s 1 ⊢ e ⇒ s 2
其中, ρ 为环境, 公式 (1) 表示在环境 ρ 中表达式 e 的值为 . s 2 为状态, 公式 (2) 表示在状态 s 1 下执行表达式 e
v s 1 与
s 2 . 基于此本文定义了 Solidity 的求值规则.
会得到新状态
语义的推导规则通常有如下形式:

P 1 P 2 ...P n
(3)
C
其中, P i (1 ⩽ i ⩽ n) 为假设或者前提, C 表示结论, 若假设或前提 P i 均成立, 则结论 C 一定成立, 若没有假设或前提,
结论依然成立, 那么结论即为公理.

2.3 内存模型
Solidity 与其他语言不同, 使用 memory、storage、callback 和 stack 这 4 个不同的数据位置, 其中 stack 只有在
为字节码赋予语义时才有研究意义, 而 calldata 位置的作用可以忽略, 因此本文中仅关注前两项 memory 和
storage 数据位置.
(1) memory: 存储函数内部的所有本地数据, 即局部变量. memory 数据在函数执行完成后被删除.
(2) storage: 存储函数外部的数据, 即状态变量. 在 storage 中的变量将永久保存在区块链上. storage 是一组存
储槽, 每个槽长 32 字节, 可通过 256 位地址寻址.
(3) callback: 存储函数的传入执行数据, 不可修改.
(4) stack: 用于加载变量和存储 EVM 生成的中间值.
Solidity 中状态变量可以是机器整数、地址、数组、结构体或者映射类型. 状态变量为 storage 类型, 永久存
储在区块链中. 函数中的局部变量默认为 memory 类型, 也可显示声明为 storage 类型. 此外, 全局变量在 storage 中
的存储位置由数据类型决定, 其规则如下.