Changeset 3191
 Timestamp:
 Apr 27, 2013, 5:00:40 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.4/Report/report.tex
r3181 r3191 651 651 \todo{don't use loop structures from CompCert, go straight to jumps} 652 652 653 \paragraph{Cast simplification} 654 655 The parser used in Cerco introduces a lot of explicit type casts. If left 656 as they are, these casts can greatly hamper the quality of the generated 657 code  especially as the architecture we consider is an $8$ bit one. 658 In \textsf{Clight}, casts are expressions. Hence, most of the work of 659 this transformation proceeds on expressions, and the onestep simulation 660 result one those is easily lifted to statement evaluations. 661 662 \todo{introduce the explicit type signature of the functions below ?} 663 664 The tranformation proceeds by recursively trying to coerce an expression to 665 a particular type, which is in practice a integer type smaller than the 666 original one. This functionality is implemented by two mutually recursive 667 functions: \textbf{simplify\_expr} and \textbf{simplify\_inside}. The latter 668 acts as a wrapper for the first one. Whenever \textbf{simplify\_inside} 669 encounters a \textbf{Ecast} expression, it tries to coerce the subexpression 670 to the desired type using \textbf{simplify\_expr}, which tries to perform the 671 actual coercion. In return, \textbf{simplify\_expr} calls back 672 \textbf{simplify\_inside} in some particular positions, where we decided to 673 be conservative in order to simplify the proofs. However, the current design 674 allows to incrementally revert to a more aggressive version, by replacing 675 recursive calls to \textbf{simplify\_inside} by calls to \textbf{simplify\_expr} 676 \emph{and} proving the corresponding invariants  where possible. 677 678 The main problem encountered with this particular pass was dealing with inconsistently 679 typed programs, a canonical case being a particular integer constant of a certain 680 size typed with another size. This prompted the need to introduce numerous 681 type checks, complexifying both the implementation and the proof. 682 683 \paragraph{Switch removal} 684 685 Our intermediate languages have no jump tables. Hence, we have to compile the 686 \lstinline[language=C]'switch' constructs away before going from \textsf{Clight} to 687 \textsf{Cminor}. Note that this is not necessarily a bad decision performancewise 688 for small switches. For instance, compilers such as GCC introduce balanced trees 689 of ``ifthenelse'' constructs. However, our implementation strategy is much simpler. 690 Let us consider the following input statement. 653 \paragraph{Cast simplification.} 654 655 The parser used in Cerco introduces a lot of explicit type casts. 656 If left as they are, these constructs can greatly hamper the 657 quality of the generated code  especially as the architecture 658 we consider is an $8$ bit one. In \textsf{Clight}, casts are 659 expressions. Hence, most of the work of this transformation 660 proceeds on expressions. The tranformation proceeds by recursively 661 trying to coerce an expression to a particular integer type, which 662 is in practice smaller than the original one. This functionality 663 is implemented by two mutually recursive functions whose signature 664 is the following. 665 666 \begin{lstlisting}[language=matita] 667 let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) 668 : Σresult:bool×expr. 669 ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ $\ldots$ 670 671 and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝ $\ldots$ 672 \end{lstlisting} 673 674 The \textsf{simplify\_inside} acts as a wrapper for 675 \textsf{simplify\_expr}. Whenever \textsf{simplify\_inside} encounters 676 a \textsf{Ecast} expression, it tries to coerce the subexpression 677 to the desired type using \textsf{simplify\_expr}, which tries to 678 perform the actual coercion. In return, \textsf{simplify\_expr} calls 679 back \textsf{simplify\_inside} in some particular positions, where we 680 decided to be conservative in order to simplify the proofs. However, 681 the current design allows to incrementally revert to a more aggressive 682 version, by replacing recursive calls to \textsf{simplify\_inside} by 683 calls to \textsf{simplify\_expr} \emph{and} proving the corresponding 684 invariants  where possible. 685 686 The \textsf{simplify\_inv} invariant encodes either the conservation 687 of the semantics during the transformation corresponding to the failure 688 of the transformation (\textsf{Inv\_eq} constructor), or the successful 689 downcast of the considered expression to the target type 690 (\textsf{Inv\_coerce\_ok}). 691 692 \begin{lstlisting}[language=matita] 693 inductive simplify_inv 694 (ge : genv) (en : env) (m : mem) 695 (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝ 696  Inv_eq : ∀result_flag. $\ldots$ 697 simplify_inv ge en m e1 e2 target_sz target_sg result_flag 698  Inv_coerce_ok : ∀src_sz,src_sg. 699 (typeof e1) = (Tint src_sz src_sg) → (typeof e2) = (Tint target_sz target_sg) → 700 (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) → 701 simplify_inv ge en m e1 e2 target_sz target_sg true. 702 \end{lstlisting} 703 704 The \textsf{conservation} invariant simply states the conservation 705 of the semantics, as in the \textsf{Inv\_eq} constructor of the previous 706 invariant. 707 708 \begin{lstlisting}[language=matita] 709 definition conservation ≝ λe,result. ∀ge,en,m. 710 res_sim ? (exec_expr ge en m e) (exec_expr ge en m result) 711 ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 712 ∧ typeof e = typeof result. 713 \end{lstlisting} 714 715 This invariant is then easily lifted to statement evaluations. 716 The main problem encountered with this particular pass was dealing with 717 inconsistently typed programs, a canonical case being a particular 718 integer constant of a certain size typed with another size. This 719 prompted the need to introduce numerous type checks, complexifying 720 both the implementation and the proof. 721 \todo{Make this a particular case of the more general statement on baking more invariants in the Clight language} 722 723 \paragraph{Switch removal.} 724 725 The intermediate languages of the frontend have no jump tables. 726 Hence, we have to compile the \lstinline[language=C]'switch' 727 constructs away before going from \textsf{Clight} to \textsf{Cminor}. 728 Note that this transformation does not necessarily deteriorate the 729 efficiency of the generated code. For instance, compilers such as GCC 730 introduce balanced trees of ``ifthenelse'' constructs for small 731 switches. However, our implementation strategy is much simpler. Let 732 us consider the following input statement. 691 733 692 734 \begin{lstlisting}[language=C] … … 701 743 \end{lstlisting} 702 744 703 Note that stmt1, stmt2, \ldots stmt\_default may contain "break" statements, 704 which have the effect of exiting the switch statement. In the absence of break, 705 the execution falls through each case sequentially. In our current implementation, 745 Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default} 746 may contain \lstinline[language=C]'break' statements, which have the 747 effect of exiting the switch statement. In the absence of break, the 748 execution falls through each case sequentially. In our current implementation, 706 749 we produce an equivalent sequence of ``ifthen'' chained by gotos: 707 750 \begin{lstlisting}[language=C] … … 745 788 we decided to omit this part of the correctness proof. 746 789 747 \paragraph{Clight to Cminor }790 \paragraph{Clight to Cminor.} 748 791 749 792 This pass is the last one operating on the Clight intermediate language. … … 772 815 discuss our implementation of memory injections, and then the simulation proof. 773 816 774 \subparagraph{Memory injections }817 \subparagraph{Memory injections.} 775 818 776 819 Our memory injections are modelled after the work of Blazy \& Leroy. … … 786 829 loads after writes were axiomatised, for lack of time. 787 830 788 \subparagraph{Simulation proof }831 \subparagraph{Simulation proof.} 789 832 790 833 The correction proof for this transformation was not terminated. We proved the
Note: See TracChangeset
for help on using the changeset viewer.