Changeset 1802 for Deliverables/D1.2/CompilerProofOutline/outline.tex
- Timestamp:
- Mar 2, 2012, 3:55:13 PM (8 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 depth-first 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.