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 2^w, 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 v_KS to an over-approximating MOS element v_MOS—i.e., γ(v_KS) ⊆ γ(v_MOS)—as well as an algorithm to convert an MOS element w_MOS to an over-approximating KS element w_KS—i.e., γ(w_MOS) ⊆ γ(w_KS).

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

• We describe how to perform a greedy, operator-by-operator abstraction method to obtain KS abstract transformers.
• We also describe a more global approach to obtaining KS abstract transformers that considers the semantics of an entire instruction, basic block or other loop-free program fragment.