Using Verified Data-Flow Analysis-based
Optimizations in Attribute Grammars
Eric Van Wyk and Lijesh Krishnan
University of Minnesota, USA
Building verified compilers is difficult, especially when complex
analyses such as type checking or data-flow analysis must be
performed. Both the type checking and program optimization communities
have developed methods for proving the correctness of these processes
and developed tools for using, respectively, verified type systems and
verified optimizations. However, it is difficult to use both of these
analyses in a single declarative framework since these processes work
on different program representations: type checking on abstract syntax
trees and data-flow analysis-based optimization on control flow or
program dependency graphs.
We present an attribute grammar specification language that has been
extended with constructs for specifying attribute-labelled control flow
graphs and both CTL and LTL-FV formulas that specify data-flow
analyses. These formulas are model-checked on these graphs to perform
the specified analyses. Thus, verified type rules and verified
data-flow analyses (verified either by hand or with automated proof
tools) can both be transcribed into a single declarative framework
based on attribute grammars to build a high-confidence language
implementations. Also, the attribute grammar specification language is
extensible so that it is relatively straight-forward to add new
constructs for different temporal logics so that alternative logics and
model checkers can be used to specify data-flow analyses in this
framework.