1 | \documentclass[a4paper, 10pt]{article} |
---|
2 | |
---|
3 | \usepackage{a4wide} |
---|
4 | \usepackage{amsfonts} |
---|
5 | \usepackage{amsmath} |
---|
6 | \usepackage{amssymb} |
---|
7 | \usepackage[english]{babel} |
---|
8 | \usepackage{color} |
---|
9 | \usepackage{diagrams} |
---|
10 | \usepackage{graphicx} |
---|
11 | \usepackage[colorlinks]{hyperref} |
---|
12 | \usepackage[utf8x]{inputenc} |
---|
13 | \usepackage{listings} |
---|
14 | \usepackage{microtype} |
---|
15 | \usepackage{skull} |
---|
16 | \usepackage{stmaryrd} |
---|
17 | |
---|
18 | \lstdefinelanguage{matita-ocaml} { |
---|
19 | mathescape=true |
---|
20 | } |
---|
21 | \lstset{ |
---|
22 | language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false, |
---|
23 | showspaces=false, showstringspaces=false, extendedchars=false, |
---|
24 | inputencoding=utf8x, tabsize=2 |
---|
25 | } |
---|
26 | |
---|
27 | \title{Proof outline for the correctness of the CerCo compiler} |
---|
28 | \date{\today} |
---|
29 | \author{The CerCo team} |
---|
30 | |
---|
31 | \begin{document} |
---|
32 | |
---|
33 | \maketitle |
---|
34 | |
---|
35 | \section{Introduction} |
---|
36 | \label{sect.introduction} |
---|
37 | |
---|
38 | \section{The RTLabs to RTL translation} |
---|
39 | \label{sect.rtlabs.rtl.translation} |
---|
40 | |
---|
41 | % dpm: type system and casting load (???) |
---|
42 | We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model: |
---|
43 | |
---|
44 | \begin{displaymath} |
---|
45 | \mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{int}_i \mid \mathtt{ptr}_i |
---|
46 | \end{displaymath} |
---|
47 | |
---|
48 | We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}. |
---|
49 | |
---|
50 | \begin{displaymath} |
---|
51 | \mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha) |
---|
52 | \end{displaymath} |
---|
53 | |
---|
54 | where |
---|
55 | |
---|
56 | \begin{displaymath} |
---|
57 | \mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID} |
---|
58 | \end{displaymath} |
---|
59 | |
---|
60 | \begin{displaymath} |
---|
61 | \mathtt{BEMem} = \mathtt{Mem} \mathtt{Value} |
---|
62 | \end{displaymath} |
---|
63 | |
---|
64 | \begin{displaymath} |
---|
65 | \mathtt{Address} = \mathtt{BEValue} \times \mathtt{BEValue} \\ |
---|
66 | \end{displaymath} |
---|
67 | |
---|
68 | \begin{displaymath} |
---|
69 | \mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null}) |
---|
70 | \end{displaymath} |
---|
71 | |
---|
72 | \begin{center} |
---|
73 | \begin{picture}(2, 2) |
---|
74 | % picture of sigma mapping memory to memory |
---|
75 | TODO |
---|
76 | \end{picture} |
---|
77 | \end{center} |
---|
78 | |
---|
79 | \begin{displaymath} |
---|
80 | \mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i |
---|
81 | \end{displaymath} |
---|
82 | |
---|
83 | \begin{displaymath} |
---|
84 | \sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M) |
---|
85 | \end{displaymath} |
---|
86 | |
---|
87 | \begin{displaymath} |
---|
88 | \begin{array}{rll} |
---|
89 | \mathtt{State} & ::= & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\ |
---|
90 | & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\ |
---|
91 | & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem} |
---|
92 | \end{array} |
---|
93 | \end{displaymath} |
---|
94 | |
---|
95 | \begin{displaymath} |
---|
96 | \mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS} |
---|
97 | \end{displaymath} |
---|
98 | |
---|
99 | \begin{displaymath} |
---|
100 | \mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State} |
---|
101 | \end{displaymath} |
---|
102 | |
---|
103 | \begin{displaymath} |
---|
104 | \sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{Frame})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem})) |
---|
105 | \end{displaymath} |
---|
106 | |
---|
107 | \begin{displaymath} |
---|
108 | \sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step} |
---|
109 | \end{displaymath} |
---|
110 | |
---|
111 | \begin{displaymath} |
---|
112 | \sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step} |
---|
113 | \end{displaymath} |
---|
114 | |
---|
115 | Return one step commuting diagram: |
---|
116 | |
---|
117 | \begin{displaymath} |
---|
118 | \begin{diagram} |
---|
119 | s & \rTo^{\text{one step of execution}} & s' \\ |
---|
120 | & \rdTo & \dTo \\ |
---|
121 | & & \llbracket s'' \rrbracket |
---|
122 | \end{diagram} |
---|
123 | \end{displaymath} |
---|
124 | |
---|
125 | Call one step commuting diagram: |
---|
126 | |
---|
127 | \begin{displaymath} |
---|
128 | \begin{diagram} |
---|
129 | s & \rTo^{\text{one step of execution}} & s' \\ |
---|
130 | & \rdTo & \dTo \\ |
---|
131 | & & \llbracket s'' \rrbracket |
---|
132 | \end{diagram} |
---|
133 | \end{displaymath} |
---|
134 | |
---|
135 | \begin{displaymath} |
---|
136 | \begin{diagram} |
---|
137 | \mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME) |
---|
138 | \end{diagram} |
---|
139 | \end{displaymath} |
---|
140 | |
---|
141 | \begin{displaymath} |
---|
142 | \begin{array}{rcl} |
---|
143 | \mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\ |
---|
144 | \mathtt{RETURN} & \longrightarrow & \mathtt{RETURN} \\ |
---|
145 | \end{array} |
---|
146 | \end{displaymath} |
---|
147 | |
---|
148 | \begin{displaymath} |
---|
149 | \begin{array}{rcl} |
---|
150 | \sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\ |
---|
151 | \sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register} |
---|
152 | \end{array} |
---|
153 | \end{displaymath} |
---|
154 | |
---|
155 | \section{The RTL to ERTL translation} |
---|
156 | \label{sect.rtl.ertl.translation} |
---|
157 | |
---|
158 | \begin{displaymath} |
---|
159 | \begin{diagram} |
---|
160 | & & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\ |
---|
161 | & \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\ |
---|
162 | \skull & & & & FINISH ME |
---|
163 | \end{diagram} |
---|
164 | \end{displaymath} |
---|
165 | |
---|
166 | \section{The ERTL to LTL translation} |
---|
167 | \label{sect.ertl.ltl.translation} |
---|
168 | |
---|
169 | \section{The LTL to LIN translation} |
---|
170 | \label{sect.ltl.lin.translation} |
---|
171 | |
---|
172 | We require a map, $\sigma$, from LTL statuses, where program counters are represented as labels in a graph data structure, to LIN statuses, where program counters are natural numbers: |
---|
173 | \begin{displaymath} |
---|
174 | \mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N} |
---|
175 | \end{displaymath} |
---|
176 | |
---|
177 | The LTL to LIN translation pass also linearises the graph data structure into a list of instructions. |
---|
178 | Pseudocode for the linearisation process is as follows: |
---|
179 | |
---|
180 | \begin{lstlisting} |
---|
181 | let rec linearise graph visited required generated todo := |
---|
182 | match todo with |
---|
183 | | l::todo -> |
---|
184 | if l $\in$ visited then |
---|
185 | let generated := generated $\cup\ \{$ Goto l $\}$ in |
---|
186 | let required := required $\cup$ l in |
---|
187 | linearise graph visited required generated todo |
---|
188 | else |
---|
189 | -- Get the instruction at label ``l'' in the graph |
---|
190 | let lookup := graph(l) in |
---|
191 | let generated := generated $\cup\ \{$ lookup $\}$ in |
---|
192 | -- Find the successor of the instruction at label ``l'' in the graph |
---|
193 | let successor := succ(l, graph) in |
---|
194 | let todo := successor::todo in |
---|
195 | linearise graph visited required generated todo |
---|
196 | | [] -> (required, generated) |
---|
197 | \end{lstlisting} |
---|
198 | |
---|
199 | |
---|
200 | \section{The LIN to ASM and ASM to MCS-51 machine code translations} |
---|
201 | \label{sect.lin.asm.translation} |
---|
202 | |
---|
203 | The LIN to ASM translation step is trivial, being almost the identity function. |
---|
204 | The only non-trivial feature of the LIN to ASM translation is that all labels are `named apart' so that there is no chance of freshly generated labels from different namespaces clashing with labels from another namespace. |
---|
205 | |
---|
206 | The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document. |
---|
207 | |
---|
208 | \end{document} |
---|