Page 21 - 《软件学报》2026年第6期

2340 软件学报 2026 年第 37 卷第 6 期

阶段任务中的平均编译和符号执行耗时进行了统计 (如表 6 所示), 可见符号执行所需的时间显著高于编译, 我们
将此差距主要归因于符号执行在路径爆炸和约束求解方面的固有限制.

3.76 3.77
3.75 3.75 3.50
3.39 3.47 3.73 3.73
3.22 3.22
3.25 2.64 2.85 3.04 3.25 2.66 2.94 3.20 3.46
平均累计调用次数 2.75 1.86 2.16 1.61 1.72 1.83 1.93 2.01 2.10 2.12 平均累计调用次数 2.75 1.74 2.06 2.37 2.64 2.92
2.42
2.25
2.25
2.35
2.04
1.75
1.75
1.49
1.40
1.25 1.00 1.07 1.29 1.46 编译器 1.25 1.00 1.39 1.73 编译器
符号执行引擎 符号执行引擎
0.75 0.99
0.75 0.75
0 1 2 3 4 5 6 7 8 9 10 0 1 2 3 4 5 6 7 8 9 10
重试次数 重试次数
(a) 二进制代码提升阶段 (b) 中间代码反编译阶段
图 6 不同重试次数下的编译器和符号执行引擎平均累计调用次数

表 6 对单个函数进行反编译的平均成本

任务阶段 编译时间 (s) 符号执行时间 (s) LLM输入 (元) LLM输出 (元)
二进制代码提升 0.018 2.797 0.018 0.030
中间代码反编译 0.443 8.040 0.010 0.012

最后, 我们统计了重试任务中 LLM 查询的平均累计调用数据量, 结果如图 7 所示. 可以看出, 在两个任务中,
LLM 查询的调用数据量均呈近似线性增长趋势, 且二进制代码提升任务所使用的输入输出调用数据量明显高于
中间代码反编译任务, 表明前者需要更多的计算资源支持. 本实验中 LLM 调用基于公有云 API 实现, 其服务费用
根据输入和输出的 token 数量进行计算, 因此上述差异直接反映了实际应用中的经济成本差异 (针对单个函数的
平均成本如表 6 所示).

9 000 6 000
8 000 7 498.74 5 099.03
7 053.97 7 787.03 5 000 3 919.10 4 711.70 5 104.11
6 588.41
平均累计调用数据量 6 000 2 732.71 4 365.42 5 563.09 3 929.87 4 562.47 5 028.25 平均累计调用数据量 4 000 1 749.42 2 666.36 3 511.53 LLM输入
7 000
4 318.78
6 092.71
4 996.92
4 852.59
3 095.39
5 000
4 250.99
3 000
3 583.40
LLM输出
4 000
3 622.88
2 220.54
3 205.57
3 000
2 000
1 547.67
1 315.62
2 790.28
1 603.25
2 000
1 741.21 2 309.36 LLM输入 1 000 1 204.16 813.82 1 070.05 1 194.92 1 433.49 1 549.03
1 000 534.60 944.79
1 044.89 LLM输出 366.78 677.87
0 0
0 1 2 3 4 5 6 7 8 9 10 0 1 2 3 4 5 6 7 8 9 10
重试次数 重试次数
(a) 二进制代码提升阶段 (b) 中间代码反编译阶段
图 7 不同重试次数下的 LLM 查询平均累计调用数据量

针对问题 2 的总结: 本文所提出的 BinDec 方法依赖的迭代重试机制整体上是有效的, 且在二进制代码提升阶
段所带来的效果提升更为显著. 然而, 这一阶段也消耗了更多的 LLM 计算资源. 在实际应用中, 需综合考虑任务成
功率与资源使用量之间的平衡, 以实现经济效益与性能的优化.
4.3 问题 3: 基于符号执行的代码等价性检查准确性如何?
本文提出的 BinDec 反编译方法, 其核心在于引入符号执行技术对 LLM 输出的代码进行语义一致性检查, 以
提升生成代码的可靠性. 因此, 验证基于符号执行的代码等价性检查的准确性具有关键意义. 我们在第 3 节所述方