Changeset 3191


Ignore:
Timestamp:
Apr 27, 2013, 5:00:40 PM (4 years ago)
Author:
garnier
Message:

Some more info on cast removal

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3181 r3191  
    651651\todo{don't use loop structures from CompCert, go straight to jumps}
    652652
    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 one-step 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 sub-expression
    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 performance-wise
    688 for small switches. For instance, compilers such as GCC introduce balanced trees
    689 of ``if-then-else'' constructs. However, our implementation strategy is much simpler.
    690 Let us consider the following input statement.
     653\paragraph{Cast simplification.}
     654
     655The parser used in Cerco introduces a lot of explicit type casts.
     656If left as they are, these constructs can greatly hamper the
     657quality of the generated code -- especially as the architecture
     658we consider is an $8$ bit one. In \textsf{Clight}, casts are
     659expressions. Hence, most of the work of this transformation
     660proceeds on expressions. The tranformation proceeds by recursively
     661trying to coerce an expression to a particular integer type, which
     662is in practice smaller than the original one. This functionality
     663is implemented by two mutually recursive functions whose signature
     664is the following.
     665
     666\begin{lstlisting}[language=matita]
     667let 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
     671and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝ $\ldots$
     672\end{lstlisting}
     673
     674The \textsf{simplify\_inside} acts as a wrapper for
     675\textsf{simplify\_expr}. Whenever \textsf{simplify\_inside} encounters
     676a \textsf{Ecast} expression, it tries to coerce the sub-expression
     677to the desired type using \textsf{simplify\_expr}, which tries to
     678perform the actual coercion. In return, \textsf{simplify\_expr} calls
     679back \textsf{simplify\_inside} in some particular positions, where we
     680decided to be conservative in order to simplify the proofs. However,
     681the current design allows to incrementally revert to a more aggressive
     682version, by replacing recursive calls to \textsf{simplify\_inside} by
     683calls to \textsf{simplify\_expr} \emph{and} proving the corresponding
     684invariants -- where possible.
     685
     686The \textsf{simplify\_inv} invariant encodes either the conservation
     687of the semantics during the transformation corresponding to the failure
     688of the transformation (\textsf{Inv\_eq} constructor), or the successful
     689downcast of the considered expression to the target type
     690(\textsf{Inv\_coerce\_ok}).
     691
     692\begin{lstlisting}[language=matita]
     693inductive 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
     704The \textsf{conservation} invariant simply states the conservation
     705of the semantics, as in the \textsf{Inv\_eq} constructor of the previous
     706invariant.
     707
     708\begin{lstlisting}[language=matita]
     709definition 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
     715This invariant is then easily lifted to statement evaluations.
     716The main problem encountered with this particular pass was dealing with
     717inconsistently typed programs, a canonical case being a particular
     718integer constant of a certain size typed with another size. This
     719prompted the need to introduce numerous type checks, complexifying
     720both 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
     725The intermediate languages of the front-end have no jump tables.
     726Hence, we have to compile the \lstinline[language=C]'switch'
     727constructs away before going from \textsf{Clight} to \textsf{Cminor}.
     728Note that this transformation does not necessarily deteriorate the
     729efficiency of the generated code. For instance, compilers such as GCC
     730introduce balanced trees of ``if-then-else'' constructs for small
     731switches. However, our implementation strategy is much simpler. Let
     732us consider the following input statement.
    691733
    692734\begin{lstlisting}[language=C]
     
    701743\end{lstlisting}
    702744
    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,
     745Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default}
     746may contain \lstinline[language=C]'break' statements, which have the
     747effect of exiting the switch statement. In the absence of break, the
     748execution falls through each case sequentially. In our current implementation,
    706749we produce an equivalent sequence of ``if-then'' chained by gotos:
    707750\begin{lstlisting}[language=C]
     
    745788we decided to omit this part of the correctness proof.
    746789
    747 \paragraph{Clight to Cminor}
     790\paragraph{Clight to Cminor.}
    748791
    749792This pass is the last one operating on the Clight intermediate language.
     
    772815discuss our implementation of memory injections, and then the simulation proof.
    773816
    774 \subparagraph{Memory injections}
     817\subparagraph{Memory injections.}
    775818
    776819Our memory injections are modelled after the work of Blazy \& Leroy.
     
    786829loads after writes were axiomatised, for lack of time.
    787830
    788 \subparagraph{Simulation proof}
     831\subparagraph{Simulation proof.}
    789832
    790833The correction proof for this transformation was not terminated. We proved the
Note: See TracChangeset for help on using the changeset viewer.