Changeset 3222 for Deliverables/D4.4
 Timestamp:
 Apr 30, 2013, 11:45:00 AM (7 years ago)
 Location:
 Deliverables/D4.4
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.4/mauro.tex
r3213 r3222 7 7 An instance of the record \verb=sem_graph_params= contains all common information about 8 8 programs of a jointlanguage whose source code can be logically organized as a graph. 9 Thus, every program of this kind will be an i habitant of the type \verb=joint_program p=,10 where \verb=p= is an i stance of \verb=sem_graph_params=. We want to stress that such a record9 Thus, every program of this kind will be an inhabitant of the type \verb=joint_program p=, 10 where \verb=p= is an instance of \verb=sem_graph_params=. We want to stress that such a record 11 11 is in a subtype relation with the record \verb=params=, which was explained in Deliverable 4.3. 12 12 13 In order to establish the correctness of our costmodel in each compiler's back end pass, where14 both source and target programs are jointgraphprograms, i.e. the source program \verb=src=15 (resp. the target program \verb=out=) is such that there is a \verb=p_in=16 (resp. \verb=p_out=) of type \verb=sem_graph_params= such that17 \verb=src : joint_program p_in= (resp. \verb=out : joint_program p_out=), we would like to13 In order to establish the correctness of our costmodel in each compiler's backend pass, where 14 both source and target programs are jointgraphprograms, i.e.\ the source program \verb=src= 15 (resp.\ the target program \verb=out=) is such that there is a \verb=p_in= 16 (resp.\ \verb=p_out=) of type \verb=sem_graph_params= such that 17 \verb=src : joint_program p_in= (resp.\ \verb=out : joint_program p_out=), we would like to 18 18 prove a statement similar to this shape. 19 19 \begin{lstlisting} … … 44 44 Since traces carry both extensional and intensional information, the main disadvantage 45 45 with this approach is that the extensional part of the proof (for example 46 the preservation the semantic al relation between states of the program under evaluation)47 and the intensional part (for example, all proof ob bligation dealing with46 the preservation the semantic relation between states of the program under evaluation) 47 and the intensional part (for example, all proof obligation dealing with 48 48 the presence of a cost label in some point of the code) are mixed together in a not very clear way. 49 49 50 Furthermore, some proof ob bligations concerning the relation among program counters50 Furthermore, some proof obligations concerning the relation among program counters 51 51 (for example, the call relation between states which is one of the field of 52 52 \verb=status_rel= record) depend only on the way the translation from source to target program is done. 53 53 In particular if the translation satisfies some suitable properties, then it is possible 54 to define some ``standard relations'' that automatically satisfy these proof ob bligations,54 to define some ``standard relations'' that automatically satisfy these proof obligations, 55 55 in an independent way from the specific source and target languages. 56 56 57 So our question is w ether there is a way to use these observation in order to factorize all common57 So our question is whether there is a way to use these observation in order to factorize all common 58 58 aspects of all correctness proofs of each pass involving joint languages. 59 59 The aim is having a layer on top of the one talking about traces, that ask the user wishing to prove 60 the correctness of a single pass involving two jointlanguages, to provide some sem naticalstate relation that60 the correctness of a single pass involving two jointlanguages, to provide some semantic state relation that 61 61 satisfies some conditions. These conditions never speak about traces and they are mostly 62 extensional, with the inte sional part being limited to some additional requirred properties of63 the translation. This layer will use the trace machine ary in order to deliver the desired correctness62 extensional, with the intensional part being limited to some additional required properties of 63 the translation. This layer will use the trace machinery in order to deliver the desired correctness 64 64 proof of the pass. 65 65 66 In order to reach this goal, we have to analy ze first whether there is a common way to perform language67 translation for each pass. After having defined and specified the translation machi enary, we will68 explain how it is possib ile to use it in order to build such a layer. So this section is organized as follows:69 in the first part we explain the translation machi enary while in the second part we explain such a layer.66 In order to reach this goal, we have to analyse first whether there is a common way to perform language 67 translation for each pass. After having defined and specified the translation machinery, we will 68 explain how it is possible to use it in order to build such a layer. So this section is organized as follows: 69 in the first part we explain the translation machinery while in the second part we explain such a layer. 70 70 71 71 \subsection{Graph translation} … … 73 73 translation of a program in terms of the way we translate each internal function. Thus, if we let 74 74 \verb=src_g_pars= and \verb=dst_g_pars= being the graph parameters of respectively the source and 75 the target program, the aim is writing a Matita's function that takes as input an object of type75 the target program, the aim is writing a \s{matita}'s function that takes as input an object of type 76 76 \verb=joint_closed_internal_function src_g_pars= together with additional information 77 77 (that we will explain better later) and gives as output an object of type … … 89 89 bind_new_instantiates ?? data' data regs ∧ 90 90 b_graph_translate_props … data' def_in def_out f_lbls f_regs. 91 ........92 91 \end{lstlisting} 93 92 … … 97 96 \subsubsection{Input requested by the translation process} 98 97 Clearly, \verb=b_graph_translate= takes as input the internal function of the source language we want to translate. 99 But it also takes in input some useful infomrmation which will be used in order to dictate the translation process. 100 These information are all contained in an instance of the following record. 98 But it also takes in input some useful information which will be used in order to dictate the translation process. 99 These informations are all contained in an instance of the following record, 100 where we skip some technical details. 101 101 102 102 \begin{lstlisting} … … 111 111 ; f_step : label → joint_step src globals → bind_step_block dst globals 112 112 ; f_fin : label → joint_fin_step src → bind_fin_block dst globals 113 ; good_f_step : 114 ∀l,s.bind_new_P' ?? 115 (λlocal_new_regs,block.let 〈 pref, op, post 〉 ≝ block in 116 ∀l. 117 let allowed_labels ≝ l :: step_labels … s in 118 let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in 119 All (label → joint_seq ??) 120 (λs'.step_labels_and_registers_in … allowed_labels allowed_registers 121 (step_seq dst globals (s' l))) 122 pref ∧ 123 step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧ 124 All (joint_seq ??) 125 (step_labels_and_registers_in … allowed_labels allowed_registers) 126 post) 127 (f_step l s) 128 ; good_f_fin : 129 ∀l,s.bind_new_P' ?? 130 (λlocal_new_regs,block.let 〈 pref, op 〉 ≝ block in 131 let allowed_labels ≝ l :: fin_step_labels … s in 132 let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in 133 All (joint_seq ??) 134 (λs.step_labels_and_registers_in … allowed_labels allowed_registers s) 135 pref ∧ 136 fin_step_labels_and_registers_in … allowed_labels allowed_registers op) 137 (f_fin l s) 113 ; good_f_step : … 114 ; good_f_fin : … 138 115 ; f_step_on_cost : 139 116 ∀l,c.f_step l (COST_LABEL … c) = … … 146 123 } 147 124 \end{lstlisting} 148 We will now summarize what each field means and how it is used in the translation process. We will say that an identifier of 149 a pseudoregister (resp. a code point) is {\em fresh} when it never appears in the code of the source function. 150 \begin{center} 151 \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} 152 Field & Explanation \\ 125 \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 126 a pseudoregister (resp.\ a code label) is {\em fresh} when it never appears in the code of the source function. 127 \begin{table} 128 \centering 129 \begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}} 130 Field & Explanation \\[5pt] 153 131 \hline 154 \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.\\ 155 \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.\\ 156 \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. \\ 157 \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. \\ 158 \texttt{new\_regs} & It is a list of identifiers for fresh pseudoregisters that are used by statements in \texttt{added\_prologue}. \\ 159 \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 codepoint of the instruction the execution flow will jump in case the guard of the conditional is evaluated to false. \\ 160 \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.\\ 161 \texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that all identifier (pseudoregisters 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 pseudoregister identifier). \\ 162 \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.\\ 163 \texttt{f\_step\_on\_cost} and \texttt{cost\_in\_f\_step}& It gives a particular restriction on the translation of a costemission statement: it tells that the translation of a costemission has to be the identity, i.e. it should be translated as the same costemission statement. Furthermore, the translation never introduce new costemission statements which do not correspond to a cost emission in the source. 132 \texttt{init\_ret} & It tells where the result for the translated function is stored.\\[5pt] 133 \texttt{init\_params} & It tells what is the translation of the formal parameters.\\[5pt] 134 \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] 135 \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] 136 \texttt{new\_regs} & It is a list of identifiers for fresh pseudoregisters that are generated when instantiating 137 this record. They are typically used to store data that must be saved across the call (e.g.\ the return address 138 popped from the internal stack).\\[5pt] 139 \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] 140 \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] 141 \texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that 142 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] 143 \texttt{good\_f\_fin} & As above, but for \verb=f_fin=.\\[5pt] 144 \texttt{f\_step\_on\_cost}, \texttt{cost\_in\_f\_step}& They give a particular restriction on the translation of a costemission statement: it tells that the translation of a costemission has to be the identity, i.e.\ it should be translated as the same costemission statement. Furthermore, the translation never introduce new costemission statements which do not correspond to a cost emission in the source.\\[5pt] 164 145 \end{tabular*} 165 \end{center} 146 \caption{The explanation of the various fields of the \verb=b_graph_translate_data= record.} 147 \label{tab:translate_data} 148 \end{table} 166 149 167 150 \subsubsection{Output given the translation process} … … 184 167 instruction of the block has $l$ as code point identifier and all succeeding instructions of the block have 185 168 fresh code points identifiers. Furthermore statements of this block may use fresh identifiers of pseudoregisters or 186 (even wors te) they may use some fresh codepoint identifiers being generated by the translation (we will see later169 (even worse) they may use some fresh codepoint identifiers being generated by the translation (we will see later 187 170 that this will be important when translating a call statement). We will use the above mentioned functions 188 171 to retrieve this information. \verb=f_lbls= takes in input an identifier $l$ for a code point in the … … 213 196 ; freshness_lbls : 214 197 (∀l.All … 215 (λlbl.¬ fresh_for_univ… lbl (joint_if_luniverse … def_in) ∧216 fresh_for_univ… lbl (joint_if_luniverse … def_out)) (f_lbls l))198 (λlbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧ 199 in_universe … lbl (joint_if_luniverse … def_out)) (f_lbls l)) 217 200 ; freshness_regs : 218 201 (∀l.All … 219 (λreg.¬ fresh_for_univ… reg (joint_if_runiverse … def_in) ∧220 fresh_for_univ… reg (joint_if_runiverse … def_out)) (f_regs l))202 (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧ 203 in_universe … reg (joint_if_runiverse … def_out)) (f_regs l)) 221 204 ; freshness_data_regs : 222 All … (λreg.¬ fresh_for_univ… reg (joint_if_runiverse … def_in) ∧223 fresh_for_univ … reg (joint_if_runiverse … def_out))205 All … (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧ 206 in_universe … reg (joint_if_runiverse … def_out)) 224 207 (new_regs … data) 225 208 ; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False … … 242 225 ; prologue_ok : 243 226 if not_emptyb … (added_prologue … data) then 244 ∃lbl.¬ fresh_for_univ… lbl (joint_if_luniverse … def_in) ∧227 ∃lbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧ 245 228 joint_if_entry … def_out 246 229 ( 〈 [ ],λ_.COST_LABEL … (get_first_costlabel … def_in), … … 250 233 }. 251 234 \end{lstlisting} 252 253 We will now summarize the meaning of each field of the record using the same approach followed 254 in the previous subsection. 255 \begin{center} 256 \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} 257 Field & Explanation \\ 235 \autoref{tab:translate_props} summarizes the meaning of each field of the record. 236 \begin{table} 237 \centering 238 \begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}} 239 Field & Explanation \\[5pt] 258 240 \hline 259 \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. \\ 260 \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. \\ 261 \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. \\ 262 \texttt{partition\_lbls} & All lists of codepoint 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. \\ 263 \texttt{partition\_regs} & All lists of pseudoregister 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. \\ 264 \texttt{freshness\_lbls} & All lists of codepoint identifiers generated by a codepoint of the code of the source internal function are fresh. \\ 265 \texttt{freshness\_regs} & All lists of pseudoregister identifiers generated by a codepoint of the code of the source internal function are fresh. \\ 266 \texttt{freshness\_data\_regs} & All identifiers of pseudoregister being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\ 267 \texttt{data\_regs\_disjoint} & All identifiers of pseudoregister 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 pseudoregister identifiers generated by a codepoint of the code of the source internal function. \\ 241 \texttt{res\_def\_out\_eq}, \texttt{pars\_def\_out\_eq}, \texttt{ss\_def\_out\_eq}& 242 The return value location, the formal parameters and the syntactic stack size are 243 all as dictated by the corresponding \verb=b_graph_translate_data= fields.\\[5pt] 244 \texttt{partition\_lbls}, \texttt{partition\_regs}& 245 \verb=f_lbls= and \verb=f_regs= are partial partitions, i.e.\ all lists in their 246 image are repetitionfree and disjoint for different input values. \\[5pt] 247 \texttt{freshness\_lbls}, \texttt{freshness\_regs}, \texttt{freshness\_data\_regs}& 248 All lists of codepoint identifiers and register generated at a source codepoint, and the registers in 249 \verb=new_regs= are fresh: 250 they were not in the former source universe and they are in the new one.\\[5pt] 251 & All identifiers of pseudoregister being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\[5pt] 252 \texttt{data\_regs\_disjoint} & All pseudoregister in \texttt{new\_regs} never appear in \verb=f_regs=. \\[5pt] 268 253 \texttt{multi\_fetch\_ok} & Given a statement $I$ and a codepoint 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 269 254 $f\_lbls(l) = [l_1,\ldots,l_{n1}]$ in the translated source code we have that $I_1$ is located in $l$ with $l1$ as syntactical 270 255 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_{n1}$ 271 and it may have a syntactical successor depending w ether $I$ is a stepstatement or not: in the former case we have that the272 syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\ 273 \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 codepoint 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 costemission 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 NOOPinstruction.256 and it may have a syntactical successor depending whether $I$ is a stepstatement or not: in the former case we have that the 257 syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\[5pt] 258 \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 codepoint 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 costemission 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. 274 259 \end{tabular*} 275 \end{center} 260 \caption{The explanation of the various fields of the \verb=b_graph_translate_props= record.} 261 \label{tab:translate_props} 262 \end{table} 276 263 277 264 \subsection{A general correctness proof} 278 In order to prove our general result, we need to define the usual semantic al (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 semanticalrelation satisfying some conditions that allow us to prove our general result.265 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. 279 266 280 267 \subsubsection{A standard calling relation} 281 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 explo t 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 semanticalone). The idea of defining a standard calling relation is to compute the codepoint identifier of this $I_k$, starting from the codepoint 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$.282 283 In order to explain how this machi enary work. we need to enter more in the detail of the translation process. Given a stepstatement268 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 codepoint identifier of this $I_k$, starting from the codepoint 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$. 269 270 In order to explain how this machinery work. we need to enter more in the detail of the translation process. Given a stepstatement 284 271 $I$, formally its translation is a triple $f\_step(s) = \langle pre,p,post \rangle$ such that $pre$ is a list of sequential 285 272 statements called {\em preamble}, $p$ is a stepstatement (we call it {\em pivot}) and $post$ is again a list of sequential statements 286 273 called {\em postamble}. When $pre = [s_1,\ldots,s_n]$ and $post = [s_1',\ldots,s_m']$, the corresponding block being the translation 287 274 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 288 posta ble, i.e.it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement.275 postamble, i.e.\ it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement. 289 276 290 277 Given a statement $I$ at a given code point $l$ in the source internal function and given the pivot statement $p$ of the translation … … 292 279 in case the preamble is empty, for the property of the translation process we have then $l = l'$, while if the preamble is nonempty. 293 280 then $l'$ is $n1$th element of $f\_lbls(l)$, where $n \geq 0$ is the length of the preamble. 294 The Matita's definition computing the code points according to the above mentioned specification is the following one.281 The \s{matita}'s definition computing the code points according to the above mentioned specification is the following one. 295 282 \begin{lstlisting} 296 283 definition sigma_label : ∀p_in,p_out : sem_graph_params. … … 304 291 ! <id,fn> ← res_to_opt … (fetch_internal_function … 305 292 (joint_globalenv p_in prog stack_size) bl); 306 ! <res,s> ← 307 find ?? (joint_if_code ?? fn)308 (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with293 ! <res,s> ← find ?? (joint_if_code ?? fn) 294 (λlbl.λ_. 295 match preamble_length … prog stack_size init init_regs f_regs bl lbl with 309 296 [ None ⇒ false 310 297  Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with … … 316 303 \end{lstlisting} 317 304 This function takes in input all the information provided by the translation process (in particular the function $f\_lbls$), a 318 function location and a codepoint identifier $l$; it fetches the internal function of the source language in the corre ponding location.305 function location and a codepoint identifier $l$; it fetches the internal function of the source language in the corresponding location. 319 306 Then it unfolds the code of the fetched function looking for a label $l'$ and a statement $I$ located in $l'$, such that, 320 307 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 … … 325 312 326 313 We can prove that, starting from a code point identifier of the translated internal function, 327 whenever there exists a codepoint identifier in the source internal function sati fying the above condition, then it is always unique.314 whenever there exists a codepoint identifier in the source internal function satisfying the above condition, then it is always unique. 328 315 The properties \verb=partition_lbls= and \verb=freshness_lbls= provided by the translation process are crucial in the proof 329 316 of this statement. 330 331 We can wrap this function inside the definition of the desired relation among program counter states in the following way 317 We can wrap this function inside the definition of the desired relation between program counter states in the following way 332 318 The conditional at the beginning is put to deal with the premain case, which is translated without following the standard 333 translation process we explain in previous section.319 translation process we explained in previous section. 334 320 \begin{lstlisting} 335 321 definition sigma_pc_opt : … … 357 343 The main result about the program counter relation we have defined is the following. If we fetch a statement $I$ in 358 344 at a given program counter $pc$ in the source program, then there is a program counter $pc'$ in the target program 359 which is in relation with $pc$ (i.e. $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot360 statement of the tran lation. The formalization of this statement in Matitais given in the following.345 which is in relation with $pc$ (i.e.\ $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot 346 statement of the translation. The formalization of this statement in \s{matita} is given in the following. 361 347 362 348 \begin{lstlisting} … … 404 390 (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call. 405 391 λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call. 406 pc ? s1 = 407 sigma_stored_pcp_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)).392 pc ? s1 = sigma_stored_pc 393 p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)). 408 394 \end{lstlisting} 409 395 … … 412 398 use the translation process we explain in the previous section. 413 399 414 \subsubsection{The semantic alrelation}415 The semantic al relation between states is the classical relation used in forward simulation proofs.416 It correlates the data of the status (e.g. register, memory, etc.). We remind that the notion of state400 \subsubsection{The semantic relation} 401 The semantic relation between states is the classical relation used in forward simulation proofs. 402 It correlates the data of the status (e.g. register, memory, \emph{etc}). We remind that the notion of state 417 403 in joint language is summarized in the following record. 418 404 \begin{lstlisting} … … 428 414 when executing a return instruction. 429 415 430 The type of the semantic alrelation between state is the following.416 The type of the semantic relation between state is the following. 431 417 432 418 \begin{lstlisting} … … 435 421 \end{lstlisting} 436 422 437 We would like to state some conditions the semantic alrelation between states have to satisfy in order423 We would like to state some conditions the semantic relation between states have to satisfy in order 438 424 to get our simulation result. We would like that this relation have some flavour of compositionality. 439 425 In particular we would like that it depends strictly on the contents of the field \verb=st_no_pc=, i.e. 440 the field that really contains data information of the state. So we need also a data relation, i.e. 426 the field that really contains data information of the state. So we need also a data relation, i.e.\ 441 427 a relation of this type. 442 428 … … 447 433 448 434 Notice that the data relation cab depend on a specific program counter of the source. This is done 449 to capture complex data relations like the ones in the ERTL to LTLpass, in which you need to know450 where data in pseudo registers of ERTL are stored by the translation (either in hardware register or435 to capture complex data relations like the ones in the \s{ERTL} to \s{LTL} pass, in which you need to know 436 where data in pseudoregisters of \s{ERTL} are stored by the translation (either in hardware register or 451 437 in memory) and this information depends on the code point on the statement being translated. 452 438 … … 484 470 % \end{lstlisting} 485 471 % 486 Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantic al472 Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantic 487 473 relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates 488 that two states that are in semantic alrelation should have the same program counter. This is due474 that two states that are in semantic relation should have the same program counter. This is due 489 475 to the way the translation is performed. In fact a statement $I$ at a code point $l$ in the source 490 476 internal function is translated with a block of instructions in the translated internal function 491 whose initial statement is at the same code point $l$. Condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok}492 postulates that two states that are in semantic al relation have the last popped calling address477 whose initial statement is at the same code point $l$. The condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok} 478 postulates that two states that are in semantic relation have the last popped calling address 493 479 in call relation. Finally \texttt{st\_rel\_def} postulates that given two states having the same 494 480 program counter, the last pop fields in call relation and the data fields also in data relation, then 495 they are in semantic alrelation.481 they are in semantic relation. 496 482 497 483 Another important condition is that the pivot statement of the translation of a call statement is … … 513 499 % \end{lstlisting} 514 500 515 The conditions we are going to present now are standard semantic alcommutation lemmas that are commonly501 The conditions we are going to present now are standard semantic commutation lemmas that are commonly 516 502 used when proving the correctness of the operational semantics of many imperative languages. We introduce some notation. 517 503 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. … … 519 505 over by states of programs of the source language. We will use $s_2,s_2',s_2'',\ldots$ to range over by 520 506 states of programs of the target language. We denote respectively with $\simeq_{S}$, $\simeq_C$ and $\simeq_L$ 521 the semantic al relation, the call relation and the costlabel relation between states. These relations have507 the semantic relation, the call relation and the costlabel relation between states. These relations have 522 508 been introduced at the beginning of this Deliverable (see Section ??). If $instr = [I_1,\ldots,I_n]$ is a list 523 509 of instructions, then we write $s_i \stackrel{instr}{\longrightarrow} s_i'$ ($i \in [1,2]$) when $s_i'$ is … … 547 533 In order to get the commutation of premain instructions (states whose function location of program counter is 1), we have 548 534 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$, 549 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 following535 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 550 536 diagram commutes. 551 537 $$ … … 578 564 \begin{itemize} 579 565 \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}$, 580 $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 commutes566 $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 581 567 $$ 582 568 \xymatrix{ … … 632 618 into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the 633 619 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 634 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 that620 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 635 621 the following diagram commutes. 636 622 $$ … … 673 659 674 660 \paragraph{Commutation of call statement (\verb=call_commutation=).} 675 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$ and676 the statement fetched in the t ranslated language at the program counter beingin call relation677 with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL id' \ arg' \ dst'$661 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 662 the statement fetched in the target function at the program counter in call relation 663 with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL \ id' \ arg' \ dst'$ 678 664 for some $id',ags',dst'$, then there are $s_2^{pre},s_2^{after},s_2'$ such that 679 665 \begin{itemize} … … 752 738 \paragraph{Commutation of return statement (\verb=return_commutation=).} 753 739 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$ 754 is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier740 is the call statement that caused the function call ened by the current return (i.e.\ it is the statement whose code point identifier 755 741 is the syntactical predecessor of the program counter of $s_1'$), then $\pi_2(f\_fin(RETURN)) = RETURN$, there are 756 742 $s_2^{pre},s_2^{after},s_2'$ such that $s_2 \stackrel{\pi_1(f\_fin(RETURN))}{\longrightarrow} s_2^{pre}$, … … 818 804 819 805 \subsubsection{Conclusion} 820 After having provided a semantic relation among states that sati fies some conditions that correspond to806 After having provided a semantic relation among states that satisfies some conditions that correspond to 821 807 commutation lemmas that are commonly proved in a forward simulation proof, it is possible to prove the 822 808 general theorem. All these condition are summarized in a propositional record called \verb=good_state_relation=. … … 843 829 R init_in init_out. 844 830 \end{lstlisting} 845 The module formalizing the formal machi enary we described in this document consists of about 3000 lines of846 Matita code. We stress the fact that this machienary proves general properties that do not depend on the847 specific back end graph compiler pass.831 The module formalizing the formal machinery we described in this document consists of about 3000 lines of 832 \s{matita} code. We stress the fact that this machinery proves general properties that do not depend on the 833 specific backend graph compiler pass. 
Deliverables/D4.4/paolo.tex
r3213 r3222 11 11 \usepackage{listings} 12 12 \usepackage[all]{xy} 13 % \usepackage{supertabular} 13 14 14 15 \newcommand{\clap}[1]{\hbox to 0pt{\hss#1\hss}} … … 66 67 \small Department of Computer Science and Engineering, University of Bologna\\ 67 68 \small \verb\{Mauro.Piccolo, Claudio.SacerdotiCoen, Paolo.Tranquilli\}@unibo.it} 68 \title{Certifying the back 69 \title{Certifying the backend pass of the CerCo annotating compiler} 69 70 \date{} 70 71 … … 72 73 \maketitle 73 74 \begin{abstract} 74 We present the certifying effort of the back 75 compiler to 8051 assembly. Apart from the usual effort needed inpropagating75 We present the certifying effort of the backend of the CerCo annotating 76 compiler to 8051 assembly. Apart from the proofs needed for propagating 76 77 the extensional part of execution traces, additional care must be taken in 77 78 order to ensure a form of intensional correctness of the pass, necessary to 78 prove th e lifting of computational costs correct. We concentrate here on two79 prove that the lifting of computational costs is correct. We concentrate here on two 79 80 aspects of the proof: how stack is dealt with during the pass, and how generic graph 80 81 language passes can be proven correct from an extensional and intensional point … … 210 211 Care must be taken in dealing with the stack. The backend pass produces a 211 212 \emph{stack model}: the amount of stack needed by each function (\verb+stack_m+), 212 together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by global s).213 together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by global variables). 213 214 While programs in the front end do not fail for stack overflow, the stack 214 215 information is lifted to source much in the same ways as time consumption information, … … 364 365 \label{subfig:stacksame} 365 366 \end{subfigure} 366 \caption{Comparison between using tight stack sizes across lang auges, i.e.\367 \caption{Comparison between using tight stack sizes across languages, i.e.\ 367 368 reading how much stack is required from the function, and using the same 368 369 stack sizes provided as a parameter to the semantics. We suppose the call stack … … 382 383 383 384 \subsection{From an unbounded to a bounded stack} 384 The way the \verb+ft_and_tlr+ is propagated is almost ever where by means of385 The way the \verb+ft_and_tlr+ is propagated is almost everywhere by means of 385 386 the proof of existence of a special relation between states that is a simulation 386 387 with respect to execution. There are more details involved than in a usual … … 418 419 The third one, defined as \verb+RTL_semantics_unique+, switches to a semantics with 419 420 a single, bounded stack space, where moreover memory has already been granted to 420 global s too. From this semantics down to \s{LIN}, all data in memory excluding421 global variables too. From this semantics down to \s{LIN}, all data in memory excluding 421 422 pieces of program counters remain the same, as specified in \autoref{subsec:evolvingstack}. 422 423 However in order to show a 
Deliverables/D4.4/report.tex
r3213 r3222 1 \documentclass[1 1pt, epsf, a4wide]{article}1 \documentclass[12pt]{article} 2 2 3 3 \usepackage{../style/cerco} … … 47 47 48 48 \begin{document} 49 49 \pagenumbering{roman} 50 50 \thispagestyle{empty} 51 51 … … 96 96 97 97 \newpage 98 99 \vspace*{7cm} 98 \addcontentsline{toc}{section}{Summary} 100 99 \paragraph{Summary} 101 100 The deliverable D4.4 is composed of the following parts: … … 177 176 whole assembler. 178 177 179 \includepdf[pages={} ]{itp2013.pdf}180 \includepdf[pages={} ]{paolo.pdf}181 \includepdf[pages={} ]{cpp2012asm.pdf}182 \includepdf[pages={} ]{cpp2012policy.pdf}178 \includepdf[pages={},addtotoc={1,section,1,Certification of the preservation of structure by a compiler's backend pass,simulation}]{itp2013.pdf} 179 \includepdf[pages={},addtotoc={1,section,1,Certifying the backend pass of the CerCo annotating compiler,backend}]{paolo.pdf} 180 \includepdf[pages={},addtotoc={1,section,1,On the correctness of an optimising assembler for the Intel MCS51 microprocessor,asm}]{cpp2012asm.pdf} 181 \includepdf[pages={},addtotoc={1,section,1,On the correctness of a branch displacement algorithm,policy}]{cpp2012policy.pdf} 183 182 184 183 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.