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

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

表 7 操作函数定义

语义元素 定义 说明
store(S,addr,τ,v) = S ′ 在地址addr处存储类型为 τ 的数据v后, 更新storage状态
load(S,addr, sizeof(τ)) = v 得到存储在地址addr到 (addr +sizeof(τ)−1) 之间的值
storage操作 delete(S,addr) = S ′ Solidity在0.6.12及之后的版本中, 使用delete删除一个元素, 并不是真的
删除, 只是把这个值变成初始值, 即非零字节设置为零
storage由插槽slot组成, storage根据变量名称及数据类型决定为其分配相
′
alloc(S,id, sizeof(τ)) = (S ,addr)
应的空间
getAddr(g,id) = addr 计算全局变量 id 在storage中的存储位置
全局环境上的操作
getsize(g,τ e ) 根据表达式类型得到所需的内存长度
getAddr(l,id) = addr 计算局部变量 id 在memory中的存储位置
局部环境上的操作
getsize(l,τ e ) 根据变量类型得到所需的内存长度

表 8 相关函数定义

语义元素 定义 说明
field_offset(id,φ) 返回结构体成员列表 φ 中名称为 id 的成员变量在storage中的偏移量
LVs_struct(s_id,addr,id) = addr+ 根据结构体首地址及成员变量名称 id 得到成员变量在storage中的存
左值函数 field_offset(id,φ s id ) 储位置
i 项在storage中的
根据数组、数组首地址以及数组下标 i, 得到数组第
LVs_arr(le,addr,i) = addr +i·getSize(g,τ le )
存储位置
V_unop(unop,v) = unop v 根据值 v 和单目运算符 unop, 计算单目运算 unop v 的值
右值函数
V_binop(binop,v 1 ,v 2 ) = v 1 binop v 2 根据值 v 1 ,v 2 和双目运算符 binop, 计算单目运算 v 1 binop v 2 的值
is_true(v,τ v ) 若数据 v 不等于0, 求值结果为 true
布尔函数
is_ false(v,τ v ) 若数据 v 不等于0, 求值结果为 false

2.5 求值规则
本文定义 Solidity 求值规则时, 将语法元素和 Solidity 状态 µ 与执行结果联系起来, Solidity 的操作语义采用
如下形式的求值规则进行定义.
p,g,l ⊢ e,µ ⇒ out 右值表达式求值

l
p,g,l ⊢ le,µ ⇒ out 左值表达式求值
′
p,g,l, f ⊢ stmt,µ ⇒ out,µ 语句求值
out := Normal | Return | Return v | Fail | v | lv | vs 求值结果
l
求值规则将合约程序 p 与全局环境 g 及局部环境 联系起来, 在当前状态 µ 下进行求值, 左值表达式的求值结
l
v
果为内存位置 lv, 右值表达式的求值结果为值 或 vs, 本文使用 ⇒ 与 ⇒ 区分左值表达式求值与右值表达式求值.
out 表示求值结果, 表达式求值与语句求值均会得到 out 中的一类结果, out 包含: Normal 表示语句正常结束, Return
表示在遇到 return 语句时中断控制流并跳出函数体且无返回值, Return v 表示 return 语句含有返回值, Fail 表示语
句执行失败, v 表示右值, lv 表示左值, vs 表示值列表.
本文关注 Solidity 本身的语法语义, 因此认为 Solidity 状态 µ 的改变仅由其存储状态 S 或内存状态 M 的改变
而决定, 然而 MSVL 中没有相应的内存结构可以区分, 因此在定义 Solidity 语句的操作语义时, 无需刻意区分
Solidity 状态 µ 具体是因存储状态 S 或内存状态 M 的改变而发生改变的.

2.6 左值表达式求值规则

Solidity 中的左值表达式定义为:

le::= id|le[e]|le.id,