Changeset 1364


Ignore:
Timestamp:
Oct 13, 2011, 11:11:03 AM (8 years ago)
Author:
mulligan
Message:

finished the report on d4.2. starting d4.3 report

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1362 r1364  
    2020
    2121\lstdefinelanguage{matita-ocaml}
    22   {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
    23    morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
     22  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try},
     23   morekeywords={[2]whd,normalize,elim,cases,destruct},
    2424   morekeywords={[3]type,of},
    2525   mathescape=true,
     
    289289  $\lambda$dest_lbl: label.
    290290  $\lambda$def: rtl_internal_function globals.
    291   $\lambda$prf: |destrs| = |srcrs|. (* assert in caml code *)
     291  $\lambda$prf: |destrs| = |srcrs|. (* assert here *)
    292292    ...
    293293\end{lstlisting}
     
    424424% SECTION.                                                                    %
    425425%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    426 \subsection{Listing of important functions}
    427 \label{subsect.listing.important.functions}
     426\subsection{Listing of important functions and axioms}
     427\label{subsect.listing.important.functions.and.axioms}
     428
     429We list some important functions in the backend compilation:
     430
     431\paragraph{From RTL/RTLabsToRTL.ma}
     432\begin{center}
     433\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     434Title & Description \\
     435\hline
     436\texttt{translate\_stmt} & Translation of an RTLabs statement to an RTL statement \\
     437\texttt{translate\_internal} & Translation of an RTLabs internal function to an RTL internal function \\
     438\texttt{rtlabs\_to\_rtl} & Translation of an RTLabs program to an RTL program
     439\end{tabular*}
     440\end{center}
     441
     442\paragraph{From joint/TranslateUtils.ma}
     443\begin{center}
     444\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     445Title & Description \\
     446\hline
     447\texttt{fresh\_regs} & Generic fresh pseudoregister generation, for any intermediate language \\
     448\texttt{adds\_graph} & Generic means of adding a statement to a graph, for any intermediate language
     449\end{tabular*}
     450\end{center}
     451
     452\paragraph{From RTL/RTLTailcall.ma}
     453\begin{center}
     454\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     455Title & Description \\
     456\hline
     457\texttt{simplify\_statement} & Remove a single tailcall \\
     458\texttt{simplify\_graph} & Remove all tailcalls in the function graph \\
     459\texttt{tailcall\_simplify} & Simplify an RTL program by removing tailcalls
     460\end{tabular*}
     461\end{center}
     462
     463\paragraph{From RTL/RTLToERTL.ma}
     464\begin{center}
     465\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     466Title & Description \\
     467\hline
     468\texttt{translate\_stmt} & Translation of an RTL statement to an ERTL statement \\
     469\texttt{translate\_funct\_internal} & Translation of an RTL internal function to an ERTL internal function \\
     470\texttt{translate} & Translation of an RTL program to an ERTL program
     471\end{tabular*}
     472\end{center}
     473
     474\paragraph{From ERTL/liveness.ma}
     475\begin{center}
     476\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     477Title & Description \\
     478\hline
     479\texttt{analyse} & Dead code analysis
     480\end{tabular*}
     481\end{center}
     482
     483\paragraph{From ERTL/Interference.ma}
     484\begin{center}
     485\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     486Title & Description \\
     487\hline
     488\texttt{build} & The (axiomatised) graph colouring for register and stack slot allocation
     489\end{tabular*}
     490\end{center}
     491
     492\paragraph{From ERTL/ERTLToLTL.ma}
     493\begin{center}
     494\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     495Title & Description \\
     496\hline
     497\texttt{translate\_statement} & Translation of an ERTL statement into multiple LTL statements \\
     498\texttt{translate\_internal} & Translation of an ERTL internal function into an LTL internal function \\
     499\texttt{ertl\_to\_ltl} & Translation of an ERTL program into an LTL program
     500\end{tabular*}
     501\end{center}
     502
     503\paragraph{From LTL/LTLToLIN.ma}
     504\begin{center}
     505\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     506Title & Description \\
     507\hline
     508\texttt{visit} & Visits, in order, every node in the statement graph for linearisation \\
     509\texttt{translate\_stmt} & Translation of an LTL statement to a LIN statement \\
     510\texttt{branch\_compress} & Place holder (currently identity) function for branch compression \\
     511\texttt{translate\_internal} & Translation of an LTL internal function into a LIN internal function \\
     512\texttt{ltl\_to\_lin} & Translation of an LTL program to a LIN program
     513\end{tabular*}
     514\end{center}
     515
     516\paragraph{From LIN/LINToASM.ma}
     517\begin{center}
     518\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
     519Title & Description \\
     520\hline
     521\texttt{translate\_statements} & Translation of a LIN statement to mutliple assembly instructions \\
     522\texttt{translate\_fun\_def} & Translation of a LIN internal function definition into assembly \\
     523\texttt{translate} & Translation of a LIN program into assembly
     524\end{tabular*}
     525\end{center}
    428526
    429527\end{document}
Note: See TracChangeset for help on using the changeset viewer.