Changeset 1802 for Deliverables/D1.2/CompilerProofOutline/outline.tex

Timestamp:

Mar 2, 2012, 3:55:13 PM (8 years ago)

Author:

tranquil

Message:

other small corrections

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (2 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -1024 +1024 @@
   | 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 +1062 @@
 $\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$.