Changeset 2806
 Timestamp:
 Mar 7, 2013, 2:51:40 PM (7 years ago)
 Location:
 src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToERTLptr.ma
r2696 r2806 82 82 (* init_stack_size ≝ *) (joint_if_stacksize … def) 83 83 (* added_prologue ≝ *) [ ] 84 (* new_regs ≝ *) [ ] 84 85 (* f_step ≝ *) (translate_step globals) 85 86 (* f_fin ≝ *) (translate_fin_step globals) 86 ??? ).87 ????). 87 88 @hide_prf 88 [ #l #c % ] 89 [ #l * [ #c'  * #f #args #dest  #a #ltrue  #s ] #c whd 90 [3: #r1 ] #l' #EQ destruct try % 91 cases s in EQ; whd in match ensure_step_block; normalize nodelta 92 try #a try #b try #c try #d try #e try #f destruct 93  #l #c % 94 ] 89 95 #l * 90 [ #l whd %{I} %{I} %1%91  whd %{I I}92  #abs #called #args whd %{I I}93  #c %{I} %{I} #l%96 [ #l' whd %{I} %{I} %{I} %2 % % 97  whd %{I} %{I I} 98  #abs #called #args whd %{I} %{I I} 99  #c #l' whd %{I} %{I} %{I} % 94 100  * #called #args #dest whd in match translate_step; normalize nodelta whd 95 [ %{I} %{I} #l % 96  #r whd %{I} %{(λ_.I)} % [ % [ % [ %{I} ]]] #l 97 [1,3: %{I} %1 % 98 *: % 99 ] 101 [ #l' %{I} %{I} %{I} % 102  #r #l' whd %{I} % [2: %{I I} ] % [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 % 100 103 ] 101  #a #l_true whd %{I} %{I} #l %{I} %2 %1 % 102  #s whd %{I} %{I} #l whd @(All_mp … (In ? (step_labels … s))) 103 [ #l' #H %2{H} ] cases s s // 104  #a #l_true whd #l %{I} %{I} % %{I} [ %2 ] %1 % 105  #s whd #l %{I} %{I} whd % 106 [ @(All_mp … (In ? (step_labels … s))) [ #l' #H %2{H} ] cases s s // ] 107 cut (∀X,l1,l2.l1 = l2 → All X (In X l1) l2) 108 [ #X #l1 #l2 #EQ destruct elim l2 [ % ] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #H %2{H} ] 109 #aux @aux cases s // 104 110 ] 105 111 qed. 
src/ERTLptr/ERTLptrToLTL.ma
r2774 r2806 435 435 (* init_stack_size ≝ *) stack_sz 436 436 (* added_prologue ≝ *) [ ] 437 (* new_regs ≝ *) [ ] 437 438 (* f_step ≝ *) (translate_step … coloured_graph stack_sz) 438 439 (* f_fin ≝ *) (translate_fin_step globals) 439 ??? ).440 ????). 440 441 @hide_prf 441 [ #l #c % ] 442 [ 443  #l #c % ] 442 444 cases daemon (* TODO *) 443 445 qed. 
src/RTL/RTLToERTL.ma
r2689 r2806 37 37 38 38 definition get_params_stack : 39 ∀globals. list register →40 bind_new register (list (joint_seq ERTL globals)) ≝41 λglobals ,params.42 νtmpr,addr1,addr2 in39 ∀globals.register → register → register → list register → 40 list (joint_seq ERTL globals) ≝ 41 λglobals. 42 λtmpr,addr1,addr2,params. 43 43 let params_length_byte : Byte ≝ bitvector_of_nat ? (params) in 44 44 [ (ertl_frame_size tmpr : joint_seq ??) ; … … 52 52 53 53 definition get_params ≝ 54 λglobals, params.54 λglobals,tmpr,addr1,addr2,params. 55 55 let n ≝ min (length … params) (length … RegisterParams) in 56 56 let 〈hdw_params, stack_params〉 ≝ list_split … n params in 57 get_params_hdw globals hdw_params @ @ get_params_stack …stack_params.57 get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params. 58 58 59 59 definition save_return : … … 130 130 131 131 definition prologue : 132 ∀globals.list register → register → register → list (register×Register) → 132 ∀globals.list register → register → register → register → register → register → 133 list (register×Register) → 133 134 bind_new register (list (joint_seq ERTL globals)) ≝ 134 λglobals,params,sral,srah, sregs.135 λglobals,params,sral,srah,tmpr,addr1,addr2,sregs. 135 136 [ (ertl_new_frame : joint_seq ??) ; 136 137 POP … sral ; 137 138 POP … srah 138 ] @ @ save_hdws … sregs @@ get_params …params.139 ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params. 139 140 140 141 definition set_params_hdw : … … 221 222 match s return λ_.bind_step_block ?? with 222 223 [ step_seq s ⇒ 223 match s return λ_.bind_step_block ?? with224 [ PUSH _ ⇒ bret …[ ] (*CSC: XXXX should not be in the syntax *)225  POP _ ⇒ bret …[ ] (*CSC: XXXX should not be in the syntax *)226  MOVE rs ⇒ bret …[PSD (\fst rs) ← \snd rs]224 bret … match s return λ_.step_block ?? with 225 [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *) 226  POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *) 227  MOVE rs ⇒ [PSD (\fst rs) ← \snd rs] 227 228  ADDRESS x prf r1 r2 ⇒ 228 bret …[ADDRESS ERTL ? x prf r1 r2]229 [ADDRESS ERTL ? x prf r1 r2] 229 230  OPACCS op destr1 destr2 srcr1 srcr2 ⇒ 230 bret …[OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]231 [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2] 231 232  OP1 op1 destr srcr ⇒ 232 bret …[OP1 ERTL ? op1 destr srcr]233 [OP1 ERTL ? op1 destr srcr] 233 234  OP2 op2 destr srcr1 srcr2 ⇒ 234 bret …[OP2 ERTL ? op2 destr srcr1 srcr2]235 [OP2 ERTL ? op2 destr srcr1 srcr2] 235 236  CLEAR_CARRY ⇒ 236 bret …[CLEAR_CARRY ??]237 [CLEAR_CARRY ??] 237 238  SET_CARRY ⇒ 238 bret …[SET_CARRY ??]239 [SET_CARRY ??] 239 240  LOAD destr addr1 addr2 ⇒ 240 bret …[LOAD ERTL ? destr addr1 addr2]241 [LOAD ERTL ? destr addr1 addr2] 241 242  STORE addr1 addr2 srcr ⇒ 242 bret …[STORE ERTL ? addr1 addr2 srcr]243 [STORE ERTL ? addr1 addr2 srcr] 243 244  COMMENT msg ⇒ 244 bret …[COMMENT … msg]245 [COMMENT … msg] 245 246  extension_seq ext ⇒ 246 match ext return λ_. bind_step_block ?? with247 match ext return λ_.step_block ?? with 247 248 [ rtl_stack_address addr1 addr2 ⇒ 248 bret …[ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]249 [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ] 249 250 ] 250 251 ] … … 273 274 definition allocate_regs : 274 275 ∀X : Type[0]. 275 ( register → register →list (register×Register) → bind_new register X) →276 (list (register×Register) → bind_new register X) → 276 277 bind_new register X ≝ 277 278 λX,f. 278 νral,rah in279 279 let allocate_regs_internal ≝ 280 280 λacc : bind_new register (list (register × Register)). … … 283 283 νr' in return (〈r', r〉 :: tl) in 284 284 ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ; 285 f ral rahto_save.285 f to_save. 286 286 287 287 definition translate_data : 288 288 ∀globals.joint_closed_internal_function RTL globals → 289 b ind_new register (b_graph_translate_data RTL ERTL globals)≝289 bound_b_graph_translate_data RTL ERTL globals ≝ 290 290 λglobals,def. 291 291 let params ≝ joint_if_params … def in 292 292 let new_stacksize ≝ 293 293 joint_if_stacksize … def + (params  RegisterParams) in 294 allocate_regs … 295 (λral,rah,to_save. 296 ! prologue ← prologue globals params ral rah to_save ; 294 allocate_regs ? 295 (λto_save. 296 νral,rah,tmpr,addr1,addr2 in 297 ! prologue ← prologue globals params ral rah tmpr addr1 addr2 to_save ; 297 298 return mk_b_graph_translate_data RTL ERTL globals 298 299 (* init_ret ≝ *) it … … 300 301 (* init_stack_size ≝ *) new_stacksize 301 302 (* added_prologue ≝ *) prologue 303 (* new_regs ≝ *) (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save) 302 304 (* f_step ≝ *) (translate_step globals) 303 305 (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save) 304 ??? ).306 ????). 305 307 @hide_prf 306 [ #l #c % ] 307 #l * 308 [1,2: cases daemon (* TODO *) 309  #l #c % 310  #l * [ #c'  #f #args #dest  #a #ltrue  #s ] #c whd 311 [2: #r1 #r2 ] whd #l' #EQ destruct try % 312 cases s in EQ; whd in match ensure_step_block; normalize nodelta 313 try #a try #b try #c try #d try #e try #f destruct 314 cases a in b; #a1 #a2 normalize nodelta #EQ destruct 315  #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 % 316 ] 317 (* #l * 308 318 [ #l whd %{I} %{I} %1 % 309 319  whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ % … … 320 330 try (%{I} %{I} #l %) 321 331 cases a a #a #b whd %{I} % [ %{I} ] #l % 322 ] 332 ]*) 323 333 qed. 324 334 
src/joint/TranslateUtils.ma
r2723 r2806 355 355 *) 356 356 357 definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝358 λX,Y,f.359 (∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧360 (∀x1,x2.361 opt_All …362 (λys1.363 opt_All …364 (λys2.365 ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2)366 (f x2))367 (f x1)).368 369 357 lemma opt_All_intro : ∀X,P,o. 370 358 (∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed. … … 385 373 @hide_prf cases pt pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed. 386 374 *) 375 376 let rec bind_new_P' R X (P : list R → X → Prop) (m : bind_new R X) on m : Prop ≝ 377 match m with 378 [ bret x ⇒ P [ ] x 379  bnew f ⇒ 380 ∀r.bind_new_P' R X (λl.P (l @ [r])) (f r) 381 ]. 382 383 definition step_registers : ∀p : uns_params.∀globals. 384 joint_step p globals → list register ≝ 385 λp,globals,s.get_used_registers_from_step … (functs … p) s. 386 387 definition step_forall_registers : ∀p : uns_params.∀globals. 388 (register → Prop) → joint_step p globals → Prop ≝ 389 λp,globals,P,s.All … P (step_registers … s). 390 391 definition fin_step_registers : ∀p : uns_params. 392 joint_fin_step p → list register ≝ 393 λp,s.match s with [ TAILCALL _ _ r ⇒ f_call_args … (functs … p) r  _ ⇒ [ ] ]. 394 395 definition fin_step_forall_registers : ∀p : uns_params. 396 (register → Prop) → joint_fin_step p → Prop ≝ 397 λp,P,s.All … P (fin_step_registers … s). 398 399 definition fin_step_forall_labels : ∀p : uns_params. 400 (label → Prop) → joint_fin_step p → Prop ≝ 401 λp,P,s.All … P (fin_step_labels … s). 402 403 definition step_labels_and_registers_in : ∀p : uns_params.∀globals. 404 list label → list register → joint_step p globals → Prop ≝ 405 λp,g,allowed_l,allowed_r,s. 406 step_forall_labels … (In ? allowed_l) s ∧ 407 step_forall_registers … (In ? allowed_r) s. 408 409 definition fin_step_labels_and_registers_in : ∀p : uns_params. 410 list label → list register → joint_fin_step p → Prop ≝ 411 λp,allowed_l,allowed_r,s. 412 fin_step_forall_labels … (In ? allowed_l) s ∧ 413 fin_step_forall_registers … (In ? allowed_r) s. 387 414 388 415 record b_graph_translate_data … … 393 420 ; init_stack_size : ℕ 394 421 ; added_prologue : list (joint_seq dst globals) 422 ; new_regs : list register (* new registers added globally *) 395 423 ; f_step : label → joint_step src globals → bind_step_block dst globals 396 424 ; f_fin : label → joint_fin_step src → bind_fin_block dst globals 397 ; good_f_step_good : 398 ∀l,s.bind_new_P ?? 399 (λblock.let 〈pref, op, post〉 ≝ block in 425 ; good_f_step : 426 ∀l,s.bind_new_P' ?? 427 (λlocal_new_regs,block.let 〈pref, op, post〉 ≝ block in 428 ∀l. 429 let allowed_labels ≝ l :: step_labels … s in 430 let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in 400 431 All (label → joint_seq ??) 401 (λs'. ∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l))432 (λs'.step_labels_and_registers_in … allowed_labels allowed_registers (step_seq dst globals (s' l))) 402 433 pref ∧ 403 (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧404 All (joint_seq ??) (step_ forall_labels … (In ? (step_labels … s))) post)434 step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧ 435 All (joint_seq ??) (step_labels_and_registers_in … allowed_labels allowed_registers) post) 405 436 (f_step l s) 406 437 ; good_f_fin : 407 ∀l,s.bind_new_P ?? 408 (λblock.let 〈pref, op〉 ≝ block in 409 All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧ 410 All … (In ? (fin_step_labels … s)) (fin_step_labels … op)) 438 ∀l,s.bind_new_P' ?? 439 (λlocal_new_regs,block.let 〈pref, op〉 ≝ block in 440 let allowed_labels ≝ l :: fin_step_labels … s in 441 let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in 442 All (joint_seq ??) (λs.step_labels_and_registers_in … allowed_labels allowed_registers s) pref ∧ 443 fin_step_labels_and_registers_in … allowed_labels allowed_registers op) 411 444 (f_fin l s) 412 445 ; f_step_on_cost : 413 446 ∀l,c.f_step l (COST_LABEL … c) = 414 447 bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉 448 ; cost_in_f_step : 449 ∀l,s,c. 450 bind_new_P ?? 451 (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c → 452 s = COST_LABEL … c) (f_step l s) 415 453 }. 454 455 definition bound_b_graph_translate_data ≝ 456 λsrc,dst,globals. 457 Σd : bind_new register (b_graph_translate_data src dst globals). 458 bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d. 459 460 unification hint 0 ≔ src,dst,globals ⊢ 461 bound_b_graph_translate_data src dst globals ≡ 462 Sig (bind_new register (b_graph_translate_data src dst globals)) (λd.bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d). 416 463 417 464 definition get_first_costlabel : ∀p,g. … … 436 483 qed. 437 484 485 definition partial_partition : ∀X.∀Y : DeqSet.(X → list Y) → Prop ≝ 486 λX,Y,f. 487 (∀x.bool_to_Prop (uniqueb … (f x))) ∧ 488 (∀x1,x2,y.y ∈ f x1 → y ∈ f x2 → x1 = x2). 489 438 490 record b_graph_translate_props 439 491 (src_g_pars, dst_g_pars : graph_params) 440 492 (globals: list ident) 441 493 (data : b_graph_translate_data src_g_pars dst_g_pars globals) 442 (data_regs : list register)443 494 (def_in : joint_closed_internal_function src_g_pars globals) 444 495 (def_out : joint_closed_internal_function dst_g_pars globals) 445 (f_lbls : label → option (list label))446 (f_regs : label → option (list register)) : Prop ≝496 (f_lbls : label → list label) 497 (f_regs : label → list register) : Prop ≝ 447 498 { res_def_out_eq : 448 499 joint_if_result … def_out = init_ret … data … … 456 507 ; partition_regs : partial_partition … f_regs 457 508 ; freshness_lbls : 458 (∀l. opt_All … (All …509 (∀l.All … 459 510 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 460 fresh_for_univ … lbl (joint_if_luniverse … def_out)) )(f_lbls l))511 fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l)) 461 512 ; freshness_regs : 462 (∀l. opt_All … (All …513 (∀l.All … 463 514 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 464 fresh_for_univ … reg (joint_if_runiverse … def_out)) )(f_regs l))515 fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l)) 465 516 ; freshness_data_regs : 466 517 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 467 fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs468 ; data_regs_disjoint : ∀l .opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l)518 fresh_for_univ … reg (joint_if_runiverse … def_out)) (new_regs … data) 519 ; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False 469 520 ; multi_fetch_ok : 470 521 ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 471 ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧522 let lbls ≝ f_lbls l in let regs ≝ f_regs l in 472 523 match s with 473 524 [ sequential s' nxt ⇒ … … 501 552 ∀globals: list ident. 502 553 (* initialization info *) 503 ∀data : b ind_new register (b_graph_translate_data src_g_pars dst_g_pars globals).554 ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals. 504 555 (* source function *) 505 556 ∀def_in : joint_closed_internal_function src_g_pars globals. … … 507 558 Σdef_out : joint_closed_internal_function dst_g_pars globals. 508 559 ∃data',regs,f_lbls,f_regs. 509 bind_new_instantiates … data' data regs ∧510 b_graph_translate_props … data' regsdef_in def_out f_lbls f_regs560 bind_new_instantiates ?? data' data regs ∧ (* so new_regs … data = regs *) 561 b_graph_translate_props … data' def_in def_out f_lbls f_regs 511 562 ≝ 512 563 λsrc_g_pars,dst_g_pars,globals,data,def. … … 545 596 (* initialization *) 546 597 (∀globals.joint_closed_internal_function src_g_pars globals → 547 b ind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) →598 bound_b_graph_translate_data src_g_pars dst_g_pars globals) → 548 599 joint_program src_g_pars → 549 600 joint_program dst_g_pars ≝
Note: See TracChangeset
for help on using the changeset viewer.