发表机构
Carnegie Mellon University（卡内基梅隆大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出智能体规划系统Agolic，利用早期符号执行运行的证据配置后续有界符号执行，在C/C++程序上平均覆盖3倍以上分支，覆盖更多分支及对比语料库未覆盖的分支，扩展了符号执行的实际覆盖范围。
AI 中文摘要
符号执行旨在探索可行的程序路径，但实际运行可能耗尽资源，而仍有大量程序行为未被覆盖。我们研究了一种补充方法，通过推理同一工具在多次有界运行间的使用方式来扩展其实际覆盖范围，同时将常规状态探索留给底层工具处理。我们提出了Agolic，一种智能体规划系统，它利用早期运行的证据来选择和配置后续的有界符号执行（BSE）运行，再由底层符号执行工具执行这些运行。规划智能、可用证据和执行模式可适配符号执行工具和分析目标。我们针对分支覆盖探索评估了一种适配方案，其中基于大语言模型（LLM）的智能体对源代码、回放的覆盖信息及早期定向尝试进行推理。我们在多个C和C++程序上评估了Agolic。在每个程序上，它都扩展了连续符号执行获得的分支覆盖，平均覆盖了超过3倍的分支数；在评估中，它比覆盖率引导的模糊测试和基于编译器的 concolic 执行各自的语料库覆盖了更多分支，且在7个程序中的6个上覆盖了所有对比语料库均未包含的分支。总体而言，这些结果表明现有符号执行工具存在大量未开发的潜力，部分潜力可通过推理其在多次运行中的能力使用方式来实现，同时将常规符号探索期间的状态选择留给底层工具处理。
英文摘要
Symbolic execution seeks to explore feasible program paths, yet a practical run may exhaust its resources while much program behaviour remains unreached. We investigate a complementary way of extending its practical reach by reasoning about how the same tool is utilised from one bounded run to the next, while leaving ordinary state exploration to the underlying tool. We present Agolic, an agentic planning system that uses evidence from earlier runs to choose and configure later bounded symbolic execution (BSE) runs, which the underlying symbolic execution tool then carries out. The planning intelligence, available evidence and execution modes can be adapted to the symbolic execution tool and analysis objective. We evaluate one adaptation for branch-coverage exploration, in which an LLM-based agent reasons over source code, replayed coverage and earlier targeting attempts. We evaluate Agolic on several C and C++ programs. On every program, it extends the branch coverage obtained by continuous symbolic execution and covers more than $3\times$ as many branches on average. It also covers more branches than each individual corpus from coverage-guided fuzzing and compiler-based concolic execution in our evaluation and reaches branches absent from all comparison corpora combined on six of the seven programs. Taken together, these results point to considerable untapped potential in existing symbolic execution tools, some of which may be realised by reasoning about how their capabilities are used across runs while leaving state selection during ordinary symbolic exploration to the underlying tool.
