# Changeset 1802 for Deliverables

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

other small corrections

File:
1 edited

### Legend:

Unmodified
 r1801 | 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. $\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$.