ISBN: 978-981-11-3671-9 DOI: 10.18178/wcse.2017.06.034
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
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.