Index: /Deliverables/D1.2/CompilerProofOutline/outline.tex
===================================================================
--- /Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1801)
+++ /Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1802)
@@ -1024,17 +1024,29 @@
| l::todo ->
if l $\in$ visited then
- let generated := generated $\cup\ \{$ Goto l $\}$ in
- let required := required $\cup$ l in
- linearise graph visited required generated todo
+ -- do not do anything if the node is alredy visited
+ linearise graph visited required generated todo
else
-- Get the instruction at label `l' in the graph
let lookup := graph(l) in
let generated := generated $\cup\ \{$ lookup $\}$ in
- -- Find the successor of the instruction at label `l' in the graph
- let successor := succ(l, graph) in
- let todo := successor::todo in
- linearise graph visited required generated todo
+ -- Find the explicit successors of the instruction at label `l' in the graph
+ let xsuccs := explsuccs(l, graph) in
+ let required := xsuccs $\cup$ required in
+ -- Update generated and required in case the implicit successor is visited
+ -- NB: succ can be none
+ let succ := succ(l, graph) in
+ let todo := succ :: xsuccs @ todo in
+ let (generated, required) :=
+ if succ is defined and succ $\in$ visited then
+ (generated $\cup\ \{$ GOTO succ $\}$, $\{$ succ $\}\ \cup$ required)
+ else
+ (generated, required) in
+ linearise graph visited required generated todo
| [] -> (required, generated)
\end{lstlisting}
+Explcit successors are labels that need to remain in the code (e.g.\ the target of a
+\texttt{GOTO} that has survived branch compression, or the branching label of a
+conditional), while the possible implicit one must be replaced by a \texttt{GOTO}
+if and only if it is a back edge of the depth-first visit.
It is easy to see that this linearisation process eventually terminates.
@@ -1050,7 +1062,8 @@
$\mathtt{visited} \approx \mathtt{generated}$, where $\approx$ is \emph{multiset} equality, as \texttt{generated} is a set of instructions where instructions may mention labels multiple times, and \texttt{visited} is a set of labels,
\item
-$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
-\item
-$\mathtt{required} \subseteq \mathtt{visited}$.
+$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succs(l,\ graph)} \subseteq \mathtt{generated} \cup \mathtt{todo}$,
+\item
+$\mathtt{required} \subseteq \mathtt{visited}\cup\mathtt{todo}
+$.
% \item
% $\mathtt{visited} \cap \mathtt{todo} = \emptyset$.