Changeset 2681
- Timestamp:
- Feb 19, 2013, 6:48:32 PM (8 years ago)
- Location:
- src
- Files:
-
- 9 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 caller-save 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 ? -
src/ERTLptr/ERTLtoERTLptr.ma
r2675 r2681 39 39 definition translate_step: 40 40 ∀globals. 41 unit →42 41 label 43 42 →joint_step ERTL globals 44 43 →bind_step_block ERTLptr globals ≝ 45 λglobals.λ _.λl.λs.44 λglobals.λl.λs. 46 45 match s return λ_.bind_step_block ERTLptr globals with 47 46 [ CALL called args dest ⇒ … … 69 68 definition translate_fin_step: 70 69 ∀globals. 71 unit →72 70 label 73 71 →joint_fin_step ERTL 74 72 →bind_fin_block ERTLptr globals ≝ 75 λglobals.λ_.λl.λs.bret … 〈[ ], fin_step_embed … s〉. 73 λglobals.λl.λs.bret … 〈[ ], fin_step_embed … s〉. 74 75 definition translate_data : 76 ∀globals.joint_closed_internal_function ERTL globals → 77 bind_new register (b_graph_translate_data ERTL ERTLptr globals) ≝ 78 λglobals,def.bret … 79 (mk_b_graph_translate_data … 80 (* init_ret ≝ *) (joint_if_result … def) 81 (* init_params ≝ *) (joint_if_params … def) 82 (* init_stack_size ≝ *) (joint_if_stacksize … def) 83 (* added_prologue ≝ *) [ ] 84 (* f_step ≝ *) (translate_step globals) 85 (* f_fin ≝ *) (translate_fin_step globals) 86 ???). 87 @hide_prf 88 [ #l #c % ] 89 #l * 90 [ #l whd %{I} %{I} %1 % 91 | whd %{I I} 92 | #abs #called #args whd %{I I} 93 | * #called #args #dest whd in match translate_step; normalize nodelta whd 94 [ %{I} %{I} #l % 95 | #r whd %{I} %{(λ_.I)} % [| % [| % [| %{I} ]]] #l 96 [1,3: %{I} %1 % 97 |*: % 98 ] 99 ] 100 | #a #l_true whd %{I} %{I} #l %{I} %2 %1 % 101 | #s whd %{I} %{I} #l whd @(All_mp … (In ? (step_labels … s))) 102 [ #l' #H %2{H} ] cases s -s // 103 ] 104 qed. 76 105 77 106 definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝ 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. 107 b_graph_transform_program ERTL ERTLptr translate_data. -
src/RTL/RTL.ma
r2640 r2681 4 4 | rtl_stack_address: register → register → rtl_seq. 5 5 6 definition RTL_uns ≝ λhas_tailcalls.mk_unserialized_params6 definition RTL_uns ≝ mk_unserialized_params 7 7 (* acc_a_reg ≝ *) register 8 8 (* acc_b_reg ≝ *) register … … 19 19 (* ext_seq ≝ *) rtl_seq 20 20 (* ext_seq_labels ≝ *) (λ_.[]) 21 (* has_tailcalls ≝ *) has_tailcalls21 (* has_tailcalls ≝ *) false 22 22 (* paramsT ≝ *) (list register). 23 23 24 definition RTL ≝ mk_graph_params (RTL_uns true).24 definition RTL ≝ mk_graph_params RTL_uns. 25 25 definition rtl_program ≝ joint_program RTL. 26 26 … … 74 74 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte 75 75 on _b : Byte to snd_arg RTL. 76 77 78 (************ Same without tail calls ****************)79 80 definition RTL_ntc ≝ mk_graph_params (RTL_uns false).81 definition rtl_ntc_program ≝ joint_program RTL_ntc. -
src/RTL/RTLToERTL.ma
r2659 r2681 1 1 include "utilities/RegisterSet.ma". 2 2 include "common/Identifiers.ma". 3 include "RTL/RTL.ma". 3 4 include "ERTL/ERTL.ma". 4 5 include "joint/TranslateUtils.ma". 5 6 6 7 include alias "basics/lists/list.ma". 7 8 definition ertl_fresh_reg:9 ∀globals.freshT ERTL globals register ≝10 λglobals,def.11 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in12 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.13 8 14 9 definition save_hdws : … … 43 38 definition get_params_stack : 44 39 ∀globals.list register → 45 bind_new (localsT ERTL)(list (joint_seq ERTL globals)) ≝40 bind_new register (list (joint_seq ERTL globals)) ≝ 46 41 λglobals,params. 47 42 νtmpr,addr1,addr2 in … … 61 56 let 〈hdw_params, stack_params〉 ≝ list_split … n params in 62 57 get_params_hdw globals hdw_params @@ get_params_stack … stack_params. 63 64 definition prologue :65 ∀globals.list register → register → register → list (register×Register) →66 bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝67 λglobals,params,sral,srah,sregs.68 [ (ertl_new_frame : joint_seq ??) ;69 POP … sral ;70 POP … srah71 ] @@ save_hdws … sregs @@ get_params … params.72 58 73 59 definition save_return : … … 93 79 ]. 94 80 81 lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf. 82 All2 A B P l1 l2 → 83 (∀x,y.P x y → R (f x y)) → 84 All C R (map2 A B C f l1 l2 prf). 85 #A #B #C #P #R #f #l1 elim l1 -l1 86 [ * [ #prf * #H % ] #hd' #tl' 87 | #hd #tl #IH * [2: #hd' #tl' ] 88 ] #prf normalize in prf; destruct 89 * #H1 #H2 #H % [ @H @H1 | @IH assumption ] qed. 90 91 lemma All2_True : ∀A,B,l1,l2.|l1| = |l2| → All2 A B (λ_.λ_.True) l1 l2. 92 #A #B #l1 elim l1 -l1 93 [ * [ #prf % ] #hd' #tl' 94 | #hd #tl #IH * [2: #hd' #tl' ] 95 ] #prf normalize in prf; destruct %{I} @IH assumption 96 qed. 97 98 lemma All_True : ∀A,l.All A (λ_.True) l. 99 #A #l elim l -l [ % | #hd #tl #IH %{I IH} ] qed. 100 95 101 definition epilogue : 96 102 ∀globals.list register → register → register → list (register × Register) → 97 list (joint_seq ERTL globals) ≝ 103 Σl : list (joint_seq ERTL globals). 104 All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝ 98 105 λglobals,ret_regs,sral,srah,sregs. 99 106 save_return … (map … (Reg ?) ret_regs) @ … … 103 110 ertl_del_frame ] @ 104 111 assign_result globals. 105 106 definition allocate_regs : 107 ∀globals,rs.rs_set rs → 108 freshT ERTL globals (list (register×Register)) ≝ 109 λglobals,rs,saved,def. 110 let allocate_regs_internal ≝ 111 λr: Register. 112 λdef_sregs. 113 let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in 114 〈def, 〈r', r〉::\snd def_sregs〉 in 115 rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉. 116 117 definition add_pro_and_epilogue : 118 ∀globals.list register → list register → 119 joint_internal_function ERTL globals → 120 joint_internal_function ERTL globals ≝ 121 λglobals,params,ret_regs,def. 122 let start_lbl ≝ joint_if_entry … def in 123 let end_lbl ≝ joint_if_exit … def in 124 state_run … def ( 125 ! sral ← ertl_fresh_reg … ; 126 ! srah ← ertl_fresh_reg … ; 127 ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ; 128 ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ; 129 let epilogue' ≝ epilogue … ret_regs sral srah sregs in 130 ! def' ← state_get … ; 131 let def'' ≝ insert_prologue … prologue' def' in 132 return insert_epilogue … epilogue' def'' 133 ). 112 @hide_prf 113 @All_append 114 [ whd in match save_return; normalize nodelta 115 cases (reduce_strong ????) ** #a #b * #c #d #prf normalize nodelta 116 @All_append 117 [ @(All_map2 … (All2_True … prf)) #x #y #_ % 118 | @(All_map … (All_True …)) #x #_ % 119 ] 120 | @All_append 121 [ @(All_map … (All_True …)) #x #_ % 122 | %{(refl …)} %{(refl …)} %{(refl …)} 123 whd in match assign_result; 124 generalize in match reduce_strong; #f normalize nodelta 125 cases (f ????) #l #prf normalize nodelta 126 @(All_map2 … (All2_True … prf)) #x #y #_ % 127 ] 128 ] 129 qed. 130 131 definition prologue : 132 ∀globals.list register → register → register → list (register×Register) → 133 bind_new register (list (joint_seq ERTL globals)) ≝ 134 λglobals,params,sral,srah,sregs. 135 [ (ertl_new_frame : joint_seq ??) ; 136 POP … sral ; 137 POP … srah 138 ] @@ save_hdws … sregs @@ get_params … params. 134 139 135 140 definition set_params_hdw : … … 150 155 151 156 definition set_params_stack : 152 ∀globals.list psd_argument → bind_new (localsT ERTL)? ≝157 ∀globals.list psd_argument → bind_new register ? ≝ 153 158 λglobals,params. 154 159 νaddr1,addr2 in … … 162 167 flatten … (map … (set_param_stack globals addr1 addr2) params). 163 168 164 definition set_params ≝ 169 definition set_params : 170 ∀globals.list psd_argument → 171 Σb : bind_new register (list (joint_seq ERTL globals)). 172 BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝ 165 173 λglobals,params. 166 174 let n ≝ min (|params|) (|RegisterParams|) in … … 169 177 let stack_params ≝ \snd hdw_stack_params in 170 178 set_params_hdw globals hdw_params @@ set_params_stack globals stack_params. 179 @hide_prf 180 @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:] 181 [ #r1 #r2 182 %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} 183 @All_append [ % ] 184 elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta 185 whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH 186 | whd whd in match set_params_hdw; normalize nodelta 187 whd in match restore_hdws; normalize nodelta @(All_map … (All_True …)) 188 #a #_ % 189 ] 190 qed. 171 191 172 192 definition fetch_result : 173 ∀globals.list register → list (joint_seq ERTL globals) ≝ 193 ∀globals.list register → 194 Σl : list (joint_seq ERTL globals). 195 All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝ 174 196 λglobals,ret_regs. 175 197 match reduce_strong ?? RegisterSTS RegisterRets with … … 185 207 ] 186 208 ]. 209 @hide_prf 210 @All_append 211 [ @(All_map2 … (All2_True … crl_proof)) #x #y #_ % 212 | cases (reduce_strong ????) #l #prf normalize nodelta 213 @(All_map2 … (All2_True … prf)) #x #y #_ % 214 ] 215 qed. 187 216 188 217 definition translate_step : 189 ∀globals.label → joint_step RTL _ntcglobals →190 bind_s eq_block ERTL globals (joint_step ERTL globals)≝218 ∀globals.label → joint_step RTL globals → 219 bind_step_block ERTL globals ≝ 191 220 λglobals.λ_.λs. 192 match s return λ_.bind_s eq_block ?? (joint_step ??)with221 match s return λ_.bind_step_block ?? with 193 222 [ step_seq s ⇒ 194 match s return λ_.bind_s eq_block ?? (joint_step ??)with195 [ PUSH _ ⇒ NOOP …(*CSC: XXXX should not be in the syntax *)196 | POP _ ⇒ NOOP …(*CSC: XXXX should not be in the syntax *)197 | MOVE rs ⇒ PSD (\fst rs) ← \snd rs223 match s return λ_.bind_step_block ?? with 224 [ 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] 198 227 | COST_LABEL lbl ⇒ 199 COST_LABEL … lbl228 bret … [COST_LABEL … lbl] 200 229 | ADDRESS x prf r1 r2 ⇒ 201 ADDRESS ERTL ? x prf r1 r2230 bret … [ADDRESS ERTL ? x prf r1 r2] 202 231 | OPACCS op destr1 destr2 srcr1 srcr2 ⇒ 203 OPACCS ERTL ? op destr1 destr2 srcr1 srcr2232 bret … [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2] 204 233 | OP1 op1 destr srcr ⇒ 205 OP1 ERTL ? op1 destr srcr234 bret … [OP1 ERTL ? op1 destr srcr] 206 235 | OP2 op2 destr srcr1 srcr2 ⇒ 207 OP2 ERTL ? op2 destr srcr1 srcr2236 bret … [OP2 ERTL ? op2 destr srcr1 srcr2] 208 237 | CLEAR_CARRY ⇒ 209 CLEAR_CARRY …238 bret … [CLEAR_CARRY ??] 210 239 | SET_CARRY ⇒ 211 SET_CARRY …240 bret … [SET_CARRY ??] 212 241 | LOAD destr addr1 addr2 ⇒ 213 LOAD ERTL ? destr addr1 addr2242 bret … [LOAD ERTL ? destr addr1 addr2] 214 243 | STORE addr1 addr2 srcr ⇒ 215 STORE ERTL ? addr1 addr2 srcr244 bret … [STORE ERTL ? addr1 addr2 srcr] 216 245 | COMMENT msg ⇒ 217 COMMENT … msg246 bret … [COMMENT … msg] 218 247 | extension_seq ext ⇒ 219 match ext with248 match ext return λ_.bind_step_block ?? with 220 249 [ rtl_stack_address addr1 addr2 ⇒ 221 [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]250 bret … [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ] 222 251 ] 223 | CALL f args ret_regs ⇒224 set_params ? args @@225 CALL ERTL ? f (|args|) it :::226 fetch_result ? ret_regs227 252 ] 253 | CALL f args ret_regs ⇒ 254 ! pref ← pi1 … (set_params ? args) ; 255 bret ? (step_block ??) 〈add_dummy_variance … pref, 256 λ_.CALL ERTL ? f (|args|) it, 257 fetch_result ? ret_regs〉 228 258 | COND r ltrue ⇒ 229 COND ERTL ? r ltrue259 bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉 230 260 ]. 231 261 232 262 definition translate_fin_step : 233 ∀globals.label → joint_fin_step RTL_ntc → 234 bind_seq_block ERTL globals (joint_fin_step ERTL) ≝ 235 λglobals.λ_.λs. 236 match s with 237 [ GOTO lbl' ⇒ GOTO … lbl' 238 | RETURN ⇒ RETURN ? 239 | TAILCALL abs _ _ ⇒ match abs in False with [ ] 240 ]. 241 242 (* hack with empty graphs used here *) 243 definition translate_funct : 244 ∀globals.joint_closed_internal_function RTL_ntc globals → 245 joint_closed_internal_function ERTL globals ≝ 246 λglobals,def. 247 let nb_params ≝ |joint_if_params ?? def| in 248 let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in 249 let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in 250 let entry' ≝ pi1 … (joint_if_entry … def) in 251 let exit' ≝ pi1 … (joint_if_exit … def) in 252 let def' ≝ init_graph_if ERTL globals 253 (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *) 254 nb_params new_locals ((joint_if_stacksize … def) + added_stacksize) 255 entry' exit' in 256 let def'' ≝ b_graph_translate … 257 (ertl_fresh_reg …) 258 def' 259 (translate_step globals) 260 (translate_fin_step globals) 261 def in 262 add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'. 263 cases daemon (* TODO *) qed. 263 ∀globals.list register → register → register → list (register × Register) → 264 label → joint_fin_step RTL → 265 bind_fin_block ERTL globals ≝ 266 λglobals.λret_regs,ral,rah,to_restore.λ_.λs. 267 match s return λ_.bind_fin_block ERTL ? with 268 [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉 269 | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉 270 | TAILCALL b _ _ ⇒ match b in False with [ ] 271 ]. 272 273 definition allocate_regs : 274 ∀X : Type[0]. 275 (register → register → list (register×Register) → bind_new register X) → 276 bind_new register X ≝ 277 λX,f. 278 νral,rah in 279 let allocate_regs_internal ≝ 280 λacc : bind_new register (list (register × Register)). 281 λr: Register. 282 ! tl ← acc ; 283 νr' in return (〈r', r〉 :: tl) in 284 ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ; 285 f ral rah to_save. 286 287 definition translate_data : 288 ∀globals.joint_closed_internal_function RTL globals → 289 bind_new register (b_graph_translate_data RTL ERTL globals) ≝ 290 λglobals,def. 291 let params ≝ joint_if_params … def in 292 let new_stacksize ≝ 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 ; 297 return mk_b_graph_translate_data RTL ERTL globals 298 (* init_ret ≝ *) it 299 (* init_params ≝ *) (|params|) 300 (* init_stack_size ≝ *) new_stacksize 301 (* added_prologue ≝ *) prologue 302 (* f_step ≝ *) (translate_step globals) 303 (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save) 304 ???). 305 @hide_prf 306 [ #l #c % ] 307 #l * 308 [ #l whd %{I} %{I} %1 % 309 | whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ % 310 | * 311 | #called #args #dest @(mp_bind … (BindNewP …)) 312 [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%] 313 [ @(All_map … H1) #a #EQ #l whd >EQ % 314 | #l % 315 | cases (fetch_result ??) @All_mp #s #EQ whd >EQ % 316 ] 317 | #a #l_true whd %{I} %{I} #l %{I} %2 %1 % 318 | * try #a try #b try #c try #d try #e whd 319 try (%{I} %{I} #l %) 320 cases a -a #a #b whd %{I} % [ %{I} ] #l % 321 ] 322 qed. 264 323 265 324 (* removing this because of how insert_prologue is now defined … … 312 371 313 372 definition rtl_to_ertl : rtl_program → ertl_program ≝ 314 λp. 315 transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)). 373 b_graph_transform_program … translate_data. -
src/joint/Joint.ma
r2655 r2681 416 416 }. 417 417 418 definition code_in_universe : ∀p,globals. 419 codeT p globals → universe LabelTag → Prop ≝ 420 λp,globals,c,u.∀l.code_has_label … c l → fresh_for_univ … l u. 421 422 lemma memb_to_present : ∀tag,A.∀i : identifier tag.∀m. 423 i ∈ m → present tag A m i. 424 #tag #A #i #m whd in ⊢ (?%→%); cases (lookup tag A m i) 425 [ * | #x #_ % #ABS destruct ] 426 qed. 427 428 lemma present_to_memb : ∀tag,A.∀i : identifier tag.∀m. 429 present tag A m i → bool_to_Prop (i∈m). 430 #tag #A #i #m whd in ⊢ (%→?%); cases (lookup tag A m i) 431 [ * #ABS cases (ABS (refl …)) | #x #_ % ] 432 qed. 433 434 lemma graph_code_in_universe_if : ∀p : graph_params.∀globals. 435 ∀c : codeT p globals.∀u.fresh_map_for_univ … c u → code_in_universe … c u ≝ 436 λp,g,c,u,H,l,G.H ? (memb_to_present … G). 437 438 lemma graph_code_in_universe_only_if : ∀p : graph_params.∀globals. 439 ∀c : codeT p globals.∀u. 440 code_in_universe … c u → fresh_map_for_univ … c u ≝ 441 λp,g,c,u,H,l,G.H ? (present_to_memb … G). 442 443 include alias "basics/logic.ma". 444 445 record good_if 446 (p : params) (globals : list ident) (def : joint_internal_function p globals) 447 : Prop ≝ 448 { unique_cost_labels : 449 ∀l1,l2,c,nxt1,nxt2. 450 stmt_at … (joint_if_code … def) l1 = 451 Some … (sequential … (COST_LABEL … c) nxt1) → 452 stmt_at … (joint_if_code … def) l2 = 453 Some … (sequential … (COST_LABEL … c) nxt2) → 454 l1 = l2 455 ; entry_costed : 456 ∃l,nxt. 457 stmt_at … (joint_if_code … def) (joint_if_entry … def) = 458 Some … (sequential … (COST_LABEL … l) nxt) 459 ; code_is_closed : code_closed … (joint_if_code … def) 460 ; code_is_in_universe : 461 code_in_universe … (joint_if_code … def) (joint_if_luniverse … def) 462 }. 463 418 464 definition joint_closed_internal_function ≝ 419 465 λp,globals. 420 Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def).466 Σdef : joint_internal_function p globals.good_if … def. 421 467 422 468 unification hint 0 ≔ p,g ⊢ 423 469 joint_closed_internal_function p g ≡ 424 Sig (joint_internal_function p g) (λ fd.code_closed p g (joint_if_code p g fd)).470 Sig (joint_internal_function p g) (λdef.good_if … def). 425 471 426 472 definition set_joint_code ≝ -
src/joint/Traces.ma
r2645 r2681 99 99 100 100 definition joint_classify_step : 101 ∀p : evaluation_params. state p →joint_step p (globals … p) → status_class ≝102 λp,st ,stmt.101 ∀p : evaluation_params.joint_step p (globals … p) → status_class ≝ 102 λp,stmt. 103 103 match stmt with 104 104 [ step_seq _ ⇒ cl_other 105 | CALL f args dest ⇒ 106 match (! bl ← block_of_call … (ev_genv p) f st ; 107 fetch_function … (ev_genv p) bl) with 108 [ OK id_fn ⇒ 109 match \snd id_fn with 110 [ Internal _ ⇒ cl_call 111 | External _ ⇒ cl_other 112 ] 113 | Error _ ⇒ cl_other 114 ] 105 | CALL f args dest ⇒ cl_call 115 106 | COND _ _ ⇒ cl_jump 116 107 ]. 117 108 118 109 definition joint_classify_final : 119 ∀p : evaluation_params. state p →joint_fin_step p → status_class ≝120 λp,st ,stmt.110 ∀p : evaluation_params.joint_fin_step p → status_class ≝ 111 λp,stmt. 121 112 match stmt with 122 113 [ GOTO _ ⇒ cl_other 123 114 | RETURN ⇒ cl_return 124 | TAILCALL _ f args ⇒ 125 match (! bl ← block_of_call … (ev_genv p) f st ; 126 fetch_function … (ev_genv p) bl) with 127 [ OK id_fn ⇒ 128 match \snd id_fn with 129 [ Internal _ ⇒ cl_tailcall 130 | External _ ⇒ cl_return 131 ] 132 | Error _ ⇒ cl_other 133 ] 115 | TAILCALL _ f args ⇒ cl_tailcall 134 116 ]. 135 117 … … 139 121 ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ; 140 122 match s with 141 [ sequential s _ ⇒ Some ? (joint_classify_step p s t s)142 | final s ⇒ Some ? (joint_classify_final p s t s)123 [ sequential s _ ⇒ Some ? (joint_classify_step p s) 124 | final s ⇒ Some ? (joint_classify_final p s) 143 125 | FCOND _ _ _ _ ⇒ Some ? cl_jump 144 126 ]. … … 152 134 lemma joint_classify_call : ∀p : evaluation_params.∀st. 153 135 joint_classify p st = Some ? cl_call → 154 ∃i_f,f',args,dest,next ,bl,i',fd'.136 ∃i_f,f',args,dest,next. 155 137 fetch_statement … (ev_genv p) (pc … st) = 156 OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧ 157 block_of_call … (ev_genv p) f' st = OK ? bl ∧ 158 fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉. 138 OK ? 〈i_f, sequential … (CALL … f' args dest) next〉. 159 139 #p #st 160 140 whd in match joint_classify; normalize nodelta 161 141 inversion (fetch_statement … (ev_genv p) (pc … st)) 162 142 [2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] 163 * #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_ 164 >m_return_bind normalize nodelta 165 [3: whd in match joint_classify_final; normalize nodelta 166 generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ] 167 normalize nodelta ] 168 #ABS destruct(ABS) ] 143 * #i_f * 144 [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_ 145 >m_return_bind normalize nodelta normalize in ⊢ (%→?); #ABS destruct 146 ] 169 147 * [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind 170 normalize nodelta 171 [2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ] 172 whd in match joint_classify_step; 173 normalize nodelta 174 inversion (block_of_call ?????) 175 [ #bl #block_of_c >m_return_bind 176 inversion (fetch_function ???) 177 [ * #i' * 178 [ #fd' #fetch' #_ 179 %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'} 180 % [ %{block_of_c} % ] 181 whd in match fetch_internal_function; normalize nodelta 182 >fetch' % 183 ] 184 ] 185 ] 186 #x #_ normalize in ⊢ (%→?); #ABS destruct(ABS) 148 normalize in ⊢ (%→?); #EQ destruct 149 %[|%[|%[|%[|%[| %]]]]] 187 150 qed. 188 151 … … 340 303 (* as_final ≝ *) (λs.is_final p (globals ?) (ev_genv p) exit_pc s ≠ None ?) 341 304 (* as_call_ident ≝ *) (joint_call_ident p) 342 (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). 305 (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). -
src/joint/TranslateUtils.ma
r2675 r2681 93 93 (* ignoring register allocation for now *) 94 94 95 (* 95 96 definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝ 96 97 λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def). 97 98 *) 98 99 (* 99 100 lemma All_fresh_not_memb : ∀tag,u,l,id,u'. … … 111 112 ] 112 113 qed. 113 *) 114 114 115 115 116 lemma fresh_was_fresh : ∀tag,id,id',u,u'. … … 132 133 #tag * #id * #u * #u' normalize #EQ destruct // 133 134 qed. 134 135 *) 135 136 (* 136 137 lemma adds_graph_list_fresh_preserve : … … 242 243 qed. 243 244 *) 244 245 (* 245 246 axiom adds_graph_ok : 246 247 ∀g_pars,globals,B,src,dst,def. … … 270 271 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧ 271 272 src ~❨B,src::l❩~> it in joint_if_code … def'. 272 273 (* preserves first statement if a cost label (should be an invariant) *) 274 definition insert_prologue ≝ 275 λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). 276 λdef : joint_internal_function g_pars globals. 277 let entry ≝ joint_if_entry … def in 278 match stmt_at … entry 279 return λx.match x with [None ⇒ false | Some _ ⇒ true] → ? 280 with 281 [ Some s ⇒ λ_. 282 let default_add ≝ λ_ : unit. 283 let 〈def', lbl〉 ≝ fresh_label … def in 284 let def'' ≝ add_graph … lbl s def' in 285 adds_graph … insts entry lbl def'' in 286 match s with 287 [ sequential s' next ⇒ 288 match s' with 289 [ step_seq s'' ⇒ 290 match s'' with 291 [ COST_LABEL _ ⇒ 292 adds_graph ?? (s'' :: insts) entry next def 293 | _ ⇒ 294 default_add it 295 ] 296 | _ ⇒ 297 default_add it 298 ] 299 | _ ⇒ 300 default_add it 301 ] 302 | None ⇒ Ⓧ 303 ] (pi2 … entry). 273 *) 274 275 definition append_seq_list : 276 ∀p,g.bind_step_block p g → bind_new register (list (joint_seq p g)) → 277 bind_step_block p g ≝ 278 λp,g,bbl,bl. 279 ! 〈pref, op, post〉 ← bbl ; ! l ← bl ; return 〈pref, op, post @ l〉. 304 280 305 281 (* … … 332 308 adds_graph … stmts src dst def. 333 309 310 (* 334 311 axiom b_adds_graph_ok : 335 312 ∀g_pars,globals,B,src,dst,def. … … 349 326 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ 350 327 src ~❨B,src::l,r❩~> dst in joint_if_code … def'. 351 328 *) 352 329 definition b_fin_adds_graph : 353 330 ∀g_pars: graph_params. … … 361 338 fin_adds_graph … stmts src def. 362 339 340 (* 363 341 axiom b_fin_adds_graph_ok : 364 342 ∀g_pars,globals,B,src,def. … … 378 356 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧ 379 357 src ~❨B,src::l,r❩~> it in joint_if_code … def'. 380 381 (* translation with inline fresh register allocation *) 382 definition b_graph_translate : 383 ∀src_g_pars,dst_g_pars : graph_params. 384 ∀globals: list ident. 385 (* initialization info *) 386 call_dest dst_g_pars → (* joint_if_result *) 387 paramsT dst_g_pars → (* joint_if_params *) 388 ℕ → (* joint_if_stacksize *) 389 (* functions dictating the translation *) 390 (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) → 391 (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) → 392 (* source function *) 393 joint_closed_internal_function src_g_pars globals → 394 (* destination function *) 395 joint_closed_internal_function dst_g_pars globals ≝ 396 λsrc_g_pars,dst_g_pars,globals, 397 init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def. 398 let init ≝ 399 mk_joint_internal_function dst_g_pars globals 400 (joint_if_luniverse … def) 401 (joint_if_runiverse … def) 402 init_ret init_params init_stack_size 403 (add ?? (empty_map ? (joint_statement ??)) (joint_if_entry … def) (RETURN …)) 404 (pi1 … (joint_if_entry … def)) in 405 let f : label → joint_statement (src_g_pars : params) globals → 406 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 407 λlbl,stmt,def. 408 match stmt with 409 [ sequential inst next ⇒ 410 b_adds_graph … (trans_step lbl inst) lbl next def 411 | final inst ⇒ 412 b_fin_adds_graph … (trans_fin_step lbl inst) lbl def 413 | FCOND abs _ _ _ ⇒ Ⓧabs 414 ] in 415 foldi … f (joint_if_code … def) init. 416 @hide_prf [ cases daemon (* TODO *) | >graph_code_has_point @mem_set_add_id ] qed. 358 *) 417 359 418 360 definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝ … … 447 389 *) 448 390 449 450 axiom b_graph_translate_ok : 451 ∀src_g_pars,dst_g_pars : graph_params. 452 ∀globals: list ident. 453 ∀init_ret,init_params,init_stack_size. 454 ∀f_step,f_fin,def_in. 455 let def_out ≝ 456 b_graph_translate src_g_pars dst_g_pars globals 457 init_ret init_params init_stack_size f_step f_fin def_in in 458 luniverse_ok ?? def_in → 459 luniverse_ok … def_out ∧ 460 joint_if_result … def_out = init_ret ∧ 461 joint_if_params … def_out = init_params ∧ 462 joint_if_stacksize … def_out = init_stack_size ∧ 463 pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧ 464 ∃f_lbls : label → option (list label). 465 ∃f_regs : label → option (list register). 466 partial_partition … f_lbls ∧ 467 partial_partition … f_regs ∧ 391 record b_graph_translate_data 392 (src, dst : graph_params) 393 (globals : list ident) : Type[0] ≝ 394 { init_ret : call_dest dst 395 ; init_params : paramsT dst 396 ; init_stack_size : ℕ 397 ; added_prologue : list (joint_seq dst globals) 398 ; f_step : label → joint_step src globals → bind_step_block dst globals 399 ; f_fin : label → joint_fin_step src → bind_fin_block dst globals 400 ; good_f_step_good : 401 ∀l,s.bind_new_P ?? 402 (λblock.let 〈pref, op, post〉 ≝ block in 403 All (label → joint_seq ??) 404 (λs'.∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l)) 405 pref ∧ 406 (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧ 407 All (joint_seq ??) (step_forall_labels … (In ? (step_labels … s))) post) 408 (f_step l s) 409 ; good_f_fin : 410 ∀l,s.bind_new_P ?? 411 (λblock.let 〈pref, op〉 ≝ block in 412 All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧ 413 All … (In ? (fin_step_labels … s)) (fin_step_labels … op)) 414 (f_fin l s) 415 ; f_step_on_cost : 416 ∀l,c.f_step l (COST_LABEL … c) = bret … [ COST_LABEL … c ] 417 }. 418 419 definition get_first_costlabel : ∀p,g. 420 joint_closed_internal_function p g → costlabel × (succ p) ≝ 421 λp,g,def. 422 match stmt_at … (joint_if_code … def) (joint_if_entry … def) 423 return λx.stmt_at ???? = x → ? with 424 [ Some s ⇒ 425 match s return λx.stmt_at ???? = Some ? x → ? with 426 [ sequential s' nxt ⇒ 427 match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with 428 [ step_seq s'' ⇒ 429 match s'' return λx.stmt_at ???? = Some ? (sequential … (step_seq … x) nxt) → ? with 430 [ COST_LABEL c ⇒ λ_.〈c, nxt〉 431 | _ ⇒ λabs.⊥ 432 ] 433 | _ ⇒ λabs.⊥ 434 ] 435 | _ ⇒ λabs.⊥ 436 ] 437 | _ ⇒ λabs.⊥ 438 ] (refl …). 439 @hide_prf 440 cases def in abs; -def #def #good_def 441 cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct 442 qed. 443 444 record b_graph_translate_props 445 (src_g_pars, dst_g_pars : graph_params) 446 (globals: list ident) 447 (data : b_graph_translate_data src_g_pars dst_g_pars globals) 448 (data_regs : list register) 449 (def_in : joint_closed_internal_function src_g_pars globals) 450 (def_out : joint_closed_internal_function dst_g_pars globals) 451 (f_lbls : label → option (list label)) 452 (f_regs : label → option (list register)) : Prop ≝ 453 { res_def_out_eq : 454 joint_if_result … def_out = init_ret … data 455 ; pars_def_out_eq : 456 joint_if_params … def_out = init_params … data 457 ; ss_def_out_eq : 458 joint_if_stacksize … def_out = init_stack_size … data 459 ; entry_eq : 460 pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) 461 ; partition_lbls : partial_partition … f_lbls 462 ; partition_regs : partial_partition … f_regs 463 ; freshness_lbls : 468 464 (∀l.opt_All … (All … 469 465 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 470 fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) ∧ 466 fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) 467 ; freshness_regs : 471 468 (∀l.opt_All … (All … 472 469 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 473 fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) ∧ 470 fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) 471 ; freshness_data_regs : 472 All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 473 fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs 474 ; data_regs_disjoint : ∀l.opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l) 475 ; multi_fetch_ok : 474 476 ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 475 477 ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧ 476 478 match s with 477 479 [ sequential s' nxt ⇒ 478 l ~❨f_step l s', l::lbls, regs❩~> nxt in joint_if_code … def_out 480 let block ≝ 481 if eq_identifier … (joint_if_entry … def_in) l then 482 append_seq_list … (f_step … data l s') (added_prologue … data) 483 else 484 f_step … data l s' in 485 l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out 479 486 | final s' ⇒ 480 l ~❨f_fin l s', l::lbls, regs❩~> it in joint_if_code … def_out487 l ~❨f_fin … data l s', l::lbls, regs❩~> it in joint_if_code … def_out 481 488 | FCOND abs _ _ _ ⇒ Ⓧabs 482 ]. 489 ] 490 }. 491 492 lemma if_merge_right : ∀A.∀b.∀x,y : A.x = y → if b then x else y = y. 493 #A * #x #y #EQ >EQ % qed. 494 495 lemma append_seq_list_nil : ∀p,g,b.append_seq_list p g b [ ] = b. 496 #p #g #b elim b -b 497 [ ** #a #b #c normalize >append_nil % 498 | #f #IH @bnew_proper #r @IH 499 ] 500 qed. 501 502 definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉. 503 504 (* translation with inline fresh register allocation *) 505 definition b_graph_translate : 506 ∀src_g_pars,dst_g_pars : graph_params. 507 ∀globals: list ident. 508 (* initialization info *) 509 ∀data : bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals). 510 (* source function *) 511 ∀def_in : joint_closed_internal_function src_g_pars globals. 512 (* destination function *) 513 Σdef_out : joint_closed_internal_function dst_g_pars globals. 514 ∃data',regs,f_lbls,f_regs. 515 bind_new_instantiates … data' data regs ∧ 516 b_graph_translate_props … data' regs def_in def_out f_lbls f_regs 517 ≝ 518 λsrc_g_pars,dst_g_pars,globals,data,def. 519 let runiv_data ≝ bcompile … (pair_swap ?? ∘ fresh RegisterTag) data (joint_if_runiverse … def) in 520 let runiv ≝ \fst runiv_data in 521 let data ≝ \snd runiv_data in 522 let entry ≝ joint_if_entry … def in 523 let init ≝ 524 mk_joint_internal_function dst_g_pars globals 525 (joint_if_luniverse … def) 526 runiv 527 (init_ret … data) (init_params … data) (init_stack_size … data) 528 (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …)) 529 («pi1 … entry, mem_set_add_id …») in 530 let f : label → joint_statement (src_g_pars : params) globals → 531 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 532 λlbl,stmt,def. 533 match stmt with 534 [ sequential inst next ⇒ 535 b_adds_graph … (f_step … data lbl inst) lbl next def 536 | final inst ⇒ 537 b_fin_adds_graph … (f_fin … data lbl inst) lbl def 538 | FCOND abs _ _ _ ⇒ Ⓧabs 539 ] in 540 let def_out ≝ foldi ??? f (joint_if_code … def) init in 541 let init_c_nxt ≝ get_first_costlabel … def in 542 let def_out_nxt ≝ adds_graph_post … (added_prologue … data) (\snd (init_c_nxt)) def_out in 543 ««add_graph … entry (sequential … (COST_LABEL … (\fst init_c_nxt)) (\snd def_out_nxt)) (\fst def_out_nxt), ?», ?». 544 @hide_prf 545 [ cases daemon 546 | cases daemon (* TODO *) 547 ] qed. 483 548 484 549 definition b_graph_transform_program : 485 550 ∀src_g_pars,dst_g_pars : graph_params. 486 ∀X : list ident → Type[0].487 551 (* initialization *) 488 552 (∀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. 553 bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) → 554 joint_program src_g_pars → 555 joint_program dst_g_pars ≝ 556 λsrc,dst,init,p. 495 557 transform_program ??? p 496 558 (λ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)). 559 b_graph_translate … (init varnames def_in) def_in)). 501 560 502 561 definition added_registers : … … 513 572 opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l). 514 573 515 (* translation without register allocation (more or less an alias) *)574 (*(* translation without register allocation (more or less an alias) *) 516 575 definition graph_translate : 517 576 ∀src_g_pars,dst_g_pars : graph_params. … … 532 591 (λl,s.return trans_step l s) 533 592 (λl,s.return trans_fin_step l s). 534 593 *) 535 594 (* 536 595 let rec add_translates -
src/joint/semanticsUtils.ma
r2675 r2681 3 3 include "utilities/hide.ma". 4 4 include "ASM/BitVectorTrie.ma". 5 include "joint/TranslateUtils.ma". 5 6 6 7 record hw_register_env : Type[0] ≝ … … 162 163 whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} 163 164 qed. 165 166 axiom b_graph_transform_program_props : 167 ∀src,dst:sem_graph_params. 168 ∀data : ∀globals.joint_closed_internal_function src globals → 169 bind_new register (b_graph_translate_data src dst globals). 170 ∀prog_in : joint_program src. 171 let prog_out ≝ b_graph_transform_program … data prog_in in 172 let src_genv ≝ globalenv_noinit ? prog_in in 173 let dst_genv ≝ globalenv_noinit ? prog_out in 174 ∃init_regs : ident → list register. 175 ∃f_lbls : ident → label → option (list label). 176 ∃f_regs : ident → label → option (list register). 177 ∀bl,id,def_in. 178 fetch_internal_function ? src_genv bl = return 〈id, def_in〉 → 179 ∃init_data,def_out. 180 fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧ 181 bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧ 182 b_graph_translate_props src dst ? init_data (init_regs id) 183 def_in def_out (f_lbls id) (f_regs id).
Note: See TracChangeset
for help on using the changeset viewer.