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

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

其中, le 为左值表达式, id 为变量名称, 为表达式, le[e] 在 Solidity 中既可以表示对数组元素的引用, 也可以表示
e
e
对映射类型的引用, 当表示对数组元素的引用时, 对 le 求值得到数组首元素的地址, 对 求值得到该元素在数组中
le 求值得到映射类
的索引值, 对 le[e] 进行左值表达式求值得到当前元素的地址. 当表示对映射类型的引用时, 对
型的地址, 对 e 求值得到映射类型中的 key 的值, 对 le[e] 进行左值表达式求值得到根据 key 值映射到键值对的地址.
全局变量的左值表达式操作语义如下:

getAddr(g,id) = addr
(E-1)
l
p,g,l ⊢ id ⇒ addr
规则 (E-1) 表示在全局环境中根据变量名称, 使用函数 getAddr(g,id) = addr 可以直接获取变量在 storage 中的
存储位置.

l
τ le = array p,g,l ⊢ le,µ ⇒ (sl,0)
p,g,l ⊢ e,µ ⇒ v addr = (sl,0)+v·getSize(g,τ le ) (E-2)
l
p,g,l ⊢ le[e],µ ⇒ addr
规则 (E-2) 表示了获取数组元素存储位置的操作语义, 首先根据 τ le 判断当前 le[e] 的类型是否为数组, 确认当

前表达式类型为数组类型后, 先对 le 求左值, 得到数组的首地址在 storage 中的位置. 根据 Solidity 的内存模型可
(sl,0), 然后对 求右值, 得到元素在数组中的索引值, 最
e
知, 数组类型总是开启一个新的插槽, 因此得到首地址为
终得到元素的实际位置为首地址加上元素的偏移量.

l
τ le = mapping p,g,l ⊢ le,µ ⇒ (sl,0)
p,g,l ⊢ e,µ ⇒ v keccak256(h(v)·(sl,0)) = addr (E-3)
l
p,g,l ⊢ le[e],µ ⇒ addr
规则 (E-3) 表示了映射类型的左值操作语义, 首先根据 τ le 判断类型是否为映射类型, 确认当前表达式类型为
le 求左值, 得到映射类型的首地址在 storage 中的位置. 根据 Solidity 的内存模型可知, 映射类型
映射类型后, 先对
e
总是开启一个新的插槽, 因此得到首地址为 (sl,0), 然后对 求右值, 得到映射类型的 key 值 v, 其中 keccak256
(h(v)·addr) 为哈希计算函数, 得到该键值在 storage 中的地址 addr.

l ( )
p,g,l ⊢ le,µ ⇒ (sl,0) LVs_struct(lv,id) = addr = (sl,0)+field_offset id,φ s id
(E-4)
l
p,g,l ⊢ le.id,µ ⇒ addr
规则 (E-4) 描述了获取结构体成员变量存储位置的操作语义. le 求左值, 得到结构体在 storage 中的首地址.
根据 Solidity 的内存模型可知, 结构体总是开启一个新的插槽, 因此得到首地址为 (sl,0). 再根据函数 LVs_
struct(lv,id) 得到成员变量在 storage 中的偏移量.

2.7 右值表达式求值规则
Solidity 中的右值表达式定义如下:

( )
∗
∗

e::= constantid le[e]le.ee 1 e |e |unop e|e 1 binop e 2 |le assign e

2
右值表达式操作语义如下:

l
p,g,l ⊢ le ⇒ addr load(S,addr,getSize(g,τ le )) = v
(E-5)
p,g,l ⊢ le,µ ⇒ v
规则 (E-5) 描述了既能够成为左值表达式又能够成为右值表达式的表达式, 如数组类型、结构体类型以及变
量名称, 对这些表达式进行右值表达式求值操作语义, 先获取表达式作为左值表达式时求值所得的地址, 再使用函
数 load(S,addr,getSize(g,τ le )) 从存储中加载其右值.

l
τ le = array p,g,l ⊢ le,µ ⇒ addr 1 p,g,l ⊢ e,µ ⇒ v 1
v = load(S,addr 2 ,getSize(g,τ le )) (E-6)
LVs_arr(addr 1 ,v 1 ) = addr 2
p,g,l ⊢ le[e],µ ⇒ v