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

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

规则 (E-6) 描述了数组元素获取相应值的操作语义. 首先判断当前 le[e] 是否为数组类型的引用, 参考左值表
达式求值规则 (E-2), 得到数组元素的存储地址, 根据地址与函数 load(S,addr,getSize(g,τ le )) 得到该数组元素在
storage 中的值.

l
τ le = mapping p,g,l ⊢ le,µ ⇒ (sl,0) p,g,l ⊢ e,µ ⇒ v
keccak256(h(v)·(sl,0)) = addr load(S,addr,getSize(g,τ e )) = v (E-7)
p,g,l ⊢ le[e],µ ⇒ v
规则 (E-7) 描述了映射类型获取相应右值的操作语义. 确认了当前表达式 le[e] 为映射类型后, 根据左值表达
式操作语义规则 (E-3), 得到映射类型的存储地址, 再根据函数获取相应的右值.

l ( )
p,g,l ⊢ le,µ ⇒ addr 1 LVs_struct(addr 1 ,id) = addr 2 = addr 1 +field_offset id,φ s id
v = load(S,addr 2 ,getSize(g,τ id )) (E-8)
p,g,l ⊢ le,id,µ ⇒ v
规则 (E-8) 描述了获取结构体体成员变量值的操作语义. 结构体成员列表 λ 存放结构体成员变量与其偏移量
( )
的映射, 先根据函数 从 λ 中得到在 storage 中的偏移量, 再通过函数 LVs_struct(addr 1 ,id) 获取结
field_offset id,φ s id
load(S,addr,getsize(g,τ id )) 得到在 storage 中对应的值.
构体成员变量的地址, 最终通过函数

l
p,g,l ⊢ le,µ ⇒ addr p,g,l ⊢ e,µ ⇒ v store(S,addr,τ v ,v) = S ′ (E-9)
p,g,l ⊢ le = e,µ ⇒ Normal
规则 (E-9) 描述了赋值表达式的操作语义. 首先通过左值表达式求值规则得到 le 的地址, 再通过右值表达式
v
求值规则得到 e 的实际值, 最后通过函数 store(S,addr,τ v ,v) 将类型为 τ v 的值 存放在 storage 中的地址 addr 处.

p,g,l ⊢ e,µ ⇒ v 1 unop::, ++ −− V_unop(unop,v 1 ) = v
(E-10)
p,g,l ⊢ unop e,µ ⇒ v
规则 (E-10) 描述了单目运算表达式的操作语义, 由于自增自减操作的语义有所不同, 因此首先判断单目运算
符的类型, 之后根据单目运算函数 V_unop(unop,v 1 ) = v 得到单目运算的结果, v = unop v 1 .

l
p,g,l ⊢ e,µ ⇒ addr
p,g,l ⊢ e,µ ⇒ v 1
unop::= ++ v = v 1 +1 store(S,addr,τ v ,v) = S ′ (E-11)
p,g,l ⊢ unop e,µ ⇒ v,µ ′
规则 (E-11) 描述了自增操作的操作语义, 与其他单目运算不同, 自增操作是对本身的变量进行重新赋值, 赋值
为原本的值加 1. 自减操作与之同理.

V_binop(binop,v 1 ,v 2 ) = v
p,g,l ⊢ e 1 ,µ ⇒ v 1 p,g,l ⊢ e 2 ,µ ⇒ v 2
(E-12)
p,g,l ⊢ e 1 binop e 2 ,µ ⇒ v
规则 (E-12) 描述了双目运算表达式的操作语义. 根据右值表达式求值规则得到 e 1 与 e 2 的值, 通过函数
V_binop(binop,e 1 ,e 2 ) = v 得到双目运算的结果, v = v 1 binop v 2 .

vs = (v 1 ,...,v k )
p,g,l ⊢ e 1 ,µ ⇒ v 1 ... p,g,l ⊢ e k ,µ ⇒ v k
(E-13)
∗
p,g,l ⊢ e ,µ ⇒ vs
规则 (E-13) 描述了参数列表的操作语义. 其中 e = (e 1 ,...,e k ), 对参数列表中每一个参数进行右值表达式求值,
∗
得到 (v 1 ,...,v k ), 且 vs = (v 1 ,...,v k ).

2.8 语句求值规则
Solidity 基本语句定义为 stmt, 包含空语句, 返回语句, 表达式语句, 条件判断语句, 顺序执行语句, 循环语句以
及函数调用语句等. 本节给出 Solidity 语句的操作语义.
空语句表示在当前状态下不执行任何操作, 即任何变量的地址与值都未发生变化, 因此执行前后状态无变化,
其操作语义如下:

p,g,l, f ⊢ ;,µ ⇒ Normal,µ (S-1)
return 语句表示在当前状态下退出函数, 不执行函数内部剩余的语句, 因此执行前后状态发生变化. return 语