Changeset 2681 for src/RTL/RTLToERTL.ma
 Timestamp:
 Feb 19, 2013, 6:48:32 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.
Note: See TracChangeset
for help on using the changeset viewer.