Changeset 1413 for Deliverables/D4.2-4.3/reports/D4-3.tex
- Timestamp:
- Oct 19, 2011, 2:54:35 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-3.tex
r1409 r1413 305 305 { 306 306 framesT: Type[0]; 307 empty_framesT: framesT; 307 308 regsT: Type[0]; 309 empty_regsT: regsT; 310 call_args_for_main: call_args p; 311 call_dest_for_main: call_dest p; 308 312 succ_pc: succ p → address → res address; 309 313 greg_store_: generic_reg p → beval → regsT → res regsT; … … 311 315 acca_store_: acc_a_reg p → beval → regsT → res regsT; 312 316 acca_retrieve_: regsT → acc_a_reg p → res beval; 313 accb_store_: acc_b_reg p → beval → regsT → res regsT; 314 accb_retrieve_: regsT → acc_b_reg p → res beval; 317 ... 315 318 dpl_store_: dpl_reg p → beval → regsT → res regsT; 316 319 dpl_retrieve_: regsT → dpl_reg p → res beval; 317 dph_store_: dph_reg p → beval → regsT → res regsT; 318 dph_retrieve_: regsT → dph_reg p → res beval; 320 ... 319 321 pair_reg_move_: regsT → pair_reg p → res regsT; 320 322 pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code … … 323 325 For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively. 324 326 Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language. 325 Here \texttt{framesT} is the type of stack frames. 327 Here \texttt{framesT} is the type of stack frames, with \texttt{empty\_framesT} an empty stack frame. 328 329 The two hypothesised values \texttt{call\_args\_for\_main} and \texttt{call\_dest\_for\_main} deal with problems with the \texttt{main} function of the program, and how it is handled. 330 In particular, we need to know when the \texttt{main} function has finished executing. 331 But this is complicated, in C, by the fact that the \texttt{main} function is explicitly allowed to be recursive (disallowed in C++). 332 Therefore, to understand whether the exiting \texttt{main} function is really exiting, or just recursively calling itself, we need to remember the address at which \texttt{main} is located. 333 This is done with \texttt{call\_dest\_for\_main}, whereas \texttt{call\_args\_for\_main} holds the \texttt{main} function's arguments. 326 334 327 335 We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}: … … 478 486 The function \texttt{opt\_to\_res} is also --- this is a `utility' function that lifts an option type into the \texttt{IO} monad. 479 487 488 \subsection{Memory models} 489 \label{subsect.memory.models} 490 491 Currently, the semantics of the front and backend intermediate languages are built around two distinct memory models. 492 The frontend languages reuse the CompCert memory model, whereas the backend languages employ a bespoke model tailored to their needs. 493 This split between the memory models is reflective of the fact that the front and backend language have different requirements from their memory models, to a certain extent. 494 495 In particular, the CompCert memory model places quite heavy restrictions on where in memory one can read from. 496 To read a value in this memory model, you must supply an address, complete with a number of `chunks' to read following that address. 497 The read is only successful if you attempt to read at a genuine `value boundary', and read the appropriate number of memory chunks for that value. 498 As a result, with the CompCert memory model you are unable to read the third byte of a 32-bit integer value directly from memory, for instance. 499 This has some consequences for the CompCert compiler, namely an inability to write a \texttt{memcpy} routine. 500 501 However, the CerCo memory model operates differently, as we need to move data `piecemeal' between stacks in the backend of the compiler. 502 As a result, the bespoke memory model allows one to read data at any memory location, not just on value boundaries. 503 This has the advantage that we can successfully write a \texttt{memcpy} routine with the CerCo compiler (remembering that \texttt{memcpy} is nothing more than `read a byte, copy a byte' repeated in a loop), an advantage over CompCert. 504 505 Right now, the two memory models are interfaced during the translation from RTLabs to RTL. 506 It is an open question whether we will unify the two memory models, using only the backend, bespoke memory model throughout the compiler, as the CompCert memory model seems to work fine for the frotend, where such byte-by-byte copying is not needed. 507 However, should we decide to port the frontend to the new memory model, it has been written in such an abstract way that doing so would be relatively straightforward. 508 480 509 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 481 510 % SECTION. % … … 487 516 These relate to fetching the next instruction to be interpreted from the control flow graph, or linearised representation, of the language. 488 517 Closing these axioms should not be a problem. 489 No further work remains, aside from `tidying up' the code. 518 519 Further, tailcalls to external functions are currently axiomatised. 520 This is due to there being a difficulty with how stackframes are handled with external function calls. 521 We leave this for further work, due to there being no pressing need to implement this feature at the present time. 522 523 There is also, as mentioned, an open problem as to whether the frontend languages should use the same memory model as the backend languages, as opposed to reusing the CompCert memory model. 524 Should this decision be taken, this will likely be straightforward but potentially time consuming. 490 525 491 526 \newpage
Note: See TracChangeset
for help on using the changeset viewer.