Signedness-agnostic program analysis: Precise integer bounds for low-level code

Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

18 Citations (Scopus)

Abstract

Many compilers target common back-ends, thereby avoiding the need to implement the same analyses for many different source languages. This has led to interest in static analysis of LLVM code. In LLVM (and similar languages) most signedness information associated with variables has been compiled away. Current analyses of LLVM code tend to assume that either all values are signed or all are unsigned (except where the code specifies the signedness). We show how program analysis can simultaneously consider each bit-string to be both signed and unsigned, thus improving precision, and we implement the idea for the specific case of integer bounds analysis. Experimental evaluation shows that this provides higher precision at little extra cost. Our approach turns out to be beneficial even when all signedness information is available, such as when analysing C or Java code.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 10th Asian Symposium, APLAS 2012, Proceedings
PublisherSpringer
Pages115-130
Number of pages16
ISBN (Print)9783642351815
DOIs
Publication statusPublished - 1 Dec 2012
Externally publishedYes
EventAsian Symposium on Programming Languages and Systems 2012 - Kyoto, Japan
Duration: 11 Dec 201213 Dec 2012
Conference number: 10th
https://link.springer.com/book/10.1007/978-3-642-35182-2 (Proceedings)

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7705 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceAsian Symposium on Programming Languages and Systems 2012
Abbreviated titleAPLAS 2012
Country/TerritoryJapan
CityKyoto
Period11/12/1213/12/12
Internet address

Cite this