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

other small corrections

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1801 r1802  
    10241024  | l::todo ->
    10251025    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
    10291028    else
    10301029      -- Get the instruction at label `l' in the graph
    10311030      let lookup := graph(l) in
    10321031      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
    10371045  | []      -> (required, generated)
    10381046\end{lstlisting}
     1047Explcit 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
     1049conditional), while the possible implicit one must be replaced by a \texttt{GOTO}
     1050if and only if it is a back edge of the depth-first visit.
    10391051
    10401052It is easy to see that this linearisation process eventually terminates.
     
    10501062$\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,
    10511063\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$.
    10551068% \item
    10561069% $\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
Note: See TracChangeset for help on using the changeset viewer.