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

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

算法 3. 目标制导符号执行.
输入: 制导信息 target_info, 事务序列队列 trans_queue, 事务序列长度 limit;
输出: 能够覆盖目标的测试用例集合.

1. solutions = dict()
2. while trans_seq = trans_queue.pop() != None or limit– – > 0:
3. state_queue = Queue(trans_seq.state)
4. while state = state_queue.pop() != None:
5. for ins in state.bb.ins:
6. switch JUMP: //若为跳转指令 JUMP
7. jumpdest = pop_stack()
8. if target_info[jumpdest] == true: //判断 jumpdest 是否被标记为可达
9. state_queue.add(generate_state(state, jumpdest, JUMP, None)) //生成新状态, 并添加到队列
10. switch JUMPI: //若为跳转指令 JUMPI
11. jumpdest, condition = pop_stack(), pop_stack() //弹出 2 次堆栈, 作为跳转目的地和条件
12. if target_info[jumpdest] == true:
13. if isSatisfy(state.condition, condition): //判断路径条件是否满足
14. state_queue.add(generate_state(state, jumpdest, JUMPI, condition))
15. if target_info[state.pc+1] == true:
16. if isSatisfy(state.condition, !condition):
17. state_queue.add(generate_state(state, state.pc+1, JUMPI, !condition))
18. switch STOP or RETURN or REVERT or SELFDESTURT: //若为终止指令
19. trans_queue.add(trans_seq.update(state)); //更新事务序列并添加至事务序列集合
20. solutions[state.pc] = (solve(state.condition), trans_seq) //求解状态的约束条件并添加到测试用例
21. default: //若为其他指令
22. symbolic_execution_ins(state, ins) //符号化执行该指令
23. return solutions
算法 3 第 1 行初始化测试用例集合, 第 2–22 行循环读取事务序列队列 trans_queue 直到为空, 或达到事务序
列的最大长度 limit; 第 3 行将事务序列 trans_seq 的合约状态 state 将其放入 state_queue 队列中, 其中 state 表示
trans_seq 经过符号化执行后的合约状态, 包含状态变量等符号约束信息; 第 4–22 行从 state_queue 中取出队首的
状态进行分析, 逐行符号化执行基本块指令: 对于 JUMP (第 6–9 行), 弹出 1 次堆栈并将其作为跳转目的地 jumpdest,
根据制导信息 target_info 判断 jumpdest 是否可达, 若可达则调用 generate_state 函数生成新的状态. 函数 generate_
state 的参数中, JUMP 表示跳转指令, 用于计算 gas 消耗, None 表示当前跳转需要满足的条件约束, 由于 JUMP 为
无条件跳转, 因此约束条件为空. 对于 JUMPI (第 10–17 行), 连续弹出 2 次堆栈, 分别作为跳转目的地 jumpdest 和
跳转条件 condition, JUMPI 的跳转地址有 2 种, 满足跳转条件 condition 则跳转至 jumpdest, 否则跳转至 state.pc+1.
对于这 2 个跳转地址, 首先通过 target_info 判断是否可达, 然后分别将 condition 以及!condition (condition 的取反)
添加到路径条件中, 调用约束求解器判断路径条件是否满足, 若满足则调用 generate_state 函数生成相应的新状态,
并添加到 state_queue 中; 对于 STOP 等终止指令 (第 18–20 行), 首先更新 trans_seq 中状态变量的符号约束等信
息, 用以记录在 trans_seq 的基础上符号化执行该状态后的合约状态, 并将其添加至 trans_queue 以继续组合和探
索其他事务, 然后调用约束求解器求出满足当前约束条件的测试用例, 并添加到测试用例集合 solutions 中. 对于其
他指令 (第 21, 22 行), 如 ADD、SUB 或 MUL 等, 符号化执行该指令并更新 gas 数量以及堆栈信息等.