Page 192 - 《软件学报》2026年第7期

赵祖威 等: 软件供应链安全中 LLM 生成代码逻辑性缺陷检测 2877

1. #include ''klee/klee.h''
2. int main() {
3. char user_message[SIZE];
4. char error_code[SIZE];
5. klee_make_symbolic(user_message, sizeof user_message, ''user_message'');
6. klee_make_symbolic(error_code, sizeof error_code, ''error_code'');
7. klee_assume(user_message[SIZE–1]=='\0');
8. klee_assume(error_code[SIZE–1]=='\0');
9. //调用待测函数
10. log_message(user_message, error_code);
11. }
图 4 符号挂载模板

本文中, 我们使用 KLEE [17,19] 作为符号执行引擎. KLEE 是当前最具代表性的符号执行工具之一, 能够遍历程
序所有可能执行路径并自动生成高覆盖率的测试用例. 凭借其在约束收集、路径搜索及测试用例生成等方面的高
效实现, KLEE 已被广泛应用于软件缺陷检测、漏洞分析以及程序测试等研究领域. 本文方法基于预定义模板为
待测程序进行符号的挂载. 图 4 展示了一个符号挂载模板, 其中定义了待测程序输入的格式 (第 3 行和第 4 行), 推
导符号约束所需的符号声明 (第 5 行和第 6 行), 以及这些约束的前置条件 (第 7 行和第 8 行), 同时还包含了供符
号执行引擎使用的其他适配信息 (第 1 行). 最终, 挂载了符号的程序将作为输入传递给符号执行引擎 KLEE, 以便
推导路径约束, 并生成相应测试用例.
● 通过符号执行生成测试输入. 符号执行是一种严格的、基于推导的程序分析技术, 用于生成满足路径约束
的测试输入. 一旦符号被挂载, 待测程序就可以被当作 KLEE 引擎的输入进行分析. KLEE 中的符号执行过程包括
两个主要部分: 符号约束收集和 SMT 约束求解. 首先, 符号约束收集模块会根据符号执行策略系统遍历程序的每
条执行路径 (例如, 第 j 条路径为 path j ). 它会收集每条路径上遇到的分支条件, 对判定为 False 的条件进行取反, 并
将判定为 True 的条件合并进合取范式 (conjunctive normal form, CNF) 中. 这个过程中会传播常量和变量, 以构造
约束条件. 随后, SMT 求解器模块会使用可满足性模理论来求解这些约束, 并且生成当前路径对应的测试输入. SMT
是对布尔可满足性问题 (SAT) 的拓展, 其目标是在特定理论 (如整数算术、实数算术、数组、位向量等) 下判断
一阶逻辑公式是否可满足. 目前主流的 SMT 求解器 (比如 Z3、STP 等) 支持多种理论的组合求解, 并在约束简化、
冲突分析与分支搜索等方面进行了高度优化, 从而显著提升了约束求解的效率. 在本文中, 对于路径 path j 的约束
集 constraints(path j ), 使用 SMT 求解器求解得到的对应的测试输入 in j 可表示为:

(2)
SMTSolve(constraints(path )) = in j
j
需要注意的是, 并非所有的条件约束都是可解的. 阶段 3 所生成的测试输入集 I SymExGe 包含了这个过程中生
n
成的所有可解输入. 总体而言, 符号执行能够系统且高效地生成一组边界测试用例, 尽可能覆盖程序的关键执行路
径, 从而显著提升测试覆盖率和缺陷检测能力. 在实际应用中, 符号执行可能因路径爆炸或非线性约束求解失败而
受到限制. 对于此类情况, 本文方法将直接采用阶段 2 中 EvalPlus 生成的测试用例继续进行缺陷检测. 通过结合符
号执行与 EvalPlus, 本文方法在保证较高覆盖率的同时, 有效增强了缺陷检测的鲁棒性与通用性.
2.4 阶段 4: 缺陷检测

在阶段 4, 我们使用阶段 2 和阶段 3 生成的测试用例, 检测 LLM 生成程序中的缺陷. 本文方法的测试输入集 I
由两个部分组成: I EvalPlus 、I SymExGen , 最终形成完整的测试输入集 I:

(3)
I = I EvalPlus ∪ I SymExGen
对于缺乏标准实现的待测程序, 我们的测试框架会利用 GPT 生成待测程序的预期输出. 通过将阶段 1 中的自
然语言描述 desc 和相应的待测程序输入 in i ∈I 作为提示词提供给 GPT, 然后由 GPT 给出该输入对应的预期输出.
由于这一过程并不依赖于待测程序或其约束条件, 因此产生的输出结果会呈现出异质性. 图 5 展示了我们使用
GPT 生成图 1 的预期输出时的提示词示例. 在方法的实际运行中, 程序功能描述与测试用例输入将被替换为实
际值.