Design and implementation of sparse global analyses for C-like languages

Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, Kwangkeun Yi

Research output: Contribution to journalArticle

12 Citations (Scopus)

Abstract

In this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the abstract interpretation framework to support relational as well as non-relational semantics properties for C-like languages. We first use the abstract interpretation framework to have a global static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, we add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our framework determines what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework; we present that existing sparse analyses are all restricted instances of our framework; we show more semantically elaborate design examples of sparse nonrelational and relational static analyses; we present their implementation results that scale to analyze up to one million lines of C programs. We also show a set of implementation techniques that turn out to be critical to economically support the sparse analysis process.

Original languageEnglish
Pages (from-to)229-238
Number of pages10
JournalACM SIGPLAN Notices
Volume47
Issue number6
DOIs
Publication statusPublished - 2012 Aug 1
Externally publishedYes

Fingerprint

Scalability
Acoustic waves
Semantics

Keywords

  • Abstract interpretation
  • Sparse analysis
  • Static analysis

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Design and implementation of sparse global analyses for C-like languages. / Oh, Hakjoo; Heo, Kihong; Lee, Wonchan; Lee, Woosuk; Yi, Kwangkeun.

In: ACM SIGPLAN Notices, Vol. 47, No. 6, 01.08.2012, p. 229-238.

Research output: Contribution to journalArticle

Oh, Hakjoo ; Heo, Kihong ; Lee, Wonchan ; Lee, Woosuk ; Yi, Kwangkeun. / Design and implementation of sparse global analyses for C-like languages. In: ACM SIGPLAN Notices. 2012 ; Vol. 47, No. 6. pp. 229-238.
@article{fca5d8800de84ff7b57ddfc37fc0d89b,
title = "Design and implementation of sparse global analyses for C-like languages",
abstract = "In this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the abstract interpretation framework to support relational as well as non-relational semantics properties for C-like languages. We first use the abstract interpretation framework to have a global static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, we add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our framework determines what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework; we present that existing sparse analyses are all restricted instances of our framework; we show more semantically elaborate design examples of sparse nonrelational and relational static analyses; we present their implementation results that scale to analyze up to one million lines of C programs. We also show a set of implementation techniques that turn out to be critical to economically support the sparse analysis process.",
keywords = "Abstract interpretation, Sparse analysis, Static analysis",
author = "Hakjoo Oh and Kihong Heo and Wonchan Lee and Woosuk Lee and Kwangkeun Yi",
year = "2012",
month = "8",
day = "1",
doi = "10.1145/2345156.2254092",
language = "English",
volume = "47",
pages = "229--238",
journal = "ACM SIGPLAN Notices",
issn = "1523-2867",
publisher = "Association for Computing Machinery (ACM)",
number = "6",

}

TY - JOUR

T1 - Design and implementation of sparse global analyses for C-like languages

AU - Oh, Hakjoo

AU - Heo, Kihong

AU - Lee, Wonchan

AU - Lee, Woosuk

AU - Yi, Kwangkeun

PY - 2012/8/1

Y1 - 2012/8/1

N2 - In this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the abstract interpretation framework to support relational as well as non-relational semantics properties for C-like languages. We first use the abstract interpretation framework to have a global static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, we add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our framework determines what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework; we present that existing sparse analyses are all restricted instances of our framework; we show more semantically elaborate design examples of sparse nonrelational and relational static analyses; we present their implementation results that scale to analyze up to one million lines of C programs. We also show a set of implementation techniques that turn out to be critical to economically support the sparse analysis process.

AB - In this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the abstract interpretation framework to support relational as well as non-relational semantics properties for C-like languages. We first use the abstract interpretation framework to have a global static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, we add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our framework determines what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework; we present that existing sparse analyses are all restricted instances of our framework; we show more semantically elaborate design examples of sparse nonrelational and relational static analyses; we present their implementation results that scale to analyze up to one million lines of C programs. We also show a set of implementation techniques that turn out to be critical to economically support the sparse analysis process.

KW - Abstract interpretation

KW - Sparse analysis

KW - Static analysis

UR - http://www.scopus.com/inward/record.url?scp=84866430641&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84866430641&partnerID=8YFLogxK

U2 - 10.1145/2345156.2254092

DO - 10.1145/2345156.2254092

M3 - Article

AN - SCOPUS:84866430641

VL - 47

SP - 229

EP - 238

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

SN - 1523-2867

IS - 6

ER -