Page 383 - 《软件学报》2025年第12期

5764 软件学报 2025 年第 36 卷第 12 期

6. queue.push( stmt D )
7. stmt C = getControlDep( stmt j ,C) //控制依赖
8. ret.add( stmt C )
9. queue.push( stmt C )
10. return ret

ret 将用于标记智能合约控制流图中各基本块的可达
在可达性分析中, 目标语句 target 和目标依赖语句集合
性, 达到剪枝控制流图的目的.
4.3 可达性分析
可达性分析指判断控制流图中各基本块是否与目标相关, 剪枝与目标无关的基本块生成制导信息, 用于指导
符号执行优化路径探索策略. 首先解析智能合约字节码并翻译为指令集合, 将指令集合根据终止和跳转指令划分
为多个基本块, 并根据跳转指令分析控制流的跳转信息, 以生成控制流图; 然后, 基于源代码和字节码之间的映射
关系, 定位目标语句和目标依赖语句所在基本块; 最后, 遍历控制流图并标记各基本块的可达性, 剪枝无法到达目
标语句的基本块以生成制导信息.
4.3.1 控制流图生成
根据表 3 所示的终止和跳转指令可将 Solidity 智能合约的指令集合划分为多个基本块. 其中, 跳转指令除了
用于划分基本块外, 还用于计算各个基本块之间的跳转关系, 结合基本块和跳转关系可生成控制流图.

表 3 智能合约字节码的终止指令和跳转指令

指令类型 名称 控制流跳转 描述
STOP － 终止合约的执行
RETURN － 读取内存值, 作为返回值并结束此次调用
终止指令
REVERT － 回滚此次调用的状态变量修改
SELFDESTURT － 销毁合约, 返还以太币给予栈顶地址
JUMP pc = pop() 无条件跳转
跳转指令 { pc+1
JUMPI pc = 条件跳转
pop()

Solidity 智能合约中跳转指令有 2 种, 即无条件跳转 JUMP 指令和条件跳转 JUMPI 指令. 表 3 中 pc (program
counter, 程序计数器) 用于表示当前指令的序号. 对于无条件跳转 JUMP, 当执行该指令时弹出栈顶元素, 该元素所
表示的 16 进制数值即为跳转的目的地基本块中的首个指令的序号. 对于条件跳转 JUMPI, 当执行该指令时连续
弹出 2 个栈顶元素, 分别记为 destination 和 condition, 判断 condition 是否为真, 若为真则跳转并执行指令序号为
destination 的指令 (即跳转到首个指令序号为 destination 的基本块), 否则顺延执行下一个指令 (即跳转到首个指令
序号为 pc+1 的基本块).
4.3.2 制导信息生成
制导信息的生成需要遍历控制流图, 标记各基本块的可达性, 然后将各基本块的可达性信息输出为便于符号
执行工具识别的存储形式.
首先, 由于目标语句以及目标依赖语句均仅提供源代码行号, 因此需要通过源代码与字节码之间的映射关系
定位目标基本块. 源代码与字节码之间的映射关系可通过解析编译器 (如 solc) 提供的 Source Mappings (https://docs.
pos : length 的形式, pos
soliditylang.org/en/latest/internals/source_mappings.html) 得到. 具体地, 先将源代码转换为
为源代码语句首个字符在代码文件中的位置, length 为源代码语句的字符长度. Source Mappings 经过处理后可得
pos : length 之间的映射关系. 得到该映射关系后, 可记录目标语句以及目标依赖语句所对应的指令
到指令序号与
序号集合作为目标指令集合.
然后, 遍历控制流图并判断各个基本块是否为目标基本块, 并对控制流图进行剪枝, 具体流程如算法 2 所示.