Changeset 3213 for Deliverables/D4.4
 Timestamp:
 Apr 29, 2013, 6:14:15 PM (8 years ago)
 Location:
 Deliverables/D4.4
 Files:

 1 added
 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.4/mauro.tex
r3194 r3213 1 \section{A modular approach to the correctness of the graph passes} 1 \section{A Modular Approach to the Correctness of the Graph Passes} 2 \label{modular} 3 4 We will now outline how the proof can be carried out generally in the 5 graph passes of the backend that share the \verb+joint+ language interface. 2 6 3 7 An instance of the record \verb=sem_graph_params= contains all common information about … … 28 32 R init_in init_out. 29 33 \end{lstlisting} 30 When proving this statement (for each concrete i stance of language),34 When proving this statement (for each concrete instance of language), 31 35 we need to proceed by cases according the classification of 32 36 each state in the source program (\verb=cl_jmp=, \verb=cl_other=, \verb=cl_call= and 33 \verb=cl_return=) and then prov ing the suitable conditions explained in34 previous Section, according to the case we are currently considering (Condition 1 for37 \verb=cl_return=) and then prove the suitable conditions explained in 38 \cite{simulation}, according to the case we are currently considering (Condition 1 for 35 39 \verb=cl_other= and \verb=cl_jump= case, Condition 2 for \verb=cl_call= or 36 Condition 3 for \verb=cl_return= case). Rough tly speaking, proving these condition40 Condition 3 for \verb=cl_return= case). Roughly speaking, proving these conditions 37 41 means producing traces of some kind in the target language that are in a suitable 38 42 correspondence with an execution step in the source language. … … 42 46 the preservation the semantical relation between states of the program under evaluation) 43 47 and the intensional part (for example, all proof obbligation dealing with 44 the presence of a cost label in some point of the code) are mixed together in a not so clear way.48 the presence of a cost label in some point of the code) are mixed together in a not very clear way. 45 49 46 50 Furthermore, some proof obbligations concerning the relation among program counters … … 109 113 ; good_f_step : 110 114 ∀l,s.bind_new_P' ?? 111 (λlocal_new_regs,block.let 〈 pref, op, post〉 ≝ block in115 (λlocal_new_regs,block.let 〈 pref, op, post 〉 ≝ block in 112 116 ∀l. 113 117 let allowed_labels ≝ l :: step_labels … s in … … 124 128 ; good_f_fin : 125 129 ∀l,s.bind_new_P' ?? 126 (λlocal_new_regs,block.let 〈 pref, op〉 ≝ block in130 (λlocal_new_regs,block.let 〈 pref, op 〉 ≝ block in 127 131 let allowed_labels ≝ l :: fin_step_labels … s in 128 132 let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in … … 134 138 ; f_step_on_cost : 135 139 ∀l,c.f_step l (COST_LABEL … c) = 136 bret ? (step_block ??) 〈 [ ], λ_.COST_LABEL dst globals c, [ ]〉140 bret ? (step_block ??) 〈 [ ], λ_.COST_LABEL dst globals c, [ ] 〉 137 141 ; cost_in_f_step : 138 142 ∀l,s,c. … … 240 244 ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 241 245 joint_if_entry … def_out 242 (〈[ ],λ_.COST_LABEL … (get_first_costlabel … def_in), added_prologue … data〉, 246 ( 〈 [ ],λ_.COST_LABEL … (get_first_costlabel … def_in), 247 added_prologue … data 〉, 243 248 f_lbls … lbl)> joint_if_entry … def_in in joint_if_code … def_out 244 249 else (joint_if_entry … def_out = joint_if_entry … def_in) … … 364 369 let trans_prog ≝ b_graph_transform_program p_in p_out init prog in 365 370 fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc = 366 return 〈 f,fn,stmt〉 →371 return 〈 f,fn,stmt 〉 → 367 372 ∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧ 368 373 match stmt with … … 387 392 ∃fn'.fetch_statement p_out … 388 393 (joint_globalenv p_out trans_prog stack_sizes) pc' 389 = return 〈 f,fn',final ?? (\snd fin_block)〉394 = return 〈 f,fn',final ?? (\snd fin_block) 〉 390 395  FCOND abs _ _ _ ⇒ Ⓧabs 391 396 ]. … … 446 451 in memory) and this information depends on the code point on the statement being translated. 447 452 448 The compositionality requirement is expressed by the followingconditions (which are part of a bigger449 record , that we are going to introduce later).450 451 \begin{lstlisting}452 ; fetch_ok_sigma_state_ok :453 ∀st1,st2,f,fn. st_rel st1 st2 →454 fetch_internal_function …455 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1))456 = return <f,fn> →457 st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2)458 ; fetch_ok_pc_ok :459 ∀st1,st2,f,fn.st_rel st1 st2 →460 fetch_internal_function …461 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1))462 = return <f,fn> →463 pc … st1 = pc … st2464 ; fetch_ok_sigma_last_pop_ok :465 ∀st1,st2,f,fn.st_rel st1 st2 →466 fetch_internal_function …467 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1))468 = return <f,fn> →469 (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs470 f_lbls f_regs (last_pop … st2)471 ; st_rel_def :472 ∀st1,st2,pc,lp1,lp2,f,fn.473 fetch_internal_function …474 (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return <f,fn> →475 st_no_pc_rel pc st1 st2 →476 lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs477 f_lbls f_regs lp2 →478 st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)479 \end{lstlisting}480 453 The compositionality requirement is expressed by several conditions (which are part of a bigger 454 record). 455 % 456 % \begin{lstlisting} 457 % ; fetch_ok_sigma_state_ok : 458 % ∀st1,st2,f,fn. st_rel st1 st2 → 459 % fetch_internal_function … 460 % (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 461 % = return <f,fn> → 462 % st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2) 463 % ; fetch_ok_pc_ok : 464 % ∀st1,st2,f,fn.st_rel st1 st2 → 465 % fetch_internal_function … 466 % (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 467 % = return <f,fn> → 468 % pc … st1 = pc … st2 469 % ; fetch_ok_sigma_last_pop_ok : 470 % ∀st1,st2,f,fn.st_rel st1 st2 → 471 % fetch_internal_function … 472 % (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 473 % = return <f,fn> → 474 % (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs 475 % f_lbls f_regs (last_pop … st2) 476 % ; st_rel_def : 477 % ∀st1,st2,pc,lp1,lp2,f,fn. 478 % fetch_internal_function … 479 % (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return <f,fn> → 480 % st_no_pc_rel pc st1 st2 → 481 % lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs 482 % f_lbls f_regs lp2 → 483 % st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2) 484 % \end{lstlisting} 485 % 481 486 Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantical 482 487 relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates … … 490 495 they are in semantical relation. 491 496 492 An 497 Another important condition is that the pivot statement of the translation of a call statement is 493 498 always a call statement. This is important in order to obtain the correctness of the call relation 494 and return relation between state. This condition is formalized by the following Matita's code, and495 we call it\texttt{call\_is\_call}.496 497 \begin{lstlisting}498 ; call_is_call :∀f,fn,bl.499 fetch_internal_function …500 (joint_globalenv P_in prog stack_sizes) bl = return <f,fn> →501 ∀id,args,dest,lbl.502 bind_new_P' ??503 (λregs1.λdata.bind_new_P' ??504 (λregs2.λblp.505 ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest')506 (f_step … data lbl (CALL P_in ? id args dest)))507 (init ? fn)508 \end{lstlisting}499 and return relation between state. % This condition is formalized by the following Matita's code, and 500 We call this condition \texttt{call\_is\_call}. 501 502 % \begin{lstlisting} 503 % ; call_is_call :∀f,fn,bl. 504 % fetch_internal_function … 505 % (joint_globalenv P_in prog stack_sizes) bl = return <f,fn> → 506 % ∀id,args,dest,lbl. 507 % bind_new_P' ?? 508 % (λregs1.λdata.bind_new_P' ?? 509 % (λregs2.λblp. 510 % ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') 511 % (f_step … data lbl (CALL P_in ? id args dest))) 512 % (init ? fn) 513 % \end{lstlisting} 509 514 510 515 The conditions we are going to present now are standard semantical commutation lemmas that are commonly … … 539 544 $s_1 \simeq_S s_2$ and $s_1' \simeq_S s_2'$. 540 545 541 \paragraph{Commutation of premain instructions .}546 \paragraph{Commutation of premain instructions (\verb=pre_main_ok=).} 542 547 In order to get the commutation of premain instructions (states whose function location of program counter is 1), we have 543 548 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$, … … 550 555 } 551 556 $$ 552 The formalization of this statement in Matita is the following one.553 \begin{lstlisting}554 ; pre_main_ok :555 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in556 ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .557 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).558 block_id … (pc_block (pc … st1)) = 1 →559 st_rel st1 st2 →560 as_label (joint_status P_in prog stack_sizes) st1 =561 as_label (joint_status P_out trans_prog stack_sizes) st2 ∧562 joint_classify … (mk_prog_params P_in prog stack_sizes) st1 =563 joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧564 (eval_state P_in … (joint_globalenv P_in prog stack_sizes)565 st1 = return st1' →566 ∃st2'. st_rel st1' st2' ∧567 eval_state P_out …568 (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2')569 \end{lstlisting}570 571 \paragraph{Commutation of conditional jump .}557 % The formalization of this statement in Matita is the following one. 558 % \begin{lstlisting} 559 % ; pre_main_ok : 560 % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 561 % ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 562 % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 563 % block_id … (pc_block (pc … st1)) = 1 → 564 % st_rel st1 st2 → 565 % as_label (joint_status P_in prog stack_sizes) st1 = 566 % as_label (joint_status P_out trans_prog stack_sizes) st2 ∧ 567 % joint_classify … (mk_prog_params P_in prog stack_sizes) st1 = 568 % joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧ 569 % (eval_state P_in … (joint_globalenv P_in prog stack_sizes) 570 % st1 = return st1' → 571 % ∃st2'. st_rel st1' st2' ∧ 572 % eval_state P_out … 573 % (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2') 574 % \end{lstlisting} 575 576 \paragraph{Commutation of conditional jump (\verb=cond_commutation=).} 572 577 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 573 578 \begin{itemize} … … 583 588 such that $l = l'$. 584 589 \end{itemize} 585 This condition is formalized in Matita in the following way.586 \begin{lstlisting}587 ; cond_commutation :588 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in589 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .590 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).591 ∀f,fn,a,ltrue,lfalse,bv,b.592 block_id … (pc_block (pc … st1)) ≠ 1 →593 let cond ≝ (COND P_in ? a ltrue) in594 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =595 return <f, fn, sequential … cond lfalse> →596 acca_retrieve … P_in (st_no_pc … st1) a = return bv →597 bool_of_beval … bv = return b →598 st_rel st1 st2 →599 ∀t_fn.600 fetch_internal_function …601 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =602 return 〈f,t_fn〉 → 603 bind_new_P' ??604 (λregs1.λdata.bind_new_P' ??605 (λregs2.λblp.(\snd blp) = [ ] ∧606 ∀mid.607 stmt_at P_out … (joint_if_code ?? t_fn) mid608 = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→609 ∃st2_pre_mid_no_pc.610 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f611 (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2)612 = return st2_pre_mid_no_pc ∧613 let new_pc ≝ if b then614 (pc_of_point P_in (pc_block (pc … st1)) ltrue)615 else616 (pc_of_point P_in (pc_block (pc … st1)) lfalse) in617 st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧618 ∃a'. ((\snd (\fst blp)) mid) = COND P_out ? a' ltrue ∧619 ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧620 bool_of_beval … bv' = return b621 ) (f_step … data (point_of_pc P_in (pc … st1)) cond)622 ) (init ? fn)623 \end{lstlisting}624 625 \paragraph{Commutation of sequential statements .}590 % This condition is formalized in Matita in the following way. 591 % \begin{lstlisting} 592 % ; cond_commutation : 593 % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 594 % ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 595 % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 596 % ∀f,fn,a,ltrue,lfalse,bv,b. 597 % block_id … (pc_block (pc … st1)) ≠ 1 → 598 % let cond ≝ (COND P_in ? a ltrue) in 599 % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 600 % return <f, fn, sequential … cond lfalse> → 601 % acca_retrieve … P_in (st_no_pc … st1) a = return bv → 602 % bool_of_beval … bv = return b → 603 % st_rel st1 st2 → 604 % ∀t_fn. 605 % fetch_internal_function … 606 % (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 607 % return 〈 f,t_fn 〉 → 608 % bind_new_P' ?? 609 % (λregs1.λdata.bind_new_P' ?? 610 % (λregs2.λblp.(\snd blp) = [ ] ∧ 611 % ∀mid. 612 % stmt_at P_out … (joint_if_code ?? t_fn) mid 613 % = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ 614 % ∃st2_pre_mid_no_pc. 615 % repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 616 % (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) 617 % = return st2_pre_mid_no_pc ∧ 618 % let new_pc ≝ if b then 619 % (pc_of_point P_in (pc_block (pc … st1)) ltrue) 620 % else 621 % (pc_of_point P_in (pc_block (pc … st1)) lfalse) in 622 % st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧ 623 % ∃a'. ((\snd (\fst blp)) mid) = COND P_out ? a' ltrue ∧ 624 % ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧ 625 % bool_of_beval … bv' = return b 626 % ) (f_step … data (point_of_pc P_in (pc … st1)) cond) 627 % ) (init ? fn) 628 % \end{lstlisting} 629 630 \paragraph{Commutation of sequential statements (\verb=seq_commutation=).} 626 631 In case of a sequential statement $I$, its translation $f\_step(I) = \langle pre , J , post \rangle$ is coerced 627 632 into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the … … 635 640 } 636 641 $$ 637 The formalization in Matita of the above statement is as follows.638 \begin{lstlisting}639 ; seq_commutation :640 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in641 ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .642 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).643 ∀f,fn,stmt,nxt.644 block_id … (pc_block (pc … st1)) ≠ 1 →645 let seq ≝ (step_seq P_in ? stmt) in646 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =647 return <f, fn, sequential … seq nxt> →648 eval_state P_in … (joint_globalenv P_in prog stack_sizes)649 st1 = return st1' →650 st_rel st1 st2 →651 ∀t_fn.652 fetch_internal_function …653 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =654 return <f,t_fn> →655 bind_new_P' ??656 (λregs1.λdata.bind_new_P' ??657 (λregs2.λblp.658 ∃l : list (joint_seq P_out659 (globals ? (mk_prog_params P_out trans_prog stack_sizes))).660 blp = (ensure_step_block ?? l) ∧661 ∃st2_fin_no_pc.662 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f663 l (st_no_pc … st2)= return st2_fin_no_pc ∧664 st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc665 ) (f_step … data (point_of_pc P_in (pc … st1)) seq)666 ) (init ? fn)667 \end{lstlisting}668 669 \paragraph{Commutation of call statement }642 % The formalization in Matita of the above statement is as follows. 643 % \begin{lstlisting} 644 % ; seq_commutation : 645 % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 646 % ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 647 % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 648 % ∀f,fn,stmt,nxt. 649 % block_id … (pc_block (pc … st1)) ≠ 1 → 650 % let seq ≝ (step_seq P_in ? stmt) in 651 % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 652 % return <f, fn, sequential … seq nxt> → 653 % eval_state P_in … (joint_globalenv P_in prog stack_sizes) 654 % st1 = return st1' → 655 % st_rel st1 st2 → 656 % ∀t_fn. 657 % fetch_internal_function … 658 % (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 659 % return <f,t_fn> → 660 % bind_new_P' ?? 661 % (λregs1.λdata.bind_new_P' ?? 662 % (λregs2.λblp. 663 % ∃l : list (joint_seq P_out 664 % (globals ? (mk_prog_params P_out trans_prog stack_sizes))). 665 % blp = (ensure_step_block ?? l) ∧ 666 % ∃st2_fin_no_pc. 667 % repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 668 % l (st_no_pc … st2)= return st2_fin_no_pc ∧ 669 % st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc 670 % ) (f_step … data (point_of_pc P_in (pc … st1)) seq) 671 % ) (init ? fn) 672 % \end{lstlisting} 673 674 \paragraph{Commutation of call statement (\verb=call_commutation=).} 670 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$ and 671 676 the statement fetched in the translated language at the program counter being in call relation … … 685 690 } 686 691 $$ 687 The statement is formalized in Matita in the following way.688 \begin{lstlisting}689 ; call_commutation :690 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in691 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .692 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).693 ∀f,fn,id,arg,dest,nxt.694 block_id … (pc_block (pc … st1)) ≠ 1 →695 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =696 return 〈f, fn, sequential P_in ? (CALL P_in ? id arg dest) nxt〉 → 697 ∀bl.698 block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1)699 = return bl →700 ∀f1,fn1.701 fetch_internal_function …702 (joint_globalenv P_in prog stack_sizes) bl = return 〈f1,fn1〉 → 703 ∀st1_pre.704 save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre →705 ∀n.stack_sizes f1 = return n →706 ∀st1'.707 setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →708 st_rel st1 st2 →709 ∀t_fn1.710 fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl =711 return 〈f1,t_fn1〉 → 712 bind_new_P' ??713 (λregs1.λdata.714 bind_new_P' ??715 (λregs2.λblp.716 ∀pc',t_fn,id',arg',dest',nxt1.717 sigma_stored_pc P_in P_out prog stack_sizes init init_regs718 f_lbls f_regs pc' = (pc … st1) →719 fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc'720 = return 〈f,t_fn,721 sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1〉→722 ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') →723 ∃st2_pre_call.724 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f725 (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧726 block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id'727 st2_pre_call = return bl ∧728 ∃st2_pre.729 save_frame … P_out (kind_of_call P_out id') dest'730 (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧731 ∃st2_after_call.732 setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre733 = return st2_after_call ∧734 bind_new_P' ??735 (λregs11.λdata1.736 ∃st2'.737 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1738 (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) =739 return st2' ∧740 st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1))741 (increment_stack_usage P_in n st1') st2'742 ) (init ? fn1)743 )744 (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest))745 ) (init ? fn)746 \end{lstlisting}747 \paragraph{Commutation of return statement }692 % The statement is formalized in Matita in the following way. 693 % \begin{lstlisting} 694 % ; call_commutation : 695 % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 696 % ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 697 % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 698 % ∀f,fn,id,arg,dest,nxt. 699 % block_id … (pc_block (pc … st1)) ≠ 1 → 700 % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 701 % return 〈 f, fn, sequential P_in ? (CALL P_in ? id arg dest) nxt 〉 → 702 % ∀bl. 703 % block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1) 704 % = return bl → 705 % ∀f1,fn1. 706 % fetch_internal_function … 707 % (joint_globalenv P_in prog stack_sizes) bl = return 〈 f1,fn1 〉 → 708 % ∀st1_pre. 709 % save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre → 710 % ∀n.stack_sizes f1 = return n → 711 % ∀st1'. 712 % setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' → 713 % st_rel st1 st2 → 714 % ∀t_fn1. 715 % fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl = 716 % return 〈 f1,t_fn1 〉 → 717 % bind_new_P' ?? 718 % (λregs1.λdata. 719 % bind_new_P' ?? 720 % (λregs2.λblp. 721 % ∀pc',t_fn,id',arg',dest',nxt1. 722 % sigma_stored_pc P_in P_out prog stack_sizes init init_regs 723 % f_lbls f_regs pc' = (pc … st1) → 724 % fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc' 725 % = return 〈 f,t_fn, 726 % sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1 〉→ 727 % ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') → 728 % ∃st2_pre_call. 729 % repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 730 % (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧ 731 % block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id' 732 % st2_pre_call = return bl ∧ 733 % ∃st2_pre. 734 % save_frame … P_out (kind_of_call P_out id') dest' 735 % (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧ 736 % ∃st2_after_call. 737 % setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre 738 % = return st2_after_call ∧ 739 % bind_new_P' ?? 740 % (λregs11.λdata1. 741 % ∃st2'. 742 % repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 743 % (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) = 744 % return st2' ∧ 745 % st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1)) 746 % (increment_stack_usage P_in n st1') st2' 747 % ) (init ? fn1) 748 % ) 749 % (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest)) 750 % ) (init ? fn) 751 % \end{lstlisting} 752 \paragraph{Commutation of return statement (\verb=return_commutation=).} 748 753 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$ 749 754 is the call statement that caused the function call ened by the current return (i.e. it is the statement whose code point identifier … … 759 764 } 760 765 $$ 761 The statement is formalized in Matita in the following way.762 \begin{lstlisting}763 ; return_commutation :764 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in765 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .766 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).767 ∀f,fn.768 block_id … (pc_block (pc … st1)) ≠ 1 →769 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =770 return 〈f, fn, final P_in ? (RETURN …)〉 → 771 ∀n. stack_sizes f = return n →772 let curr_ret ≝ joint_if_result … fn in773 ∀st_pop,pc_pop.774 pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret775 (st_no_pc … st1) = return 〈st_pop,pc_pop〉 → 776 ∀nxt.∀f1,fn1,id,args,dest.777 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop =778 return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 → 779 st_rel st1 st2 →780 ∀t_fn.781 fetch_internal_function …782 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) =783 return 〈f,t_fn〉 → 784 bind_new_P' ??785 (λregs1.λdata.786 bind_new_P' ??787 (λregs2.λblp.788 \snd blp = (RETURN …) ∧789 ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f790 (\fst blp) (st_no_pc … st2)= return st_fin ∧791 ∃t_st_pop,t_pc_pop.792 pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f793 (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧ 794 sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs795 t_pc_pop = pc_pop ∧796 if eqZb (block_id (pc_block pc_pop)) (1) then797 st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)798 (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*)799 else800 bind_new_P' ??801 (λregs4.λdata1.802 bind_new_P' ??803 (λregs3.λblp1.804 ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1805 (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧806 st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt)807 (decrement_stack_usage ? n st_pop) st2'808 ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest))809 ) (init ? fn1)810 ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …))811 ) (init ? fn)812 \end{lstlisting}766 % The statement is formalized in Matita in the following way. 767 % \begin{lstlisting} 768 % ; return_commutation : 769 % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 770 % ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 771 % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 772 % ∀f,fn. 773 % block_id … (pc_block (pc … st1)) ≠ 1 → 774 % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 775 % return 〈 f, fn, final P_in ? (RETURN …) 〉 → 776 % ∀n. stack_sizes f = return n → 777 % let curr_ret ≝ joint_if_result … fn in 778 % ∀st_pop,pc_pop. 779 % pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret 780 % (st_no_pc … st1) = return 〈 st_pop,pc_pop 〉 → 781 % ∀nxt.∀f1,fn1,id,args,dest. 782 % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop = 783 % return 〈 f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt 〉 → 784 % st_rel st1 st2 → 785 % ∀t_fn. 786 % fetch_internal_function … 787 % (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 788 % return 〈 f,t_fn 〉 → 789 % bind_new_P' ?? 790 % (λregs1.λdata. 791 % bind_new_P' ?? 792 % (λregs2.λblp. 793 % \snd blp = (RETURN …) ∧ 794 % ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 795 % (\fst blp) (st_no_pc … st2)= return st_fin ∧ 796 % ∃t_st_pop,t_pc_pop. 797 % pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f 798 % (joint_if_result … t_fn) st_fin = return 〈 t_st_pop,t_pc_pop 〉 ∧ 799 % sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs 800 % t_pc_pop = pc_pop ∧ 801 % if eqZb (block_id (pc_block pc_pop)) (1) then 802 % st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) 803 % (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*) 804 % else 805 % bind_new_P' ?? 806 % (λregs4.λdata1. 807 % bind_new_P' ?? 808 % (λregs3.λblp1. 809 % ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 810 % (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧ 811 % st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) 812 % (decrement_stack_usage ? n st_pop) st2' 813 % ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest)) 814 % ) (init ? fn1) 815 % ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …)) 816 % ) (init ? fn) 817 % \end{lstlisting} 813 818 814 819 \subsubsection{Conclusion} … … 828 833 f_lbls f_regs st_no_pc_rel st_rel → 829 834 let trans_prog ≝ b_graph_transform_program … init prog in 830 ∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in → 831 ∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧ 835 ∀init_in. 836 make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in → 837 ∃init_out. 838 make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧ 832 839 ∃[1] R. 833 840 status_simulation_with_init 
Deliverables/D4.4/paolo.tex
r3194 r3213 58 58 \lstset{extendedchars=false} 59 59 \lstset{inputencoding=utf8x} 60 \DeclareUnicodeCharacter{8797}{:= }60 \DeclareUnicodeCharacter{8797}{:=\ } 61 61 \DeclareUnicodeCharacter{10746}{++} 62 62 \DeclareUnicodeCharacter{9001}{\ensuremath{\langle}} 63 63 \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} 64 64 \DeclareUnicodeCharacter{8230}{.\!\!.\!\!.\@\ } 65 \author{Mauro Piccolo, Claudio Sacerdoti Coen and Paolo Tranquilli\\[15pt] 66 \small Department of Computer Science and Engineering, University of Bologna\\ 67 \small \verb\{Mauro.Piccolo, Claudio.SacerdotiCoen, Paolo.Tranquilli\}@unibo.it} 68 \title{Certifying the back end pass of the CerCo annotating compiler} 65 69 \date{} 66 \author{}67 70 68 71 \begin{document} 69 70 \thispagestyle{empty}71 72 \vspace*{1cm}73 \begin{center}74 \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}75 \end{center}76 77 \begin{minipage}{\textwidth}78 72 \maketitle 79 \end{minipage} 80 81 \vspace*{0.5cm} 82 \begin{center} 83 \begin{LARGE} 84 \textbf{ 85 Report n. D4.4\\ 86 ?????????????? 87 } 88 \end{LARGE} 89 \end{center} 90 91 \vspace*{2cm} 92 \begin{center} 93 \begin{large} 94 Version 1.1 95 \end{large} 96 \end{center} 97 98 \vspace*{0.5cm} 99 \begin{center} 100 \begin{large} 101 Main Authors:\\ 102 ???????????? 103 \end{large} 104 \end{center} 105 106 \vspace*{\fill} 107 108 \noindent 109 Project Acronym: \cerco{}\\ 110 Project full title: Certified Complexity\\ 111 Proposal/Contract no.: FP7ICT2009C243881 \cerco{}\\ 112 113 \clearpage 114 \pagestyle{myheadings} 115 \markright{\cerco{}, FP7ICT2009C243881} 116 117 \newpage 118 119 \vspace*{7cm} 120 \paragraph{Abstract} 121 BLA BLA BLA 122 \newpage 123 124 \tableofcontents 125 126 \newpage 73 \begin{abstract} 74 We present the certifying effort of the back end of the CerCo annotating 75 compiler to 8051 assembly. Apart from the usual effort needed in propagating 76 the extensional part of execution traces, additional care must be taken in 77 order to ensure a form of intensional correctness of the pass, necessary to 78 prove the lifting of computational costs correct. We concentrate here on two 79 aspects of the proof: how stack is dealt with during the pass, and how generic graph 80 language passes can be proven correct from an extensional and intensional point 81 of view. 82 \end{abstract} 127 83 128 84 \section{The BackEnd Correctness Proof at a Glance} 85 \label{sec:glance} 129 86 130 87 The backend part of the compiler takes an \s{RTLabs} program together with 131 88 an initialising cost label and gives the assembly code to be fed to the 132 89 assembler. From the semantic point of view, at this stage of the compiler, 133 we are interested in propagating structured traces, as explained in \cite{ ?}.90 we are interested in propagating structured traces, as explained in \cite{simulation}. 134 91 135 92 A schema with all the backend passes and the salient and common points of each one is the following: … … 156 113 The next two passes live in the graph part of \verb+joint+, and can benefit from 157 114 a generic approach to graph translation and its proof of correctness, as described 158 in~\ cite{mauro}.115 in~\autoref{modular}. 159 116 160 117 Next, a generic \verb+joint+ linearisation pass is performed to go from … … 171 128 to relate the states in the two languages. 172 129 173 \subsection{A common invariant} This block of traces with properties is recurrent enough to merit the 130 \subsection{A common invariant} 131 This block of traces with properties is recurrent enough to merit the 174 132 \s{matita} definition in \autoref{fig:ft_and_tlr}. We rely on the fact 175 133 that all semantics from \s{RTLabs} down to object code can be expressed … … 201 159 The additional property \verb+tlr_unrpt+ 202 160 tells that program counters do not repeat locally (i.e.\ between two labels) 203 in \verb+tlr+, a property needed for the soundness of the cost static analysis 204 (cf.~\cite{?}). 161 in \verb+tlr+, a property needed for the soundness of the cost static analysis. 205 162 206 163 \subsection{The statement} … … 212 169 only with respect to the \s{ASM} to object code correctness 213 170 \footnote{\verb+sigma+ and \verb+pol+ are what allows to maps instructions 214 between \s{ASM} and the produced object code. This information is gained during215 the jump expansion pass, cf.~\cite{ ?}.}.171 between \s{ASM} and the produced object code. This information is gained during 172 the jump expansion pass, cf.~\cite{policy}.}. 216 173 217 174 \begin{figure} … … 261 218 frontend traces, and we put it to use during the backend pass, 262 219 where we pass to a unique bounded stack space for all functions. More details 263 will be presented in \autoref{sec: ?}.220 will be presented in \autoref{sec:stack}. 264 221 265 222 The above explanation is why the backend correctness results requires some additional preconditions … … 270 227 actually the initial state). 271 228 272 \section{Dealing with the stack} 229 \section{Dealing with the Stack} 230 \label{sec:stack} 273 231 Setting apart the extensional details of the proofs, a delicate point is how 274 232 we deal with stack. … … 428 386 with respect to execution. There are more details involved than in a usual 429 387 extensional proof, regarding the intensional preservation. The details are 430 contained in~\cite{ ?}.388 contained in~\cite{simulation}. 431 389 432 390 Here we concentrate on a particular aspect that eludes the generic treatment: … … 467 425 as it is integrated in the fact that the execution step does not fail. 468 426 469 \include{mauro} 427 \input{mauro.tex} 428 429 \bibliographystyle{plain} 430 \bibliography{report} 470 431 \end{document} 
Deliverables/D4.4/report.tex
r3194 r3213 79 79 \begin{large} 80 80 Main Authors:\\ 81 XXXX %Dominic P. Mulligan and Claudio Sacerdoti Coen 81 Jaap Boender, Dominic P. Mulligan, Mauro Piccolo,\\ Claudio Sacerdoti Coen and 82 Paolo Tranquilli 82 83 \end{large} 83 84 \end{center} … … 97 98 98 99 \vspace*{7cm} 99 \paragraph{Abstract} 100 xxx 100 \paragraph{Summary} 101 The deliverable D4.4 is composed of the following parts: 102 103 \begin{enumerate} 104 105 \item This summary. 106 107 \item The paper \cite{simulation}. 108 109 \item The paper \cite{backend}. 110 111 \item The paper \cite{asm}. 112 113 \item The paper \cite{policy}. 114 115 \end{enumerate} 116 117 This document and all the related \textsf{matita} developments can be downloaded at the 118 page: 119 \begin{center} 120 {\tt http://cerco.cs.unibo.it/} 121 \end{center} 122 123 \bibliographystyle{unsrt} 124 {\scriptsize\bibliography{report}} 101 125 102 126 \newpage 103 127 104 \tableofcontents 128 \paragraph{Aim} 129 The aim of WP4 is is to build the trusted version of the compiler backend, 130 from the intermediate \textsf{RTLabs} language down to assembly. The development 131 is made in \textsf{matita}, and it allows the trsuted compiler to be extracted 132 to \textsf{OCaml}. 105 133 106 \newpage 134 The main planned contributions of deliverable D4.4 are formally checked proof 135 of the semantics correspondence between the intermediate code and the target 136 code, and of the preservation/modification of the control flow for complexity 137 analysis. 107 138 108 \section{Task} 109 \label{sect.task} 139 \paragraph{Preservation of structure} 140 In \cite{simulation} we present a genric approach to proving a forward 141 simulation preserving the intensional structure of traces. 110 142 111 The Grant Agreement describes deliverable D4.4 as follows: 112 \begin{quotation} 113 \textbf{Backend correctness proof}: Formally checked proof of the semantics correspondence between the intermediate code and the target code, and of the preservation/modification of the control flow for complexity analysis. An extensive validation of implementation of the Untrusted Cerco Prototype D5.1 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted CerCo Compiler sources and CIC encoding (D2.2, D5.1 and D4.2). 114 \end{quotation} 143 When a language 144 starts to be able to meddle with return addresses that live in memory, the call structure 145 is no more guaranteed to be preserved after the highlevel, structured 146 languages. This is has little meaning as far as pure extensional semantic 147 preservation is requiredafter all, if the source language meddles with the 148 call structure there is no problem as long as the target language will follow. 149 However in our approach we have cost labels spanning multiple calls, so that 150 the cost of what follows a call is ``paid'' in advance. This has no hope of 151 being correct if there is no guarantee that upon return from a call we land 152 after the call itself. 115 153 116 \newpage 154 In this part of the deliverable we will present our approach to this problem, 155 which goes by including in semantic traces structural conditions, and giving 156 generic proof obligations that enrich the classic stepbystep extensional 157 preservation proof with the necessary hypotheses to ensure the preservation 158 of the call and label structures. This approach can be applied on all passes 159 starting from the \textsf{RTLabs} to \textsf{RTL} down to the assembly one. 160 161 \paragraph{The backend correctness proof} 162 In \cite{backend}, we give an outline of the actual correctness proof for the 163 passes from \textsf{RTLabs} down to assembly. We skip the details of the 164 extensional parts of each pass and we concentrate on two main aspects: 165 how we deal with stack and how we ensure the conditions explained in 166 \cite{simulation} in the passes involving graph languages. 167 168 \paragraph{The assembler correctness proof} 169 In \cite{asm}, we present a proof of correctness of our assembler to object 170 code, given a correct policy for branch expansion (see next paragraph). 171 172 \paragraph{A branch expansion policy maker} 173 In \cite{policy} we finally present our algorithm for branch expansion, that is 174 how generic assembly jumps are expanded to the different type of jumps 175 available in the 8051 architecture (short, absolute and long). The correctness 176 of this algorithm is proved, and is what required by the correctness of the 177 whole assembler. 117 178 118 179 \includepdf[pages={}]{itp2013.pdf}
Note: See TracChangeset
for help on using the changeset viewer.