Changeset 3351

Jun 14, 2013, 11:54:19 AM (4 years ago)


1 edited


  • Papers/itp-2013/ccexec2.tex

    r3350 r3351  
    880880Another reason why the standard argument breaks is due to the requirement that
    881 function calls should yield back control after the calling point. This must be
    882 enforced just after
    886 A compiler preserves the program semantics by suppressing or introducing
    887 $\tau$ actions.
    889 Intuitively, it is because
    891 To understand why, consider the case of a function call
    892 and the pass that fixes the parameter passing conventions. A function
    893 call in the source code takes in input an arbitrary number of pseudo-registers (the actual parameters to pass) and returns an arbitrary number of pseudo-registers (where the result is stored). A function call in the target language has no
    894 input nor output parameters. The pass must add explicit code before and after
    895 the function call to move the pseudo-registers content from/to the hardware
    896 registers or the stack in order to implement the parameter passing strategy.
    897 Similarly, each function body must be augmented with a preamble and a postamble
    898 to complete/initiate the parameter passing strategy for the call/return phase.
    899 Therefore what used to be a call followed by the next instruction to execute
    900 after the function return, now becomes a sequence of instructions, followed by
    901 a call, followed by another sequence. The two states at the beginning of the
    902 first sequence and at the end of the second sequence are in relation with
    903 the status before/after the call in the source code, like in an usual forward
    904 simulation. How can we prove however the additional condition for function calls
    905 that asks that when the function returns the instruction immediately after the
    906 function call is called? To grant this invariant, there must be another relation
    907 between the address of the function call in the source and in the target code.
    908 This additional relation is to be used in particular to relate the two stacks.
     881function calls should yield back control after the calling point. Some passes
     882need to translate a function call to a function call followed by some
     883instructions (for example to restore caller-saved registers in the pass that
     884sets the parameter convenction). In the forward simulation proof, these
     885instructions are taken care of when simulating the \texttt{RETURN} step:
     886the state just after the return in the source code is matched by the state $s_2$
     887after these steps in the object code. However, the aforementioned requirement
     888does not involve $s_2$, but the state reached after the return in the object
     889code, that preceeds $s_2$ in the execution fragment. Therefore the requirement
     890cannot be enforced with the standard forward simulation argument.
     892In this section we present now a modified forward simulation argument that
     893can be used to prove at once that a compiler preserves the semantics of the
     894program, its weak traces and that the compiler propagates measurability.
    913896% @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
    13811364% an equivalence relation.
    13831368We summarise here the results of the previous sections. Each intermediate
    13841369unstructured language can be given a semantics based on structured traces,
Note: See TracChangeset for help on using the changeset viewer.