Constraint normalization and parameterized caching for quantitative program analysis
Constraint normalization and parameterized caching for quantitative program analysis
复制标题
用于定量程序分析的约束归一化和参数化缓存
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
T. Bultan
中科院分区：
文献类型：
--
作者：
Tegan Brennan;Nestan Tsiskaridze;Nicolás Rosner;Abdulbaki Aydin;T. Bultan
符号程序分析技术依赖于可满足性检查约束求解器，而定量程序分析技术依赖于模型计数约束求解器。因此，可满足性检查和模型计数的效率对于现代程序分析技术的效率至关重要。在本文中，我们提出了一个约束缓存框架，以加快潜在的昂贵的可满足性和模型计数查询。这个框架的组成部分是我们新的约束规范化过程下，约束的解决方案集的基数，但不一定是解决方案集本身，被保存。我们将这些约束规范化技术扩展到字符串约束，以支持字符串操作代码的分析。一组理论的框架，概括了早期的结果约束规范化是用来表达我们的规范化技术。我们还提出了一个参数化的缓存方法，除了存储模型计数查询的结果，我们还存储一个模型计数器对象中的约束存储，使我们能够有效地重新计算满足不同的最大边界模型的数量。我们实现我们的缓存框架在我们的工具腰果，这是建立作为一个扩展的绿色缓存框架，并将其与符号执行工具符号路径（SPF）和模型计数约束求解器ABC。我们的实验表明，约束缓存可以显着提高性能的符号和定量程序分析。例如，Cashew可以将SMC/Kaluza基准测试中的10，104个唯一约束标准化为394个标准形式，在SMC/Kaluza-Big数据集上实现10倍的加速，在我们基于SPF的侧通道分析实验中实现平均3倍的加速。
Symbolic program analysis techniques rely on satisfiability-checking constraint solvers, while quantitative program analysis techniques rely on model-counting constraint solvers. Hence, the efficiency of satisfiability checking and model counting is crucial for efficiency of modern program analysis techniques. In this paper, we present a constraint caching framework to expedite potentially expensive satisfiability and model-counting queries. Integral to this framework is our new constraint normalization procedure under which the cardinality of the solution set of a constraint, but not necessarily the solution set itself, is preserved. We extend these constraint normalization techniques to string constraints in order to support analysis of string-manipulating code. A group-theoretic framework which generalizes earlier results on constraint normalization is used to express our normalization techniques. We also present a parameterized caching approach where, in addition to storing the result of a model-counting query, we also store a model-counter object in the constraint store that allows us to efficiently recount the number of satisfying models for different maximum bounds. We implement our caching framework in our tool Cashew, which is built as an extension of the Green caching framework, and integrate it with the symbolic execution tool Symbolic PathFinder (SPF) and the model-counting constraint solver ABC. Our experiments show that constraint caching can significantly improve the performance of symbolic and quantitative program analyses. For instance, Cashew can normalize the 10,104 unique constraints in the SMC/Kaluza benchmark down to 394 normal forms, achieve a 10x speedup on the SMC/Kaluza-Big dataset, and an average 3x speedup in our SPF-based side-channel analysis experiments.
影响因子：
1.2
作者：
Clark, David;Hunt, Sebastian;Malacaria, Pasquale
通讯作者：
Malacaria, Pasquale
DOI：
10.1145/1920261.1920300
发表时间：
2010-12
期刊：
--
影响因子：
--
作者：
J. Heusser;P. Malacaria
通讯作者：
J. Heusser;P. Malacaria
DOI：
10.1145/2382756.2382791
发表时间：
2012
期刊：
ACM SIGSOFT Software Engineering Notes
影响因子：
--
作者：
Phan Q
通讯作者：
Phan Q