• Login
    View Item 
    •   MINDS@UW Home
    • MINDS@UW Madison
    • College of Letters and Science, University of Wisconsin–Madison
    • Department of Computer Sciences, UW-Madison
    • CS Technical Reports
    • View Item
    •   MINDS@UW Home
    • MINDS@UW Madison
    • College of Letters and Science, University of Wisconsin–Madison
    • Department of Computer Sciences, UW-Madison
    • CS Technical Reports
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Abstract Domains of Affine Relations

    Thumbnail
    File(s)
    Technical Report (1.044Mb)
    Date
    2013-05-13
    Author
    Elder, Matt
    Lim, Junghee
    Sharma, Tushar
    Anderson, Tycho
    Reps, Thomas
    Publisher
    University of Wisconsin-Madison Department of Computer Sciences
    Metadata
    Show full item record
    Abstract
    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/65531
    Citation
    TR1792-R1 (revised Feb. 10, 2014)
    Part of
    • CS Technical Reports

    Contact Us | Send Feedback
     

     

    Browse

    All of MINDS@UWCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    LoginRegister

    Contact Us | Send Feedback