 Timestamp:
 Mar 7, 2013, 2:51:40 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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