Static analysis of linear absolute value equalities among variables of a program

The classic linear (technically, affine) equality abstract domain, which can infer linear equality relations among variables of a program automatically, is one of the earliest and fundamental abstract domains. However, it cannot express non-convex properties that appear naturally due to the inherent disjunctive behaviors in programs. In this paper, we introduce a new abstract domain, namely the abstract domain of linear absolute value equalities (AVE), which generalizes the linear equality abstract domain with absolute value terms of variables. More clearly, we leverage the absolute value function to design the new abstract domain for discovering linear equality relations among values and absolute values of program variables. Moreover, since linear absolute value equalities can only express limited form of inequalities while programs often involve various inequalities, to help the AVE domain, we propose a so-called signed interval abstract domain as an extension of the classic interval abstract domain. The key idea is to use two intervals to track respectively the positive part and the negative part of the interval range for each variable. On this basis, we propose to combine the two new abstract domains to improve precision of each other during analysis. Experimental results are encouraging: In practice, the AVE abstract domain (together with the signed interval abstract domain) can find interesting piece-wise linear invariants that are non-convex and out of the expressiveness of the linear equality domain.