Changeset 3351
- Timestamp:
- Jun 14, 2013, 11:54:19 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/itp-2013/ccexec2.tex
r3350 r3351 879 879 880 880 Another 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 883 884 \textbf{XXXXXXXXXXXXXXXXXX} 885 886 A compiler preserves the program semantics by suppressing or introducing 887 $\tau$ actions. 888 889 Intuitively, it is because 890 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. 909 910 911 881 function calls should yield back control after the calling point. Some passes 882 need to translate a function call to a function call followed by some 883 instructions (for example to restore caller-saved registers in the pass that 884 sets the parameter convenction). In the forward simulation proof, these 885 instructions are taken care of when simulating the \texttt{RETURN} step: 886 the state just after the return in the source code is matched by the state $s_2$ 887 after these steps in the object code. However, the aforementioned requirement 888 does not involve $s_2$, but the state reached after the return in the object 889 code, that preceeds $s_2$ in the execution fragment. Therefore the requirement 890 cannot be enforced with the standard forward simulation argument. 891 892 In this section we present now a modified forward simulation argument that 893 can be used to prove at once that a compiler preserves the semantics of the 894 program, its weak traces and that the compiler propagates measurability. 912 895 913 896 % @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ … … 1381 1364 % an equivalence relation. 1382 1365 1366 \textbf{----------------------------} 1367 1383 1368 We summarise here the results of the previous sections. Each intermediate 1384 1369 unstructured language can be given a semantics based on structured traces,
Note: See TracChangeset
for help on using the changeset viewer.