This is an old revision of the document!
Abstract Interpretation Recipe
Program Representation
Control-flow graph: where
- is set of program points
- are control-flow graph edges
- , so each is relation describing the meaning of command between and
Summary of key steps
- design abstract domain that represents sets of program states
- define giving meaning to elements of
- define lattice ordering on such that
- define that maps an abstract element and a CFG statement to new abstract element, such that
(for example, by defining function so that becomes a Galois Connection on Lattices)
- extend to work on control-flow graphs, by defining as follows (below, )
\[
F^{\#}(g^{\#})(p_2) = g^{\#}(p_2) \sqcup \bigsqcup_{(p_1,p_2) \in E} sp^{\#}(g^{\#}(p_1),r(p_1,p_2))
\] which is analogous to Collecting Semantics
- compute (this is easier than computing collecting semantics because lattice is simpler than ):
\[
g^{\#}_* = \bigsqcup_{n \ge 0} (F^{\#})^{n}(\bot^{\#})
\]
where for all