Changeset 1059 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Jul 6, 2011, 6:09:39 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1057 r1059 4 4 include "common/Graphs.ma". 5 5 include "common/Maps.ma". 6 include "common/IntValue.ma". 6 (* include "common/IntValue.ma". *) 7 include "common/FrontEndOps.ma". 7 8 8 9 definition add_graph ≝ … … 280 281 rtl_st_int r i dest_lbl. 281 282 282 definition translate_cst ≝ 283 λcst. 284 λdestrs. 285 λstart_lbl. 286 λdest_lbl. 287 λdef. 288 match cst with 289 [ cast_int i ⇒ 290 match destrs with 291 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 292  _ ⇒ 293 (* this case needs changing when Z is added to stdlib as we are using 294 nats instead of ints here! *) 295 let size ≝ length ? destrs in 296 let is ≝ map … (to_int size) (break size (of_int size (nat_of_bitvector ? i)) size) in 297 let is' ≝ map … (bitvector_of_nat ?) is in 298 let l ≝ map2 … (translate_cst_int_internal dest_lbl) destrs is' ? in 299 adds_graph l start_lbl dest_lbl def 300 ] 301  cast_addrsymbol id ⇒ 302 let 〈r1, r2〉 ≝ make_addr ? destrs ? in 303 add_graph start_lbl (rtl_st_addr r1 r2 id dest_lbl) def 304  _ ⇒ ? 305 ]. 306  cast_addrsymbol id ⇒ 307 match destrs with 308 [ nil ⇒ None ? 309  cons hd tl ⇒ 310 match tl with 311 [ nil ⇒ None ? 312  cons hd' tl' ⇒ 313 Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def) 314 ] 315 ] 316  cast_offset off ⇒ 317 match destrs with 318 [ nil ⇒ None ? 319  cons hd tl ⇒ 320 match tl with 321 [ nil ⇒ None ? 322  cons hd' tl' ⇒ 323 let 〈def, tmpr〉 ≝ fresh_reg def in 324 adds_graph [ 325 rtl_st_stack_addr hd hd' start_lbl; 326 rtl_st_int tmpr off start_lbl; 327 rtl_st_op2 Add hd hd tmpr start_lbl; 328 rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl; 329 rtl_st_op2 Addc hd' hd' tmpr start_lbl 330 ] start_lbl dest_lbl def 331 ] 332 ] 333  cast_stack ⇒ ? 334  cast_sizeof size ⇒ ? 335 (*  cast_float f ⇒ None ? *) (* what are we doing with floats? *) 336 ]. 337 338 let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with 339 340  AST.Cst_stack > 341 let (r1, r2) = make_addr destrs in 342 add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def 343 344  AST.Cst_offset off > 345 let i = concrete_offset off in 346 translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def 347 348  AST.Cst_sizeof size > 349 let i = concrete_size size in 350 translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def 283 axiom translate_cst: 284 ∀cst: constant. 285 ∀destrs: list register. 286 ∀start_lbl: label. 287 ∀dest_lbl: label. 288 ∀def: rtl_internal_function. 289 rtl_internal_function. 290 291 definition translate_move_internal ≝ 292 λstart_lbl: label. 293 λdestr: register. 294 λsrcr: register. 295 rtl_st_move destr srcr start_lbl. 296 297 definition translate_move ≝ 298 λdestrs: list register. 299 λsrcrs: list register. 300 λstart_lbl: label. 301 λprf:  destrs  =  srcrs . 302 let 〈crl, crr〉 ≝ reduce register destrs srcrs in 303 let 〈commonl, restl〉 ≝ crl in 304 let 〈commonr, restr〉 ≝ crr in 305 let f_common ≝ translate_move_internal start_lbl in 306 let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in 307 let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 308 add_translates [ translate1 ; translate2 ] start_lbl. 309 310 let rec translate_move destrs srcrs start_lbl = 311 let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in 312 let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in 313 let translates1 = adds_graph (List.map2 f_common common1 common2) in 314 let translates2 = translate_cst (AST.Cst_int 0) rest1 in 315 add_translates [translates1 ; translates2] start_lbl 351 316 352 317 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.