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

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

(1) 值类型仅使用它们所需的字节, 若当前插槽的剩余空间不足以存放一个值类型, 则将其存放在下一个存储
插槽.
(2) 结构体与数组类型总是放在一个存储插槽的开始, 结构体与数组中的各元素按规则紧密存储.
(3) 映射与动态数组不可预知大小, 因此仅占用 32 字节, 其包含的元素存储的位置由 keccak-256 哈希函数计
算确定. 映射所占用的插槽实际上并未使用, 但仍需要. 动态数组所占用的插槽存放数组中元素的数量.
可知基本类型仅使用存储它们所需的字节, 结构体和数组等总是占用一整个新插槽, 因此 storage 地址由插槽
索引值 sl 以及插槽内偏移量 δ 决定.

2.4 语义元素
本文定义 Solidity 状态 µ =< a,σ, M > 为一个三元组, 包含当前合约在区块链中的地址 address, 记为 a, 以太坊
σ 和内存 memory M, memory 用于保存当前正在执行的函数的局部变量. 执行智能合约代码会改变
网络状态 状态
a
以太坊网络的状态, 从形式化的角度来看, 以太坊网络状态 σ 可由智能合约地址 映射得到, 定义网络状态
p, 以及存储 S ,
σ =< b, p,S > 为一个三元组, 包含合约余额 b, 即账户所持有的货币数量, 合约程序 storage 的状态
storage 用于保存合约的状态变量.
表 6 为 Solidity 语义元素的定义, 其中左值 lv 表示变量在 storage 中或者 memory 中的地址, sl 为 storage 插槽
δ
索引, storage 地址 addr 是一个由存储插槽索引与偏移量 组成的序偶对. 求值环境包括全局环境 g 与局部环境 l.
fd 为函数定义, 全局环境 g 将程序全局变量和函数名映射到存储插槽索引, 若为函数, 则可以从索引映射到函数定
义局部环境. 局部环境 l 将局部变量映射到 memory 地址. 内存状态 M 从 memory 地址映射到其内容, 存储状态 S
从 storage 插槽索引映射到其内容. τ 表示表达式所对应的类型.

表 6 语义元素

语义元素 定义 说明
左值 lv lv ::= loc|addr loc表示局部变量在memory中的地址, addr 表示全局变量在storage中的地址
storage地址 addr addr ::= (sl,δ) storage插槽索引与偏移量组成的序偶对
全局环境 g g ::= (id → sl)×(sl → fd) 从全局变量映射到storage插槽索引, 并从插槽索引映射到函数定义
函数局部环境 l l ::= id → loc 从局部变量映射到memory地址, 函数局部环境 l 用于保存当前函数内部的局部变量
内存memory状态 M ::= loc → v 从memory地址映射到内容
存储storage状态 S ::= sl → v 从storage插槽索引映射到内容
类型 τ τ e 表达式 e 的类型
结构体成员变量 λ id 结构体 id 的成员列表

表 7 给出了在存储 storage 状态、全局环境和局部环境上的操作. 在 storage 状态上有 store、 load、 delete、
alloc 这 4 个基本操作, 函数 store 在 storage 地址 addr 处存储类型为 的值 v. 函数 load 在 storage 地址 addr 处根
τ
据内存长度加载其对应的内容. 函数 alloc 能够在 storage 地址 addr 处根据类型 τ 分配相应的存储长度. Solidity 的
storage 永久存储在区块链之上, 区块链作为一种公有资源, 为避免滥用, 鼓励使用者主动对空间进行回收, 释放空
间时会返还 gas, 但是 Solidity 中的 delete 与其他语言有所不同, 并非释放空间, 而是对变量进行初始化.
,
在全局环境上和局部环境上均有函数 getAddr 和函数 getSize getAddr 可以根据全局环境或局部环境以及变
量名称从 storage 或者 memory 中获取其映射的内容. 函数 getSize 可根据全局环境或局部环境以及当前变量的类
型, 获取其所需的内存长度.
表 8 给出了部分函数定义, 左值函数用于对地址的求值, 在左值表达式求值时给出具体应用, 其中, 函数
field_offset(id,φ) 根据结构成员列表 φ 进行查询, 得到名称为 id 的成员变量的偏移量. 函数 LVs_struct(s_id,addr,id)
id 在 addr 得到成员变量
首先根据函数 field_offset(id,φ) 得到成员变量 storage 中的偏移量, 再结合结构体的首地址
在 storage 中的实际位置. 函数 LVs_arr(le,addr,i) 首先根据数组类型 与索引值计算元组相对于数组首地址的偏
τ
addr, 得到成员变量在 storage 中的实际位置. 右值函数中给出了单目运算与双目运算
移量, 再结合数组的首地址
的函数. 布尔函数中根据变量的类型与值, 计算真值.