Changeset 3223
 Timestamp:
 Apr 30, 2013, 12:05:24 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.4/Report/report.tex
r3218 r3223 305 305 code. 306 306 307 \todo{move of initialisation code?} 307 Following D2.2, we previous generated code for global variable 308 initialisation in \textsf{Cminor}, for which we reserved a cost label 309 to represent the execution time for initialisation. However, the 310 backend must also add an initial call to the main function, whose 311 cost must also be accounted for, so we decided to move the 312 initialisation code to the backend and merge the costs. 308 313 309 314 \subsection{Main goals} … … 409 414 observable witness is preserved, so the program must behave correctly. 410 415 411 \section{ Intermediate goals for the frontend}416 \section{Goals for the frontend} 412 417 \label{sec:fegoals} 413 418 … … 561 566 instead of \textbf{break}). 562 567 \end{itemize} 563 564 568 In order to tackle the first point, we implemented a version of memory 565 extensions similar to Compcert's. What has been done is the simulation proof 566 for all ``easy'' cases, that do not interact with the switch removal per se, 567 plus a bit of the switch case. This comprises propagating the memory extension 568 through each statement (except switch), as well as various invariants that 569 are needed for the switch case (in particular, freshness hypotheses). The 570 details of the evaluation process for the source switch statement and its 571 target counterpart can be found in the file \textbf{switchRemoval.ma}, 572 along more details on the transformation itself. 569 extensions similar to CompCert's. 570 571 For the simulation we decided to prove a sufficient amount to give us 572 confidence in the definitions and approach, but curtail the proof 573 because this pass does not contribute to the intensional correctness 574 result. We tackled several simple cases, that do not interact with 575 the switch removal per se, to show that the definitions were usable, 576 and part of the switch case to check that the approach is 577 reasonable. This comprises propagating the memory extension through 578 each statement (except switch), as well as various invariants that are 579 needed for the switch case (in particular, freshness hypotheses). The 580 details of the evaluation process for the source switch statement and 581 its target counterpart can be found in the file 582 \textbf{switchRemoval.ma}, along more details on the transformation 583 itself. 573 584 574 585 Proving the correctness of the second point would require reasoning on the … … 820 831 both the implementation and the proof more complex, even though more 821 832 comprehensive checks are made in the next stage. 822 \todo{Make this a particular case of the more general statement on baking more invariants in the Clight language}833 %\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language} 823 834 824 835 \subsubsection{Clight to Cminor} … … 827 838 Its input is a full \textsf{Clight} program, and its output is a 828 839 \textsf{Cminor} program. Note that we do not use an equivalent of 829 Comp cert's \textsf{C\#minor} language: we translate directly to a840 CompCert's \textsf{C\#minor} language: we translate directly to a 830 841 variant of \textsf{Cminor}. This presents the advantage of not 831 842 requiring the special loop constructs, nor the explicit block … … 855 866 Our memory injections are modelled after the work of Blazy \& Leroy. 856 867 However, the corresponding paper is based on the first version of the 857 Comp cert memory model, whereas we use a much more concrete model, allowing bytelevel858 manipulations (as in the later version of Comp cert's memory model). We proved868 CompCert memory model, whereas we use a much more concrete model, allowing bytelevel 869 manipulations (as in the later version of CompCert's memory model). We proved 859 870 roughly 80 \% of the required lemmas. Some difficulties encountered were notably 860 871 due to some overly relaxed conditions on pointer validity (fixed during development). … … 867 878 \paragraph{Simulation proof.} 868 879 869 The correctness proof for this transformation was not completed. We proved the 870 simulation result for expressions and for some subset of the critical statement cases. 871 Notably lacking are the function entry and exit, where the memory injection is 872 properly set up. As would be expected, a significant amount of work has to be performed 873 to show the conservation of all invariants at each simulation step. 874 875 \todo{list cases, explain while loop, explain labeling problem} 880 We proved the simulation result for expressions and a representative 881 selection of statements. In particular we tackled 882 \lstinline[language=C]'while' statements to ensure that we correctly 883 translate loops because our approach differs from CompCert by 884 converting directly to \textsf{Cminor} \lstinline[language=C]'goto's 885 rather than maintaining a notion of loops. We also have a partial 886 proof for function entry, covering the setup of the memory injection, 887 but not function exit. Exits, and the remaining statements, have been 888 axiomatised. 889 890 Careful management of the proof state was required due to the proof 891 terms that are embedded in \textsf{Cminor} code to show that some 892 invariants are respected. These proof terms can be large and awkward, 893 and while generalising them away is usually sufficient, it can be 894 difficult when they appear under a binder. 895 896 %The correctness proof for this transformation was not completed. We proved the 897 %simulation result for expressions and for some subset of the critical statement cases. 898 %Notably lacking are the function entry and exit, where the memory injection is 899 %properly set up. As would be expected, a significant amount of work has to be performed 900 %to show the conservation of all invariants at each simulation step. 901 902 %\todo{list cases, explain while loop, explain labeling problem} 876 903 877 904 \subsubsection{Cminor to RTLabs}
Note: See TracChangeset
for help on using the changeset viewer.