Control- & Data-Flow Analysis

Session date: 16 October 2023

Session host: Jeff Smits

Summary:

Data-flow analysis is the static analysis of programs to estimate their approximate run-time behaviour 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 optimisations.

In this presentation I want to familiarise you with the concept of data-flow analysis, explain Monotone Frameworks as a mathematical foundation for this kind of analysis, and show how you can derive a practical solver from it. If we have enough time I’ll also go into a bit of my research: designing the FlowSpec DSL in which you can define data-flow analysis on a high level.

Relevant papers

FlowSpec: A declarative specification language for intra-procedural flow-Sensitive data-flow analysis

Jeff Smits, Guido Wachsmuth, and Eelco Visser

Journal of Computer Languages, Mar 2020

Abs HTML

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.