Changeset 3168 for Deliverables
 Timestamp:
 Apr 19, 2013, 12:30:32 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.4/Report/report.tex
r3167 r3168 2 2 \usepackage[mathletters]{ucs} 3 3 \usepackage[utf8x]{inputenc} 4 \usepackage{stmaryrd} 4 5 \usepackage{listings} 5 6 \usepackage{../../style/cerco} … … 579 580 \todo{don't use loop structures from CompCert, go straight to jumps} 580 581 582 \paragraph{Cast simplification} 583 584 The parser used in Cerco introduces a lot of explicit type casts. If left 585 as they are, these casts can greatly hamper the quality of the generated 586 code  especially as the architecture we consider is an $8$ bit one. 587 In \textsf{Clight}, casts are expressions. Hence, most of the work of 588 this transformation proceeds on expressions, and the onestep simulation 589 result one those is easily lifted to statement evaluations. 590 591 \todo{introduce the explicit type signature of the functions below ?} 592 593 The tranformation proceeds by recursively trying to coerce an expression to 594 a particular type, which is in practice a integer type smaller than the 595 original one. This functionality is implemented by two mutually recursive 596 functions: \textbf{simplify\_expr} and \textbf{simplify\_inside}. The latter 597 acts as a wrapper for the first one. Whenever \textbf{simplify\_inside} 598 encounters a \textbf{Ecast} expression, it tries to coerce the subexpression 599 to the desired type using \textbf{simplify\_expr}, which tries to perform the 600 actual coercion. In return, \textbf{simplify\_expr} calls back 601 \textbf{simplify\_inside} in some particular positions, where we decided to 602 be conservative in order to simplify the proofs. However, the current design 603 allows to incrementally revert to a more aggressive version, by replacing 604 recursive calls to \textbf{simplify\_inside} by calls to \textbf{simplify\_expr} 605 \emph{and} proving the corresponding invariants  where possible. 606 607 The main problem encountered with this particular pass was dealing with inconsistently 608 typed programs, a canonical case being a particular integer constant of a certain 609 size typed with another size. This prompted the need to introduce numerous 610 type checks, complexifying both the implementation and the proof. 611 612 \paragraph{Switch removal} 613 614 Our intermediate languages have no jump tables. Hence, we have to compile the 615 \lstinline[language=C]'switch' constructs away before going from \textsf{Clight} to 616 \textsf{Cminor}. Note that this is not necessarily a bad decision performancewise 617 for small switches. For instance, compilers such as GCC introduce balanced trees 618 of ``ifthenelse'' constructs. However, our implementation strategy is much simpler. 619 Let us consider the following input statement. 620 621 \begin{lstlisting}[language=C] 622 switch(e) { 623 case v1: 624 stmt1; 625 case v2: 626 stmt2; 627 default: 628 stmt_default; 629 } 630 \end{lstlisting} 631 632 Note that stmt1, stmt2, \ldots stmt\_default may contain "break" statements, 633 which have the effect of exiting the switch statement. In the absence of break, 634 the execution falls through each case sequentially. In our current implementation, 635 we produce an equivalent sequence of ``ifthen'' chained by gotos: 636 \begin{lstlisting}[language=C] 637 fresh = e; 638 if(fresh == v1) { 639 $\llbracket$stmt1$\rrbracket$; 640 goto lbl_case2; 641 }; 642 if(fresh == v2) { 643 lbl_case2: 644 $\llbracket$stmt2;$\rrbracket$ 645 goto lbl_case2; 646 }; 647 $\llbracket$stmt_default$\rrbracket$; 648 exit_label: 649 \end{lstlisting} 650 651 The proof had to tackle the following points: 652 \begin{itemize} 653 \item the source and target memories are not the same (cf. fresh variable), 654 \item the flow of control is changed in a nonlocal way (e.g. \textbf{goto} 655 instead of \textbf{break}). 656 \end{itemize} 657 658 In order to tackle the first point, we implemented a version of memory 659 extensions similar to Compcert's. What has been done is the simulation proof 660 for all ``easy'' cases, that do not interact with the switch removal per se, 661 plus a bit of the switch case. This comprises propagating the memory extension 662 through each statement (except switch), as well as various invariants that 663 are needed for the switch case (in particular, freshness hypotheses). The 664 details of the evaluation process for the source switch statement and its 665 target counterpart can be found in the file \textbf{switchRemoval.ma}, 666 along more details on the transformation itself. 667 668 Proving the correctness of the second point would require reasoning on the 669 semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight} 670 semantics, this is implemented as a functionwide lookup of the target label. 671 The invariant we would need is the fact that a global label lookup on a freshly 672 created goto is equivalent to a local lookup. This would in turn require the 673 propagation of some freshness hypotheses on labels. For reasons expressed above, 674 we decided to omit this part of the correctness proof. 675 676 \paragraph{Clight to Cminor} 677 678 This pass is the last one operating on the Clight intermediate language. 679 Its input is a full \textsf{Clight} program, and its output is a \textsf{Cminor} 680 program. Note that we do not use an equivalent of the C\#minor language: we 681 translate directly to Cminor. This presents the advantage of not requiring the 682 special loop constructs, nor the explicit block structure. Another salient 683 point of our approach is that a significant part of the properties needed for 684 the simulation proof were directly encoded in dependently typed translation 685 functions. This concerns more precisely freshness conditions and welltypedness 686 conditions. The main effects of the transformation from \textsf{Clight} to 687 \textsf{Cminor} are listed below. 688 689 \begin{itemize} 690 \item Variables are classified as being either globals, stackallocated 691 locals or potentially registerallocated locals. The value of registerallocated 692 local variables is moved out of the modelled memory and stored in a 693 dedicated environment. 694 \item In Clight, each local variable has a dedicated memory block, whereas 695 stackallocated locals are bundled together on a functionbyfunction basis. 696 \item Loops are converted to jumps. 697 \end{itemize} 698 699 The first two points require memory injections which are more flexible that those 700 needed in the switch removal case. In the remainder of this section, we briefly 701 discuss our implementation of memory injections, and then the simulation proof. 702 703 \subparagraph{Memory injections} 704 705 Our memory injections are modelled after the work of Blazy \& Leroy. 706 However, the corresponding paper is based on the first version of the 707 Compcert memory model, whereas we use a much more concrete model, allowing bytelevel 708 manipulations (as in the later version of Compcert's memory model). We proved 709 roughly 80 \% of the required lemmas. Some difficulties encountered were notably 710 due to some too relaxed conditions on pointer validity (problem fixed during development). 711 Some more conditions had to be added to take care of possible overflows when converting 712 from \textbf{Z} block bounds to $16$ bit pointer offsets (in pratice, these overflows 713 only occur in edge cases that are easily ruled out  but this fact is not visible 714 in memory injections). Concretely, some of the lemmas on the preservation of simulation of 715 loads after writes were axiomatised, for lack of time. 716 717 \subparagraph{Simulation proof} 718 719 The correction proof for this transformation was not terminated. We proved the 720 simulation result for expressions and for some subset of the critical statement cases. 721 Notably lacking are the function entry and exit, where the memory injection is 722 properly set up. As can be guessed, a significant amount of work has to be performed 723 to show the conservation of all invariants at each simulation step. 724 725 \todo{list cases, explain while loop, explain labeling problem} 726 581 727 \section{Checking cost labelling properties} 582 728
Note: See TracChangeset
for help on using the changeset viewer.