 Timestamp:
 Feb 18, 2013, 6:26:22 PM (7 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLtoERTLptr.ma
r2674 r2675 39 39 definition translate_step: 40 40 ∀globals. 41 unit → 41 42 label 42 43 →joint_step ERTL globals 43 44 →bind_step_block ERTLptr globals ≝ 44 λglobals.λ l.λs.45 λglobals.λ_.λl.λs. 45 46 match s return λ_.bind_step_block ERTLptr globals with 46 47 [ CALL called args dest ⇒ … … 68 69 definition translate_fin_step: 69 70 ∀globals. 71 unit → 70 72 label 71 73 →joint_fin_step ERTL 72 74 →bind_fin_block ERTLptr globals ≝ 73 λglobals.λl.λs.bret … 〈[ ], fin_step_embed … s〉. 74 75 definition translate_internal : ∀globals: list ident. 76 joint_closed_internal_function ERTL globals → 77 joint_closed_internal_function ERTLptr globals ≝ 78 λglobals,int_fun. 79 (* initialize internal function *) 80 b_graph_translate ERTL ERTLptr globals 81 (joint_if_result … int_fun) 82 (joint_if_params … int_fun) 83 (joint_if_stacksize … int_fun) 84 (translate_step …) 85 (translate_fin_step …) 86 int_fun. 87 cases daemon. 88 qed. 75 λglobals.λ_.λl.λs.bret … 〈[ ], fin_step_embed … s〉. 89 76 90 77 definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝ 91 λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)). 78 b_graph_transform_program ERTL ERTLptr (λ_.unit) 79 (λglobals,int_fun. 80 〈〈joint_if_result … int_fun, 81 joint_if_params … int_fun, 82 joint_if_stacksize … int_fun〉, 83 it〉) 84 translate_step 85 translate_fin_step. 
src/joint/TranslateUtils.ma
r2674 r2675 255 255 All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ 256 256 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 257 src ~❨B, l❩~> dst in joint_if_code … def'.257 src ~❨B,src::l❩~> dst in joint_if_code … def'. 258 258 259 259 axiom fin_adds_graph_ok : … … 269 269 All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧ 270 270 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 271 src ~❨B, l❩~> it in joint_if_code … def'.271 src ~❨B,src::l❩~> it in joint_if_code … def'. 272 272 273 273 (* preserves first statement if a cost label (should be an invariant) *) … … 348 348 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧ 349 349 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ 350 src ~❨B, l,r❩~> dst in joint_if_code … def'.350 src ~❨B,src::l,r❩~> dst in joint_if_code … def'. 351 351 352 352 definition b_fin_adds_graph : … … 377 377 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧ 378 378 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ 379 src ~❨B, l,r❩~> it in joint_if_code … def'.379 src ~❨B,src::l,r❩~> it in joint_if_code … def'. 380 380 381 381 (* translation with inline fresh register allocation *) … … 391 391 (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) → 392 392 (* source function *) 393 joint_ internal_function src_g_pars globals →393 joint_closed_internal_function src_g_pars globals → 394 394 (* destination function *) 395 joint_ internal_function dst_g_pars globals ≝395 joint_closed_internal_function dst_g_pars globals ≝ 396 396 λsrc_g_pars,dst_g_pars,globals, 397 397 init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def. … … 414 414 ] in 415 415 foldi … f (joint_if_code … def) init. 416 @hide_prf >graph_code_has_point @mem_set_add_idqed.416 @hide_prf [ cases daemon (* TODO *)  >graph_code_has_point @mem_set_add_id ] qed. 417 417 418 418 definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝ … … 453 453 ∀init_ret,init_params,init_stack_size. 454 454 ∀f_step,f_fin,def_in. 455 luniverse_ok ?? def_in →456 code_closed … (joint_if_code … def_in) →457 455 let def_out ≝ 458 456 b_graph_translate src_g_pars dst_g_pars globals 459 457 init_ret init_params init_stack_size f_step f_fin def_in in 458 luniverse_ok ?? def_in → 460 459 luniverse_ok … def_out ∧ 461 code_closed … (joint_if_code … def_out) ∧462 460 joint_if_result … def_out = init_ret ∧ 463 461 joint_if_params … def_out = init_params ∧ … … 478 476 match s with 479 477 [ sequential s' nxt ⇒ 480 l ~❨f_step l s', l bls, regs❩~> nxt in joint_if_code … def_out478 l ~❨f_step l s', l::lbls, regs❩~> nxt in joint_if_code … def_out 481 479  final s' ⇒ 482 l ~❨f_fin l s', l bls, regs❩~> it in joint_if_code … def_out480 l ~❨f_fin l s', l::lbls, regs❩~> it in joint_if_code … def_out 483 481  FCOND abs _ _ _ ⇒ Ⓧabs 484 482 ]. 483 484 definition b_graph_transform_program : 485 ∀src_g_pars,dst_g_pars : graph_params. 486 ∀X : list ident → Type[0]. 487 (* initialization *) 488 (∀globals.joint_closed_internal_function src_g_pars globals → 489 (call_dest dst_g_pars) × (paramsT dst_g_pars) × ℕ × (X globals)) → 490 (* functions dictating the translation *) 491 (∀globals.X globals → label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) → 492 (∀globals.X globals → label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) → 493 joint_program src_g_pars → joint_program dst_g_pars ≝ 494 λsrc,dst,X,init,f_step,f_fin,p. 495 transform_program ??? p 496 (λvarnames.transf_fundef ?? (λdef_in. 497 let 〈fields, init_data〉 ≝ init varnames def_in in 498 let 〈init_ret, init_params, init_stack_size〉 ≝ fields in 499 b_graph_translate … init_ret init_params init_stack_size 500 (f_step ? init_data) (f_fin ? init_data) def_in)). 485 501 486 502 definition added_registers : 
src/joint/semanticsUtils.ma
r2674 r2675 3 3 include "utilities/hide.ma". 4 4 include "ASM/BitVectorTrie.ma". 5 include "joint/TranslateUtils.ma".6 5 7 6 record hw_register_env : Type[0] ≝ … … 163 162 whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} 164 163 qed. 165 166 (*lemma b_graph_translate_eval :167 ∀src : sem_graph_params.168 ∀dst : sem_graph_params.169 ∀globals: list ident.170 ∀init_ret,init_params,init_stack_size.171 ∀f_step,f_fin,def_in.172 let def_out ≝173 b_graph_translate src_g_pars dst_g_pars globals174 init_ret init_params init_stack_size f_step f_fin def_in in175 ∀st : state_pc src176 *)
Note: See TracChangeset
for help on using the changeset viewer.