TY - JOUR
T1 - A sparse evaluation technique for detailed semantic analyses
AU - Ko, Yoonseok
AU - Heo, Kihong
AU - Oh, Hakjoo
N1 - Funding Information:
This work was supported by the Engineering Research Center of Excellence Program of Korea Ministry of Science, ICT & Future Planning (MSIP)/National Research Foundation of Korea (NRF) (Grant NRF-2008-0062609 ).
Publisher Copyright:
© 2014 Elsevier Ltd. All rights reserved.
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
U2 - 10.1016/j.cl.2014.05.001
DO - 10.1016/j.cl.2014.05.001
M3 - Article
AN - SCOPUS:84912150052
SN - 2665-9182
VL - 40
SP - 99
EP - 111
JO - Journal of Computer Languages
JF - Journal of Computer Languages
IS - 3-4
ER -