Circular Linear Progressions in SWEET
2014 (English)Report (Other academic)
The SWEET tool offers numerous static program analyses based on abstract interpretation, such as value analyses and a variety of flow analyses. For a long time, the main abstract domain used in SWEET to represent sets of concrete integers has been an interval domain that can model the wraparound behavior of fixed-precision arithmetic. Although this domain is made attractive by its simplicity, it cannot abstract sparse value sets with sufficient precision. Sparse value sets in which the elements are separated by a constant stride commonly occur, e.g., when analyzing array accesses to derive the possible byte offsets into the array. To improve the accuracy of SWEET's analyses in such situations, we extended SWEET with a variant of Sen and Srikant's domain of Circular Linear Progressions, which keeps stride information together with the interval bounds. This report describes our implementation, in which we improved the expressiveness of the original domain by lifting some restrictions on the parameters defining the objects of the domain.
Place, publisher, year, edition, pages
Västerås, Sweden: Mälardalen Real-Time Research Centre, Mälardalen University , 2014.
MRTC Reports, ISSN 1404-3041
Computer and Information Science
IdentifiersURN: urn:nbn:se:mdh:diva-33733ISRN: MDH-MRTC-297/2014-1-SEOAI: oai:DiVA.org:mdh-33733DiVA: diva2:1048494
ProjectsAPARTS - Advanced Program Analysis for Real-Time Systems