# Changeset 3222

Ignore:
Timestamp:
Apr 30, 2013, 11:45:00 AM (6 years ago)
Message:

added pages to included papers. final version.

Files:
5 edited

Unmodified
Removed
• ## Deliverables/D4.4/mauro.tex

 r3213 An instance of the record \verb=sem_graph_params= contains all common information about programs of a joint-language whose source code can be logically organized as a graph. Thus, every program of this kind will be an ihabitant of the type \verb=joint_program p=, where \verb=p= is an istance of \verb=sem_graph_params=. We want to stress that such a record Thus, every program of this kind will be an inhabitant of the type \verb=joint_program p=, where \verb=p= is an instance of \verb=sem_graph_params=. We want to stress that such a record is in a sub-type relation with the record \verb=params=, which was explained in  Deliverable 4.3. In order to establish the correctness of our cost-model in each compiler's backend pass, where both source and target programs are joint-graph-programs, i.e. the source program \verb=src= (resp. the target program \verb=out=) is such that there is a \verb=p_in= (resp. \verb=p_out=) of type \verb=sem_graph_params= such that \verb=src : joint_program p_in= (resp. \verb=out : joint_program p_out=), we would like to In order to establish the correctness of our cost-model in each compiler's back-end pass, where both source and target programs are joint-graph-programs, i.e.\ the source program \verb=src= (resp.\ the target program \verb=out=) is such that there is a \verb=p_in= (resp.\ \verb=p_out=) of type \verb=sem_graph_params= such that \verb=src : joint_program p_in= (resp.\ \verb=out : joint_program p_out=), we would like to prove a statement similar to this shape. \begin{lstlisting} Since traces carry both extensional and intensional information, the main disadvantage with this approach is that the extensional part of the proof (for example the preservation the semantical relation between states of the program under evaluation) and the intensional part (for example, all proof obbligation dealing with the preservation the semantic relation between states of the program under evaluation) and the intensional part (for example, all proof obligation dealing with the presence of a cost label in some point of the code) are mixed together in a not very clear way. Furthermore, some proof obbligations concerning the relation among program counters Furthermore, some proof obligations concerning the relation among program counters (for example, the call relation between states which is one of the field of \verb=status_rel= record) depend only on the way the translation from source to target program is done. In particular if the translation satisfies some suitable properties, then it is possible to define some standard relations'' that automatically satisfy these proof obbligations, to define some standard relations'' that automatically satisfy these proof obligations, in an independent way from the specific source and target languages. So our question is wether there is a way to use these observation in order to factorize all common So our question is whether there is a way to use these observation in order to factorize all common aspects of all correctness proofs of each pass involving joint languages. The aim is having a layer on top of the one talking about traces, that ask the user wishing to prove the correctness of a single pass involving two joint-languages, to provide some semnatical state relation that the correctness of a single pass involving two joint-languages, to provide some semantic state relation that satisfies some conditions. These conditions never speak about traces and they are mostly extensional, with the intesional part being limited to some additional requirred properties of the translation. This layer will use the trace machineary in order to deliver the desired correctness extensional, with the intensional part being limited to some additional required properties of the translation. This layer will use the trace machinery in order to deliver the desired correctness proof of the pass. In order to reach this goal, we have to analyze first whether there is a common way to perform language translation for each pass. After having defined and specified the translation machienary, we will explain how it is possibile to use it in order to build such a layer. So this section is organized as follows: in the first part we explain the translation machienary while in the second part we explain such a layer. In order to reach this goal, we have to analyse first whether there is a common way to perform language translation for each pass. After having defined and specified the translation machinery, we will explain how it is possible to use it in order to build such a layer. So this section is organized as follows: in the first part we explain the translation machinery while in the second part we explain such a layer. \subsection{Graph translation} translation of a program in terms of the way we translate each internal function. Thus, if we let \verb=src_g_pars= and \verb=dst_g_pars= being the graph parameters of respectively the source and the target program, the aim is writing a Matita's function that takes as input an object of type the target program, the aim is writing a \s{matita}'s function that takes as input an object of type \verb=joint_closed_internal_function src_g_pars= together with additional information (that we will explain better later) and gives as output an object of type bind_new_instantiates ?? data' data regs ∧ b_graph_translate_props … data' def_in def_out f_lbls f_regs. ........ \end{lstlisting} \subsubsection{Input requested by the translation process} Clearly, \verb=b_graph_translate= takes as input the internal function of the source language we want to translate. But it also takes in input some useful infomrmation which will be used in order to dictate the translation process. These information are all contained in an instance of the following record. But it also takes in input some useful information which will be used in order to dictate the translation process. These informations are all contained in an instance of the following record, where we skip some technical details. \begin{lstlisting} ; f_step : label → joint_step src globals → bind_step_block dst globals ; f_fin : label → joint_fin_step src → bind_fin_block dst globals ; good_f_step : ∀l,s.bind_new_P' ?? (λlocal_new_regs,block.let 〈 pref, op, post 〉 ≝ block in ∀l. let allowed_labels ≝ l :: step_labels … s in let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in All (label → joint_seq ??) (λs'.step_labels_and_registers_in … allowed_labels allowed_registers (step_seq dst globals (s' l))) pref ∧ step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧ All (joint_seq ??) (step_labels_and_registers_in … allowed_labels allowed_registers) post) (f_step l s) ; good_f_fin : ∀l,s.bind_new_P' ?? (λlocal_new_regs,block.let 〈 pref, op 〉 ≝ block in let allowed_labels ≝ l :: fin_step_labels … s in let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in All (joint_seq ??) (λs.step_labels_and_registers_in … allowed_labels allowed_registers s) pref ∧ fin_step_labels_and_registers_in … allowed_labels allowed_registers op) (f_fin l s) ; good_f_step : … ; good_f_fin : … ; f_step_on_cost : ∀l,c.f_step l (COST_LABEL … c) = } \end{lstlisting} We will now summarize what each field means and how it is used in the translation process. We will say that an identifier of a pseudo-register (resp. a code point) is {\em fresh} when it never appears in the code of the source function. \begin{center} \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} Field & Explanation \\ \autoref{tab:translate_data} summarizes what each field means and how it is used in the translation process. We will say that an identifier of a pseudo-register (resp.\ a code label) is {\em fresh} when it never appears in the code of the source function. \begin{table} \centering \begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}} Field & Explanation \\[5pt] \hline \texttt{init\_ret} & It tells how to fill the field \texttt{joint\_if\_result}, i.e. it tells what is the translation of the result for the translated function.\\ \texttt{init\_params} & It tells how to fill the field \texttt{joint\_if\_params}, i.e. it tells what is the translation of the formal parameters of the translated function.\\ \texttt{init\_stack\_size} & It tells how to fill the field \texttt{joint\_if\_stacksize} of the translated function, which is used in orderto deal with cost model of stack usage. \\ \texttt{added\_prologue} & It is a list of sequential statements of the target language which is always added at the beginning of the translated function. \\ \texttt{new\_regs} & It is a list of identifiers for fresh pseudo-registers that are used by statements in \texttt{added\_prologue}. \\ \texttt{f\_step} & It is a function that tells how to translate all {\em step statements} i.e. statements admitting a syntactical successor. Statements of this kind are all sequential statements, a cost emission statement, a call statement and a conditional statement: in the two latter cases the syntactical successors are respectively the returning address (at the end of a function call) and the code-point of the instruction the execution flow will jump in case the guard of the conditional is evaluated to false. \\ \texttt{f\_fin} & It is a function that tells how to translate all {\em final statements} i.e. statements do not admitting a syntactical successor. Statements of this kind are return statements, unconditioned jump statements and tailcalls.\\ \texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that all identifier (pseudo-registers or code points) used by the block of step statements being the translation of a step statement either come from the statement being translated or they are fresh and generated by the universe field of the translated function (\verb=joint_if_luniverse= in case of code point identifier or \verb=joint_if_runiverse= in case of pseudo-register identifier).  \\ \texttt{good\_f\_fin} & It tells that the translation function of all final statements is well formed. Such a condition is similar to the one given for step statements.\\ \texttt{f\_step\_on\_cost} and \texttt{cost\_in\_f\_step}& It gives a particular restriction on the translation of a cost-emission statement: it tells that the translation of a cost-emission has to be the identity, i.e. it should be translated as the same cost-emission statement. Furthermore, the translation never introduce new cost-emission statements which do not correspond to a cost emission in the source. \texttt{init\_ret} & It tells where the result for the translated function is stored.\\[5pt] \texttt{init\_params} & It tells what is the translation of the formal parameters.\\[5pt] \texttt{init\_stack\_size} & It tells how to fill the field \texttt{joint\_if\_stacksize} of the translated function, which tells how much stack is required by the function at the given stage of compilation. \\[5pt] \texttt{added\_prologue} & It is a list of sequential statements of the target language which is always added at the beginning of the translated function. \\[5pt] \texttt{new\_regs} & It is a list of identifiers for fresh pseudo-registers that are generated when instantiating this record. They are typically used to store data that must be saved across the call (e.g.\ the return address popped from the internal stack).\\[5pt] \texttt{f\_step} & It is a function that tells how to translate all {\em step statements} i.e.\ statements admitting a syntactical successor. Statements of this kind are sequential statements, a cost emission statement, a call statement or a conditional statement: in the two latter cases the syntactical successors are respectively the returning address (at the end of a function call) and the point where the flow will continue in case the guard is false. \\[5pt] \texttt{f\_fin} & As above, but for {\em final statements} i.e.\ statements do not admitting a syntactical successor. Statements of this kind are return and unconditioned jump statements.\\[5pt] \texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that the block \verb=f_step I= for a step \verb=I= only uses code labels and register appearing in \verb=I=, \verb=new_regs= or generated by the appropriate identifier universe fields of the translated function. \\[5pt] \texttt{good\_f\_fin} & As above, but for \verb=f_fin=.\\[5pt] \texttt{f\_step\_on\_cost}, \texttt{cost\_in\_f\_step}& They give a particular restriction on the translation of a cost-emission statement: it tells that the translation of a cost-emission has to be the identity, i.e.\ it should be translated as the same cost-emission statement. Furthermore, the translation never introduce new cost-emission statements which do not correspond to a cost emission in the source.\\[5pt] \end{tabular*} \end{center} \caption{The explanation of the various fields of the \verb=b_graph_translate_data= record.} \label{tab:translate_data} \end{table} \subsubsection{Output given the translation process} instruction of the block has $l$ as code point identifier and all succeeding instructions of the block have fresh code points identifiers. Furthermore statements of this block may use fresh identifiers of pseudo-registers or (even worste) they may use some fresh code-point identifiers being generated by the translation (we will see later (even worse) they may use some fresh code-point identifiers being generated by the translation (we will see later that this will be important when translating a call statement). We will use the above mentioned functions to retrieve this information. \verb=f_lbls= takes in input an identifier $l$ for a code point in the ; freshness_lbls : (∀l.All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l)) (λlbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧ in_universe … lbl (joint_if_luniverse … def_out)) (f_lbls l)) ; freshness_regs : (∀l.All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l)) (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧ in_universe … reg (joint_if_runiverse … def_out)) (f_regs l)) ; freshness_data_regs : All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ fresh_for_univ … reg (joint_if_runiverse … def_out)) All … (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧ in_universe … reg (joint_if_runiverse … def_out)) (new_regs … data) ; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False ; prologue_ok : if not_emptyb … (added_prologue … data) then ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ ∃lbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧ joint_if_entry … def_out -( 〈 [ ],λ_.COST_LABEL … (get_first_costlabel … def_in), }. \end{lstlisting} We will now summarize the meaning of each field of the record using the same approach followed in the previous subsection. \begin{center} \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} Field & Explanation \\ \autoref{tab:translate_props} summarizes the meaning of each field of the record. \begin{table} \centering \begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}} Field & Explanation \\[5pt] \hline \texttt{res\_def\_out\_eq} & It tells that the result of the translated function is the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\ \texttt{pars\_def\_out\_eq} & It tells that the formal parameters of the translated function are the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\ \texttt{ss\_def\_out\_eq} & It tells that the \verb=joint_if_stacksize= field of the translated function is the one specified in the suitable field of the record of type \verb=b_graph_translate_data= provided in input. \\ \texttt{partition\_lbls} & All lists of code-point identifiers generated by distinct code point identifiers of the code of the source internal function are pairwise disjoint and every fresh identifier of the list appears at most once, without any repetition. \\ \texttt{partition\_regs} & All lists of pseudo-register identifiers generated by distinct code point identifiers of the code of the source internal function are pairwise disjoint and every fresh identifier of the list appears at most once, without any repetion. \\ \texttt{freshness\_lbls} & All lists of code-point identifiers generated by a code-point of the code of the source internal function are fresh.  \\ \texttt{freshness\_regs} & All lists of pseudo-register identifiers generated by a code-point of the code of the source internal function are fresh.  \\ \texttt{freshness\_data\_regs} & All identifiers of pseudo-register being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\ \texttt{data\_regs\_disjoint} &  All identifiers of pseudo-register being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input never appear in any list of pseudo-register identifiers generated by a code-point of the code of the source internal function. \\ \texttt{res\_def\_out\_eq}, \texttt{pars\_def\_out\_eq}, \texttt{ss\_def\_out\_eq}& The return value location, the formal parameters and the syntactic stack size are all as dictated by the corresponding \verb=b_graph_translate_data= fields.\\[5pt] \texttt{partition\_lbls}, \texttt{partition\_regs}& \verb=f_lbls= and \verb=f_regs= are partial partitions, i.e.\ all lists in their image are repetition-free and disjoint for different input values. \\[5pt] \texttt{freshness\_lbls}, \texttt{freshness\_regs}, \texttt{freshness\_data\_regs}& All lists of code-point identifiers and register generated at a source code-point, and the registers in \verb=new_regs= are fresh: they were not in the former source universe and they are in the new one.\\[5pt] & All identifiers of pseudo-register being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\[5pt] \texttt{data\_regs\_disjoint} &  All pseudo-register in \texttt{new\_regs} never appear in \verb=f_regs=. \\[5pt] \texttt{multi\_fetch\_ok} & Given a statement $I$ and a code-point identifier $l$ of the source internal function such that $I$ is located in $l$, if the translation process translate $I$ into a statement block $\langle I_1,\ldots ,I_n\rangle$ then $f\_lbls(l) = [l_1,\ldots,l_{n-1}]$ in the translated source code we have that $I_1$ is located in $l$ with $l1$ as syntactical successor, $I_2$ is located in $l_1$ with $l_2$ as syntactical successor, and so on with the last statement $I_n$ located in $l_{n-1}$ and it may have a syntactical successor depending wether $I$ is a step-statement or not: in the former case we have that the syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\ \texttt{prologue\_ok} & If the field \texttt{added\_prologue} of the record of type \verb=b_graph_translate_data= provided in input is empty, then the code-point identifier of the first instruction of the translated function is the same of the one of the source internal function. Otherwise the two code points are different, with the first instruction of the translated function being a cost-emission statement followed by the instructions of  \texttt{added\_prologue}; the last instruction of \texttt{added\_prologue} has an identifier $l$ as syntactical successor and $l$ is the same identifier as the one of the first instruction of the source internal function and in $l$ we fetch a NOOP instruction. and it may have a syntactical successor depending whether $I$ is a step-statement or not: in the former case we have that the syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\[5pt] \texttt{prologue\_ok} & If the field \texttt{added\_prologue} of the record of type \verb=b_graph_translate_data= provided in input is empty, then the code-point identifier of the first instruction of the translated function is the same of the one of the source internal function. Otherwise the two code points are different, with the first instruction of the translated function being a cost-emission statement followed by the instructions of  \texttt{added\_prologue}; the last instruction of \texttt{added\_prologue} has an identifier $l$ as syntactical successor and $l$ is the same identifier as the one of the first instruction of the source internal function and in $l$ we fetch a \s{NOP} instruction. \end{tabular*} \end{center} \caption{The explanation of the various fields of the \verb=b_graph_translate_props= record.} \label{tab:translate_props} \end{table} \subsection{A general correctness proof} In order to prove our general result, we need to define the usual semantical (data) relation among states of the source and target language and call relation between states. We remind that two states are in call relation whenever a call statement is fetched at state's current program counter. These two relations have to satify some condition, already explained at the beginning of this deliverable (see Section ??). In this section we will give some general conditions that these two relations have to satisfy in order to obtain the desired simulation result. We begin our analysis from the latter relation (the call one) and then we show how to relate it with a semantical relation satisfying some conditions that allow us to prove our general result. In order to prove our general result, we need to define the usual semantic (data) relation among states of the source and target language and call relation between states. We remind that two states are in call relation whenever a call statement is fetched at state's current program counter. These two relations have to satisfy some condition, already explained at the beginning of this deliverable (see Section ??). In this section we will give some general conditions that these two relations have to satisfy in order to obtain the desired simulation result. We begin our analysis from the latter relation (the call one) and then we show how to relate it with a semantic relation satisfying some conditions that allow us to prove our general result. \subsubsection{A standard calling relation} Two states are in call relation whenever it is possible to fetch a call statement at the program counter given by the two states. We will explot the properties of the translation explained in previous subsection in order to define a standard calling relation. We remind that the translation of a given statement $I$ is a block of statements $b= \langle I_1,\ldots I_n\rangle$ with $n \geq 1$. When $I$ is a call, then we will require that there is a unique $k \in [1,n]$ such $I_k$ has to be a call statement (we will see the formalization of this condition in the following subsection when we relate the calling relation with the semantical one). The idea of defining a standard calling relation is to compute the code-point identifier of this $I_k$, starting from the code-point identifier of the statement $I$ in the code of the source internal function. We will see how to use the information provided by the translation process (in particular the function \verb=f_lbls=) in order to obtain this result. We will see that, for technical reason, we will compute the code point of $I$ starting from the code point of $I_k$. In order to explain how this machienary work. we need to enter more in the detail of the translation process. Given a step-statement Two states are in call relation whenever it is possible to fetch a call statement at the program counter given by the two states. We will exploit the properties of the translation explained in previous subsection in order to define a standard calling relation. We remind that the translation of a given statement $I$ is a block of statements $b= \langle I_1,\ldots I_n\rangle$ with $n \geq 1$. When $I$ is a call, then we will require that there is a unique $k \in [1,n]$ such $I_k$ has to be a call statement (we will see the formalization of this condition in the following subsection when we relate the calling relation with the semantic one). The idea of defining a standard calling relation is to compute the code-point identifier of this $I_k$, starting from the code-point identifier of the statement $I$ in the code of the source internal function. We will see how to use the information provided by the translation process (in particular the function \verb=f_lbls=) in order to obtain this result. We will see that, for technical reason, we will compute the code point of $I$ starting from the code point of $I_k$. In order to explain how this machinery work. we need to enter more in the detail of the translation process. Given a step-statement $I$, formally its translation is a triple $f\_step(s) = \langle pre,p,post \rangle$ such that $pre$ is a list of sequential statements called {\em preamble}, $p$ is a step-statement (we call it {\em pivot}) and $post$ is again a list of sequential statements called {\em postamble}. When $pre = [s_1,\ldots,s_n]$ and $post = [s_1',\ldots,s_m']$, the corresponding block being the translation of $I$ is $\langle s_1,\ldots,s_n,p,s_1',\ldots,s_m'\rangle$. In case $I$ is a final statement, than its translation does not have postable, i.e. it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement. postamble, i.e.\ it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement. Given a statement $I$ at a given code point $l$ in the source internal function and given the pivot statement $p$ of the translation in case the preamble is empty, for the property of the translation process we have then $l = l'$, while if the preamble is non-empty. then $l'$ is $n-1$-th element of $f\_lbls(l)$, where $n \geq 0$ is the length of the preamble. The Matita's definition computing the code points according to the above mentioned specification is the following one. The \s{matita}'s definition computing the code points according to the above mentioned specification is the following one. \begin{lstlisting} definition sigma_label : ∀p_in,p_out : sem_graph_params. ! ← res_to_opt … (fetch_internal_function … (joint_globalenv p_in prog stack_size) bl); ! ← find ?? (joint_if_code ?? fn) (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with ! ← find ?? (joint_if_code ?? fn) (λlbl.λ_. match preamble_length … prog stack_size init init_regs f_regs bl lbl with [ None ⇒ false | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with \end{lstlisting} This function takes in input all the information provided by the translation process (in particular the function $f\_lbls$), a function location and a code-point identifier $l$; it fetches the internal function of the source language in the correponding location. function location and a code-point identifier $l$; it fetches the internal function of the source language in the corresponding location. Then it unfolds the code of the fetched function looking for a label $l'$ and a statement $I$ located in $l'$, such that, either $l = l'$ in case the preamble of the translation of $I$ is empty or $l'$ is the $n -1$-th where $n \geq 0$ is the length We can prove that, starting from a code point identifier of the translated internal function, whenever there exists a code-point identifier in the source internal function satifying the above condition, then it is always unique. whenever there exists a code-point identifier in the source internal function satisfying the above condition, then it is always unique. The properties \verb=partition_lbls= and \verb=freshness_lbls= provided by the translation process are crucial in the proof of this statement. We can wrap this function inside the definition of the desired relation among program counter states in the following way We can wrap this function inside the definition of the desired relation between program counter states in the following way The conditional at the beginning is put to deal with the pre-main case, which is translated without following the standard translation process we explain in previous section. translation process we explained in previous section. \begin{lstlisting} definition sigma_pc_opt : The main result about the program counter relation we have defined is the following. If we fetch a statement $I$ in at a given program counter $pc$ in the source program, then there is a program counter $pc'$ in the target program which is in relation with $pc$ (i.e. $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot statement of the tranlation. The formalization of this statement in Matita is given in the following. which is in relation with $pc$ (i.e.\ $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot statement of the translation. The formalization of this statement in \s{matita} is given in the following. \begin{lstlisting} (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call. λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call. pc ? s1 = sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)). pc ? s1 = sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)). \end{lstlisting} use the translation process we explain in the previous section. \subsubsection{The semantical relation} The semantical relation between states is the classical relation used in forward simulation proofs. It correlates the data of the status (e.g. register, memory, etc.). We remind that the notion of state \subsubsection{The semantic relation} The semantic relation between states is the classical relation used in forward simulation proofs. It correlates the data of the status (e.g. register, memory, \emph{etc}). We remind that the notion of state in joint language is summarized in the following record. \begin{lstlisting} when executing a return instruction. The type of the semantical relation between state is the following. The type of the semantic relation between state is the following. \begin{lstlisting} \end{lstlisting} We would like to state some conditions the semantical relation between states have to satisfy in order We would like to state some conditions the semantic relation between states have to satisfy in order to get our simulation result. We would like that this relation have some flavour of compositionality. In particular we would like that it depends strictly on the contents of the field \verb=st_no_pc=, i.e. the field that really contains data information of the state. So we need also a data relation, i.e. the field that really contains data information of the state. So we need also a data relation, i.e.\ a relation of this type. Notice that the data relation cab depend on a specific program counter of the source. This is done to capture complex data relations like the ones in the ERTL to LTL pass, in which you need to know where data in pseudoregisters of ERTL are stored by the translation (either in hardware register or to capture complex data relations like the ones in the \s{ERTL} to \s{LTL} pass, in which you need to know where data in pseudo-registers of \s{ERTL} are stored by the translation (either in hardware register or in memory) and this information depends on the code point on the statement being translated. % \end{lstlisting} % Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantical Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantic relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates that two states that are in semantical relation should have the same program counter. This is due that two states that are in semantic relation should have the same program counter. This is due to the way the translation is performed. In fact a statement $I$ at a code point $l$ in the source internal function is translated with a block of instructions in the translated internal function whose initial statement is at the same code point $l$. Condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok} postulates that two states that are in semantical relation have the last popped calling address whose initial statement is at the same code point $l$. The condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok} postulates that two states that are in semantic relation have the last popped calling address in call relation. Finally \texttt{st\_rel\_def} postulates that given two states having the same program counter, the last pop fields in call relation and the data fields also in data relation, then they are in semantical relation. they are in semantic relation. Another important condition is that the pivot statement of the translation of a call statement is % \end{lstlisting} The conditions we are going to present now are standard semantical commutation lemmas that are commonly The conditions we are going to present now are standard semantic commutation lemmas that are commonly used when proving the correctness of the operational semantics of many imperative languages. We introduce some notation. We will use $I,J\ldots$ to range over by statements. We will use $l_1,\ldots,l_n$ to range over by code point identifiers. over by states of programs of the source language. We will use $s_2,s_2',s_2'',\ldots$ to range over by states of programs of the target language. We denote respectively with $\simeq_{S}$, $\simeq_C$ and $\simeq_L$ the semantical relation, the call relation and the cost-label relation between states. These relations have the semantic relation, the call relation and the cost-label relation between states. These relations have been introduced at the beginning of this Deliverable (see Section ??). If $instr = [I_1,\ldots,I_n]$ is a list of instructions, then we write $s_i \stackrel{instr}{\longrightarrow} s_i'$ ($i \in [1,2]$) when $s_i'$ is In order to get the commutation of pre-main instructions (states whose function location of program counter is -1), we have to prove the following condition: for all $s_1,s_1',s_2$ such that $s_1 \stackrel{I}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$, then there exists an $s_2'$ such that $s_2 \stackrel{J}{\longrightarrow} s_2'$ and $s_1 \simeq_S s_2'$ i.e. such that the following then there exists an $s_2'$ such that $s_2 \stackrel{J}{\longrightarrow} s_2'$ and $s_1 \simeq_S s_2'$ i.e.\ such that the following diagram commutes. $$\begin{itemize} \item there are s_2^{fin} and s_2' such that s_2 \stackrel{\pi_1(f\_step(COND \ r \ l))}{\longrightarrow} s_2^{fin}, s_2^{fin} \stackrel{\pi_2(f\_step(COND \ r \ l))} s_2' and s_1' \simeq_S s_2', i.e. the following diagram commutes s_2^{fin} \stackrel{\pi_2(f\_step(COND \ r \ l))} s_2' and s_1' \simeq_S s_2', i.e.\ the following diagram commutes$$ \xymatrix{ into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the following way. For all $s_1,s_1',s_2$ such that $s_1 \stackrel{I}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$ then there is $s_2'$ such that $s_2 \stackrel{f\_step(I)}{\longrightarrow} s_s'$ and $s_1' \simeq_S s_2'$, i.e. such that there is $s_2'$ such that $s_2 \stackrel{f\_step(I)}{\longrightarrow} s_s'$ and $s_1' \simeq_S s_2'$, i.e.\ such that the following diagram commutes.  \paragraph{Commutation of call statement (\verb=call_commutation=).} For all $s_1,s_1',s_2$ such that $s_1 \stackrel{CALL \ id \ arg \ dst}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$ and the statement fetched in the translated language at the program counter being in call relation with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL id' \ arg' \ dst'$ For all $s_1,s_1',s_2$ such that we have $s_1 \stackrel{CALL \ id \ arg \ dst}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$ and the statement fetched in the target function at the program counter in call relation with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL \ id' \ arg' \ dst'$ for some $id',ags',dst'$, then there are $s_2^{pre},s_2^{after},s_2'$ such that \begin{itemize} \paragraph{Commutation of return statement (\verb=return_commutation=).} For all $s_1,s_1',s_2$ such that $s_1 \stackrel{RETURN}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$, if $CALL \ id \ arg \ dst$ is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier is the call statement that caused the function call ened by the current return (i.e.\ it is the statement whose code point identifier is the syntactical predecessor of the program counter of $s_1'$), then $\pi_2(f\_fin(RETURN)) = RETURN$, there are $s_2^{pre},s_2^{after},s_2'$ such that $s_2 \stackrel{\pi_1(f\_fin(RETURN))}{\longrightarrow} s_2^{pre}$, \subsubsection{Conclusion} After having provided a semantic relation among states that satifies some conditions that correspond to After having provided a semantic relation among states that satisfies some conditions that correspond to commutation lemmas that are commonly proved in a forward simulation proof, it is possible to prove the general theorem. All these condition are summarized in a propositional record called \verb=good_state_relation=. R init_in init_out. \end{lstlisting} The module formalizing the formal machienary we described in this document consists of about 3000 lines of Matita code. We stress the fact that this machienary proves general properties that do not depend on the specific backend graph compiler pass. The module formalizing the formal machinery we described in this document consists of about 3000 lines of \s{matita} code. We stress the fact that this machinery proves general properties that do not depend on the specific back-end graph compiler pass.
• ## Deliverables/D4.4/paolo.tex

 r3213 \usepackage{listings} \usepackage[all]{xy} % \usepackage{supertabular} \newcommand{\clap}[1]{\hbox to 0pt{\hss#1\hss}} \small Department of Computer Science and Engineering, University of Bologna\\ \small \verb|\{Mauro.Piccolo, Claudio.SacerdotiCoen, Paolo.Tranquilli\}@unibo.it|} \title{Certifying the back end pass of the CerCo annotating compiler} \title{Certifying the back-end pass of the CerCo annotating compiler} \date{} \maketitle \begin{abstract} We present the certifying effort of the back end of the CerCo annotating compiler to 8051 assembly. Apart from the usual effort needed in propagating We present the certifying effort of the back-end of the CerCo annotating compiler to 8051 assembly. Apart from the proofs needed for propagating the extensional part of execution traces, additional care must be taken in order to ensure a form of intensional correctness of the pass, necessary to prove the lifting of computational costs correct. We concentrate here on two prove that the lifting of computational costs is correct. We concentrate here on two aspects of the proof: how stack is dealt with during the pass, and how generic graph language passes can be proven correct from an extensional and intensional point Care must be taken in dealing with the stack. The back-end pass produces a \emph{stack model}: the amount of stack needed by each function (\verb+stack_m+), together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by globals). together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by global variables). While programs in the front end do not fail for stack overflow, the stack information is lifted to source much in the same ways as time consumption information, \label{subfig:stacksame} \end{subfigure} \caption{Comparison between using tight stack sizes across langauges, i.e.\ \caption{Comparison between using tight stack sizes across languages, i.e.\ reading how much stack is required from the function, and using the same stack sizes provided as a parameter to the semantics. We suppose the call stack \subsection{From an unbounded to a bounded stack} The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of The way the \verb+ft_and_tlr+ is propagated is almost everywhere by means of the proof of existence of a special relation between states that is a simulation with respect to execution. There are more details involved than in a usual The third one, defined as \verb+RTL_semantics_unique+, switches to a semantics with a single, bounded stack space, where moreover memory has already been granted to globals too. From this semantics down to \s{LIN}, all data in memory excluding global variables too. From this semantics down to \s{LIN}, all data in memory excluding pieces of program counters remain the same, as specified in \autoref{subsec:evolvingstack}. However in order to show a
• ## Deliverables/D4.4/report.tex

 r3213 \documentclass[11pt, epsf, a4wide]{article} \documentclass[12pt]{article} \usepackage{../style/cerco} \begin{document} \pagenumbering{roman} \thispagestyle{empty} \newpage \vspace*{7cm} \addcontentsline{toc}{section}{Summary} \paragraph{Summary} The deliverable D4.4 is composed of the following parts: whole assembler. \includepdf[pages={-}]{itp2013.pdf} \includepdf[pages={-}]{paolo.pdf} \includepdf[pages={-}]{cpp-2012-asm.pdf} \includepdf[pages={-}]{cpp-2012-policy.pdf} \includepdf[pages={-},addtotoc={1,section,1,Certification of the preservation of structure by a compiler's back-end pass,simulation}]{itp2013.pdf} \includepdf[pages={-},addtotoc={1,section,1,Certifying the back-end pass of the CerCo annotating compiler,backend}]{paolo.pdf} \includepdf[pages={-},addtotoc={1,section,1,On the correctness of an optimising assembler for the Intel MCS-51 microprocessor,asm}]{cpp-2012-asm.pdf} \includepdf[pages={-},addtotoc={1,section,1,On the correctness of a branch displacement algorithm,policy}]{cpp-2012-policy.pdf} \end{document}
• ## Papers/cpp-asm-2012/cpp-2012-asm.tex

 r2416 \begin{document} \pagestyle{plain} \maketitle
• ## Papers/itp-2013/ccexec.tex

 r3213 \begin{document} \pagestyle{plain} \title{Certification of the Preservation of Structure by a Compiler's Back-end Pass\thanks{The project CerCo acknowledges the financial support of the Future and
Note: See TracChangeset for help on using the changeset viewer.