Changeset 3127
 Timestamp:
 Apr 12, 2013, 4:03:35 PM (8 years ago)
 Location:
 Deliverables/D4.4
 Files:

 1 added
 1 moved
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.4/mauro.tex
r3126 r3127 10 10 \usepackage[utf8x]{inputenc} 11 11 \usepackage{listings} 12 \usepackage[all]{xy} 13 14 \newcommand{\unif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{\equiv}}} 15 \newcommand{\founif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{=}}} 16 \newcommand{\vect}[1]{\ensuremath{\stackrel{\to}{#1}}} 17 \newcommand{\sem}[1]{\ensuremath{[\![#1]\!]}} 18 \newcommand{\bsem}[2]{\ensuremath{[\![#1;\;#2]\!]}} 19 20 \renewcommand{\verb}{\lstinline} 21 \def\lstlanguagefiles{lstgrafite.tex} 22 \lstset{language=Grafite} 23 12 24 \usepackage{lscape} 13 25 \usepackage{stmaryrd} … … 119 131 \verb=src : joint_program p_in= (resp. \verb=out : joint_program p_out=), we would like to 120 132 prove a statement similar to this shape. 121 \begin{ verbatim}133 \begin{lstlisting} 122 134 theorem joint_correctness : ∀p_in,p_out : sem_graph_params. 123 135 ∀prog : joint_program p_in.∀stack_size. … … 133 145 (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)) 134 146 R init_in init_out. 135 \end{ verbatim}147 \end{lstlisting} 136 148 When proving this statement (for each concrete istance of language), 137 149 we need to proceed by cases according the classification of … … 168 180 In order to reach this goal, we have to analyze first whether there is a common way to perform language 169 181 translation for each pass. After having defined and specified the translation machienary, we will 170 explain how it is possibile to use it in order to build such a layer. 182 explain how it is possibile to use it in order to build such a layer. So this section is organized as follows: 183 in the first part we explain the translation machienary while in the second part we explain such a layer. 184 185 \subsection{Graph translation} 186 Since a program is just a collection of functions, the compositional approach suggests us to define the 187 translation of a program in terms of the way we translate each internal function. Thus, if we let 188 \verb=src_g_pars= and \verb=dst_g_pars= being the graph parameters of respectively the source and 189 the target program, the aim is writing a Matita's function that takes as input an object of type 190 \verb=joint_closed_internal_function src_g_pars= together with additional information 191 (that we will explain better later) and gives as output an object of type 192 \verb=joint_closed_internal_function dst_g_pars= with some properties, that corresponds 193 to the result of the translation (for the definition of \verb=joint_closed_internal_function=, see 194 Deliverable 4.2 and 4.3) . The signature of the definition is the following one. 195 \begin{lstlisting} 196 definition b_graph_translate : 197 ∀src_g_pars,dst_g_pars : graph_params. 198 ∀globals: list ident. 199 ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals. 200 ∀def_in : joint_closed_internal_function src_g_pars globals. 201 Σdef_out : joint_closed_internal_function dst_g_pars globals. 202 ∃data',regs,f_lbls,f_regs. 203 bind_new_instantiates ?? data' data regs ∧ 204 b_graph_translate_props … data' def_in def_out f_lbls f_regs. 205 ........ 206 \end{lstlisting} 207 208 Let us now discuss in detail what are the parameter to be provide in input and what is the output of the 209 translation process. 210 211 \subsubsection{Input requested by the translation process} 212 Clearly, \verb=b_graph_translate= takes as input the internal function of the source language we want to translate. 213 But it also takes in input some useful infomrmation which will be used in order to dictate the translation process. 214 These information are all contained in an instance of the following record. 215 216 \begin{lstlisting} 217 record b_graph_translate_data 218 (src, dst : graph_params) 219 (globals : list ident) : Type[0] ≝ 220 { init_ret : call_dest dst 221 ; init_params : paramsT dst 222 ; init_stack_size : ℕ 223 ; added_prologue : list (joint_seq dst globals) 224 ; new_regs : list register 225 ; f_step : label → joint_step src globals → bind_step_block dst globals 226 ; f_fin : label → joint_fin_step src → bind_fin_block dst globals 227 ; good_f_step : 228 ∀l,s.bind_new_P' ?? 229 (λlocal_new_regs,block.let 〈pref, op, post〉 ≝ block in 230 ∀l. 231 let allowed_labels ≝ l :: step_labels … s in 232 let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in 233 All (label → joint_seq ??) 234 (λs'.step_labels_and_registers_in … allowed_labels allowed_registers 235 (step_seq dst globals (s' l))) 236 pref ∧ 237 step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧ 238 All (joint_seq ??) 239 (step_labels_and_registers_in … allowed_labels allowed_registers) 240 post) 241 (f_step l s) 242 ; good_f_fin : 243 ∀l,s.bind_new_P' ?? 244 (λlocal_new_regs,block.let 〈pref, op〉 ≝ block in 245 let allowed_labels ≝ l :: fin_step_labels … s in 246 let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in 247 All (joint_seq ??) 248 (λs.step_labels_and_registers_in … allowed_labels allowed_registers s) 249 pref ∧ 250 fin_step_labels_and_registers_in … allowed_labels allowed_registers op) 251 (f_fin l s) 252 ; f_step_on_cost : 253 ∀l,c.f_step l (COST_LABEL … c) = 254 bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉 255 ; cost_in_f_step : 256 ∀l,s,c. 257 bind_new_P ?? 258 (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c → 259 s = COST_LABEL … c) (f_step l s) 260 } 261 \end{lstlisting} 262 We will now summarize what each field means and how it is used in the translation process. We will say that an identifier of 263 a pseudoregister (resp. a code point) is {\em fresh} when it never appears in the code of the source function. 264 \begin{center} 265 \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} 266 Field & Explanation \\ 267 \hline 268 \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.\\ 269 \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.\\ 270 \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. \\ 271 \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. \\ 272 \texttt{new\_regs} & It is a list of identifiers for fresh pseudoregisters that are used by statements in \texttt{added\_prologue}. \\ 273 \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. \\ 274 \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.\\ 275 \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). \\ 276 \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.\\ 277 \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. 278 \end{tabular*} 279 \end{center} 280 281 \subsubsection{Output given the translation process} 282 Clearly \verb=g_graph_translate= gives in output the translated internal function. Unfortunately, 283 for what we are going to develop later, this information is insufficient because we need some information 284 about the correspondence between the source internal function and the translated one. Such an information 285 is given by the second component of the $\Sigma$type returned by the translation process. 286 We remind that the return type of \verb=b_graph_translate= is the following. 287 \begin{lstlisting} 288 Σdef_out : joint_closed_internal_function dst_g_pars globals. 289 ∃data',regs,f_lbls,f_regs. 290 bind_new_instantiates ?? data' data regs ∧ 291 b_graph_translate_props … data' def_in def_out f_lbls f_regs. 292 \end{lstlisting} 293 The correspondence between the source internal function and the translated one is made explicit by two functions: 294 \verb=f_lbls : code_point src_g_pars → list (code_point dst_g_pars)= and 295 \verb=f_regs : code_point src_g_pars → list (register)=. To understand their meaning, we need to stress the 296 fact that the translation process translates every statement appearing in the code of the source internal function 297 in a given code point $l$ into a block of statements in the code of the translated function where the first 298 instruction of the block has $l$ as code point identifier and all succeeding instructions of the block have 299 fresh code points identifiers. Furthermore statements of this block may use fresh identifiers of pseudoregisters or 300 (even worste) they may use some fresh codepoint identifiers being generated by the translation (we will see later 301 that this will be important when translating a call statement). We will use the above mentioned functions 302 to retrieve this information. \verb=f_lbls= takes in input an identifier $l$ for a code point in the 303 source code and it gives back the list of all fresh code point identifiers generated by the translation process 304 of the statement in the source located in $l$. \verb=f_regs= takes in input an identifier $l$ for a code point 305 in the source code and it gives back the list of all fresh register identifiers generated by the translation process 306 of the statement in the source located in $l$. 307 308 The above mentioned properties about the functions \verb=f_lbls= and \verb=f_regs=, together with some other 309 ones, are expressed and formalized by the following propositional record. 310 \begin{lstlisting} 311 record b_graph_translate_props 312 (src_g_pars, dst_g_pars : graph_params) 313 (globals: list ident) 314 (data : b_graph_translate_data src_g_pars dst_g_pars globals) 315 (def_in : joint_closed_internal_function src_g_pars globals) 316 (def_out : joint_closed_internal_function dst_g_pars globals) 317 (f_lbls : label → list label) 318 (f_regs : label → list register) : Prop ≝ 319 { res_def_out_eq : 320 joint_if_result … def_out = init_ret … data 321 ; pars_def_out_eq : 322 joint_if_params … def_out = init_params … data 323 ; ss_def_out_eq : 324 joint_if_stacksize … def_out = init_stack_size … data 325 ; partition_lbls : partial_partition … f_lbls 326 ; partition_regs : partial_partition … f_regs 327 ; freshness_lbls : 328 (∀l.All … 329 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 330 fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l)) 331 ; freshness_regs : 332 (∀l.All … 333 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 334 fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l)) 335 ; freshness_data_regs : 336 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 337 fresh_for_univ … reg (joint_if_runiverse … def_out)) 338 (new_regs … data) 339 ; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False 340 ; multi_fetch_ok : 341 ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 342 let lbls ≝ f_lbls l in let regs ≝ f_regs l in 343 match s with 344 [ sequential s' nxt ⇒ 345 let block ≝ 346 if not_emptyb … (added_prologue … data) ∧ 347 eq_identifier … (joint_if_entry … def_in) l then 348 bret … [ ] 349 else 350 f_step … data l s' in 351 l (block, l::lbls, regs)> nxt in joint_if_code … def_out 352  final s' ⇒ 353 l (f_fin … data l s', l::lbls, regs)> it in joint_if_code … def_out 354  FCOND abs _ _ _ ⇒ Ⓧabs 355 ] 356 ; prologue_ok : 357 if not_emptyb … (added_prologue … data) then 358 ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 359 joint_if_entry … def_out 360 (〈[ ],λ_.COST_LABEL … (get_first_costlabel … def_in), added_prologue … data〉, 361 f_lbls … lbl)> joint_if_entry … def_in in joint_if_code … def_out 362 else (joint_if_entry … def_out = joint_if_entry … def_in) 363 }. 364 \end{lstlisting} 365 366 We will now summarize the meaning of each field of the record using the same approach followed 367 in the previous subsection. 368 \begin{center} 369 \begin{tabular*}{\textwidth}{p{4cm}p{11cm}} 370 Field & Explanation \\ 371 \hline 372 \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. \\ 373 \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. \\ 374 \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. \\ 375 \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. \\ 376 \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. \\ 377 \texttt{freshness\_lbls} & All lists of codepoint identifiers generated by a codepoint of the code of the source internal function are fresh. \\ 378 \texttt{freshness\_regs} & All lists of pseudoregister identifiers generated by a codepoint of the code of the source internal function are fresh. \\ 379 \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. \\ 380 \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. \\ 381 \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 382 $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 383 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}$ 384 and it may have a syntactical successor depending wether $I$ is a stepstatement or not: in the former case we have that the 385 syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\ 386 \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 NOOP instruction. 387 \end{tabular*} 388 \end{center} 389 390 \subsection{A general correctness proof} 391 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. 392 393 \subsubsection{A standard calling relation} 394 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 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$. 395 396 In order to explain how this machienary work. we need to enter more in the detail of the translation process. Given a stepstatement 397 $I$, formally its translation is a triple $f\_step(s) = \langle pre,p,post \rangle$ such that $pre$ is a list of sequential 398 statements called {\em preamble}, $p$ is a stepstatement (we call it {\em pivot}) and $post$ is again a list of sequential statements 399 called {\em postamble}. When $pre = [s_1,\ldots,s_n]$ and $post = [s_1',\ldots,s_m']$, the corresponding block being the translation 400 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 401 postable, i.e. it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement. 402 403 Given a statement $I$ at a given code point $l$ in the source internal function and given the pivot statement $p$ of the translation 404 of $I$ staying at codepoint $l'$ in the translated internal function, there is an easy way to relate $l$ and $l'$. Notice that, 405 in case the preamble is empty, for the property of the translation process we have then $l = l'$, while if the preamble is nonempty. 406 then $l'$ is $n1$th element of $f\_lbls(l)$, where $n \geq 0$ is the length of the preamble. 407 The Matita's definition computing the code points according to the above mentioned specification is the following one. 408 \begin{lstlisting} 409 definition sigma_label : ∀p_in,p_out : sem_graph_params. 410 joint_program p_in → (ident → option ℕ) → 411 (∀globals.joint_closed_internal_function p_in globals 412 →bound_b_graph_translate_data p_in p_out globals) → 413 (block → list register) → lbl_funct_type → regs_funct_type → 414 block → label → option label ≝ 415 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched. 416 ! bl ← code_block_of_block bl ; 417 ! <id,fn> ← res_to_opt … (fetch_internal_function … 418 (joint_globalenv p_in prog stack_size) bl); 419 ! <res,s> ← 420 find ?? (joint_if_code ?? fn) 421 (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with 422 [ None ⇒ false 423  Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with 424 [ None ⇒ false 425  Some x ⇒ eq_identifier … searched x 426 ] 427 ]); 428 return res. 429 \end{lstlisting} 430 This function takes in input all the information provided by the translation process (in particular the function $f\_lbls$), a 431 function location and a codepoint identifier $l$; it fetches the internal function of the source language in the correponding location. 432 Then it unfolds the code of the fetched function looking for a label $l'$ and a statement $I$ located in $l'$, such that, 433 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 434 of the preamble of $I$. The function $find$ is the procedure realizing this search. If $preamble\_length$ is the function giving in 435 output the length of the preamble and if $nth\_opt$ is the function giving the $n$th element of a list, then this condition can 436 be summarized as following: we are looking for a label $l'$ such that $l$ is the $n$th element of the list $l :: f\_lbls (l)$, 437 where $n$ is the length of the preamble. 438 439 We can prove that, starting from a code point identifier of the translated internal function, 440 whenever there exists a codepoint identifier in the source internal function satifying the above condition, then it is always unique. 441 The properties \verb=partition_lbls= and \verb=freshness_lbls= provided by the translation process are crucial in the proof 442 of this statement. 443 444 We can wrap this function inside the definition of the desired relation among program counter states in the following way 445 The conditional at the beginning is put to deal with the premain case, which is translated without following the standard 446 translation process we explain in previous section. 447 \begin{lstlisting} 448 definition sigma_pc_opt : 449 ∀p_in,p_out : sem_graph_params. 450 joint_program p_in → (ident → option ℕ) → 451 (∀globals.joint_closed_internal_function p_in globals 452 →bound_b_graph_translate_data p_in p_out globals) → 453 (block → list register) → lbl_funct_type → regs_funct_type → 454 program_counter → option program_counter ≝ 455 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. 456 let target_point ≝ point_of_pc p_out pc in 457 if eqZb (block_id (pc_block pc)) (1) then 458 return pc 459 else 460 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs 461 f_lbls f_regs (pc_block pc) target_point; 462 return pc_of_point p_in (pc_block pc) source_point. 463 464 definition sigma_stored_pc ≝ 465 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. 466 match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with 467 [None ⇒ null_pc (pc_offset … pc)  Some x ⇒ x]. 468 \end{lstlisting} 469 470 The main result about the program counter relation we have defined is the following. If we fetch a statement $I$ in 471 at a given program counter $pc$ in the source program, then there is a program counter $pc'$ in the target program 472 which is in relation with $pc$ (i.e. $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot 473 statement of the tranlation. The formalization of this statement in Matita is given in the following. 474 475 \begin{lstlisting} 476 lemma fetch_statement_sigma_stored_pc : 477 ∀p_in,p_out,prog,stack_sizes, 478 init,init_regs,f_lbls,f_regs,pc,f,fn,stmt. 479 b_graph_transform_program_props p_in p_out stack_sizes 480 init prog init_regs f_lbls f_regs → 481 block_id … (pc_block pc) ≠ 1 → 482 let trans_prog ≝ b_graph_transform_program p_in p_out init prog in 483 fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc = 484 return 〈f,fn,stmt〉 → 485 ∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧ 486 match stmt with 487 [ sequential step nxt ⇒ 488 ∃step_block : step_block p_out (prog_names … trans_prog). 489 bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step) 490 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧ 491 ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 492 init_regs f_lbls f_regs pc' = pc ∧ 493 ∃fn',nxt'. 494 fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' = 495 if not_emptyb … (added_prologue … data) ∧ 496 eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn) 497 then OK ? <f,fn',sequential ?? (NOOP …) nxt'> 498 else OK ? <f,fn', 499 sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'> 500  final fin ⇒ 501 ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin) 502 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧ 503 ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 504 init_regs f_lbls f_regs pc' = pc ∧ 505 ∃fn'.fetch_statement p_out … 506 (joint_globalenv p_out trans_prog stack_sizes) pc' 507 = return 〈f,fn',final ?? (\snd fin_block)〉 508  FCOND abs _ _ _ ⇒ Ⓧabs 509 ]. 510 \end{lstlisting} 511 512 If we combine the statement above with the fact that the pivot statement of the translation 513 of a call statement is always a call statement (which we will formalize better in the 514 following section), then we can define our standard calling relation in the following way. 515 516 \begin{lstlisting} 517 (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call. 518 λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call. 519 pc ? s1 = 520 sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)). 521 \end{lstlisting} 522 523 We stress the fact that such a call relation will be always defined in this way for all jointlanguages, 524 in an independent way from the specific pass. The only condition we will ask is that the pass should 525 use the translation process we explain in the previous section. 526 527 \subsubsection{The semantical relation} 528 The semantical relation between states is the classical relation used in forward simulation proofs. 529 It correlates the data of the status (e.g. register, memory, etc.). We remind that the notion of state 530 in joint language is summarized in the following record. 531 \begin{lstlisting} 532 record state_pc (semp : sem_state_params) : Type[0] ≝ 533 { st_no_pc :> state semp 534 ; pc : program_counter 535 ; last_pop : program_counter 536 }. 537 \end{lstlisting} 538 It consists of three fields: the field \verb=st_no_pc= contains all data information of the state 539 (the content of the registers, of the memory and so on), the field \verb=pc= contains the current 540 program counter, while the field \verb=last_pop= is the address of the last popped calling address 541 when executing a return instruction. 542 543 The type of the semantical relation between state is the following. 544 545 \begin{lstlisting} 546 definition joint_state_pc_relation ≝ 547 λP_in,P_out : sem_graph_params.state_pc P_in → state_pc P_out → Prop. 548 \end{lstlisting} 549 550 We would like to state some conditions the semantical relation between states have to satisfy in order 551 to get our simulation result. We would like that this relation have some flavour of compositionality. 552 In particular we would like that it depends strictly on the contents of the field \verb=st_no_pc=, i.e. 553 the field that really contains data information of the state. So we need also a data relation, i.e. 554 a relation of this type. 555 556 \begin{lstlisting} 557 definition joint_state_relation ≝ 558 λP_in,P_out.program_counter → state P_in → state P_out → Prop. 559 \end{lstlisting} 560 561 Notice that the data relation cab depend on a specific program counter of the source. This is done 562 to capture complex data relations like the ones in the ERTL to LTL pass, in which you need to know 563 where data in pseudoregisters of ERTL are stored by the translation (either in hardware register or 564 in memory) and this information depends on the code point on the statement being translated. 565 566 The compositionality requirement is expressed by the following conditions (which are part of a bigger 567 record, that we are going to introduce later). 568 569 \begin{lstlisting} 570 ; fetch_ok_sigma_state_ok : 571 ∀st1,st2,f,fn. st_rel st1 st2 → 572 fetch_internal_function … 573 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 574 = return <f,fn> → 575 st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2) 576 ; fetch_ok_pc_ok : 577 ∀st1,st2,f,fn.st_rel st1 st2 → 578 fetch_internal_function … 579 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 580 = return <f,fn> → 581 pc … st1 = pc … st2 582 ; fetch_ok_sigma_last_pop_ok : 583 ∀st1,st2,f,fn.st_rel st1 st2 → 584 fetch_internal_function … 585 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 586 = return <f,fn> → 587 (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs 588 f_lbls f_regs (last_pop … st2) 589 ; st_rel_def : 590 ∀st1,st2,pc,lp1,lp2,f,fn. 591 fetch_internal_function … 592 (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return <f,fn> → 593 st_no_pc_rel pc st1 st2 → 594 lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs 595 f_lbls f_regs lp2 → 596 st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2) 597 \end{lstlisting} 598 599 Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantical 600 relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates 601 that two states that are in semantical relation should have the same program counter. This is due 602 to the way the translation is performed. In fact a statement $I$ at a code point $l$ in the source 603 internal function is translated with a block of instructions in the translated internal function 604 whose initial statement is at the same code point $l$. Condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok} 605 postulates that two states that are in semantical relation have the last popped calling address 606 in call relation. Finally \texttt{st\_rel\_def} postulates that given two states having the same 607 program counter, the last pop fields in call relation and the data fields also in data relation, then 608 they are in semantical relation. 609 610 An other important condition is that the pivot statement of the translation of a call statement is 611 always a call statement. This is important in order to obtain the correctness of the call relation 612 and return relation between state. This condition is formalized by the following Matita's code, and 613 we call it \texttt{call\_is\_call}. 614 615 \begin{lstlisting} 616 ; call_is_call :∀f,fn,bl. 617 fetch_internal_function … 618 (joint_globalenv P_in prog stack_sizes) bl = return <f,fn> → 619 ∀id,args,dest,lbl. 620 bind_new_P' ?? 621 (λregs1.λdata.bind_new_P' ?? 622 (λregs2.λblp. 623 ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') 624 (f_step … data lbl (CALL P_in ? id args dest))) 625 (init ? fn) 626 \end{lstlisting} 627 628 The conditions we are going to present now are standard semantical commutation lemmas that are commonly 629 used when proving the correctness of the operational semantics of many imperative languages. We introduce some notation. 630 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. 631 We will use $r_1,\ldots,r_n$ to range over by register identifiers. We will use $s_1,s_1',s_1'',\ldots$ to range 632 over by states of programs of the source language. We will use $s_2,s_2',s_2'',\ldots$ to range over by 633 states of programs of the target language. We denote respectively with $\simeq_{S}$, $\simeq_C$ and $\simeq_L$ 634 the semantical relation, the call relation and the costlabel relation between states. These relations have 635 been introduced at the beginning of this Deliverable (see Section ??). If $instr = [I_1,\ldots,I_n]$ is a list 636 of instructions, then we write $s_i \stackrel{instr}{\longrightarrow} s_i'$ ($i \in [1,2]$) when $s_i'$ is 637 the state being the result of the evaluation of the sequence of instructions $instr$ (performed in the order 638 they appear in the list) starting from the initial state $s_i$. When $instr = [I]$ is a singleton, we use 639 to omit square brackets and we write $s_i \stackrel{I}{\longrightarrow} s_i'$. 640 We will denote with $\pi_i$ ($i \in [1,t]$) the projecting functions of $t$uples. We will denote with $f\_step$ and $f\_fin$ 641 the translating functions of respectively stepstatements and final statements. We remind that $f\_step$ gives 642 a triple as output (a list of instruction called preamble,an instruction called pivot and a list of instructions 643 called postamble) while $f\_fin$ gives a pair as output (a list of instruction called preamble and an instruction 644 called pivot). Furthermore, we denote with $prologue$ the content of the field \texttt{added\_prologue} of the record 645 provided in input to the translation process. 646 647 Many commutation conditions can be depicted using diagrams. We will use them to give a pictorial flavour of the conditions 648 we will ask in order to obtain the final correctness statement. Given the states $s_1,s_1',s_2,s_2'$ and the instructions 649 $I,J_1,\ldots,J_k$, the following diagram 650 $$ 651 \xymatrix{ 652 s_1 \ar@{>}[rr]^{I} \ar@{}[d]^{\simeq_S} && s_1' \ar@{}[d]^{\simeq_S}\\ 653 s_2 \ar[rr]^{[J_1,\ldots,J_k]} && s_2' 654 } 655 $$ 656 depicts a situation in which the state $s_1 \stackrel{I}{\longrightarrow} s_1'$, $s_2 \stackrel{I}{\longrightarrow} s_2'$, 657 $s_1 \simeq_S s_2$ and $s_1' \simeq_S s_2'$. 658 659 \paragraph{Commutation of premain instructions.} 660 In order to get the commutation of premain instructions (states whose function location of program counter is 1), we have 661 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$, 662 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 663 diagram commutes. 664 $$ 665 \xymatrix{ 666 s_1 \ar@{>}[rr]^{I} \ar@{}[d]^{\simeq_S} && s_1' \ar@{}[d]^{\simeq_S}\\ 667 s_2 \ar[rr]^{J} && s_2' 668 } 669 $$ 670 The formalization of this statement in Matita is the following one. 671 \begin{lstlisting} 672 ; pre_main_ok : 673 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 674 ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 675 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 676 block_id … (pc_block (pc … st1)) = 1 → 677 st_rel st1 st2 → 678 as_label (joint_status P_in prog stack_sizes) st1 = 679 as_label (joint_status P_out trans_prog stack_sizes) st2 ∧ 680 joint_classify … (mk_prog_params P_in prog stack_sizes) st1 = 681 joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧ 682 (eval_state P_in … (joint_globalenv P_in prog stack_sizes) 683 st1 = return st1' → 684 ∃st2'. st_rel st1' st2' ∧ 685 eval_state P_out … 686 (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2') 687 \end{lstlisting} 688 689 \paragraph{Commutation of conditional jump.} 690 For all $s_1,s_1'$ and $s_2$ such that $s_1 \stackrel{COND \ r \ l}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$ then 691 \begin{itemize} 692 \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}$, 693 $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 694 $$ 695 \xymatrix{ 696 s_1 \ar@{>}[rrrrrr]^{COND \ l \ r} \ar@{}[d]^{\simeq_S} &&&&&& s_1' \ar@{}[d]^{\simeq_S}\\ 697 s_2 \ar[rrr]^{\pi_1(f\_step(COND \ r \ l))} &&& s_2^{fin} \ar[rrr]^{\pi_2(f\_step(COND \ r \ l))} &&& s_2' 698 } 699 $$ 700 \item $\pi_3(f\_step(COND \ r \ l))$ is empty, while $\pi_2(f\_step(COND \ r \ l)) = COND \ r' \ l'$ is a conditional jump 701 such that $l = l'$. 702 \end{itemize} 703 This condition is formalized in Matita in the following way. 704 \begin{lstlisting} 705 ; cond_commutation : 706 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 707 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 708 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 709 ∀f,fn,a,ltrue,lfalse,bv,b. 710 block_id … (pc_block (pc … st1)) ≠ 1 → 711 let cond ≝ (COND P_in ? a ltrue) in 712 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 713 return <f, fn, sequential … cond lfalse> → 714 acca_retrieve … P_in (st_no_pc … st1) a = return bv → 715 bool_of_beval … bv = return b → 716 st_rel st1 st2 → 717 ∀t_fn. 718 fetch_internal_function … 719 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 720 return 〈f,t_fn〉 → 721 bind_new_P' ?? 722 (λregs1.λdata.bind_new_P' ?? 723 (λregs2.λblp.(\snd blp) = [ ] ∧ 724 ∀mid. 725 stmt_at P_out … (joint_if_code ?? t_fn) mid 726 = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ 727 ∃st2_pre_mid_no_pc. 728 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 729 (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) 730 = return st2_pre_mid_no_pc ∧ 731 let new_pc ≝ if b then 732 (pc_of_point P_in (pc_block (pc … st1)) ltrue) 733 else 734 (pc_of_point P_in (pc_block (pc … st1)) lfalse) in 735 st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧ 736 ∃a'. ((\snd (\fst blp)) mid) = COND P_out ? a' ltrue ∧ 737 ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧ 738 bool_of_beval … bv' = return b 739 ) (f_step … data (point_of_pc P_in (pc … st1)) cond) 740 ) (init ? fn) 741 \end{lstlisting} 742 743 \paragraph{Commutation of sequential statements.} 744 In case of a sequential statement $I$, its translation $f\_step(I) = \langle pre , J , post \rangle$ is coerced 745 into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the 746 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 747 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 748 the following diagram commutes. 749 $$ 750 \xymatrix{ 751 s_1 \ar@{>}[rr]^{I} \ar@{}[d]^{\simeq_S} && s_1' \ar@{}[d]^{\simeq_S}\\ 752 s_2 \ar[rr]^{f\_step(I)} && s_2' 753 } 754 $$ 755 The formalization in Matita of the above statement is as follows. 756 \begin{lstlisting} 757 ; seq_commutation : 758 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 759 ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 760 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 761 ∀f,fn,stmt,nxt. 762 block_id … (pc_block (pc … st1)) ≠ 1 → 763 let seq ≝ (step_seq P_in ? stmt) in 764 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 765 return <f, fn, sequential … seq nxt> → 766 eval_state P_in … (joint_globalenv P_in prog stack_sizes) 767 st1 = return st1' → 768 st_rel st1 st2 → 769 ∀t_fn. 770 fetch_internal_function … 771 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 772 return <f,t_fn> → 773 bind_new_P' ?? 774 (λregs1.λdata.bind_new_P' ?? 775 (λregs2.λblp. 776 ∃l : list (joint_seq P_out 777 (globals ? (mk_prog_params P_out trans_prog stack_sizes))). 778 blp = (ensure_step_block ?? l) ∧ 779 ∃st2_fin_no_pc. 780 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 781 l (st_no_pc … st2)= return st2_fin_no_pc ∧ 782 st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc 783 ) (f_step … data (point_of_pc P_in (pc … st1)) seq) 784 ) (init ? fn) 785 \end{lstlisting} 786 787 \paragraph{Commutation of call statement} 788 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 789 the statement fetched in the translated language at the program counter being in call relation 790 with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL id' \ arg' \ dst'$ 791 for some $id',ags',dst'$, then there are $s_2^{pre},s_2^{after},s_2'$ such that 792 \begin{itemize} 793 \item $s_2 \stackrel{\pi_1(f\_step(CALL \ id \ arg \ dst))}{\longrightarrow} s_2^{pre}$, 794 \item $s_2^{pre} \stackrel{CALL \ id' \arg' \ dst'}{\longrightarrow} s_2^{after}$, 795 \item $s_2^{after} \stackrel{prologue}{\longrightarrow} s_2'$, 796 \item $s_1' \simeq_L s_2^{after}$ and $s_1' \simeq_S s_2'$. 797 \end{itemize} 798 The situation is depicted by the following diagram. 799 $$ 800 \xymatrix{ 801 s_1 \ar@{}[d]^{\simeq_S} \ar@{}[d]^{\simeq_S} \ar[rrrrrrrrrr]^{CALL \ id \ arg \ dst} &&&&&&&&&& s_1' \ar@{}[d]^{\simeq_S} \\ 802 s_2 \ar[rrrr]^{\pi_1(f\_step(CALL \ id \ arg \ dst))} &&&& s_2^{pre} \ar[rrr]^{CALL \ id' \ arg' \ dst'} &&& s_2^{after} \ar[rrr]^{prologue} &&& s_2' 803 } 804 $$ 805 The statement is formalized in Matita in the following way. 806 \begin{lstlisting} 807 ; call_commutation : 808 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 809 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 810 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 811 ∀f,fn,id,arg,dest,nxt. 812 block_id … (pc_block (pc … st1)) ≠ 1 → 813 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 814 return 〈f, fn, sequential P_in ? (CALL P_in ? id arg dest) nxt〉 → 815 ∀bl. 816 block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1) 817 = return bl → 818 ∀f1,fn1. 819 fetch_internal_function … 820 (joint_globalenv P_in prog stack_sizes) bl = return 〈f1,fn1〉 → 821 ∀st1_pre. 822 save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre → 823 ∀n.stack_sizes f1 = return n → 824 ∀st1'. 825 setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' → 826 st_rel st1 st2 → 827 ∀t_fn1. 828 fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl = 829 return 〈f1,t_fn1〉 → 830 bind_new_P' ?? 831 (λregs1.λdata. 832 bind_new_P' ?? 833 (λregs2.λblp. 834 ∀pc',t_fn,id',arg',dest',nxt1. 835 sigma_stored_pc P_in P_out prog stack_sizes init init_regs 836 f_lbls f_regs pc' = (pc … st1) → 837 fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc' 838 = return 〈f,t_fn, 839 sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1〉→ 840 ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') → 841 ∃st2_pre_call. 842 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 843 (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧ 844 block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id' 845 st2_pre_call = return bl ∧ 846 ∃st2_pre. 847 save_frame … P_out (kind_of_call P_out id') dest' 848 (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧ 849 ∃st2_after_call. 850 setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre 851 = return st2_after_call ∧ 852 bind_new_P' ?? 853 (λregs11.λdata1. 854 ∃st2'. 855 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 856 (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) = 857 return st2' ∧ 858 st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1)) 859 (increment_stack_usage P_in n st1') st2' 860 ) (init ? fn1) 861 ) 862 (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest)) 863 ) (init ? fn) 864 \end{lstlisting} 865 \paragraph{Commutation of return statement} 866 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$ 867 is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier 868 is the syntactical predecessor of the program counter of $s_1'$), then $\pi_2(f\_fin(RETURN)) = RETURN$, there are 869 $s_2^{pre},s_2^{after},s_2'$ such that $s_2 \stackrel{\pi_1(f\_fin(RETURN))}{\longrightarrow} s_2^{pre}$, 870 $s_2^{pre} \stackrel{RETURN}{\longrightarrow} s_2^{after}$, 871 $s_2^{after} \stackrel{\pi_3(f\_step(CALL \ id \ arg \ dst))}{\longrightarrow} s_2'$ and $s_1' \simeq_S s_2'$. The following diagram 872 depicts the above described requested situation. 873 $$ 874 \xymatrix{ 875 s_1 \ar@{}[d]^{\simeq_S} \ar@{}[d]^{\simeq_S} \ar[rrrrrrrrrrr]^{RETURN} &&&&&&&&&&& s_1' \ar@{}[d]^{\simeq_S} \\\ 876 s_2 \ar[rrrr]^{\pi_1(f\_fin(RETURN))} &&&& s_2^{pre} \ar[rrr]^{RETURN} &&& s_2^{after} \ar[rrrr]^{\pi_3(f\_step(CALL \ id \ arg \ dst))} &&&& s_2' 877 } 878 $$ 879 The statement is formalized in Matita in the following way. 880 \begin{lstlisting} 881 ; return_commutation : 882 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 883 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 884 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 885 ∀f,fn. 886 block_id … (pc_block (pc … st1)) ≠ 1 → 887 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 888 return 〈f, fn, final P_in ? (RETURN …)〉 → 889 ∀n. stack_sizes f = return n → 890 let curr_ret ≝ joint_if_result … fn in 891 ∀st_pop,pc_pop. 892 pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret 893 (st_no_pc … st1) = return 〈st_pop,pc_pop〉 → 894 ∀nxt.∀f1,fn1,id,args,dest. 895 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop = 896 return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 → 897 st_rel st1 st2 → 898 ∀t_fn. 899 fetch_internal_function … 900 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 901 return 〈f,t_fn〉 → 902 bind_new_P' ?? 903 (λregs1.λdata. 904 bind_new_P' ?? 905 (λregs2.λblp. 906 \snd blp = (RETURN …) ∧ 907 ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 908 (\fst blp) (st_no_pc … st2)= return st_fin ∧ 909 ∃t_st_pop,t_pc_pop. 910 pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f 911 (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧ 912 sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs 913 t_pc_pop = pc_pop ∧ 914 if eqZb (block_id (pc_block pc_pop)) (1) then 915 st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) 916 (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*) 917 else 918 bind_new_P' ?? 919 (λregs4.λdata1. 920 bind_new_P' ?? 921 (λregs3.λblp1. 922 ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 923 (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧ 924 st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) 925 (decrement_stack_usage ? n st_pop) st2' 926 ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest)) 927 ) (init ? fn1) 928 ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …)) 929 ) (init ? fn) 930 \end{lstlisting} 931 932 \subsubsection{Conclusion} 933 After having provided a semantic relation among states that satifies some conditions that correspond to 934 commutation lemmas that are commonly proved in a forward simulation proof, it is possible to prove the 935 general theorem. All these condition are summarized in a propositional record called \verb=good_state_relation=. 936 The statement we are able to prove have the following shape. 937 \begin{lstlisting} 938 theorem joint_correctness : ∀p_in,p_out : sem_graph_params. 939 ∀prog : joint_program p_in.∀stack_size : ident → option ℕ. 940 ∀init : (∀globals.joint_closed_internal_function p_in globals → 941 bound_b_graph_translate_data p_in p_out globals). 942 ∀init_regs : block → list register.∀f_lbls : lbl_funct_type. 943 ∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out. 944 ∀st_rel : joint_state_pc_relation p_in p_out. 945 good_state_relation p_in p_out prog stack_size init init_regs 946 f_lbls f_regs st_no_pc_rel st_rel → 947 let trans_prog ≝ b_graph_transform_program … init prog in 948 ∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in → 949 ∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧ 950 ∃[1] R. 951 status_simulation_with_init 952 (joint_abstract_status (mk_prog_params p_in prog stack_size)) 953 (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)) 954 R init_in init_out. 955 \end{lstlisting} 956 The module formalizing the formal machienary we described in this document consists of about 3000 lines of 957 Matita code. We stress the fact that this machienary proves general properties that do not depend on the 958 specific backend compiler pass. Without this layer one would have to prove these properties each specific 959 pass multiplying the number of Matita's lines by $n$ where $n$ is the number of backend pass. 960 961 962 171 963 172 964
Note: See TracChangeset
for help on using the changeset viewer.