Abstract Domains of Affine Relations

File(s)
Date
2013-05-13Author
Elder, Matt
Lim, Junghee
Sharma, Tushar
Anderson, Tycho
Reps, Thomas
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Metadata
Show full item recordAbstract
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 Mueller-Olm/Seidl (MOS) and
King/Sondergaard (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., gamma(v_KS) subseteq gamma(v_MOS) -- as well as an algorithm
to convert an MOS element w_MOS to an over-approximating KS element
w_KS -- i.e., gamma(w_MOS) subseteq gamma(w_KS).
The paper provides insight on the range of options that one has for
performing affine-relation analysis in a program analyzer.
o We describe how to perform a greedy, operator-by-operator
abstraction method to obtain KS abstract transformers.
o 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.
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.
Subject
Howell form
modular arithmetic
symbolic abstraction
ane relation
abstract interpretation
abstract domain
static analysis
Permanent Link
http://digital.library.wisc.edu/1793/65531Type
Technical Report
Citation
TR1792-R1 (revised Feb. 10, 2014)