Access-based abstract memory localization in static analysis

Hakjoo Oh, Kwangkeun Yi

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called "abstract garbage collection" or "framing". In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable part. Our technique first estimates, by an efficient pre-analysis, which parts of input states will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure's body and reduces the average analysis time and memory by 92.1% and 71.2%, respectively, without sacrificing the analysis precision. In addition, we present three extensions of access-based localization: (1) we generalize the idea and apply the localization more frequently such as at loop bodies and basic blocks as well as procedure bodies, additionally reducing analysis time by an average of 31.8%; (2) we present a technique to mitigate a performance problem of localization in handling recursive procedures, and show that this extension improves the average analysis time by 42%; (3) we show how to incorporate the access-based localization into relational numeric analyses.

Original languageEnglish
Pages (from-to)1701-1727
Number of pages27
JournalScience of Computer Programming
Volume78
Issue number9
DOIs
Publication statusPublished - 2013 Sep 1
Externally publishedYes

Fingerprint

Static analysis
Data storage equipment
Block codes
Experiments

Keywords

  • Abstract interpretation
  • Localization
  • Static analysis

ASJC Scopus subject areas

  • Software

Cite this

Access-based abstract memory localization in static analysis. / Oh, Hakjoo; Yi, Kwangkeun.

In: Science of Computer Programming, Vol. 78, No. 9, 01.09.2013, p. 1701-1727.

Research output: Contribution to journalArticle

@article{731f5ec24fab4390a5b49c368beb1fa1,
title = "Access-based abstract memory localization in static analysis",
abstract = "On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called {"}abstract garbage collection{"} or {"}framing{"}. In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable part. Our technique first estimates, by an efficient pre-analysis, which parts of input states will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure's body and reduces the average analysis time and memory by 92.1{\%} and 71.2{\%}, respectively, without sacrificing the analysis precision. In addition, we present three extensions of access-based localization: (1) we generalize the idea and apply the localization more frequently such as at loop bodies and basic blocks as well as procedure bodies, additionally reducing analysis time by an average of 31.8{\%}; (2) we present a technique to mitigate a performance problem of localization in handling recursive procedures, and show that this extension improves the average analysis time by 42{\%}; (3) we show how to incorporate the access-based localization into relational numeric analyses.",
keywords = "Abstract interpretation, Localization, Static analysis",
author = "Hakjoo Oh and Kwangkeun Yi",
year = "2013",
month = "9",
day = "1",
doi = "10.1016/j.scico.2013.04.002",
language = "English",
volume = "78",
pages = "1701--1727",
journal = "Science of Computer Programming",
issn = "0167-6423",
publisher = "Elsevier",
number = "9",

}

TY - JOUR

T1 - Access-based abstract memory localization in static analysis

AU - Oh, Hakjoo

AU - Yi, Kwangkeun

PY - 2013/9/1

Y1 - 2013/9/1

N2 - On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called "abstract garbage collection" or "framing". In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable part. Our technique first estimates, by an efficient pre-analysis, which parts of input states will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure's body and reduces the average analysis time and memory by 92.1% and 71.2%, respectively, without sacrificing the analysis precision. In addition, we present three extensions of access-based localization: (1) we generalize the idea and apply the localization more frequently such as at loop bodies and basic blocks as well as procedure bodies, additionally reducing analysis time by an average of 31.8%; (2) we present a technique to mitigate a performance problem of localization in handling recursive procedures, and show that this extension improves the average analysis time by 42%; (3) we show how to incorporate the access-based localization into relational numeric analyses.

AB - On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called "abstract garbage collection" or "framing". In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable part. Our technique first estimates, by an efficient pre-analysis, which parts of input states will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure's body and reduces the average analysis time and memory by 92.1% and 71.2%, respectively, without sacrificing the analysis precision. In addition, we present three extensions of access-based localization: (1) we generalize the idea and apply the localization more frequently such as at loop bodies and basic blocks as well as procedure bodies, additionally reducing analysis time by an average of 31.8%; (2) we present a technique to mitigate a performance problem of localization in handling recursive procedures, and show that this extension improves the average analysis time by 42%; (3) we show how to incorporate the access-based localization into relational numeric analyses.

KW - Abstract interpretation

KW - Localization

KW - Static analysis

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

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

U2 - 10.1016/j.scico.2013.04.002

DO - 10.1016/j.scico.2013.04.002

M3 - Article

AN - SCOPUS:84878828244

VL - 78

SP - 1701

EP - 1727

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

IS - 9

ER -