Changeset 3351

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

...

File:
1 edited

Legend:

Unmodified
 r3350 Another reason why the standard argument breaks is due to the requirement that function calls should yield back control after the calling point. This must be enforced just after \textbf{XXXXXXXXXXXXXXXXXX} A compiler preserves the program semantics by suppressing or introducing $\tau$ actions. Intuitively, it is because To understand why, consider the case of a function call and the pass that fixes the parameter passing conventions. A function 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 input nor output parameters. The pass must add explicit code before and after the function call to move the pseudo-registers content from/to the hardware registers or the stack in order to implement the parameter passing strategy. Similarly, each function body must be augmented with a preamble and a postamble to complete/initiate the parameter passing strategy for the call/return phase. Therefore what used to be a call followed by the next instruction to execute after the function return, now becomes a sequence of instructions, followed by a call, followed by another sequence. The two states at the beginning of the first sequence and at the end of the second sequence are in relation with the status before/after the call in the source code, like in an usual forward simulation. How can we prove however the additional condition for function calls that asks that when the function returns the instruction immediately after the function call is called? To grant this invariant, there must be another relation between the address of the function call in the source and in the target code. This additional relation is to be used in particular to relate the two stacks. function calls should yield back control after the calling point. Some passes need to translate a function call to a function call followed by some instructions (for example to restore caller-saved registers in the pass that sets the parameter convenction). In the forward simulation proof, these instructions are taken care of when simulating the \texttt{RETURN} step: the state just after the return in the source code is matched by the state $s_2$ after these steps in the object code. However, the aforementioned requirement does not involve $s_2$, but the state reached after the return in the object code, that preceeds $s_2$ in the execution fragment. Therefore the requirement cannot be enforced with the standard forward simulation argument. In this section we present now a modified forward simulation argument that can be used to prove at once that a compiler preserves the semantics of the program, its weak traces and that the compiler propagates measurability. % @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ % an equivalence relation. \textbf{----------------------------} We summarise here the results of the previous sections. Each intermediate unstructured language can be given a semantics based on structured traces,