符号执行是在上世纪70年代提出的一种程序分析技术,用于检验程序是否违反某些属性,因为其可以在复杂软件中寻找深度错误而受到人们的广泛关注。约束求解耗时一直是符号执行的瓶颈之一,约束求解结果重用是一种通过重用已求解约束的求解结果从而有效提高符号执行效率的方法。现有的约束求解结果重用方法采用不同的重用策略实现约束求解结果的重用,但是它们都基于相同的假设:约束在重用中是作为整体不可分割的,即它们都是将约束作为整体进行重用。整体重用实际上严重地限制了符号执行中的重用能力,在符号执行程序产生的约束较为复杂以及程序规模增长时,采用整体重用的策略较难找到相匹配的约束。另一方面,我们看到,符号执行所产生的约束存在非常明显的规律性:大批量的约束中都是由相同和相似的一系列子句组合而成。这是因为符号执行程序生成的约束通常代表了一条执行路径的约束条件,而约束中的子句对应着程序中相应分支的分支条件。程序的路径由不同的程序分支组合而成,于是产生的约束也存在大量的相同或相似子句。这一现象启发我们,基于子句而非整个约束重用,可能是更好的重用策略,可以取得更好的重用效果。基于此,我们提出了一种基于子句而非整体重用的约束求解结果重用方法ClauseCache。ClauseCache基于分解式存储和组合式重用来实现约束的求解结果重用。已求解的约束解被分解为子句解来存储,当为新生成的约束寻找可重用解时,ClauseCache为新约束的每个子句找到一组候选解,然后在子句候选解中找到可行的组合,来满足整体约束。ClauseCache方法可以在更细粒度上进行重用,相对与整体约束重用,具有更好的重用能力。我们从理论上也证明了该方法的重用能力超过了基于等价、基于子集/超集、基于蕴含关系重用三类重用方法。由于子句候选解组合空间巨大,我们通过两步快速过滤操作以及一步启发式探索来达到快速搜索的目的。在为待求解约束查找可重用解时,首先基于“同一个变量在不同子句中的值必须相同”这一原则,对每个变量的候选值做筛选。之后,我们利用变量候选值对各个子句的候选解进行进一步过滤,通过这两步过滤对搜索空间剪枝,有效地缩小需要探索的子句组合解空间。最后通过启发式探索,从过滤之后的子句候选解组合中找到一组可行解。由于快速过滤中使用了大量的集合交并计算,我们采用了两个基于BitSet的索引来将集合计算的复杂度降低到常数级。我们实现了Java版本的ClauseCache,并将其集成到我们开发的Java动态符号执行工具JConcolic中,使其能直接在符号执行程序时重用。ClauseCache可以与jConcolic中的约束切片、约束规范化、约束约减等其他约束优化方法一起使用,通过进一步简化待求解约束来优化约束求解。我们在真实程序集上对ClauseCache的重用效果进行验证,对ClauseCache的绝对重用能力和在实际动态符号执行中的重用能力分别进行了评估。在实际动态符号执行中,又分别在三个典型的重用场景评估了ClauseCache的重用能力和重用效率:(1)单个程序中的重用;(2)跨程序版本重用;(3)跨程序重用。实验表明,ClauseCache的绝对重用能力强于GreenTrie、Klee-R(Klee的重用方法)和Green。在实际的动态符号执行场景中,相比当前最先进的4种重用方法:Green,GreenTrie,Utopia和KLEE的重用方法,ClauseCache也可以显著地改善重用率和查询时间,有效地提高符号执行的效率。