WCSE

Precision Adjustment Strategies Based on Constraint Simplification in Polyhedra Abstract Domain

Abstract— Some precision adjustment strategies based on constraint simplification are introduced to find a trade-off between precision and its cost in program analysis. In program analysis built on numerical abstract domains, a constraint (such as Linear Inequation in Polyhedra abstract domain) implies the relationships between program variables. The main idea of precision adjustment strategies in this paper is simplifying the constraints in some pivotal program locations before these constraints are fed to abstract transfer functions. The strategy at Function Start Location(FSL) replaces expressions with constraints related to their ranges. The strategy at Loop Start Location(LSL) simplifies constraints' coefficients through combining several analogous constraints to a typical constraint. The strategy at Ordinary Location(OL) decreases the quantities of variables in constraints by replacing these variables with their ranges. Our framework is implemented on the top of Apron which is dependent on Convex Polyhedra and Linear Equalities library (POLKA). According to a series of experiments on different programs, we demonstrate that the application of precision adjustment strategies can improve the efficiency of program analysis.

Index Terms— program analysis, abstract domain, abstract interpretation, precision adjustment

Xiang Chen, Min Zhou, Ming Gu
Tsinghua University, CHINA

[Download]

Cite: Xiang Chen, Min Zhou, Ming Gu, "Precision Adjustment Strategies Based on Constraint Simplification in Polyhedra Abstract Domain," Proceedings of 2017 the 7th International Workshop on Computer Science and Engineering, pp. 195-203, Beijing, 25-27 June, 2017.