A symbolic analysis framework for static analysis of imperative programming languages

Bernd Burgstaller, Bernhard Scholz, Johann Blieberger

Research output: Contribution to journalArticle

5 Citations (Scopus)

Abstract

We present a generic symbolic analysis framework for imperative programming languages. Our framework is capable of computing all valid variable bindings of a program at given program points. This information is invaluable for domain-specific static program analyses such as memory leak detection, program parallelization, and the detection of superfluous bound checks, variable aliases and task deadlocks. We employ path expression algebra to model the control flow information of programs. A homomorphism maps path expressions into the symbolic domain. At the center of the symbolic domain is a compact algebraic structure called supercontext. A supercontext contains the complete control and data flow analysis information valid at a given program point. Our approach to compute supercontexts is based purely on algebra and is fully automated. This novel representation of program semantics closes the gap between program analysis and computer algebra systems, which makes supercontexts an ideal symbolic intermediate representation for all domain-specific static program analyses. Our approach is more general than existing methods because it can derive solutions for arbitrary (even intra-loop and nested loop) nodes of reducible and irreducible control flow graphs. We prove the correctness of our symbolic analysis method. Our experimental results show that the problem sizes arising from real-world applications such as the SPEC95 benchmark suite are tractable for our symbolic analysis framework.

Original languageEnglish
Pages (from-to)1418-1439
Number of pages22
JournalJournal of Systems and Software
Volume85
Issue number6
DOIs
Publication statusPublished - 2012 Jun 1

Fingerprint

Static analysis
Computer programming languages
Algebra
Data flow analysis
Flow graphs
Leak detection
Flow control
Computer systems
Semantics
Data storage equipment

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Hardware and Architecture

Cite this

@article{126fc0fe598344f8beee5eb9a513ad84,
title = "A symbolic analysis framework for static analysis of imperative programming languages",
abstract = "We present a generic symbolic analysis framework for imperative programming languages. Our framework is capable of computing all valid variable bindings of a program at given program points. This information is invaluable for domain-specific static program analyses such as memory leak detection, program parallelization, and the detection of superfluous bound checks, variable aliases and task deadlocks. We employ path expression algebra to model the control flow information of programs. A homomorphism maps path expressions into the symbolic domain. At the center of the symbolic domain is a compact algebraic structure called supercontext. A supercontext contains the complete control and data flow analysis information valid at a given program point. Our approach to compute supercontexts is based purely on algebra and is fully automated. This novel representation of program semantics closes the gap between program analysis and computer algebra systems, which makes supercontexts an ideal symbolic intermediate representation for all domain-specific static program analyses. Our approach is more general than existing methods because it can derive solutions for arbitrary (even intra-loop and nested loop) nodes of reducible and irreducible control flow graphs. We prove the correctness of our symbolic analysis method. Our experimental results show that the problem sizes arising from real-world applications such as the SPEC95 benchmark suite are tractable for our symbolic analysis framework.",
author = "Bernd Burgstaller and Bernhard Scholz and Johann Blieberger",
year = "2012",
month = "6",
day = "1",
doi = "10.1016/j.jss.2011.11.1039",
language = "English",
volume = "85",
pages = "1418--1439",
journal = "Journal of Systems and Software",
issn = "0164-1212",
publisher = "Elsevier Inc.",
number = "6",

}

A symbolic analysis framework for static analysis of imperative programming languages. / Burgstaller, Bernd; Scholz, Bernhard; Blieberger, Johann.

In: Journal of Systems and Software, Vol. 85, No. 6, 01.06.2012, p. 1418-1439.

Research output: Contribution to journalArticle

TY - JOUR

T1 - A symbolic analysis framework for static analysis of imperative programming languages

AU - Burgstaller, Bernd

AU - Scholz, Bernhard

AU - Blieberger, Johann

PY - 2012/6/1

Y1 - 2012/6/1

N2 - We present a generic symbolic analysis framework for imperative programming languages. Our framework is capable of computing all valid variable bindings of a program at given program points. This information is invaluable for domain-specific static program analyses such as memory leak detection, program parallelization, and the detection of superfluous bound checks, variable aliases and task deadlocks. We employ path expression algebra to model the control flow information of programs. A homomorphism maps path expressions into the symbolic domain. At the center of the symbolic domain is a compact algebraic structure called supercontext. A supercontext contains the complete control and data flow analysis information valid at a given program point. Our approach to compute supercontexts is based purely on algebra and is fully automated. This novel representation of program semantics closes the gap between program analysis and computer algebra systems, which makes supercontexts an ideal symbolic intermediate representation for all domain-specific static program analyses. Our approach is more general than existing methods because it can derive solutions for arbitrary (even intra-loop and nested loop) nodes of reducible and irreducible control flow graphs. We prove the correctness of our symbolic analysis method. Our experimental results show that the problem sizes arising from real-world applications such as the SPEC95 benchmark suite are tractable for our symbolic analysis framework.

AB - We present a generic symbolic analysis framework for imperative programming languages. Our framework is capable of computing all valid variable bindings of a program at given program points. This information is invaluable for domain-specific static program analyses such as memory leak detection, program parallelization, and the detection of superfluous bound checks, variable aliases and task deadlocks. We employ path expression algebra to model the control flow information of programs. A homomorphism maps path expressions into the symbolic domain. At the center of the symbolic domain is a compact algebraic structure called supercontext. A supercontext contains the complete control and data flow analysis information valid at a given program point. Our approach to compute supercontexts is based purely on algebra and is fully automated. This novel representation of program semantics closes the gap between program analysis and computer algebra systems, which makes supercontexts an ideal symbolic intermediate representation for all domain-specific static program analyses. Our approach is more general than existing methods because it can derive solutions for arbitrary (even intra-loop and nested loop) nodes of reducible and irreducible control flow graphs. We prove the correctness of our symbolic analysis method. Our experimental results show that the problem sizes arising from real-world applications such as the SPEC95 benchmark suite are tractable for our symbolic analysis framework.

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

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

U2 - 10.1016/j.jss.2011.11.1039

DO - 10.1016/j.jss.2011.11.1039

M3 - Article

AN - SCOPUS:84859532705

VL - 85

SP - 1418

EP - 1439

JO - Journal of Systems and Software

JF - Journal of Systems and Software

SN - 0164-1212

IS - 6

ER -