Changeset 1047 for src/RTLabs
 Timestamp:
 Jun 29, 2011, 5:38:27 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1046 r1047 30 30 ]. 31 31 32 axiom fresh_reg: rtl_internal_function → rtl_internal_function × register. 33 32 axiom register_fresh: universe RegisterTag → register. 33 34 definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝ 35 λdef. 36 let r ≝ register_fresh (rtl_if_runiverse def) in 37 let locals ≝ r :: rtl_if_locals def in 38 let rtl_if_luniverse' ≝ rtl_if_luniverse def in 39 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 40 let rtl_if_sig' ≝ rtl_if_sig def in 41 let rtl_if_result' ≝ rtl_if_result def in 42 let rtl_if_params' ≝ rtl_if_params def in 43 let rtl_if_locals' ≝ locals in 44 let rtl_if_stacksize' ≝ rtl_if_stacksize def in 45 let rtl_if_graph' ≝ rtl_if_graph def in 46 let rtl_if_entry' ≝ rtl_if_entry def in 47 let rtl_if_exit' ≝ rtl_if_exit def in 48 〈mk_rtl_internal_function 49 rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result' 50 rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph' 51 rtl_if_entry' rtl_if_exit', r〉. 52 34 53 let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝ 35 54 match n with … … 49 68  nil ⇒ None (register × register) 50 69 ] 51  nil ⇒ None (register × register) 52 ]. 70  nil ⇒ None (register × register) (* registers are not an address *) 71 ]. 72 73 let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝ 74 match n with 75 [ O ⇒ [ ] 76  S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n') 77 ]. 78 79 definition choose_rest ≝ 80 λA: Type[0]. 81 λleft, right: list A. 82 match left with 83 [ nil ⇒ 84 match right with 85 [ nil ⇒ None ? 86  _ ⇒ Some ? right 87 ] 88  _ ⇒ Some ? left 89 ]. 90 91 definition complete_regs ≝ 92 λdef. 93 λsrcrs1. 94 λsrcrs2. 95 let nb_added ≝ abs ((length ? srcrs1)  (length ? srcrs2)) in 96 let 〈def, added_regs〉 ≝ fresh_regs def nb_added in 97 if gtb nb_added 0 then 98 〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉 99 else 100 〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉. 101 102 definition size_of_sig_type ≝ 103 λsig. 104 match sig with 105 [ ASTint isize sign ⇒ 106 let isize' ≝ match isize with [ I8 ⇒ 8  I16 ⇒ 16  I32 ⇒ 32 ] in 107 Some ? (isize' ÷ (nat_of_bitvector ? int_size)) 108  ASTfloat _ ⇒ None ? 109  ASToffset ⇒ Some ? (nat_of_bitvector ? int_size) 110  ASTptr rgn ⇒ Some ? (nat_of_bitvector ? ptr_size) 111 ]. 112 113 definition concrete_size ≝ . 114 115 definition concrete_offset ≝ . 53 116 54 117 inductive register_type: Type[0] ≝ … … 246 309 [ cast_int i ⇒ 247 310 match destrs with 248 [ nil ⇒ None ?311 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 249 312  cons hd tl ⇒ 250 313 match tl with … … 253 316 ] 254 317 ] 255  cast_addr _symbol id ⇒318  cast_addrsymbol id ⇒ 256 319 match destrs with 257 320 [ nil ⇒ None ? … … 263 326 ] 264 327 ] 265  cast_ stack_offset off ⇒328  cast_offset off ⇒ 266 329 match destrs with 267 330 [ nil ⇒ None ? … … 280 343 ] 281 344 ] 282  cast_float f ⇒ None ? 345  cast_stack ⇒ ? 346  cast_sizeof size ⇒ ? 347 (*  cast_float f ⇒ None ? *) (* what are we doing with floats? *) 283 348 ]. 284 349
Note: See TracChangeset
for help on using the changeset viewer.