Changeset 3263 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 May 10, 2013, 1:40:31 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r3255 r3263 393 393 394 394 definition translate_fin_step: 395 ∀globals.ℕ → label → joint_fin_step ERTL → bind_fin_block LTL globals ≝ 396 λglobals,stack_sz,lbl,s. 395 ∀globals.list (joint_seq LTL globals) → 396 label → joint_fin_step ERTL → bind_fin_block LTL globals ≝ 397 λglobals,epilogue,lbl,s. 397 398 bret … (match s with 398 [ RETURN ⇒ 〈 delframe ? stack_sz, RETURN ?〉399 [ RETURN ⇒ 〈epilogue, RETURN ?〉 399 400  GOTO l ⇒ 〈[ ], GOTO ? l〉 400 401  TAILCALL abs _ _ ⇒ Ⓧabs … … 407 408 bind_new register (b_graph_translate_data ERTL LTL globals) ≝ 408 409 λthe_fixpoint,build,globals,int_fun. 410 νν RegisterCalleeSaved as callee_saved_store in 409 411 (* colour registers *) 410 let after ≝ analyse_liveness the_fixpoint globals int_fun in 411 let coloured_graph ≝ build … int_fun after in 412 (* compute new stack size *) 412 let after ≝ analyse_liveness the_fixpoint globals int_fun callee_saved_store in 413 let coloured_graph ≝ build … int_fun after callee_saved_store in 414 let callee_saved_pairs ≝ zip_pottier … RegisterCalleeSaved callee_saved_store in 415 let localss ≝ joint_if_local_stacksize ?? int_fun in 416 let save ≝ \fold[append ?, nil ?]_{R_r ∈ callee_saved_pairs} 417 (move ? localss false 418 (colouring … coloured_graph (inl … (\snd R_r))) 419 (decision_colour (\fst R_r))) in 420 let restore ≝ \fold[append ?, nil ?]_{R_r ∈ callee_saved_pairs} 421 (move ? localss false 422 (decision_colour (\fst R_r)) 423 (colouring … coloured_graph (inl … (\snd R_r)))) in 413 424 let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in 414 425 bret … … … 416 427 (* init_ret ≝ *) it 417 428 (* init_params ≝ *) it 418 (* init_stack_size ≝ *) stack_sz 419 (* added_prologue ≝ *) (newframe ? stack_sz) 420 (* new_regs ≝ *) [ ] 421 (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz) 422 (* f_fin ≝ *) (translate_fin_step globals stack_sz) 429 (* added_local_stacksize ≝ *) 0 430 (* added_params_stacksize ≝ *) 0 431 (* added_spilled_stacksize ≝ *) (spilled_no … coloured_graph) 432 (* added_prologue ≝ *) (newframe ? stack_sz @ save) 433 (* new_regs ≝ *) callee_saved_store 434 (* f_step ≝ *) (translate_step ? int_fun localss … coloured_graph stack_sz) 435 (* f_fin ≝ *) (translate_fin_step globals (restore @ delframe ? stack_sz)) 423 436 ????). 424 437 @hide_prf 425 [ 426  #l #c % ] 438 [3: #l #c % ] 427 439 cases daemon (* TODO *) 428 440 qed. … … 437 449 let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in 438 450 〈ltlprog, stack_cost … ltlprog, 2^16  globals_stacksize … ltlprog〉. 439 %451 #r0 #r1 #r2 #r3 #r4 #r5 #r6 #r7 % 440 452 qed. 441 453 … … 444 456 ∀p_in. 445 457 let cost_m ≝ \snd (\fst (ertl_to_ltl fix col p_in)) in 446 stack_cost_model_le (stack_cost ? p_in) cost_m. 447 #fix #col #p_in whd 448 @list_map_opt_All2 449 [ @(λid_def1,id_def2. 450 match \snd id_def1 with 451 [ Internal f1 ⇒ 452 match \snd id_def2 with 453 [ Internal f2 ⇒ 454 \fst id_def1 = \fst id_def2 ∧ 455 le (joint_if_stacksize … f1) (joint_if_stacksize … f2) 456  _ ⇒ False 457 ] 458  External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False  External _ ⇒ True ] 459 ]) 460  * #id * #f1 * #id' * #f2 normalize nodelta [*: * %] 461 ** #H %{H} % ] 462 @All2_of_map * #id * #f normalize nodelta [2: %] 463 % [%] 464 cases (b_graph_translate ?????) #f_out * #data ** 465 [2: #hd #tl ] * #f_lbls * #f_regs * [*] whd in ⊢ (%→?); #EQ_data 466 #props >(ss_def_out_eq … props) >EQ_data 467 generalize in match (joint_if_stacksize ???); generalize in match (spilled_no ??); 468 p_in // 469 qed. 470 458 stack_cost_model_le (stack_cost ? p_in) cost_m ≝ 459 λfix,col.joint_transform_monotone_stacksizes ….
Note: See TracChangeset
for help on using the changeset viewer.