Theory Example
section ‹Example›
text ‹\label{sec:example}›
theory Example
imports TD_plain TD_equiv
begin
text ‹As an example, let us consider a program analysis, namely the analysis of must-be initialized
program variables for the following program:›
text ‹▩‹a = 17
while true:
b = a * a
if b < 10: break
a = a - 1››
text ‹The program corresponds to the following control-flow graph.\newline\includegraphics{cfg.pdf}›
text ‹From the control-flow graph of the program, we generate the equation system to be solved by
the TD. The left-hand side of an equation consists of an unknown which represents a program point.
The right-hand side for some unknown describes how the set of must-be initialized variables at the
corresponding program point can be computed from the sets of must-be initialized variables at the
predecessors.›
subsection‹Definition of the Domain›
datatype pv = a | b
text ‹A fitting domain to describe possible values for the must-be initialized analysis, is an
inverse power set lattice of the set of all program variables. The least informative value which
is always a true over-approximation for the must-be initialized analysis is the empty set
(called top), whereas the initial value to start fixpoint iteration from is the set
@{term "{a, b}"} (called bot). The join operation, which is used to combine the values of
several incoming edges to obtain a sound over-approximation over all paths, corresponds to the
intersection of sets.›
typedef D = "Pow ({a, b})"
by auto
setup_lifting D.type_definition_D
lift_definition top :: "D" is "{}" by simp
lift_definition bot :: D is "{a, b}" by simp
lift_definition join :: "D ⇒ D ⇒ D" is Set.inter by blast
text‹Additionally, we define some helper functions to create values of type D.›
lift_definition insert :: "pv ⇒ D ⇒ D"
is "λe d. if e ∈ {a, b} then Set.insert e d else d"
by auto
definition set_to_D :: "pv set ⇒ D" where
"set_to_D = (λs. fold (λe acc. if e ∈ s then insert e acc else acc) [a, b] top)"
text‹We show that the considered domain fulfills the sort constraints bot and equal as expected by
the solver.›
instantiation D :: bot
begin
definition bot_D :: D
where "bot_D = bot"
instance ..
end
instantiation D :: equal
begin
definition equal_D :: "D ⇒ D ⇒ bool"
where "equal_D d1 d2 = ((Rep_D d1) = (Rep_D d2))"
instance by standard (simp add: equal_D_def Rep_D_inject)
end
subsection‹Definition of the Equation System›
text ‹The following equation system can be generated for the must-be initialized analysis and the
program from above.$$
\mathcal{T}:\quad
\begin{aligned}
\mathrm{w} &= \emptyset \\
\mathrm{z} &= \left(\mathrm{y}\,\cup\,\{\mathtt{a}\}\right)\,\cap\,\left(\mathrm{w}\,\cup\,
\{\mathtt{a}\}\right) \\
\mathrm{y} &= \mathrm{z}\,\cup\,\{\mathtt{b}\} \\
\mathrm{x} &= \mathrm{y}\,\cap\,\mathrm{z}
\end{aligned}
$$
Below we define this equation system and express the right-hand sides with strategy trees.›