Changeset 1733 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 24, 2012, 10:10:18 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1732 r1733 180 180 \subsection{Cminor to RTLabs translation} 181 181 182 In this part of the compiler we transform the program's functions into 183 control flow graphs. It is closely related to CompCert's Cminorsel to 184 RTL transformation, albeit with targetindependent operations. 185 186 We already enforce several invariants with dependent types: some type 187 safety is enforced mostly using the type information from Cminor; and 188 that the graph is closed (by showing that each successor was recently 189 added, or corresponds to a \lstinline[language=C]'goto' label which 190 are all added before the end). Note that this relies on a 191 monotonicity property; CompCert maintains a similar property in a 192 similar way while building RTL graphs. We will also add a result 193 showing that all of the pseudoregister names are distinct for use by 194 later stages using the same method as Cminor. 195 196 The simulation will relate Cminor states to RTLabs states about to 197 execute the corresponding code (with a corresponding continuation). 198 Each Cminor statement becomes zero or more RTLabs statements, with a 199 decreasing measure based on the statement and continuations similar to 200 CompCert's. We may also follow CompCert in using a relational 201 specification of this stage so as to abstract away from the functional 202 (and highly dependently typed) definition. 203 204 The first two labelling properties remain as before; we will show that 205 cost labels are preserved, so the function entry point will be a cost 206 label, and successors that are cost labels map still map to cost 207 labels, preserving the condition on branches. We replace the property 208 for loops with the notion that we will always reach a cost label or 209 the end of the function by following a bounded number of successors. 210 This can be easily seen in Cminor using the requirement for cost 211 labels at the head of loops and after gotos. It remains to show that 212 this is preserved by the translation to RTLabs. % how? 213 182 214 \subsection{RTLabs structured trace generation} 215 216 This proofonly step incorporates the function call structure and cost 217 labelling properties into the execution trace. As the function calls 218 are nested within the trace, we need to distinguish between 219 terminating and nonterminating function calls. 220 221 Thus we use the excluded middle (specialised to a function termination 222 property) to do this. Terminating functions are built by following 223 the trace, breaking it into chunks between cost labels and recursively 224 processing function calls. The main difficulties here are the 225 nonstructurally recursive nature of the function (instead we use the 226 size of the termination proof as a measure) and using the properties 227 on RTLabs cost labelling to create the correct structure. We also 228 show that the lower stack frames are preserved during function calls 229 in order to prove that after returning from a function call we execute 230 the correct code. This part of the work has already been constructed, 231 but still requires a simple proof to show that flattening the structured 232 trace recreates the original flat trace. 233 234 The nonterminating case uses the excluded middle to decide whether to 235 use the function described above to construct an inductive terminating 236 structured trace, or a coinductive version for nontermination. It 237 follows the trace like the terminating version to build up chunks of 238 trace from costlabel to costlabel (which, by the finite distance to 239 a cost label property shown before, can be represented by an inductive 240 type), unless it encounters a nonterminating function in which case 241 it corecursively processes that. This part of the trace 242 transformation is currently under construction, and will also need a 243 flattening result to show that it is correct. 183 244 184 245 \section{The RTLabs to RTL translation}
Note: See TracChangeset
for help on using the changeset viewer.