 Timestamp:
 May 10, 2013, 1:40:31 PM (8 years ago)
 Location:
 src/joint
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Joint.ma
r3145 r3263 481 481 joint_if_result : call_dest p; 482 482 joint_if_params : paramsT p; 483 joint_if_stacksize: nat;484 483 joint_if_local_stacksize: nat; (* size of the stack devoted to "forced" stack positions 485 484 (that are already on stack in the front end) *) 485 joint_if_params_stacksize: nat; (* size of the stack devoted to parameters *) 486 joint_if_spilled_stacksize: nat; (* size of the stack devoted to spilled registers *) 486 487 joint_if_code : codeT p globals ; 487 488 joint_if_entry : code_point p (* Paolo: condition entry ∈ code is ensured by good_if ; 488 489 joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *) 489 490 }. 491 492 definition joint_if_stacksize ≝ λp,globals,fn. 493 joint_if_spilled_stacksize p globals fn + joint_if_params_stacksize … fn + 494 joint_if_local_stacksize … fn. 490 495 491 496 definition regs_in_universe : ∀p,globals. … … 560 565 (joint_if_params … int_fun) (joint_if_stacksize … int_fun) 561 566 (joint_if_local_stacksize … int_fun) 567 (joint_if_params_stacksize … int_fun) 562 568 graph entry (*exit*). 563 569 … … 569 575 luniverse (joint_if_runiverse … p) (joint_if_result … p) 570 576 (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) 577 (joint_if_params_stacksize … p) 571 578 (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). 572 579 … … 578 585 (joint_if_luniverse … p) runiverse (joint_if_result … p) 579 586 (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) 587 (joint_if_params_stacksize … p) 580 588 (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). 581 589 … … 588 596 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 589 597 (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p) 598 (joint_if_params_stacksize … p) 590 599 code 591 600 (joint_if_entry … p) 
src/joint/TranslateUtils.ma
r3037 r3263 412 412 { init_ret : call_dest dst 413 413 ; init_params : paramsT dst 414 ; init_stack_size : ℕ 414 ; added_local_stacksize : ℕ 415 ; added_params_stacksize : ℕ 416 ; added_spilled_stacksize : ℕ 415 417 ; added_prologue : list (joint_seq dst globals) 416 418 ; new_regs : list register (* new registers added globally *) … … 499 501 ; pars_def_out_eq : 500 502 joint_if_params … def_out = init_params … data 501 ; ss_def_out_eq : 502 joint_if_stacksize … def_out = init_stack_size … data 503 ; local_ss_def_out_eq : 504 joint_if_local_stacksize … def_out = 505 joint_if_local_stacksize … def_in + added_local_stacksize … data 506 ; params_ss_def_out_eq : 507 joint_if_params_stacksize … def_out = 508 joint_if_params_stacksize … def_in + added_params_stacksize … data 509 ; spilled_ss_def_out_eq : 510 joint_if_spilled_stacksize … def_out = 511 joint_if_spilled_stacksize … def_in + added_spilled_stacksize … data 503 512 ; partition_lbls : partial_partition … f_lbls 504 513 ; partition_regs : partial_partition … f_regs … … 541 550 542 551 definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉. 552 543 553 definition set_entry ≝ 544 554 λglobals: list ident. … … 551 561 (joint_if_params … int_fun) (joint_if_stacksize … int_fun) 552 562 (joint_if_local_stacksize … int_fun) 563 (joint_if_params_stacksize … int_fun) 553 564 (joint_if_code … int_fun) entry (*exit*). 554 565 … … 576 587 (joint_if_luniverse … def) 577 588 runiv 578 (init_ret … data) (init_params … data) (init_stack_size … data) 579 (joint_if_local_stacksize … def) 589 (init_ret … data) (init_params … data) 590 (joint_if_local_stacksize … def + added_local_stacksize … data) 591 (joint_if_params_stacksize … def + added_params_stacksize … data) 592 (joint_if_spilled_stacksize … def + added_spilled_stacksize … data) 580 593 (empty_map ? (joint_statement ??)) 581 594 entry in … … 677 690 add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). 678 691 *) 692 693 include "joint/joint_stacksizes.ma". 694 695 lemma bind_new_P_mp' : ∀R,X,P,Q,m. 696 (∀l,x.P l x → Q l x) → 697 bind_new_P' R X P m → bind_new_P' R X Q m. 698 #R #X #P #Q #m lapply Q Q lapply P P elim m m 699 [ #x #P #Q #H #G @H @G 700  #f #IH #P #Q #H #G #r 701 @IH [3: @(G r) *:] #l @H 702 ] 703 qed. 704 705 lemma joint_transform_monotone_stacksizes : 706 ∀src_g_pars,dst_g_pars : graph_params. 707 (* initialization *) 708 ∀data. 709 ∀p_in. 710 let p_out ≝ b_graph_transform_program src_g_pars dst_g_pars data p_in in 711 stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out). 712 #src #dst #data #p_in 713 whd 714 @list_map_opt_All2 715 [ @(λid_def1,id_def2. 716 match \snd id_def1 with 717 [ Internal f1 ⇒ 718 match \snd id_def2 with 719 [ Internal f2 ⇒ 720 \fst id_def1 = \fst id_def2 ∧ 721 le (joint_if_stacksize … f1) (joint_if_stacksize … f2) 722  _ ⇒ False 723 ] 724  External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False  External _ ⇒ True ] 725 ]) 726  * #id * #f1 * #id' * #f2 normalize nodelta [*: * %] 727 ** #H %{H} % ] 728 @All2_of_map * #id * #f normalize nodelta [2: %] 729 % [%] 730 cases (b_graph_translate ?????) 731 whd in match (jp_functions dst ?); 732 lapply f f 733 generalize in match (?@jp_functions ??); #globals 734 #f_in #f_out * #data' * #regs * #f_lbls * #f_regs * #inst #props 735 whd in match joint_if_stacksize; normalize nodelta 736 @le_plus [ @le_plus ] 737 [ >(spilled_ss_def_out_eq … props) 738  >(params_ss_def_out_eq … props) 739  >(local_ss_def_out_eq … props) 740 ] // 741 qed. 
src/joint/linearise.ma
r3037 r3263 849 849 (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig) 850 850 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) 851 (joint_if_stacksize ?? f_sig) (joint_if_local_stacksize ?? f_sig) 852 code 0 (* exit is dummy! *), hide_prf ??», 851 (joint_if_local_stacksize ?? f_sig) 852 (joint_if_params_stacksize ?? f_sig) 853 (joint_if_spilled_stacksize ?? f_sig) 854 code 0, hide_prf ??», 853 855 sigma〉, proj1 ?? (pi2 ?? code_sigma)». 854 856 cases daemon (*)
Note: See TracChangeset
for help on using the changeset viewer.