Changeset 1398 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 17, 2011, 8:20:05 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-3.tex
r1397 r1398 97 97 \vspace*{7cm} 98 98 \paragraph{Abstract} 99 We describe the encoding in the Calculus of Constructions of the semantics of the CerCo compiler's backend intermediate languages. 100 The CerCo backend consists of five distinct languages: RTL, RTLntl, ERTL, LTL and LIN. 101 We describe a process of heavy abstraction of the intermediate languages and their semantics. 102 We hope that this process will ease the burden of Deliverable D4.4, the proof of correctness for the compiler. 99 103 100 104 \newpage … … 183 187 }. 184 188 \end{lstlisting} 189 We summarise what these types mean: 190 \begin{center} 191 \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} 192 Type & Explanation \\ 193 \hline 194 \texttt{acc\_a\_reg} & The type of the accumulator A register. In some languages this is implemented as the hardware accumulator, whereas in others this is a pseudoregister.\\ 195 \texttt{acc\_b\_reg} & Similar to the accumulator A field, but for the processor's auxilliary accumulator, B. \\ 196 \texttt{dpl\_reg} & \\ 197 \texttt{dph\_reg} & \\ 198 \texttt{pair\_reg} & \\ 199 \texttt{generic\_reg} & \\ 200 \texttt{call\_args} & \\ 201 \texttt{call\_dest} & \\ 202 \texttt{extend\_statements} & 203 \end{tabular*} 204 \end{center} 185 205 186 206 As mentioned in the report for Deliverable D4.2, the record \texttt{params\_\_} is enough to be able to specify the instructions of the joint languages: … … 192 212 \end{lstlisting} 193 213 194 We extend \texttt{params\_\_} with a type corresponding 214 We extend \texttt{params\_\_} with a type corresponding to labels, \texttt{succ}, obtaining a new record type of parameters called \texttt{params\_}: 195 215 \begin{lstlisting} 196 216 record params_: Type[1] ≝ … … 200 220 }. 201 221 \end{lstlisting} 202 222 The type \texttt{succ} corresponds to labels, in the case of control flow graph based languages, or is instantiated to the unit type for the linearised language, LIN. 223 Using \texttt{param\_} we can define statements of the joint language: 203 224 \begin{lstlisting} 204 225 inductive joint_statement (p:params_) (globals: list ident): Type[0] := … … 207 228 | RETURN: joint_statement p globals. 208 229 \end{lstlisting} 209 230 Note that in the joint language, instructions are `linear', in that they have an immediate successor. 231 Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program. 232 233 For the semantics, we need further parametererised types. 234 In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}: 210 235 \begin{lstlisting} 211 236 record params0: Type[1] ≝ … … 215 240 }. 216 241 \end{lstlisting} 217 242 We further extend \texttt{params0} with a type for local variables in internal function calls: 218 243 \begin{lstlisting} 219 244 record params1 : Type[1] ≝
Note: See TracChangeset
for help on using the changeset viewer.