 Timestamp:
 Feb 19, 2013, 6:48:32 PM (7 years ago)
 Location:
 src/ERTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r2490 r2681 289 289 290 290 definition translate_address : 291 ∀globals.bool → ∀i. member ? (eq_identifier ?) iglobals → decision → decision →291 ∀globals.bool → ∀i.i ∈ globals → decision → decision → 292 292 list (joint_seq LTL globals) ≝ 293 293 λglobals,carry_lives_after,id,prf,addr1,addr2. … … 300 300 ∀globals.∀after : valuation register_lattice. 301 301 coloured_graph after → 302 ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals)≝302 ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝ 303 303 λglobals,after,grph,stack_sz,lbl,s. 304 bret … ( 304 305 let lookup ≝ λr.colouring … grph (inl … r) in 305 306 let lookup_arg ≝ λa.match a with … … 311 312 match s with 312 313 [ step_seq s' ⇒ 313 match s' return λ_.s eq_block LTL globals (joint_step LTL globals)with314 [ COMMENT c ⇒ COMMENT … c315  COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl314 match s' return λ_.step_block LTL globals with 315 [ COMMENT c ⇒ [COMMENT … c] 316  COST_LABEL cost_lbl ⇒ [COST_LABEL … cost_lbl] 316 317  POP r ⇒ 317 318 POP … A :: … … 330 331 (lookup_arg addr1) 331 332 (lookup_arg addr2) 332  CLEAR_CARRY ⇒ CLEAR_CARRY …333  SET_CARRY ⇒ CLEAR_CARRY …333  CLEAR_CARRY ⇒ [CLEAR_CARRY ??] 334  SET_CARRY ⇒ [CLEAR_CARRY ??] 334 335  OP2 op dst arg1 arg2 ⇒ 335 336 translate_op2_smart ? carry_lives_after op … … 367 368 move (lookup r) (arg_decision_imm (byte_of_nat stack_sz)) 368 369 ] 369  CALL f n_args _ ⇒ 370 ] 371  COND r ltrue ⇒ 372 〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉 373  CALL f n_args _ ⇒ 370 374 match f with 371 [ inl f ⇒ [ CALL LTL ? (inl … f) n_args it ] 375 [ inl f ⇒ 376 〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉 372 377  inr dp ⇒ 373 378 let 〈dpl, dph〉 ≝ dp in 374 move_to_dp … (lookup_arg dpl) (lookup_arg dph) @375 [ CALL LTL ? (inr … 〈it, it〉) n_args it ]379 〈add_dummy_variance … (move_to_dp … (lookup_arg dpl) (lookup_arg dph)), 380 λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉 376 381 ] 377 ] 378  COND r ltrue ⇒ 379 〈move RegisterA (lookup r),COND … it ltrue〉 380 ]. 382 ]). 381 383 382 384 definition translate_fin_step: 383 ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL)≝385 ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝ 384 386 λglobals,lbl,s. 385 match s return λ_.seq_block LTL globals (joint_fin_step LTL) with 387 bret … (〈[ ], 388 match s with 386 389 [ RETURN ⇒ RETURN ? 387 390  GOTO l ⇒ GOTO ? l 388 391  TAILCALL abs _ _ ⇒ Ⓧabs 389 ] .390 391 definition translate_ internal: ∀globals: list ident.392 ]〉). 393 394 definition translate_data : ∀globals. 392 395 joint_closed_internal_function ERTL globals → 393 joint_closed_internal_function LTL globals ≝ 394 λglobals,int_fun. 395 (* initialize graph *) 396 let entry ≝ pi1 … (joint_if_entry … int_fun) in 397 let exit ≝ pi1 … (joint_if_exit … int_fun) in 398 (* colour registers *) 399 let after ≝ analyse_liveness globals int_fun in 400 let coloured_graph ≝ build after in 401 (* compute new stack size *) 402 let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in 403 (* initialize internal function *) 404 let init ≝ init_graph_if LTL globals 405 (joint_if_luniverse … int_fun) 406 (joint_if_runiverse … int_fun) 407 it it [ ] stack_sz entry exit in 408 graph_translate … 409 init 410 (translate_step … coloured_graph stack_sz) 411 (translate_fin_step …) 412 int_fun. 413 cases daemon (* TODO *) qed. 396 bind_new register (b_graph_translate_data ERTL LTL globals) ≝ 397 λglobals,int_fun. 398 (* colour registers *) 399 let after ≝ analyse_liveness globals int_fun in 400 let coloured_graph ≝ build after in 401 (* compute new stack size *) 402 let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in 403 bret … 404 (mk_b_graph_translate_data ERTL LTL globals 405 (* init_ret ≝ *) it 406 (* init_params ≝ *) it 407 (* init_stack_size ≝ *) stack_sz 408 (* added_prologue ≝ *) [ ] 409 (* f_step ≝ *) (translate_step … coloured_graph stack_sz) 410 (* f_fin ≝ *) (translate_fin_step globals) 411 ???). 412 @hide_prf 413 [ #l #c % ] 414 cases daemon (* TODO *) 415 qed. 414 416 415 417 definition ertl_to_ltl: ertl_program → ltl_program ≝ 416 λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).418 b_graph_transform_program … translate_data. 
src/ERTL/liveness.ma
r2490 r2681 83 83 ] 84 84 (* Potentially destroys all callersave hardware registers. *) 85  CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉86 85 ] 86  CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉 87 87  COND r lbl_true ⇒ rl_bottom 88 88 ] 89 89  final _ ⇒ rl_bottom 90  FCOND abs _ _ _ ⇒ Ⓧabs 90 91 ]. 91 92 … … 138 139 ] 139 140 (* Reads the hardware registers that are used to pass parameters. *) 140  CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉141 141  _ ⇒ rl_bottom 142 142 ] 143  CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉 143 144  COND r lbl_true ⇒ rl_psingleton r 144 145 ] … … 149 150  TAILCALL abs _ _ ⇒ match abs in False with [ ] 150 151 ] 152  FCOND abs _ _ _ ⇒ Ⓧabs 151 153 ]. 152 154 … … 218 220  _ ⇒ None ? 219 221 ] 220  COND __ ⇒ None ?222  _ ⇒ None ? 221 223 ] 222 224  _ ⇒ None ?
Note: See TracChangeset
for help on using the changeset viewer.