Changeset 2952 for src/joint/semanticsUtils.ma
 Timestamp:
 Mar 26, 2013, 2:01:15 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semanticsUtils.ma
r2946 r2952 136 136 on _pars : sem_lin_params to sem_params. 137 137 138 (* watch out, implementation dependent: 139 an_identifier SymbolTag one must be unused (used for premain) 140 *) 141 definition pre_main_id : ident ≝ an_identifier … one. 142 138 (* TODO move elsewhere *) 143 139 lemma lookup_opt_pm_set_elim : ∀A.∀P : option A → Prop.∀p,q,o,m. 144 140 (p = q → P o) → … … 162 158 qed. 163 159 164 (* we just manually overwrite genv_t tables with the pre_main.165 the RTLabs → RTL pass will need to ensure no pre_main_id is actually present *)166 definition joint_globalenv :167 ∀pars : sem_params.joint_program pars → genv_t ? ≝168 λpars,prog.169 let genv ≝ drop_fn … pre_main_id (globalenv … (λx.x) prog) in170 mk_genv_t ?171 (insert … one (Internal … (pre_main_generator … pars prog)) (functions … genv))172 (nextfunction … genv)173 (add … (symbols … genv) pre_main_id (mk_block (1)))174 ?.175 @hide_prf176 whd in match insert; normalize nodelta #b177 @lookup_opt_pm_set_elim #H destruct178 [ #_ %{pre_main_id} @lookup_add_hit ]179 #G cases (functions_inv … G) #id #EQ %{id}180 @lookup_add_elim #EQid destruct [2: assumption ]181 @⊥ whd in match drop_fn in EQ; normalize nodelta in EQ;182 >lookup_remove_hit in EQ; #ABS destruct183 qed.184 185 160 lemma fetch_statement_eq : ∀p:sem_params.∀g. 186 ∀ge : genv _t (joint_function p g).∀ptr : program_counter.161 ∀ge : genv p g.∀ptr : program_counter. 187 162 ∀i,fn,s. 188 163 fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 → … … 196 171 197 172 lemma fetch_statement_inv : ∀p:sem_params.∀g. 198 ∀ge : genv _t (joint_function p g).∀ptr : program_counter.173 ∀ge : genv p g.∀ptr : program_counter. 199 174 ∀i,fn,s. 200 175 fetch_statement … ge ptr = OK … 〈i, fn, s〉 → … … 204 179 #p #g #ge #ptr #i #fn #s #H 205 180 elim (bind_inversion ????? H) * #i #f' * #EQ1 H #H 206 elim (bind_inversion ????? H) #s' * #H181 elim (bind_inversion ????? H) #s' * H #H 207 182 lapply (opt_eq_from_res ???? H) H #EQ2 208 183 whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} … … 421 396 include alias "common/Pointers.ma". 422 397 423 lemma fetch_function_transf : 424 ∀A,B,V,init.∀prog_in : program A V. 425 ∀trans : ∀vars.A vars → B vars. 426 let prog_out ≝ transform_program … prog_in trans in 398 (* TODO move *) 399 lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l. 400 #A #P #Q #l #H elim l l [2: #hd #tl #IH] * #G whd /3 by or_introl, or_intror/ qed. 401 402 definition joint_globalenv : 403 ∀p : sem_params.∀pr:joint_program p. 404 (ident → option ℕ) → genv p (prog_var_names … pr) ≝ 405 λp,prog,stacksizes. 406 let genv ≝ globalenv … (λx.x) prog in 407 mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog). 408 #s #H 409 elim (find_symbol_exists ?? (λx.x) … prog s ?) 410 [ #bl #EQ >EQ % #ABS destruct ] 411 @Exists_append_r 412 @(Exists_mp … H) // 413 qed. 414 415 lemma opt_to_res_bind : ∀X,Y,m,f,e.opt_to_res Y e (! x ← m ; f x) = 416 ! x ← opt_to_res X e m ; opt_to_res Y e (f x). 417 #X #Y * [2: #x] #f #e % qed. 418 419 lemma fetch_function_transf: 420 ∀src,dst : sem_params.∀prog_in : joint_program src. 421 ∀stacksizes. 422 ∀trans : ∀vars.joint_function src vars → joint_function dst vars. 423 let prog_out ≝ 424 mk_joint_program dst 425 (transform_program … prog_in trans) (init_cost_label … prog_in) in 427 426 ∀bl. 428 fetch_function … (globalenv … init prog_out) bl = 429 ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ; 430 return 〈i, trans … f〉. 431 #A #B #V #init #prog_in #trans #bl 432 whd in match fetch_function; normalize nodelta 433 >(symbol_for_block_transf A B V init prog_in trans) 434 cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind 427 fetch_function … (joint_globalenv … prog_out stacksizes) bl = 428 if eqZb (block_id bl) (1) then 429 return 〈pre_main_id, Internal ? (pre_main_generator … dst prog_out)〉 430 else 431 ! 〈id, f〉 ← fetch_function … (joint_globalenv … prog_in stacksizes) bl ; 432 return 〈id, trans … f〉. 433 #src #dst #p #sizes #tf whd 434 lapply (transform_program_match … tf p) 435 #MATCH 436 whd in match fetch_function; 437 whd in match joint_globalenv; normalize nodelta 438 #bl @eqZb_elim #Hbl normalize nodelta [ % ] 439 >symbol_for_block_transf 440 >opt_to_res_bind >opt_to_res_bind in ⊢ (???%); >m_bind_bind 441 @m_bind_ext_eq #id 435 442 whd in match find_funct_ptr; normalize nodelta 436 whd in match (block_region (pi1 ?? bl)); 437 cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try % 438 >(functions_transf A B V init prog_in trans p) 439 cases (lookup_opt ???) // 443 cases bl bl ** [2,3: #p] normalize nodelta #_ try % 444 lapply (functions_match … (globalenv_match … MATCH) p) try @(λx.x) 445 [#v #w * //] 446 lapply (sym_eq ????) 447 whd in match prog_var_names; normalize nodelta 448 #E >(K ?? E) E normalize nodelta 449 cases (lookup_opt ???) [2: #x ] normalize nodelta 450 cases (lookup_opt ???) [2,4: #y ] normalize nodelta 451 * % 440 452 qed. 441 453 442 454 lemma fetch_internal_function_transf : 443 ∀A,B,V,init.∀prog_in : program (λvars.fundef (A vars)) V. 444 ∀trans : ∀vars.A vars → B vars. 445 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in 455 ∀src,dst : sem_params.∀prog_in : joint_program src. 456 ∀stacksizes. 457 ∀trans : ∀vars.joint_closed_internal_function src vars → joint_closed_internal_function dst vars. 458 let prog_out ≝ 459 mk_joint_program dst 460 (transform_program … prog_in (λvars.transf_fundef … (trans vars))) (init_cost_label … prog_in) in 446 461 ∀bl. 447 fetch_internal_function … (globalenv … init prog_out) bl = 448 ! 〈i, f〉 ← fetch_internal_function … (globalenv … init prog_in) bl ; 449 return 〈i, trans … f〉. 450 #A #B #V #init #prog #trans #bl 451 whd in match fetch_internal_function; normalize nodelta 452 >(fetch_function_transf … prog) 453 cases (fetch_function ???) 454 [ * #id * #f %  #e % ] 462 fetch_internal_function … (joint_globalenv … prog_out stacksizes) bl = 463 if eqZb (block_id bl) (1) then 464 return 〈pre_main_id, pre_main_generator … dst prog_out〉 465 else 466 ! 〈i, f〉 ← fetch_internal_function … (joint_globalenv … prog_in stacksizes) bl ; 467 return 〈i, trans … f〉. 468 #src #dst #p #sizes #tf whd 469 #bl whd in match fetch_internal_function; normalize nodelta 470 >(fetch_function_transf … p) 471 @eqZb_elim #Hbl [%] normalize nodelta >m_bind_bind >m_bind_bind 472 @m_bind_ext_eq * #id * #f % 455 473 qed. 456 474 … … 485 503 definition b_graph_transform_program_props ≝ 486 504 λsrc,dst : sem_graph_params. 505 λstacksizes. 487 506 λdata,prog_in. 488 507 λinit_regs : block → list register. … … 490 509 λf_regs : block → label → list register. 491 510 let prog_out ≝ b_graph_transform_program src dst data prog_in in 492 let src_genv ≝ joint_globalenv src prog_in in493 let dst_genv ≝ joint_globalenv dst prog_out in511 let src_genv ≝ joint_globalenv src prog_in stacksizes in 512 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 494 513 ∀bl,def_in. 495 514 block_id … bl ≠ 1 → … … 503 522 lemma make_b_graph_transform_program_props : 504 523 ∀src,dst:sem_graph_params. 524 ∀stacksizes. 505 525 ∀data : ∀globals.joint_closed_internal_function src globals → 506 526 bound_b_graph_translate_data src dst globals. 507 527 ∀prog_in : joint_program src. 508 528 let prog_out ≝ b_graph_transform_program … data prog_in in 509 let src_genv ≝ joint_globalenv src prog_in in510 let dst_genv ≝ joint_globalenv dst prog_out in529 let src_genv ≝ joint_globalenv src prog_in stacksizes in 530 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 511 531 ∃init_regs : block → list register. 512 532 ∃f_lbls : block → label → list label. 513 533 ∃f_regs : block → label → list register. 514 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.534 b_graph_transform_program_props src dst stacksizes data prog_in init_regs f_lbls f_regs. 515 535 cases daemon (* TOREDO 516 536 #src #dst #data #prog_in … … 612 632 qed. 613 633 634 lemma if_elim' : ∀A : Type[0].∀P : A → Prop.∀b : bool.∀c1,c2 : A. 635 (b → P c1) → (¬(bool_to_Prop b) → P c2) → P (if b then c1 else c2). 636 #A #P * /3 by Prop_notb/ qed. 637 614 638 lemma b_graph_transform_program_fetch_internal_function : 615 639 ∀src,dst:sem_graph_params. 640 ∀stacksizes. 616 641 ∀data : ∀globals.joint_closed_internal_function src globals → 617 642 bound_b_graph_translate_data src dst globals. … … 620 645 ∀f_lbls : block → label → list label. 621 646 ∀f_regs : block → label → list register. 622 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →647 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs → 623 648 let prog_out ≝ b_graph_transform_program … data prog_in in 624 let src_genv ≝ joint_globalenv src prog_in in625 let dst_genv ≝ joint_globalenv dst prog_out in649 let src_genv ≝ joint_globalenv src prog_in stacksizes in 650 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 626 651 ∀bl : Σbl.block_region … bl = Code.∀id,def_in. 627 652 block_id … bl ≠ 1 → … … 632 657 b_graph_translate_props src dst ? init_data 633 658 def_in def_out (f_lbls bl) (f_regs bl). 634 #src #dst # data #prog_in659 #src #dst #stacksizes #data #prog_in 635 660 #init_regs #f_lbls #f_regs #props 636 661 #bl #id #def_in #NEQ 637 662 #H @('bind_inversion H) * #id' * #def_in' H 638 normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct 639 @('bind_inversion (opt_eq_from_res … H)) H #id' #EQ1 640 #H @('bind_inversion H) H #def_in' #H 641 whd in ⊢ (??%%→?); #EQ destruct 663 normalize nodelta [2: #_ whd in ⊢ (??%%→?); #ABS destruct ] 664 whd in match fetch_function; normalize nodelta 665 >(eqZb_false … NEQ) normalize nodelta 666 #H @('bind_inversion (opt_eq_from_res … H)) H #id'' #EQ1 667 #H @('bind_inversion H) H #def_in'' #H 668 whd in ⊢ (??%%→??%%→?); #EQ2 #EQ3 destruct 642 669 cases (props … NEQ H) 643 670 #loc_data * #def_out ** #H1 #H2 #H3 … … 646 673 whd in match fetch_internal_function; 647 674 whd in match fetch_function; normalize nodelta 648 cases daemon (* TOREDO 675 >(eqZb_false … NEQ) normalize nodelta 649 676 >symbol_for_block_transf >EQ1 >m_return_bind 650 >H1 % *)677 >H1 % 651 678 qed. 652 679 653 680 lemma b_graph_transform_program_fetch_statement : 654 ∀src,dst:sem_graph_params. 681 ∀src,dst:sem_graph_params.∀stacksizes. 655 682 ∀data : ∀globals.joint_closed_internal_function src globals → 656 683 bound_b_graph_translate_data src dst globals. … … 659 686 ∀f_lbls : block → label → list label. 660 687 ∀f_regs : block → label → list register. 661 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →688 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs → 662 689 let prog_out ≝ b_graph_transform_program … data prog_in in 663 let src_genv ≝ joint_globalenv src prog_in in664 let dst_genv ≝ joint_globalenv dst prog_out in690 let src_genv ≝ joint_globalenv src prog_in stacksizes in 691 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 665 692 ∀pc,id,def_in,s. 666 693 block_id … (pc_block … pc) ≠ 1 → … … 686 713  FCOND abs _ _ _ ⇒ Ⓧabs 687 714 ]. 688 #src #dst # data #prog_in715 #src #dst #stacksizes #data #prog_in 689 716 #init_regs #f_lbls #f_regs #props 690 717 #pc #id #def_in #s #NEQ … … 701 728 702 729 lemma b_graph_transform_program_fetch_statement_plus : 703 ∀src,dst:sem_graph_params. 730 ∀src,dst:sem_graph_params.∀stacksizes. 704 731 ∀data : ∀globals.joint_closed_internal_function src globals → 705 732 bound_b_graph_translate_data src dst globals. … … 708 735 ∀f_lbls : block → label → list label. 709 736 ∀f_regs : block → label → list register. 710 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →737 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs → 711 738 let prog_out ≝ b_graph_transform_program … data prog_in in 712 let src_genv ≝ joint_globalenv src prog_in in713 let dst_genv ≝ joint_globalenv dst prog_out in739 let src_genv ≝ joint_globalenv src prog_in stacksizes in 740 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 714 741 ∀pc,id,def_in,s. 715 742 block_id … (pc_block … pc) ≠ 1 → … … 744 771  FCOND abs _ _ _ ⇒ Ⓧabs 745 772 ]. 746 #src #dst # data #prog_in773 #src #dst #stacksizes #data #prog_in 747 774 #init_regs #f_lbls #f_regs #props 748 775 #pc #id #def_in #s #NEQ
Note: See TracChangeset
for help on using the changeset viewer.