面向符号执行的基于部分解的约束求解缓存技术研究报告
一、 研究团队与发表信息
本研究由来自中国国防科技大学、湖南大学和新加坡管理大学的研究人员合作完成。共同第一作者为国防科技大学的帅子祺（Ziqi Shuai）和陈振邦（Zhenbang Chen），其他作者包括国防科技大学的马科林（Kelin Ma）、刘坤林（Kunlin Liu）、王吉（Ji Wang），湖南大学的张宇峰（Yufeng Zhang）以及新加坡管理大学的孙军（Jun Sun）。该研究以论文“Partial Solution Based Constraint Solving Cache in Symbolic Execution”的形式，发表于ACM软件工程汇刊（Proceedings of the ACM on Software Engineering）的第1卷FSE专刊，于2024年7月12日正式出版，并可在ACM数字图书馆获取。
二、 学术背景与研究动机
本研究的核心领域是软件工程中的自动程序分析，具体聚焦于符号执行（Symbolic Execution）技术的效率优化。符号执行是一种精确的程序分析技术，它通过将程序输入抽象为符号值，系统地探索程序的不同执行路径。其核心在于维护每条路径的路径条件（Path Condition, PC），这是一个描述到达当前状态所需满足的输入约束的公式。每当执行到条件分支语句时，符号执行引擎需要调用底层的约束求解器（如SMT求解器）来判断分支条件在当前路径条件下是否可满足，从而决定是否继续探索该分支。
约束求解是符号执行中最耗时且最具挑战性的环节，通常占据总分析时间的绝大部分，并且可能因为求解超时而导致无法探索某些程序路径。为了减少求解器的调用次数，缓存（Caching）是一种被主流符号执行引擎（如KLEE、Symbolic Pathfinder）广泛采用的有效优化机制。其基本思想是将已求解过的约束公式（或其规范化形式）及其结果（可满足时的解或不可满足的结论）缓存起来，当后续遇到相同或相似的约束时，可以直接复用缓存结果。
然而，现有的缓存机制（如严格匹配、基于子集和基于超集的复用）其有效性高度依赖于被测程序的特征和符号执行的搜索策略。在许多情况下，缓存命中率并不理想，提升缓存在各种程序上的普适有效性是一个开放性问题。研究者观察到，约束求解本身也是一个在输入空间中进行搜索的过程。在求解一个复杂公式时，求解器（尤其是基于冲突驱动子句学习的SAT/SMT求解器）会尝试许多中间赋值，这些中间赋值可能只满足原公式的一部分子约束，被称为“部分解”（Partial Solution）。这些部分解在传统求解过程中被丢弃，但它们可能恰好满足程序中其他路径的约束条件。本研究基于这一关键洞察，提出了利用约束求解过程中产生的部分解来丰富缓存的创新方法，旨在从另一个维度（利用求解器内部的搜索过程）提升缓存的命中率和符号执行的效率。
本研究的目标是设计并实现一种通用的、基于部分解的约束求解缓存机制，该方法应独立于现有的搜索启发式策略，并能集成到不同的主流符号执行引擎和SMT求解器中，从而在多种现实世界基准程序上有效提升符号执行探索的路径数量和分析速度。
三、 研究流程与详细方法
本研究包含三个核心流程：方法设计、系统实现与实验评估。
1. 方法设计流程 此流程的核心是提出“基于部分解的缓存”算法框架，并将其无缝集成到符号执行的工作流中。研究设计了一个包含两个主要算法（算法1和算法2）的系统性方案。 * 研究主体与处理方式：该流程以抽象的符号执行框架和缓存查询-更新逻辑为研究对象。 * 详细流程： * 算法1：符号执行主循环。该算法扩展了经典的符号执行框架。它维护一个待处理状态的工作列表。每次从工作列表中选取一个状态后，执行当前语句。对于条件分支，计算两个方向（真分支和假分支）的新路径条件，并调用cacheandsolve函数（算法2）来判定其可满足性。只有当分支可行时，才将新状态加入工作列表。该框架本身不感知具体的缓存实现细节，从而保证了新方法与现有搜索策略（如DFS、BFS）的兼容性。 * 算法2：缓存与求解函数。这是本研究的核心创新点。该函数接收一个路径条件查询（φ）和一个全局缓存（Cache）。Cache由两部分组成：结果缓存（RCache，存储公式的可满足性结果）和解缓存（SCache，为每个公式存储一个解集合）。 * 详细工作流： 1. 缓存查询：首先尝试通过三种传统机制复用缓存：严格匹配、超集复用（若查询是缓存中某个可满足公式的子集）和子集复用（若查询包含某个不可满足公式的子集，则直接判不可满足；或利用缓存中某个子集公式的解去快速测试是否能满足当前查询）。 2. 缓存未命中与求解：如果上述查询均失败（缓存未命中），则调用底层的SMT求解器对φ进行求解。关键在于，除了获取最终结果（res）外，还要求求解器返回在求解过程中生成的一组“部分解”（partial-solutions）。 3. 基于部分解的缓存丰富：这是本研究的核心步骤。在得到求解结果和部分解后，算法不仅将(φ, res)存入缓存，还会利用部分解来主动创建和丰富更多缓存条目。具体做法是：为当前路径条件φ构造一组“相关的”子约束集合CS，包括φ的所有前缀（prefix(φ)）以及所有“偏离路径”（offthepath(φ)）的约束（即那些在当前路径上被否定的分支条件）。然后，遍历每一个部分解ps，检查ps能满足CS中的哪些约束c。如果ps满足c，并且c在SCache中存储的解数量未达到预设上限K_b，则将ps添加到c对应的解集合中，并将c在RCache中的结果标记为“可满足”。这一步骤使得大量原本会被丢弃的中间赋值，转化为未来可能被复用的缓存资源，极大地增加了缓存覆盖的约束空间。 * 新颖算法/软件：本研究提出了全新的“基于部分解的缓存丰富”算法（算法2的第23-31行），这是方法的核心创新。此外，研究还探讨了如何在主流的冲突驱动子句学习（CDCL）SAT求解框架（算法4）中高效地收集和采样部分解，并通过追踪符号变量的编码（bitblast步骤，算法3）来将SAT层级的中间赋值重构为SMT层级的位向量部分解，从而支持QF_ABV、QF_BV、QF_ABVFP等多种SMT理论。
2. 系统实现流程 此流程旨在验证方法的通用性和可部署性，研究团队在多个现有成熟系统上进行了实现。 * 研究对象与样本：该流程的研究对象是两套主流的符号执行引擎：KLEE（针对C程序）和Symbolic Pathfinder (SPF，针对Java程序）；以及两个主流的SMT求解器：STP和Z3。 * 详细流程： * SMT求解器扩展： * 对于STP，修改了其后端SAT求解器MiniSat，使其能够生成并报告SAT层级的冲突赋值（即部分解），并在STP层面将其重构为位向量公式的部分解，同时新增了相应的接口。 * 对于Z3，修改了其内部定制的SAT求解器，以支持部分解收集，并同样增加了接口。这使得Z3能够为QF_BV和QF_ABVFP理论提供部分解。 * 符号执行引擎集成： * 在KLEE中，修改了其现有的反例缓存数据结构，将单个解扩展为一个解集合，并集成了基于算法2的缓存查询与更新逻辑。 * 在支持浮点运算的KLEE-Float变体上，利用扩展后的Z3来收集浮点约束求解的部分解。 * 在SPF中，将新方法集成到其缓存层框架Green中，特别是其grulia服务，使其能够利用Z3提供的部分解来丰富基于SAT-delta值的缓存机制。 * 新颖实验方法：研究通过实际修改开源工业级工具（KLEE, SPF, STP, Z3）来验证方法的可行性，这种“实现于主流平台”的策略显著增强了研究的说服力和实用价值。实现中引入了两个关键参数：K_p（从求解器收集的部分解数量上限）和K_b（每个缓存条目存储的解数量上限），以平衡缓存有效性和管理开销。
3. 实验评估流程 此流程旨在通过严格的实证研究，回答关于方法有效性、效率以及参数鲁棒性的三个研究问题。 * 研究对象与样本量：研究选择了三组具有代表性的真实世界基准程序进行测试。 1. 实验一（QF_ABV）：使用KLEE+STP。选取了15个来自开源社区的C程序和库（如json-c, SQLite3, libtommath等），总计超过42万行代码。这些程序能产生大量复杂的、能触发部分解的数组和位向量约束。 2. 实验二（QF_ABVFP）：使用KLEE-Float+Z3。从GNU科学计算库（GSL）中随机选取了32个涉及浮点运算的函数作为测试目标，验证方法在极具挑战性的非线性浮点约束下的效果。 3. 实验三（QF_BV）：使用SPF+Green+Z3。从Green框架的标准Java基准程序中选取了13个程序（总计约4000行代码），涵盖排序、数据结构、算法等多种类型。 * 实验处理与数据收集： * 对每个实验，分别配置启用新方法（“P”模式）和原始方法（“O”模式）。 * 对每个测试程序，采用多种搜索策略（DFS、BFS以及KLEE的随机覆盖新策略RCN）运行符号执行，超时时间设为30分钟。 * 为减少随机性，每个任务重复运行5次，取平均值。 * 收集的关键指标包括：在相同时限内探索的路径或状态数量（#paths/#states）、缓存命中率（chr）以及分析总时间（t(s)）或求解时间开销（to(s)）。 * 为了评估参数影响，在每组实验中，对参数K_p和K_b各选取了三个不同的值进行组合测试，共9种配置。 * 数据分析工作流：通过对比“P”模式和“O”模式在相同设置下的性能指标（路径数、时间），计算提升百分比和加速比，来量化方法的有效性。通过绘制路径探索趋势图，直观展示方法随时间推移的优势。通过分析不同参数配置下的结果，评估方法的鲁棒性。
四、 主要研究结果
1. 实验一（QF_ABV， C程序）结果： 尽管KLEE原有的反例缓存对可满足的数组/位向量查询已经相当有效（导致未命中查询中不可满足的比例较高，而部分解主要对可满足查询有益），但新方法仍然显示出稳定的提升。在DFS、BFS和RCN三种策略下，新方法平均将探索的路径数分别提升了7.0%、16.0%和23.1%。从路径探索趋势图（图2a）可见，新方法在不同时间点上探索的路径数均高于基线方法。在效率方面，为了探索到基线方法在30分钟内能达到的最大路径数，新方法分别获得了1.07倍、1.11倍和1.15倍的加速比（Speedup）。这证明了即使在缓存机制已经较强的场景下，利用部分解仍能带来额外的收益。
2. 实验二（QF_ABVFP， 浮点程序）结果： 浮点约束求解更为复杂，传统缓存效果相对较差（平均缓存命中率常低于0.5）。新方法在这里取得了显著成效。在DFS、BFS和RCN策略下，新方法平均将探索路径数大幅提升了71.0%、70.8%和93.8%。在某些函数（如gsl_poly_complex_solve_cubic）上，提升甚至超过1000%，因为基线方法可能因早期求解超时而提前终止，而新方法利用缓存得以继续深入探索。路径探索趋势图（图2b）同样显示新方法具有明显优势。相应的加速比达到1.67倍、1.36倍和1.50倍。结果表明，对于求解代价高昂的浮点程序符号执行，基于部分解的缓存能带来质的改进。
3. 实验三（QF_BV， Java程序）结果： 新方法在Java程序符号执行上也表现优异。对于能在时限内完成分析的程序（如remainder, triangle），新方法在DFS和BFS下分别取得了最高12.5倍和80.67倍的惊人加速比。对于未能在时限内完成的大型程序，新方法在相同时限内探索的状态数（#states）相比基线有显著提升，在DFS和BFS下平均提升分别为114.3%和56.8%。这清晰地表明，新方法能更高效地推进符号执行的状态空间探索。
4. 参数鲁棒性结果： 跨三个实验的参数调优测试表明，虽然参数K_p和K_b的最佳值因程序类型和约束复杂度而异，但在每个实验设定的不同参数配置下，新方法相比基线都展现出了一致的性能提升。这证明了该方法的鲁棒性，即只要参数设置在一个合理的范围内，就能获得正向收益。研究者也给出了参数设置的一般性指导原则：K_p应与约束求解的复杂性正相关（复杂则取大值），K_b应与路径约束的结构复杂度负相关（结构简单、扫描开销低则可取大值）。
五、 研究结论与价值
本研究得出结论：利用约束求解过程中自然产生的“部分解”来丰富缓存，是一种有效且通用的提升符号执行效率的方法。该方法的核心价值在于，它将求解器内部搜索的“副产品”转化为有价值的缓存资源，从而从新的角度攻击了缓存命中率这一经典难题。
科学价值：
应用价值：
六、 研究亮点
七、 其他有价值内容
研究还对可能引入的开销（如部分解匹配检查和快速测试的开销）进行了讨论，并明智地引入了K_p和K_b两个参数来实现效果与开销之间的权衡。论文通过一个精心设计的小例子（图1）清晰地对比了传统缓存方法与新方法在节省求解次数上的差异，使得核心思想非常易于理解。此外，研究公开了实验复现所需的构件（artifact），体现了研究的可重复性。