Weakly Relational Absolute Value Numerical Abstract Domain

Numerical properties are among the most important attributes of programs, for thereason that they can help us find program runtime error (such as division by zero,arithmetic overflow, etc.), and provide foundations for some non-numerical analysis(such as alias analysis, shape analysis, etc.). In the field of numerical analysis,non-convex properties are still difficult to be extracted even many efforts have beenspent on it.Abstract interpretation is one of the main techniques to extract numericalproperties of programs. However, weak relational numerical abstract domains cannotdescribe non-convex numerical properties of programs, and some relational abstractdomains which can describe non-convex properties have exponential time complexityand are not applicable in large-scale systems. In this paper, we propose a weak relationalabsolute value numerical abstract domain. It can describe non-convex properties ofprograms and has polynomial time complexity, which makes it more applicable in largeprograms.In this paper, we add absolute value to the octagon abstract domain to construct ourweak relational absolute value numerical abstract domain. We present the representationof the new domain and three normalization algorithms with different accuracy and timeconsumption. Complete operators related to this abstract domain were also designed,which include abstract union, widening/narrowing operator, etc. And all algorithmshave been implemented in APRON.With Interproc as front-end, APRON as abstract domain library, Fixpoint as fixedpoint solver, a Spl-oriented experimental platform has been built successfully. We alsodiscuss the criterion (fairness, transparency, diversity, etc.) to select benchmark,according to which12test cases were selected. On our experimental platform，thedifference of accuracy and time consumption between three normalization algorithms,between our weak relational absolute value numerical domain and octagon domain,between our domain and AVI domain were obtained on the12test cases. Experimentalresults show that our weak relational absolute value numerical domain can describenon-convex numerical properties, and strike a good balance on the accuracy and timeconsumption which makes it significant in theory and application.