|
| 摘要: |
| 基于约束的多面体抽象域的处理能力主要受限于其高代价的(强)接合操作，即两多面体的凸闭包计算。针对基于约束的多面体抽象域提出了一系列低代价的弱接合操作，以作为凸闭包计算的可靠替代候选。为了能够在分析效率和精度之间取得合理权衡，还提出了一种启发式策略，以把强、弱接合动态地、有机地结合起来进行程序分析。实验结果表明，弱接合能够极大地提升基于约束的多面体抽象域的效率、可扩展性和鲁棒性。 |
| 关键词: 静态分析 抽象解释 多面体抽象域 凸闭包 强接合 弱接合 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60725206, 60921062, 60803042, 90818024 (国家自然科学基金); the Hu’nan Provincial Natural Science Foundation of China under Grant No.07JJ1011 (湖南省自然科学基金) |
|
| Weak Join for the Constraint-Based Polyehdra Abstract Domain |
|
CHEN Li-Qian, WANG Ji, LIU Wan-Wei
|
| Abstract: |
| The main tractability problem of the constraint-based polyhedra abstract domain can be derived from the costly (strong) join operation, that is, the convex hull computation. This paper presents a series of cheap weak join operations as a sound substitution for the convex hull operation of the constraint-based polyhedra domain. To achieve a trade-off between efficiency and precision, a heuristic strategy is proposed which dynamically combines both strong join and weak join during program analysis. Experimental results show that the weak join operation can significantly improve the efficiency, scalability and robustness of the constraint-based polyhedra domain. |
| Key words: static analysis abstract interpretation polyhedra abstract domain convex hull strong join weak join |
