Changeset 1802 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Mar 2, 2012, 3:55:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1801 r1802 1024 1024  l::todo > 1025 1025 if l $\in$ visited then 1026 let generated := generated $\cup\ \{$ Goto l $\}$ in 1027 let required := required $\cup$ l in 1028 linearise graph visited required generated todo 1026  do not do anything if the node is alredy visited 1027 linearise graph visited required generated todo 1029 1028 else 1030 1029  Get the instruction at label `l' in the graph 1031 1030 let lookup := graph(l) in 1032 1031 let generated := generated $\cup\ \{$ lookup $\}$ in 1033  Find the successor of the instruction at label `l' in the graph 1034 let successor := succ(l, graph) in 1035 let todo := successor::todo in 1036 linearise graph visited required generated todo 1032  Find the explicit successors of the instruction at label `l' in the graph 1033 let xsuccs := explsuccs(l, graph) in 1034 let required := xsuccs $\cup$ required in 1035  Update generated and required in case the implicit successor is visited 1036  NB: succ can be none 1037 let succ := succ(l, graph) in 1038 let todo := succ :: xsuccs @ todo in 1039 let (generated, required) := 1040 if succ is defined and succ $\in$ visited then 1041 (generated $\cup\ \{$ GOTO succ $\}$, $\{$ succ $\}\ \cup$ required) 1042 else 1043 (generated, required) in 1044 linearise graph visited required generated todo 1037 1045  [] > (required, generated) 1038 1046 \end{lstlisting} 1047 Explcit successors are labels that need to remain in the code (e.g.\ the target of a 1048 \texttt{GOTO} that has survived branch compression, or the branching label of a 1049 conditional), while the possible implicit one must be replaced by a \texttt{GOTO} 1050 if and only if it is a back edge of the depthfirst visit. 1039 1051 1040 1052 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, 1051 1063 \item 1052 $\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$, 1053 \item 1054 $\mathtt{required} \subseteq \mathtt{visited}$. 1064 $\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succs(l,\ graph)} \subseteq \mathtt{generated} \cup \mathtt{todo}$, 1065 \item 1066 $\mathtt{required} \subseteq \mathtt{visited}\cup\mathtt{todo} 1067 $. 1055 1068 % \item 1056 1069 % $\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
Note: See TracChangeset
for help on using the changeset viewer.