符号执行不再卡在环境建模：智能体补上数据库模型，CrossHair 可执行函数从 4.5% 升到 81%
核心概要
符号执行工具 CrossHair 在真实 Python Web 应用上几乎跑不动，因为代码没有契约，调用数据库的部分也无法符号化。一个把 AI 编码智能体与 CrossHair 组合起来的流水线自动为函数写契约、为数据库合成符号模型，在 11 个开源应用、1,156,044 行代码上把可执行函数比例从 4.5% 提高到 81%，并找出 221 个经测试复现的缺陷。这些缺陷多为输入域边角情况，其中一部分是同模型直接阅读代码所遗漏的。
深度剖析
符号执行现在能进入此前基本无法分析的一类代码：依赖数据库的 Python Web 应用。 不加任何环境时，CrossHair 在 5,406 个已加契约函数中只能执行 243 个，占 4.5%；仅按项目测试套件的方式初始化框架，可执行 1,595 个，占 29.5%。 在 11 个开源应用、共 1,156,044 行 Python 代码上，合成环境后 CrossHair 执行 4,394 个函数，占 81%，每个仓库的执行比例在 66% 到 89% 之间。
流水线由智能体补齐符号执行缺少的两样输入：函数契约和外部环境模型。 此前这些桩、惰性初始化边界和数据库模型都要按项目手写，因此这类技术很少落到大型数据库应用上。 智能体从框架知识技能包和仓库检查出发，生成受模式约束的 ORM 桩与有界惰性初始化插件，经 CrossHair 插件接口装入而不改动引擎，并反复修复直到 CrossHair 能加载。
每个候选缺陷都要经过审计和真实执行复现才算数。 符号执行给出的反例可能来自过强的契约或过近似的环境，并不等于应用缺陷。 审计智能体把 2,113 个被反驳函数分为 241 个真实缺陷、1,281 个误报、562 个工具产物和 29 个仅位于已安装库内的失败；流水线共报告 1,050 个经单元测试复现的缺陷，其中 920 个在运行中的应用上端到端复现。
符号执行找到的缺陷与同模型直接阅读代码找到的缺陷类型不同，二者互补。 同一模型直接检查代码的基线复现了 1,824 个缺陷，总数多于本流水线的 1,050 个。 本流水线找到 312 个基线遗漏的缺陷，其中 73 个由 CrossHair 发现；CrossHair 的缺陷多为空字符串、缺失字段、异常字符等输入域边角情况，基线的缺陷多为输出错误。
启示与展望
演示范围是 11 个流行的开源 Python Web 应用，覆盖 Django 和 SQLAlchemy 两种 ORM，全部实验使用同一个前沿模型和同一套流水线。作者明确不主张符号执行比同模型阅读代码找到更多或更重要的缺陷，只主张在智能体提供环境后它能在大规模数据库应用上运行并找到其擅长的输入域边角缺陷。
契约由智能体合成，过强的后置条件会制造开发者不认为是缺陷的发现，而断言过少则不会报警，因此缺陷计数是偏重精确率的下界而非召回率度量。可达率消融只区分了框架初始化与合成环境整体，未拆分桩、惰性初始化和框架替身各自的贡献；每个仓库只报告一种配置，未给出重复运行的方差。