eelco-visser-compiler-const.../lecture/16.html

934 lines
16 KiB
HTML

<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<meta name="description" content="">
<meta name="author" content="Eelco Visser">
<meta name="generator" content="Jekyll v3.8.5">
<title>Lecture 16: Data-Flow Analysis</title>
<!-- <base href="/2021"> -->
<!--link rel="canonical" href="https://getbootstrap.com/docs/4.3/examples/starter-template/"-->
<link rel="icon" href="../img/logo/pl_ico2_2B3_icon.ico" type="image/x-icon">
<!-- Bootstrap core CSS -->
<!--link href="https://getbootstrap.com/docs/4.3/dist/css/bootstrap.min.css" rel="stylesheet" integrity="sha384-ggOyR0iXCbMQv3Xipma34MD+dH/1fQ784/j6cY/iJTQUOhcWr7x9JvoRxT2MZw1T" crossorigin="anonymous"-->
<link rel="stylesheet" href="https://stackpath.bootstrapcdn.com/bootstrap/4.3.1/css/bootstrap.min.css" integrity="sha384-ggOyR0iXCbMQv3Xipma34MD+dH/1fQ784/j6cY/iJTQUOhcWr7x9JvoRxT2MZw1T" crossorigin="anonymous">
<style>
.bd-placeholder-img {
font-size: 1.125rem;
text-anchor: middle;
-webkit-user-select: none;
-moz-user-select: none;
-ms-user-select: none;
user-select: none;
}
@media (min-width: 768px) {
.bd-placeholder-img-lg {
font-size: 3.5rem;
}
}
</style>
<!-- Custom styles for this template -->
<link href="../css/main.css" rel="stylesheet">
<link href="../css/borders-responsive.css" rel="stylesheet">
<link rel="stylesheet" href="../css/pl.css">
</head>
<body>
<nav class="navbar navbar-expand-md navbar-dark bg-dark fixed-top">
<a class="navbar-brand" href="../index.html">
TU Delft | CS4200
</a>
<button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarsExampleDefault" aria-controls="navbarsExampleDefault" aria-expanded="false" aria-label="Toggle navigation">
<span class="navbar-toggler-icon"></span>
</button>
<div class="collapse navbar-collapse" id="navbarsExampleDefault">
<ul class="navbar-nav mr-auto">
<li class="nav-item active">
<a class="nav-link" href="../lectures/index.html" tabindex="-1" aria-disabled="true">Lectures</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../homework/index.html" tabindex="-1" aria-disabled="true">Homework</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../project/index.html" tabindex="-1" aria-disabled="true">Project</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../news/index.html" tabindex="-1" aria-disabled="true">News</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../blog/index.html" tabindex="-1" aria-disabled="true">Blog</a>
</li>
</ul>
</div>
</nav>
<div class="container">
<div class="row">
<div class="col-sm-12 col-md-12 col-lg-12 col-xl-12">
<a href="../lectures/2021/16-data-flow-analysis/CS4200-2021-16-data-flow-analysis.pdf">
<img class="border border-dark" width="100%" src="../lectures/2021/16-data-flow-analysis/CS4200-2021-16-data-flow-analysis/CS4200-2021-16-data-flow-analysis.031.png"/>
</a>
<div class="mt-3 mb-3 pt-3 pb-3 text-dark border-top border-bottom border-grey">
<div class="text-dark font-weight-bold">
<h1>
Lecture 16: Data-Flow Analysis
</h1>
</div>
<div>
Eelco Visser
</div>
<div>
Lecture
| <a class="text-primary" href="../lectures/2021/16-data-flow-analysis/CS4200-2021-16-data-flow-analysis.pdf">PDF</a>
</div>
<div>
December 23, 2021
</div>
</div>
</div>
</div>
<div class="row">
<div class="col-sm-12 col-md-12 col-lg-9 border-lg-right border-grey">
<p>In this lecture we study data-flow analysis and the mathmetical framework of monotone frameworks, a foundation for the definition of data-flow analyses.</p>
<p>We also introduce the FlowSpec language for declarative definition of intra-procedural, flow-sensitive data-flow analyses.
FlowSpec provides rules for mapping an AST to a control-flow graph and for defining the transfer functions associated with nodes in the graph.</p>
<h3 id="references">References</h3>
<ul class="list-group list-group-flush pb-3">
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-info pl-3">
<div>
<a name="MoellerS20"></a>
<a class="font-weight-bold text-dark" target="_blank" href="https://cs.au.dk/~amoeller/spa/">Static Program Analysis</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://researchr.org/alias/anders-m%C3%B8ller">Anders Møller</a>, <a class="text-secondary" href="http://www.brics.dk/~mis/">Michael I. Schwartzbach</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
[<a class="text-secondary" href="https://cs.au.dk/~amoeller/spa/" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/MoellerS20/bibtex">bib</a>, <a href="https://researchr.org/publication/MoellerS20" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="16.html#AbstractMoellerS20" role="button" aria-expanded="false" aria-controls="AbstractMoellerS20"">abstract</a>]
<!-- MoellerS20 -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractMoellerS20">
<div class="">
Static program analysis is the art of reasoning about the behavior of computer programs without actually running them. This is useful not only in optimizing compilers for producing efficient code but also for automatic error detection and other tools that can help programmers. As known from Turing and Rice, all interesting properties of the behavior of programs written in common programming languages are mathematically undecidable. This means that automated reasoning of software generally must involve approximation. It is also well known that testing may reveal errors but not show their absence. In contrast, static program analysis can - with the right kind of approximations - check all possible executions of the programs and provide guarantees about their properties. The challenge when developing such analyses is how to ensure high precision and efficiency to be practically useful. This teaching material concisely presents the essential principles and algorithms for static program analysis. We emphasize a constraint-based approach where suitable constraint systems conceptually divide analysis into a front-end that generates constraints from program code and a back-end that solves the constraints to produce the analysis results. The style of presentation is intended to be precise but not overly formal. The readers are assumed to be familiar with advanced programming language concepts and the basics of compiler construction. The concepts are explained using a tiny imperative programming language, TIP, which suffices to illustrate the main challenges that arise with mainstream languages.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-danger pl-3">
<div>
<a name="SmitsWV20"></a>
<a class="font-weight-bold text-dark" target="_blank" href="https://doi.org/10.1016/j.cola.2019.100924">FlowSpec: A declarative specification language for intra-procedural flow-Sensitive data-flow analysis</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://researchr.org/profile/jeffsmits/publications">Jeff Smits</a>, <a class="text-secondary" href="https://www.linkedin.com/in/guidowachsmuth/">Guido Wachsmuth</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
JCL (JVLC) 57 2020
[<a class="text-secondary" href="https://doi.org/10.1016/j.cola.2019.100924" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/SmitsWV20/bibtex">bib</a>, <a href="https://researchr.org/publication/SmitsWV20" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="16.html#AbstractSmitsWV20" role="button" aria-expanded="false" aria-controls="AbstractSmitsWV20"">abstract</a>]
<!-- SmitsWV20 -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractSmitsWV20">
<div class="">
Data-flow analysis is the static analysis of programs to estimate their approximate run-time behavior or approximate intermediate run-time values. It is an integral part of modern language specifications and compilers. In the specification of static semantics of programming languages, the concept of data-flow allows the description of well-formedness such as definite assignment of a local variable before its first use. In the implementation of compiler back-ends, data-flow analyses inform optimizations. Data-flow analysis has an established theoretical foundation. What lags behind is implementations of data-flow analysis in compilers, which are usually ad-hoc. This makes such implementations difficult to extend and maintain. In previous work researchers have proposed higher-level formalisms suitable for whole-program analysis in a separate tool, incremental analysis within editors, or bound to a specific intermediate representation. In this paper, we present FlowSpec, an executable formalism for specification of data-flow analysis. FlowSpec is a domain-specific language that enables direct and concise specification of data-flow analysis for programming languages, designed to express flow-sensitive, intra-procedural analyses. We define the formal semantics of FlowSpec in terms of monotone frameworks. We describe the design of FlowSpec using examples of standard analyses. We also include a description of our implementation of FlowSpec. In a case study we evaluate FlowSpec with the static analyses for Green-Marl, a domain-specific programming language for graph analytics.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-primary pl-3">
<div>
<a name="SmitsV17"></a>
<a class="font-weight-bold text-dark" target="_blank" href="http://doi.acm.org/10.1145/3136014.3136029">FlowSpec: declarative dataflow analysis specification</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://researchr.org/profile/jeffsmits/publications">Jeff Smits</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
SLE 2017
[<a class="text-secondary" href="http://doi.acm.org/10.1145/3136014.3136029" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/SmitsV17/bibtex">bib</a>, <a href="https://researchr.org/publication/SmitsV17" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="16.html#AbstractSmitsV17" role="button" aria-expanded="false" aria-controls="AbstractSmitsV17"">abstract</a>]
<!-- SmitsV17 -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractSmitsV17">
<div class="">
We present FlowSpec, a declarative specification language for the domain of dataflow analysis. FlowSpec has declarative support for the specification of control flow graphs of programming languages, and dataflow analyses on these control flow graphs. We define the formal semantics of FlowSpec, which is rooted in Monotone Frameworks. We also discuss a prototype implementation of the language, built in the Spoofax Language Workbench. Finally, we evaluate the expressiveness and conciseness of the language with two case studies. These case studies are analyses for Green-Marl, an industrial, domain-specific language for graph processing. The first case study is a classical dataflow analysis, scaled to this full language. The second case study is a domain-specific analysis of Green-Marl.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-info pl-3">
<div>
<a name="NielsenNH05"></a>
<a class="font-weight-bold text-dark" target="_blank" href="http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-65410-0">Principles of program analysis (2. corr. print)</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://researchr.org/alias/flemming-nielson">Flemming Nielson</a>, <a class="text-secondary" href="https://researchr.org/alias/hanne-riis-nielson">Hanne Riis Nielson</a>, <a class="text-secondary" href="https://researchr.org/alias/chris-hankin">Chris Hankin</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
[<a class="text-secondary" href="http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-65410-0" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/NielsenNH05/bibtex">bib</a>, <a href="https://researchr.org/publication/NielsenNH05" class="text-secondary" target="_blank">researchr</a>]
<!-- NielsenNH05 -->
</div>
</div>
</li>
</ul>
</div>
<div class="col-sm-12 col-md-12 col-lg-3 col-xl-3 " >
<div class="sticky-top top70 d-none d-lg-block d-xl-block">
<div class="pb4 mb3 border-bottom border-grey ">
<nav>
<ul class="pagination justify-content-left">
<li class="page-item">
<a class="page-link" href="15.html">
&laquo;
</a>
</li>
<li class="page-item">
<a class="page-link" href="../lectures/index.html">
^
</a>
</li>
<li class="page-item">
<a class="page-link" href="17.html">&raquo;</a>
</li>
</ul>
</nav>
</div>
<ul id="my_toc" class="toc list-group list-group-flush d-none d-lg-block d-xl-block p-0 ml-0 mt-3">
<li class="list-group-item pl-0 ml-0 border-0 pl-0 pt-0 pb-1 pr-0 m-0 mr-3"><a href="16.html#references">References</a></li>
</ul>
</div>
</div>
</div>
<div class="row">
<div class="col-12">
<div class="border-top border-bottom border-grey mt-3 pt-3">
<nav>
<ul class="pagination justify-content-center">
<li class="page-item">
<a class="page-link" href="15.html">
Previous
</a>
</li>
<li class="page-item">
<a class="page-link" href="17.html">Next</a>
</li>
<li class="page-item">
<a class="page-link" href="../lectures/index.html">
Index
</a>
</li>
</ul>
</nav>
</div>
</div>
</div>
</div>
<!-- Optional JavaScript -->
<!-- jQuery first, then Popper.js, then Bootstrap JS -->
<script src="https://code.jquery.com/jquery-3.3.1.slim.min.js" integrity="sha384-q8i/X+965DzO0rT7abK41JStQIAqVgRVzpbzo5smXKp4YfRvH+8abtTE1Pi6jizo" crossorigin="anonymous"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/popper.js/1.14.7/umd/popper.min.js" integrity="sha384-UO2eT0CpHqdSJQ6hJty5KVphtPhzWj9WO1clHTMGa3JDZwrnQq4sF86dIHNDz0W1" crossorigin="anonymous"></script>
<script src="https://stackpath.bootstrapcdn.com/bootstrap/4.3.1/js/bootstrap.min.js" integrity="sha384-JjSmVgyd0p3pXB1rRibZUAYoIIy6OrQ6VrjIEaFf/nJGzIxFDsf4x0xIM+B07jRM" crossorigin="anonymous"></script>
</body>
</html>