符号执行中约束求解结果重用技术的比较

符号执行中约束求解结果重用技术的比较 Comparison of Constraint Solving Solutions Reuse Techniques in Symbolic Execution 1 first-author 胡小辉，女，硕士生，主要研究方向为符号执行。 E-mail：huxiaohui@whu.edu.cn 胡小辉，女，硕士生，主要研究方向为符号执行。 E-mail：huxiaohui@whu.edu.cn huxiaohui@whu.edu.cn 1 2 1 1 1 武汉大学 计算机学院，湖北 武汉430072 武汉大学 计算机学院，湖北 武汉430072 School of Computer Science, Wuhan University, Wuhan 430072,Hubei, China School of Computer Science, Wuhan University, Wuhan 430072,Hubei, China 中国科学院 武汉病毒研究所，湖北 武汉430071 中国科学院 武汉病毒研究所，湖北 武汉430071 Wuhan Institute of Virology, Chinese Academy Sciences, Wuhan 430071, Hubei, China Wuhan Institute of Virology, Chinese Academy Sciences, Wuhan 430071, Hubei, China 约束求解耗时一直是符号执行的瓶颈之一，约束求解结果重用是一种有效提高符号执行效率的方法。本文对约束求解重用技术Green、Klee-R、GreenTrie及Green、Utopia进行比较，证明了前三者重用能力从高到低依次是GreenTrie，Klee-R，Green，后两者中Utopia的重用能力高于Green。在动态符号执行场景下对四种重用方法的重用效率进行了实验比较，证明重用技术的重用效率并不完全取决于重用能力，并进一步从程序的特点、约束的类型以及约束的次序对重用效率的影响进行了分析和比较。本文的工作为约束求解重用领域的研究提供了综述和评估，可以为未来该领域的研究提供借鉴。 Constraint solving is the blockneck in symbolic execution and constraint solving solutions reuse is an effective way to reduce cost of symbolic execution . We conduct a comparative study on four solution reuse approaches. Among Green, Klee-R, GreenTrie ,we prove that the reuse ability from high to low is GreenTrie, Klee-R, Green, and between Utopia and Green,Utopia s reuse ability is higher than that of Green. We also compare the efficiency of four reuse methods under the dynamic symbolic execution scenario and prove that the efficiency of a reuse technology does not depend entirely on its reuse ability. We further analyze the factors which affect the reuse efficiency, including characteristics of programs, the type of constraints and the order of constraints. A survey and an evaluation on the solution reuse approaches have been made useful for future research. 符号执行 约束求解 重用 symbolic execution constraint solving reuse 0　 引 言 1 符号执行是在20世纪70年代提出的一种程序分析技术，用于检验程序是否违反某些属性 [ 1 1 ] 。由于它可以在复杂软件中寻找深度错误，因而受到人们的广泛关注 [ 2 2 , 3 3 ] 。符号执行与具体执行是相对的，在具体执行时，程序用一组特定的输入值去执行，只能探索到程序的一条路径，而符号执行用符号值代替具体值来模拟程序执行，可以同时探索程序在不同输入下可以采取的多条路径。 在符号执行过程中，程序所探索的路径条件被收集起来，传送到约束求解器中求解路径条件是否可满足，以此来判断该条路径的可行性，同时求解的结果可被用作相应路径的具体输入值。由于约束求解可满足问题是一个NP完全问题，约束求解一直是符号执行中最耗时的任务。尽管约束求解技术近年来取得了重大进展，使符号执行技术在应用上取得了巨大的进步，但它仍然是符号执行的瓶颈之一。 为了缓解约束求解的耗时问题，有许多优化技术被提出来，包括不相关约束消除 [ 4 4 , 5 5 ] ，约束求解结果重用 [ 6 6 , 7 7 ] 和增量求解 [ 8 8 ] 。其中，约束求解结果重用技术通过重用已经求解过的约束的求解结果，尽可能地避免对路径约束的求解，已被证明是一种十分有效的优化方法。在回归测试以及在被分析程序中有循环或者数组的时候，约束求解结果重用技术可以大幅度地提高符号执行的效率。 目前，国内外学者提出了多种用于符号执行的约束求解结果重用技术，代表性的工作有Green [ 5 5 ] 、Recal [ 9 9 ] 、GreenTrie [ 10 10 ] 、Utopia [ 11 11 ] 等。然而，一种重用技术是否能够真正提高符号执行的效率，取决于多方面的因素。不同重用技术在重用能力和效率方面具有各自的局限性，不同的程序的约束类型、约束规模、约束产生的次序也会影响到重用的效果。在目前的重用技术相关文献中，对此并没有清晰的论述。 本文将对目前约束求解领域目前的几种约束求解结果重用技术的重用能力、重用效率进行比较研究，分析影响重用效果的因素，以期为未来该领域的研究提供借鉴。本文第1节主要介绍符号执行中约束求解结果重用技术中的基本概念；第2节介绍当前几种约束求解结果重用技术的原理；第3节主要从理论上和实验中分别对几种约束求解结果重用技术的重用能力和重用效率进行分析比较，并对影响重用效果的因素进行了分析；第4节为结论部分。 1　 约束求解结果重用 1 在符号执行中，约束是一个逻辑公式。约束求解（SAT/SMT）的目的是为该公式找一组解让公式为真。如果能够找到一组解，则该约束是可满足的,否则该约束是不可满足的。 例如约束 <math id="M1"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417070&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417063&type= 20.65866661 2.96333337 是可满足的，它至少存在一个解，如 x =1，也就是说 x 为1时约束为真。而约束 <math id="M2"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417084&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417077&type= 24.29933357 2.96333337 则是不可满足的，因为没有解使其为真。 定义1 约束求解结果 约束求解结果 R 可以表示为 R = S | <math id="M3"><mi mathvariant="normal">∅</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417100&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417092&type= 3.72533321 3.64066648 。对于可满足约束，求解结果是约束的解S，对于不可满足的约束，求解结果是一个空集 <math id="M4"><mi mathvariant="normal">∅</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417140&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417107&type= 3.72533321 3.64066648 。 定义2 约束求解结果的重用 约束求解结果的重用是指在符号执行中，通过查找之前的约束求解结果，找到使当前约束满足的解，或者证明当前约束不可满足，来避免耗时的约束求解的一种优化方法。 在重用技术的具体实现中，符号执行工具每次调用约束求解器之前，先利用重用技术检测是否有可以重用的求解结果。如果有可重用结果，则不用求解约束，直接返回结果。如果没有找到可重用结果，则需要调用求解器进行约束求解。 定义3 重用的有效性 对于一次符号执行来说，如果不用重用技术求解完所有的约束所耗费的时间是 T ，而使用重用技术后，检测和存储可重用约束所耗费时间是 T r ,求解不可重用约束所耗费时间为 T s ，如果 <math id="M5"><mi>T</mi><mo>></mo><msub><mrow><mi>T</mi></mrow><mrow><mi mathvariant="normal">r</mi></mrow></msub><mo>+</mo><msub><mrow><mi>T</mi></mrow><mrow><mi mathvariant="normal">s</mi></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417152&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417147&type= 18.88066673 3.81000018 ,则该重用技术对于本次符号执行是有效的。 因此，从原理上看，为了提高重用的有效性，一方面需要提高重用率减少约束求解器的调用次数，来减少 T s ；另一方面需要提高重用算法的效率，来减少 T r 。 在理想情况下，我们希望同时提高重用率和重用效率。然而，在实际的重用技术中，这两者会相互影响。一般重用率的提高会需要更复杂的重用算法，造成重用效率的下降。 2　 约束求解结果重用技术的分类 1 我们根据约束求解结果重用技术采用的重用规则的不同，将目前的约束求解结果重用技术分为四种：1） 基于等价的重用；2） 基于超集和子集的重用；3） 基于蕴含关系的重用；4） 基于解空间相似性的重用。 2.1　基于等价的重用 2 Visser等 [ 5 5 ] 提出了一种基于等价的重用技术Green。如果两个约束 C 和 <math id="M6"><mi>C</mi><mi mathvariant="normal">'</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417162&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417158&type= 3.30199981 3.30199981 是等价的，那么其解也是相同的。例如约束 <math id="M7"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417177&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417170&type= 20.65866661 2.96333337 是可满足，存在一个解 x =1约束为真，约束 <math id="M8"><mi>y</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>y</mi><mo><</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417189&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417184&type= 20.31999969 3.81000018 与 x > <math id="M9"><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417200&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417194&type= 13.80066681 2.96333337 是等价的，则约束 <math id="M10"><mi>y</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>y</mi><mo><</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417211&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417206&type= 20.31999969 3.81000018 也是可满足的 ，y =1是使其为真的一个解。 2.2　基于超集和子集的重用 2 符号执行工具Klee [ 7 7 ] 在约束求解部分采取了一种基于超集和子集的约束求解结果重用策略来提高约束求解的效率，为了表述方便，在本文中称其为Klee-R。Klee-R基于定理：若约束 <math id="M11"><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">1</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">2</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">3</mn></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417221&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417216&type= 18.45733452 3.89466667 是可满足的，那么 <math id="M12"><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">1</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">2</mn></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417232&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417226&type= 11.09133339 3.89466667 也是可满足的，且 <math id="M13"><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">1</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">2</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">3</mn></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417244&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417238&type= 18.45733452 3.89466667 的解是可满足 <math id="M14"><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">1</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">2</mn></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417253&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417249&type= 11.09133339 3.89466667 的;若约束 <math id="M15"><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">1</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">2</mn></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417261&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417257&type= 11.09133339 3.89466667 是不可满足的，那么 <math id="M16"><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">1</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">2</mn></mrow></msub><mo>∧</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">3</mn></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417269&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417264&type= 18.45733452 3.89466667 也是不可满足的。例如约束 <math id="M17"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mn mathvariant="normal">5</mn><mo>∧</mo><mi>y</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417296&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417274&type= 35.98333359 3.81000018 是可满足的，存在一个解 <math id="M18"><mfenced open="{" close="}" separators="|"><mrow><mi>x</mi><mo>=</mo><mn mathvariant="normal">1</mn><mo>,</mo><mi>y</mi><mo>=</mo><mn mathvariant="normal">0</mn></mrow></mfenced></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417303&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417301&type= 21.67466736 4.82599974 使约束为真，约束 <math id="M19"><mi>x</mi><mo><</mo><mn mathvariant="normal">5</mn><mo>∧</mo><mi>y</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417311&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417307&type= 24.12999916 3.81000018 是其子集，则约束 <math id="M20"><mi>x</mi><mo><</mo><mn mathvariant="normal">5</mn><mo>∧</mo><mi>y</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417322&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417318&type= 24.12999916 3.81000018 也是可满足的， <math id="M21"><mfenced open="{" close="}" separators="|"><mrow><mi>x</mi><mo>=</mo><mn mathvariant="normal">1</mn><mo>,</mo><mi>y</mi><mo>=</mo><mn mathvariant="normal">0</mn></mrow></mfenced></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417329&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417327&type= 21.67466736 4.82599974 是使其为真的一个解。约束 <math id="M22"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417335&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417332&type= 24.29933357 2.96333337 是不可满足的，约束 <math id="M23"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn><mo>∧</mo><mi>y</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417341&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417338&type= 39.62399673 3.81000018 是其超集，则约束 <math id="M24"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn><mo>∧</mo><mi>y</mi><mo><</mo><mo>-</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417352&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417346&type= 39.62399673 3.81000018 也是不可满足的。 2.3　基于蕴含关系的重用 2 Jia等 [ 10 10 ] 提出了一种基于蕴含关系的约束求解结果重用技术GreenTrie。GreenTrie重用技术基于以下的定理：如果 <math id="M25"><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">1</mn></mrow></msub><mo>→</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">2</mn></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417364&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417358&type= 12.69999981 3.64066648 ， C 2 是可满足的，那么 C 1 也是可满足的, C 2 的解是满足 C 1 的；如果 <math id="M26"><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">2</mn></mrow></msub><mo>→</mo><msub><mrow><mi>C</mi></mrow><mrow><mn mathvariant="normal">1</mn></mrow></msub></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417378&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417370&type= 12.69999981 3.64066648 ， C 1 是不可满足的，那么 C 2 也是不可满足的。例如 <math id="M27"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417389&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417384&type= 20.65866661 2.96333337 是可满足的，存在一个解 x =1约束为真，由于约束 <math id="M28"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mn mathvariant="normal">5</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417399&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417395&type= 20.65866661 2.96333337 逻辑蕴含着约束 <math id="M29"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mn mathvariant="normal">10</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417405&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417403&type= 22.52133369 2.96333337 ，则约束 <math id="M30"><mi>x</mi><mo>></mo><mn mathvariant="normal">0</mn><mo>∧</mo><mi>x</mi><mo><</mo><mn mathvariant="normal">10</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417409&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417407&type= 22.52133369 2.96333337 也是可满足的， x =1是使其为真的一个解。 2.4　基于解空间相似性的重用 2 Aquino等 [ 11 11 ] 提出了一种基于解空间相似性的约束求解结果重用技术Utopia。Utopia是一种启发式的重用技术，它认为解空间相似的约束之间更容易重用。Utopia从已求解约束中找到与待求解约束解空间最相似的约束，将其解代入待求解约束中进行验证,判断是否能重用。为了衡量约束之间的解空间相似性，Utopia提出了一个数学模型，通过计算出来约束之间的距离来近似表示约束之间解空间相似性。 3　 约束求解结果重用技术的比较 1 在本节中，我们对四类约束求解结果重用技术进行分析，从重用能力，重用效率，重用影响因素上对各种约束求解结果的重用能力进行比较。 3.1　重用能力 2 重用能力指的是在相同的程序中，相同的条件下，约束求解结果重用技术能重用的约束数量。不同的重用技术可利用的重用的场景不同，在重用能力上存在差别。 3.1.1　理论分析 3 在第2节中我们介绍了四种约束求解重用技术的原理，Green是基于等价关系的重用，Klee-R是基于子集/超集上的重用，GreenTrie是基于蕴含关系的重用，Utopia是基于解空间相似性的重用。为了方便对重用能力的表述，有如下定义： 定义4 若方法 M 1 <math id="M31"><mo>⊒</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417422&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417416&type= 2.11666679 3.30199981 方法 M 2 ，表示在同样约束库的情况下，对于任意约束 C ，如果方法 M 2 能够为 C 找到重用解，那么方法 M 1 也一定可以为 C 找到重用解。 定理 1 重用能力上，GreenTrie <math id="M32"><mo>⊒</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417432&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417426&type= 2.11666679 3.30199981 Klee-R <math id="M33"><mo>⊒</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417444&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417437&type= 2.11666679 3.30199981 Green。 证 设有已求解约束 C 和待求解约束 <math id="M34"><mi>C</mi><mi mathvariant="normal">'</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417455&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417450&type= 3.30199981 3.30199981 ，1） 若 C 是可满足的，其求解结果为 S ，且 <math id="M35"><mi>C</mi><mi mathvariant="normal">'</mi><mo>⇔</mo><mi>C</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417465&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417460&type= 10.58333302 3.30199981 ,则 <math id="M36"><mi>C</mi><mi mathvariant="normal">'</mi><mo>⊆</mo><mi>C</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417480&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417473&type= 10.49866676 3.47133350 ，则 <math id="M37"><mi>C</mi><mi mathvariant="normal">'</mi><mo>→</mo><mi>C</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417493&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417487&type= 10.58333302 3.30199981 ；2） 若 C 是不可满足的，且 <math id="M38"><mi>C</mi><mi mathvariant="normal">'</mi><mo>⇔</mo><mi>C</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417506&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417500&type= 10.58333302 3.30199981 ，则 <math id="M39"><mi>C</mi><mi mathvariant="normal">'</mi><mo>⊇</mo><mi>C</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417523&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417514&type= 10.49866676 3.47133350 ，则 <math id="M40"><mi>C</mi><mo>→</mo><mi>C</mi><mi mathvariant="normal">'</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417536&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417530&type= 10.75266743 3.30199981 ，即，如果约束 C 可以被Green重用，那么约束 C 一定也可以被Klee-R重用，一定也可以被GreenTrie重用。倒过来则不成立。所以重用能力：GreenTrie <math id="M41"><mo>⊒</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417548&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417541&type= 2.11666679 3.30199981 Klee-R <math id="M42"><mo>⊒</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417560&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417554&type= 2.11666679 3.30199981 Green。证毕。 定理 2 重用能力上，Utopia <math id="M43"><mo>⊒</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417573&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417566&type= 2.11666679 3.30199981 Green。 证 假设有已知求解约束 C 和待求解约束 <math id="M44"><mi>C</mi><mi mathvariant="normal">'</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417583&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417578&type= 3.30199981 3.30199981 ，Utopia中度量解空间相似性的模型为 A ，设 <math id="M45"><mi>f</mi><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>A</mi><mo stretchy="false">）</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417595&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417588&type= 12.10733318 3.97933340 是度量约束解空间的相似函数， <math id="M46"><mi mathvariant="normal">D</mi><mi mathvariant="normal">i</mi><mi mathvariant="normal">s</mi><mo stretchy="false">(</mo><mi>C</mi><mi mathvariant="normal">'</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo>=</mo><mfenced open="|" close="" separators="|"><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>C</mi><mi mathvariant="normal">'</mi><mo>,</mo><mi>A</mi><mo stretchy="false">)</mo><mo>-</mo><mfenced open="" close="|" separators="|"><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>A</mi><mo stretchy="false">)</mo></mrow></mfenced></mrow></mfenced></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417607&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417601&type= 54.10200119 5.58799982 表示 C 和 <math id="M47"><mi>C</mi><mi mathvariant="normal">'</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417616&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417612&type= 3.30199981 3.30199981 之间的解空间相似性， <math id="M48"><mi mathvariant="normal">D</mi><mi mathvariant="normal">i</mi><mi mathvariant="normal">s</mi><mo stretchy="false">(</mo><mi>C</mi><mi mathvariant="normal">'</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417623&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417619&type= 16.34066582 3.89466667 越小表示两个约束之间的解空间相似性越高；若 C 可以被Green方法重用， <math id="M49"><mi>C</mi><mi mathvariant="normal">'</mi><mo>⇔</mo><mi>C</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417631&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417627&type= 10.58333302 3.30199981 ，则 <math id="M50"><mi>f</mi><mo stretchy="false">(</mo><mi>C</mi><mi mathvariant="normal">'</mi><mo>,</mo><mi>A</mi><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>A</mi><mo stretchy="false">)</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417640&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417636&type= 30.14133263 4.14866638 ， <math id="M51"><mi mathvariant="normal">D</mi><mi mathvariant="normal">i</mi><mi mathvariant="normal">s</mi><mo stretchy="false">(</mo><mi>C</mi><mi mathvariant="normal">'</mi><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo>=</mo><mfenced open="|" close="|" separators="|"><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>C</mi><mi mathvariant="normal">'</mi><mo>,</mo><mi>A</mi><mo stretchy="false">)</mo><mo>-</mo><mi>f</mi><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>A</mi><mo stretchy="false">)</mo></mrow></mfenced><mo>=</mo><mn mathvariant="normal">0</mn></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417651&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417645&type= 60.96000290 4.91066647 ，对于重用库中的约束集合 R c ， <math id="M52"><mo>∀</mo><msub><mrow><mi>C</mi></mrow><mrow><mi>m</mi></mrow></msub><mo>∈</mo><msub><mrow><mi>R</mi></mrow><mrow><mi>c</mi></mrow></msub><mo>,</mo><mi mathvariant="normal">D</mi><mi mathvariant="normal">i</mi><mi mathvariant="normal">s</mi><mo stretchy="false">(</mo><msub><mrow><mi>C</mi></mrow><mrow><mi>m</mi></mrow></msub><mo>,</mo><mi>C</mi><mi mathvariant="normal">'</mi><mo stretchy="false">)</mo><mo>≥</mo><mi mathvariant="normal">D</mi><mi mathvariant="normal">i</mi><mi mathvariant="normal">s</mi><mo stretchy="false">(</mo><mi>C</mi><mo>,</mo><mi>C</mi><mi mathvariant="normal">'</mi><mo stretchy="false">)</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417660&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417655&type= 54.94866943 4.82599974 ，则 C 一定是可重用的候选约束之一。1） 若 C 是可满足的，其求解结果为 S ，因为 <math id="M53"><mi>C</mi><mi mathvariant="normal">'</mi><mo>⇔</mo><mi>C</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417668&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417663&type= 10.58333302 3.30199981 ，所以 S 一定满足于 <math id="M54"><mi>C</mi><mi mathvariant="normal">'</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417678&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417673&type= 3.30199981 3.30199981 ； 2）若 C 是不可满足的，因为 <math id="M55"><mi>C</mi><mi mathvariant="normal">'</mi><mo>⇔</mo><mi>C</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417688&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417683&type= 10.58333302 3.30199981 ，则 <math id="M56"><mi>C</mi><mi mathvariant="normal">'</mi></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417698&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417693&type= 3.30199981 3.30199981 也是不可满足的，即 C 可以被Utopia方法重用，所以重用能力：Utopia <math id="M57"><mo>⊒</mo></math> http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417704&type= http://html.publish.founderss.cn/rc-pub/api/common/picture?pictureId=3417701&type= 2.11666679 3.30199981 Green。证毕。 对于GreenTrie和Utopia，以及Klee-R和Utopia的重用能力，因为没有相通的比较之处，重用能力无法比较。 3.1.2　实验比较 3 为了实现对各类约束求解结果重用技术公平比较，实验程序均用动态符号执行引擎jConcolic进行符号执行（jConcolic是本实验室开发的基于动态符号执行工具jDart [ 12 12 ] 的一个动态符号执行引擎），由jConcolic提供统一的约束求解接口，约束求解模块以及所有的重用技术都通过实现该约束求解接口，集成到jConcolic上。在需要约束求解时，都调用SMT求解器 Microsoft Z3 [ 13 13 ] 来进行约束求解。 本文实验集包括各重用技术的测试集(去掉了无法在jConcolic中运行的程序)和4个补充浮点程序，程序与实验集的对应关系如 表1 表1 所示，其中Wbs、Bintree、Treemap、BinomiealHeap和AvlTree通过符号执行可以得到超过10 000个约束。通过这几个程序可以观察各类重用技术在大规模的约束求解中的表现。 注： Y表示程序来自于该实验集 程序 约束总数 Green Green-Trie Utopia 补充 Trityp 16 Y Y Tcas 99 Y Y Y ReverseWord 90 Y Multiplication 73 Y SwapWords 1 171 Y Wbs 13 823 Y Bintree 21 264 Y Y Treemap 10 841 Y Y Y BinomiealHeap 31 571 Y Y AvlTree 19 674 Y HeapSort 2 382 Y MulKnapsack 7 129 Y RamerDouglas 239 Y 符号执行每个程序，并保证在每个程序执行之前存储约束求解结果的库初始值为空，在符号执行的过程中，每次约束求解之前我们会查询库中是否有约束求解结果可以重用于当前待求解的约束，若有，直接从库中取出结果作为该约束的解，否则，调用Z3约束求解器对待求解的约束进行求解，并将约束和求解的结果放入到库中。 3.1.3　结果分析 3 由 表2 表2 中的结果可知，Klee-R的重用数目总是高于Green的，GreenTrie的重用数目总是高于Klee-R的，Utopia的重用数目总是高于Green的。这与定理1和定理2结果一致。 注： hit是指通过重用技术从库中找到可重用的解的约束的数目（包含可满足和不可满足两种情况）。 程序 需要求解的约束总数 Green/hit Klee-R/hit GreenTrie/hit Utopia/hit Trityp 16 1 1 1 3 Tcas 99 70 72 76 15 ReverseWord 90 86 86 86 86 Multiplication 73 26 26 28 28 SwapWords 1 171 3 3 3 7 Wbs 13 823 13 788 13 788 13 788 210 Bintree 21 264 2 428 2 474 2 387 4 066 Treemap 10 841 8 764 8 765 8 765 5 464 BinomiealHeap 31 571 2 130 2 152 2 160 2 164 AvlTree 19 674 8 632 9 283 11 457 6 123 HeapSort 2 382 16 16 16 16 MulKnapsack 7 129 0 0 186 100 RamerDouglas 239 85 85 85 85 从 表2 表2 还可以看出Utopia的重用能力并不总是比GreenTrie以及Klee-R强。在实验集的13个程序中，Utopia有8个重用数目最多，GreenTrie有9个重用数目最多，Utopia和GreenTrie的重用能力互有高低。另一方面，Utopia在其中6个程序中重用数目比Klee-R要多，而在另外的4个程序中，Klee-R的重用比Utopia多。可见Utopia的重用能力并没有完全超过GreenTrie和Klee-R,只是在某些场景下表现的比GreenTrie和Klee-R要好。 3.2　重用效率 2 只有在使用重用技术可以提高重用效率的情况下，我们才称该重用方法是有效的。本节我们将通过实验对四种重用技术的重用效率进行比较和分析。 3.2.1　实验比较 3 符号执行引擎（jConcolic）和实验集与3.1节相同。在每个程序进行符号执行之前，保证存储约束以及约束求解结果的库为空。为了比较四种重用技术的有效性，用Z3求解器直接求解的总时间作为基准，与采用重用技术得到所有约束解的总时间作为对照。其中采用重用技术所需要得到约束解的总时间包括：从库中查询是否有可重用的解的总时间，无法从库中找到可重用的解时将约束传入到约束求解器中的求解总时间，以及将求解出来的约束和结果存入库中的总时间。 为了减少由实验环境带来的执行时间的误差，在进行实验的时候计算机不执行其他任务，且对每次实验都重复5次取平均值。实验结果如 表3 表3 所示。 注： 黑体数字表示求解每个程序的所有约束所用的最短时间 程序 Z3 Green Klee-R GreenTrie Utopia Trityp 0.453 0.439 0.444 0.468 0.389 Tcas 1.243 0.826 0.469 0.588 1.388 ReverseWord 1.399 0.281 0.187 0.234 0.218 Multiplication 14.081 15.420 19.424 14.592 14.569 SwapWords 11.911 13.407 18.330 17.611 22.190 Wbs 11.983 4.176 0.775 0.862 122.034 Bintree 258.269 238.313 1 595.368 247.519 388.997 Treemap 166.065 29.694 29.673 28.033 56.765 BinomiealHeap 347.934 363.089 2 548.200 408.273 359.297 AvlTree 225 535 136 395 255 573 101 824 155 204 HeapSort 17 919 18 431 44 750 17 862 19 574 MulKnapsack 1 207 527 1 259 763 1 796 252 1 255 402 1 256 458 RamerDouglas 6 981 6 206 6 271 6 314 6 162 s 3.2.2　结果分析 3 从 表3 表3 看重用技术并不总是有效的。在四类重用技术能重用的约束数目都比较少的情况下（重用情况见 表2 表2 ，如SwapWords程序），重用技术并不能有效减少约束求解的次数，反而因为查询和存储约束的过程造成了额外的开销，使用了重用技术之后的效率并未提高反而下降。 重用能力并不是决定重用效率的唯一因素，重用算法本身的效率也会决定重用的效率。从 表3 表3 中可以看到，尽管GreenTrie的重用能力强于Klee-R和Green，但是其总的求解时间并不总是少于Klee-R和Green。因为GreenTrie的重用算法比Klee-R和Green的重用算法要复杂，耗时更多，在重用率相近的情况下，GreenTrie并没有凸显其重用能力强的优势。 重用算法本身的效率包含查询可重用解的效率和存储约束求解结果的效率，两者都会影响到重用效率。在约束较少的程序中，Klee-R是四种重用技术中获得最高效率次数最多的重用技术，虽然Green的重用算法相比Klee-R的重用算法更加简单，但是Green采用redis数据库来存储约束求解结果，而Klee-R在符号执行过程中直接用内存存储，导致Green在效率上不如Klee-R。然而，在有较多约束的程序中，如Bintree和BinomiealHeap两个程序中，Klee-R所用的总求解时间都远远高于其他重用技术，甚至是直接求解所用时间的6倍和7倍。这是因为Klee-R查找超集的算法伸缩性很差，在待求解约束的子句规模增长的时候，其查询效率急剧下降，造成其整体效率的下降。 3.3　影响重用的因素 2 3.3.1　程序本身的特点 3 程序本身的特点会直接影响到约束重用的效果。可以设想，在极端情况下，如果程序在符号执行过程中需要求解的约束都完全相同，那么利用重用技术在整个符号执行过程中只需要求解一次即可；相反，如果程序在符号执行过程中要求解的约束都极其不相同，那么利用重用技术可能找不到可以重用的结果，在这种情况下，使用重用技术不仅无法提高符号执行的效率，在每次求解约束之前的查询过程和求解约束之后的存储过程，还会变成额外的负担。而如果程序中有循环，有对数组的处理，在程序中可能出现大量相同甚至相似的约束，重用的可能性更高，重用的效果会更突出。 如实验集中的SwapWords程序，从 表2 表2 中可以看到需要求解的约束总数为1 171个，但是四种重用技术重用的约束数目最多才7个。因为SwapWords程序中的条件变化较多，在符号执行过程中本身没有太多被当前重用技术重用的场景，在这种重用率下，四种方法最终的求解总时间都高于用直接约束求解的求解总时间（见 表3 表3 ），尤其是Utopia方法，因为它是一个启发式的重用技术，每次在求解约束之前都会从约束库中找出解空间最相似的 k 个值进行验证，且并无其他过滤过程，虽然其重用数目高于其他三种重用技术，但是最终所用的时间是最多的，几乎是直接求解所花时间的两倍。而Tcas程序中本身有数组，Treemap程序中有递归，这些程序中会产生大量相似甚至相同的约束，导致其可重用的可能性大大提高，重用效率也会提高，总的求解时间分别缩短为原来的1/5和2/5。 因此，程序本身是否存在与重用技术相适应的可重用场景会影响重用效果，有较多相同或相似约束的程序重用可能性更高。 3.3.2　约束的类型 3 约束的类型对重用技术是有限制的，即不同的重用技术往往只适应于特定类型的约束重用，本节将从重用技术的原理上来分析其各自适应的约束类型。 Green是基于等价的约束求解结果重用，其判定能否重用的方式比较简单，对于约束类型实际上没有要求，无论是线性整数类型约束，或者是浮点类型约束，或者是字符串类型约束，只要两组约束形式是等价的，即可以重用。但是Green也有非常大的局限性，因为在程序中要得到两组完全相同的约束是十分困难的，在符号执行中，程序中所有的变量都表示成输入值的函数，所以最终生成的约束中会包含很多嵌套关系，约束最终会显得十分复杂，这无疑给等价重用增加了新的难度。 Klee-R是基于超集子集的重用技术，其适用的约束类型和Green是相同的，对约束的类型没有要求，因为Klee-R实现判断子集/超集的方式就是通过判断约束子句的等价关系来实现的。Klee-R比Green能识别出更多的约束重用场景，但是Klee-R在求解结果库中找到一组特定约束的子集本身是很耗时的，尤其是在待求解约束的子句规模增长的时候，造成Klee-R并不适宜于大规模的约束查询。 GreenTrie是基于蕴含关系的重用技术，它与Green和Klee-R的不同之处在于，GreenTrie会通过判断约束子句的蕴含关系来判断约束之间是否可以重用。GreenTrie通过蕴含关系的判断对约束做了一定简化，可以解决一部分由于约束子句之间相互包含造成冗余约束无法匹配的问题。另一方面，约束之间的蕴含关系是需要规则定义的，如何判断两组约束之间的蕴含关系并不是一个简单的问题。目前在GreenTrie方法中只提出了针对整数类型和浮点类型的部分蕴含判断规则，对于其他类型的约束如要适用，需要提出针对该种类型约束的蕴含规则和对应的判断蕴含的算法。 Utopia通过提出一个数学模型来衡量约束之间的解空间相似性，但是该种数学模型只能衡量线性整数约束以及无量词的非线性浮点类型约束，对于其他类型约束无法判断。另外由于该数学模型要求对每个约束中的每个变量值代入3个不同的值进行数值计算，所以对于本身只有二值的布尔类型变量，需要做特殊的处理，对于无法用数值计算的约束都不适用。 从以上分析可知，Green和Klee-R适用于任意类型约束，GreenTrie只实现了整数约束和浮点约束的部分蕴含关系重用，Utopia只适用于线性整数约束以及无量词的非线性浮点类型约束。 3.3.3　约束的次序 3 符号执行是通过遍历程序搜索空间来实现对程序的分析，我们在遍历程序的时候可以选择不同的遍历策略，如BFS（广度优先）策略，DFS（深度优先）策略等。考虑到重用的约束来源即是先被符号执行遍历到的约束，那么约束被执行到的次序也会影响到重用的效果。我们采用与3.1相同的环境进行实验，研究同一种重用技术在符号执行时采用不同的路径遍历策略方式造成的影响。实验集中SwapWords重用太少，BinomiealHeap由于约束较为复杂，求解结果十分不稳定，在不同的约束求解策略中无法进行公平的比较，所以将这两个程序从实验集中去掉。实验结果如 表4 表4 ~ 表7 表7 。 注： 黑体表示每个程序中最高的重用数目 程序 约束总数 BFS DFS Random Trityp 16 1 0 1 Tcas 99 70 61 64 ReverseWord 90 86 84 82 Multiplication 73 26 16 15 Wbs 13 823 13 788 13 783 13 783 Bintree 21 264 2 428 6 914 4 606 Treemap 10 841 8 764 8 510 8 432 AvlTree 19 674 8 632 8 620 13 522 HeapSort 2 382 17 14 1 504 MulKnapsack 7 129 0 0 3 693 RamerDouglas 239 85 85 98 注： 黑体表示每个程序中最高的重用数目 程序 约束总数 BFS DFS Random Trityp 16 3 2 2 Tcas 99 15 15 15 ReverseWord 90 86 84 82 Multiplication 73 28 20 19 Wbs 13 823 210 489 495 Bintree 21 264 4 066 10 082 6 327 Treemap 10 841 5 464 5 209 5 112 AvlTree 19 674 6 123 5 953 5 918 HeapSort 2 382 16 13 47 MulKnapsack 7 129 100 56 1 260 RamerDouglas 239 85 85 79 其中BFS表示广度优先策略，即是在动态符号执行变异条件时，总是优先变异顶部的条件。DFS表示深度优先策略，即是在动态符号执行变异条件时，总是优先变异底部的条件。Random代表随机路径选择策略，即是在符号执行变异条件时，从约束的子句中任选一个未变异的条件进行变异，得到新的路径约束。在符号执行程序的过程中，统计采用同一种重用方法在不同的遍历策略情况下得到的重用数目。 从表 4 4 , 5 5 , 6 6 , 7 7 中可以看出，同一种重用技术在不同的路径遍历策略下，其重用情况会有差异。每一种重用技术都会受到路径遍历策略的影响，且在有些程序中受到路径遍历策略的影响非常大。但是并没有某一种重用技术在某一种路径策略下一直表现得很好，也并没有某一种路径策略总是优于其他路径策略。结合表4~7可知，四种重用技术几乎都在同一个程序中的同一个路径遍历策略中表现的最好。经过分析认为原因是，Green、Klee-R、GreenTrie都是基于约束语义相似性的重用，所以他们在重用中的趋势是相同的。Utopia通过判断解空间的相似性来实现重用也取得了类似的结果，说明不同的程序是有最佳的路径策略可以实现更好的重用效果，最终还是和程序本身的特点有关。 注： 黑体表示每个程序中最高的重用数目 程序 约束总数 BFS DFS Random Trityp 16 1 0 1 Tcas 99 72 63 69 ReverseWord 90 86 84 84 Multiplication 73 26 17 16 Wbs 13 823 13 788 13 783 13 793 Bintree 21 264 2 474 6 849 4 742 Treemap 10 841 8 765 8 511 8 461 AvlTree 19 674 9 283 10 178 14 466 HeapSort 2 382 16 14 1 534 MulKnapsack 7 129 0 0 3 907 RamerDouglas 239 85 85 114 注： 黑体表示每个程序中最高的重用数目 程序 约束总数 BFS DFS Random Trityp 16 1 0 1 Tcas 99 76 66 71 ReverseWord 90 86 84 82 Multiplication 73 28 19 19 Wbs 13 823 13 788 13 783 13 792 Bintree 21 264 2 387 7 157 4 800 Treemap 10 841 8 765 8 511 8 432 AvlTree 19 674 11 457 11 792 15 276 HeapSort 2 382 16 14 1 567 MulKnapsack 7 129 186 114 3 536 RamerDouglas 239 85 85 107 因此，每种重用技术的重用效果都会受到路径遍历策略的影响，但是每种重用技术使用哪种路径遍历策略能取得更好的重用效果取决于程序本身特点。 4　 结 语 1 本文对目前的约束求解结果重用技术做了比较，从理论上分析了各个重用技术的重用能力的差别，也通过实验评估了各种方法在重用率、重用效率方面的优势和限制，同时对影响重用效果的因素进行分析。本文的工作对约束求解结果重用领域的研究提供了综述和评估，可以为未来的研究提供借鉴。 约束求解结果重用技术作为提高符号执行效率的一种有效的手段，目前尚在起步阶段，已有的重用技术并不多，且对约束都是作为整体重用，但是实际问题中的约束存在复杂嵌套问题，整体重用很难解决这类问题。另外，当前的约束重用技术都只能支持线性整数约束以及无量词非线性浮点性约束，对于字符串约束以及其他更为复杂的约束类型，未来的重用技术可以展开研究，一方面可以作为约束求解的一种辅助方法，另一方面约束求解器求解此类约束问题耗时较长，实现这类约束的重用将会极大地提高符号执行中约束求解的效率。 参考文献 KING J C . Symbolic execution and program testing [J]. Communications of the ACM , 1976 , 19 ( 7 ): 385 - 394 . DOI: 10.1145/360248.360252 http://dx.doi.org/10.1145/360248.360252 . Symbolic execution and program testing BOUNIMOVA E , GODEFROID P , MOLNAR D . Billions and billions of constraints: Whitebox fuzz testing in production [C]// Proceedings of the 2013 International Conference on Software Engineering . Washington D C : IEEE , 2013 : 122 - 131 . DOI: 10.1109/ICSE.2013.6606558 http://dx.doi.org/10.1109/ICSE.2013.6606558 . Billions and billions of constraints: Whitebox fuzz testing in production CADAR C , SEN K . Symbolic execution for software testing: Three decades later [J]. Communications of the ACM , 2013 , 56 ( 2 ): 82 - 90 . DOI: 10.1145/2408776.2408795 http://dx.doi.org/10.1145/2408776.2408795 . Symbolic execution for software testing: Three decades later AVGERINOS T , REBERT A , CHA S K , et al . Enhancing symbolic execution with veritesting [C]// Proceedings of the 36th International Conference on Software Engineering . New York : ACM , 2014 : 1083 - 1094 . DOI: 10.1145/2568225.2568293 http://dx.doi.org/10.1145/2568225.2568293 . Enhancing symbolic execution with veritesting VISSER W , GELDENHUYS J , DWYER M B . Green: Reducing, reusing and recycling constraints in program analysis [C]// Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering . New York : ACM , 2012 : 58 . DOI: 10.1145/2393596.2393665 http://dx.doi.org/10.1145/2393596.2393665 . Green: Reducing, reusing and recycling constraints in program analysis YANG G W , PĂSĂREANU C S , KHURSHID S . Memoized symbolic execution [C]// Proceedings of the 2012 International Symposium on Software Testing and Analysis . New York : ACM , 2012 : 144 - 154 . DOI: 10.1145/2338965.2336771 http://dx.doi.org/10.1145/2338965.2336771 . Memoized symbolic execution CADAR C , DUNBAR D , ENGLER D R . KLEE: Unassisted and automatic generation of high⁃coverage tests for complex systems programs [C]// USENIX Symposium on Operating Systems Design and Implementation . Berkeley : USENIX Association , 2008 , 8 : 209 - 224 . KLEE: Unassisted and automatic generation of high⁃coverage tests for complex systems programs LIU T H , ARAÚJO M , D’AMORIM M , et al . A comparative study of incremental constraint solving approaches in symbolic execution [C]// Haifa Verification Conference(HVC 2014: Hardware and Software: Verification and Testing) . Cham ： Springer , 2014 : 284 - 299 . DOI: 10.1007/978-3-319-13338-6_21 http://dx.doi.org/10.1007/978-3-319-13338-6_21 . A comparative study of incremental constraint solving approaches in symbolic execution AQUINO A , BIANCHI F A , CHEN M , et al . Reusing constraint proofs in program analysis [C]// Proceedings of the 2015 International Symposium on Software Testing and Analysis . New York : ACM , 2015 : 305 - 315 . DOI: 10.1145/2610384.2631831 http://dx.doi.org/10.1145/2610384.2631831 . Reusing constraint proofs in program analysis JIA X Y , GHEZZI C , YING S . Enhancing reuse of constraint solutions to improve symbolic execution [C]// Proceedings of the 2015 International Symposium on Software Testing and Analysis . New York : ACM , 2015 : 177 - 187 . DOI: 10.1145/2771783.2771806 http://dx.doi.org/10.1145/2771783.2771806 . Enhancing reuse of constraint solutions to improve symbolic execution AQUINO A , DENARO G , PEZZÈ M . Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions [C]// Proceedings of the 39th International Conference on Software Engineering . Washington D C : IEEE , 2017 : 427 - 437 . DOI: 10.1109/ICSE.2017.46 http://dx.doi.org/10.1109/ICSE.2017.46 . Heuristically matching solution spaces of arithmetic formulas to efficiently reuse solutions LUCKOW K , DIMJAŠEVIĆ M , GIANNAKOPOULOU D , et al . jDart: A dynamic symbolic analysis framework [C]// International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Berlin : Springer , 2016 : 442 - 459 . jDart: A dynamic symbolic analysis framework Microsoft .Z 3 Theorem Prove [EB/OL].[ 2015-04-13 ]. https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 . Theorem Prove 10.14188/j.1671-8836.2018.0199 TP311.5 A 1671-8836（2020）03-0277-08 HU Xiaohui,YING Shi,ZHAO Xuebo, et al .Comparison of Constraint Solving Solutions Reuse Techniques in Symbolic Execution [J]. J Wuhan Univ （ Nat Sci Ed ）,2020,66(3):277-284. DOI: 10.14188/j.1671-8836.2018.0199 http://dx.doi.org/10.14188/j.1671-8836.2018.0199 (Ch). HU Xiaohui,YING Shi,ZHAO Xuebo,et al.Comparison of Constraint Solving Solutions Reuse Techniques in Symbolic Execution [J].J Wuhan Univ（Nat Sci Ed）,2020,66(3):277-284. DOI:10.14188/j.1671-8836.2018.0199(Ch). 胡小辉,应时,赵学博, 等.符号执行中约束求解结果重用技术的比较[J].武汉大学学报（理学版）,2020,66(3):277-284. DOI:10.14188/j.1671-8836.2020.03.010 胡小辉,应时,赵学博, 等.符号执行中约束求解结果重用技术的比较[J].武汉大学学报（理学版）,2020,66(3):277-284. DOI:10.14188/j.1671-8836.2020.03.010 国家重点研发计划项目（2016YFC1202204） 2018-09-16 2020-06-24 2020-09-30 武汉大学学报（理学版） 3 66