Integer Implementation And Efficiency Improvement For Polyhedron Abstract Domain

Software involves a lot of numeric variables, such as loop count,arraysubscript,and length of buffer. Ranges of the numeric variables are critical to thedetection of runtime error in the program (such as division by zero and arrayout-of-bounds).Abstract interpretation provides a general framework for value rangeanalysis, and abstract domains are a key ingredient in this framework. Different abstractdomains can be used to derive different numerical properties.Polyhedra abstract domainis one of the most powerful and commonly used abstract domains which can be used toderive linear invariant.The main problem of polyhedra abstract domain is the scalability.This is mainlycaused by two reasons. One is the high complexity of domain operations, and the otheris the rational implementations, which leads to high cost in computing and storage.In this paper, in order to improve the scalability, we firstly proposed a machineinteger implementation for polyhedron domain.The machine integer implementationeasily results to big coefficient problems, even interger overflow.To ensure thereliability,we proposed an algorithm to limit the coefficients in constraints.Furthermore,to improve the efficiency of analysis, we present some strategies to improve the coreoperations of polyhedra abstract domain. We proposed a method of using floating pointlinear programming instead of precise linear programming, simultaneously we study onhow to ensure its reliability. In order to solve the problem of increasing number ofpolyhedral constraints, which Fourier-Motzkin variable elimination method leads to, weproposed an algorithm, which leads to minimal loss of accuracy, to limit the number ofconstraints.Based on the above-mentioned, we realize the algorithm in the the open sourcenumerical abstract domain library APRON. The experimental results show that themethods, proposed in this paper, are possible to effectively improve the computationalefficiency of polyhedron abstract domain and are important for the enhancement of thescalability of polyhedron domain.