Abstract Domains of Affine Relations

Matt Elder, Junghee Lim, Tushar Sharma, Tycho Andersen, and Thomas Reps
University of Wisconsin

This paper considers some known abstract domains for affine-relation analysis, along with several variants, and studies how they relate to each other. The various domains represent sets of points that satisfy affine relations over variables that hold machine integers, and are based on an extension of linear algebra to modules over a ring (in particular, arithmetic performed modulo 2w, for some machine-integer width w).

We show that the abstract domains of Müller-Olm/Seidl (MOS) and King/Søndergaard (KS) are, in general, incomparable. However, we give sound interconversion methods. That is, we give an algorithm to convert a KS element vKS to an over-approximating MOS element vMOS—i.e., γ(vKS) ⊆ γ(vMOS)—as well as an algorithm to convert an MOS element wMOS to an over-approximating KS element wKS—i.e., γ(wMOS) ⊆ γ(wKS).

The paper provides insight on the range of options that one has for performing affine-relation analysis in a program analyzer.

The latter method can yield best abstract transformers, and hence can be more precise than the former method. However, the latter method is more expensive.

We also explain how to use the KS domain for interprocedural program analysis using a bit-precise concrete semantics, but without bit-blasting.

(Click here to access the paper: PDF.)