A sparse evaluation technique for detailed semantic analyses

Yoonseok Ko, Kihong Heo, Hakjoo Oh

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

We present a sparse evaluation technique that is effectively applicable to a set of elaborate semantic-based static analyses. Existing sparse evaluation techniques are effective only when the underlying analyses have comparably low precision. For example, if a pointer analysis precision is not affected by numeric statements like x:=1 then existing sparse evaluation techniques can remove the statement, but otherwise, the statement cannot be removed. Our technique, which is a fine-grained sparse evaluation technique, is effectively applicable even to elaborate analyses. A key insight of our technique is that, even though a statement is relevant to an analysis, it is typical that analyzing the statement involves only a tiny subset of its input abstract memory and the most are irrelevant. By exploiting this sparsity, our technique transforms the original analysis into a form that does not involve the fine-grained irrelevant semantic behaviors. We formalize our technique within the abstract interpretation framework. In experiments with a C static analyzer, our technique improved the analysis speed by on average 14x.

Original languageEnglish
Pages (from-to)99-111
Number of pages13
JournalComputer Languages, Systems and Structures
Volume40
Issue number3-4
DOIs
Publication statusPublished - 2014 Oct 1
Externally publishedYes

Fingerprint

Semantics
Data storage equipment
Experiments

Keywords

  • Abstract interpretation
  • Data-flow analysis
  • Sparse evaluation
  • Static analysis

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications

Cite this

A sparse evaluation technique for detailed semantic analyses. / Ko, Yoonseok; Heo, Kihong; Oh, Hakjoo.

In: Computer Languages, Systems and Structures, Vol. 40, No. 3-4, 01.10.2014, p. 99-111.

Research output: Contribution to journalArticle

@article{ade35d6ad1fd42cab3f5ca674ba84ddf,
title = "A sparse evaluation technique for detailed semantic analyses",
abstract = "We present a sparse evaluation technique that is effectively applicable to a set of elaborate semantic-based static analyses. Existing sparse evaluation techniques are effective only when the underlying analyses have comparably low precision. For example, if a pointer analysis precision is not affected by numeric statements like x:=1 then existing sparse evaluation techniques can remove the statement, but otherwise, the statement cannot be removed. Our technique, which is a fine-grained sparse evaluation technique, is effectively applicable even to elaborate analyses. A key insight of our technique is that, even though a statement is relevant to an analysis, it is typical that analyzing the statement involves only a tiny subset of its input abstract memory and the most are irrelevant. By exploiting this sparsity, our technique transforms the original analysis into a form that does not involve the fine-grained irrelevant semantic behaviors. We formalize our technique within the abstract interpretation framework. In experiments with a C static analyzer, our technique improved the analysis speed by on average 14x.",
keywords = "Abstract interpretation, Data-flow analysis, Sparse evaluation, Static analysis",
author = "Yoonseok Ko and Kihong Heo and Hakjoo Oh",
year = "2014",
month = "10",
day = "1",
doi = "10.1016/j.cl.2014.05.001",
language = "English",
volume = "40",
pages = "99--111",
journal = "Journal of Computer Languages",
issn = "2665-9182",
publisher = "Elsevier Ltd",
number = "3-4",

}

TY - JOUR

T1 - A sparse evaluation technique for detailed semantic analyses

AU - Ko, Yoonseok

AU - Heo, Kihong

AU - Oh, Hakjoo

PY - 2014/10/1

Y1 - 2014/10/1

N2 - We present a sparse evaluation technique that is effectively applicable to a set of elaborate semantic-based static analyses. Existing sparse evaluation techniques are effective only when the underlying analyses have comparably low precision. For example, if a pointer analysis precision is not affected by numeric statements like x:=1 then existing sparse evaluation techniques can remove the statement, but otherwise, the statement cannot be removed. Our technique, which is a fine-grained sparse evaluation technique, is effectively applicable even to elaborate analyses. A key insight of our technique is that, even though a statement is relevant to an analysis, it is typical that analyzing the statement involves only a tiny subset of its input abstract memory and the most are irrelevant. By exploiting this sparsity, our technique transforms the original analysis into a form that does not involve the fine-grained irrelevant semantic behaviors. We formalize our technique within the abstract interpretation framework. In experiments with a C static analyzer, our technique improved the analysis speed by on average 14x.

AB - We present a sparse evaluation technique that is effectively applicable to a set of elaborate semantic-based static analyses. Existing sparse evaluation techniques are effective only when the underlying analyses have comparably low precision. For example, if a pointer analysis precision is not affected by numeric statements like x:=1 then existing sparse evaluation techniques can remove the statement, but otherwise, the statement cannot be removed. Our technique, which is a fine-grained sparse evaluation technique, is effectively applicable even to elaborate analyses. A key insight of our technique is that, even though a statement is relevant to an analysis, it is typical that analyzing the statement involves only a tiny subset of its input abstract memory and the most are irrelevant. By exploiting this sparsity, our technique transforms the original analysis into a form that does not involve the fine-grained irrelevant semantic behaviors. We formalize our technique within the abstract interpretation framework. In experiments with a C static analyzer, our technique improved the analysis speed by on average 14x.

KW - Abstract interpretation

KW - Data-flow analysis

KW - Sparse evaluation

KW - Static analysis

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

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

U2 - 10.1016/j.cl.2014.05.001

DO - 10.1016/j.cl.2014.05.001

M3 - Article

VL - 40

SP - 99

EP - 111

JO - Journal of Computer Languages

JF - Journal of Computer Languages

SN - 2665-9182

IS - 3-4

ER -