Changeset 1047
 Timestamp:
 Jun 29, 2011, 5:38:27 PM (8 years ago)
 Location:
 src
 Files:

 2 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 
src/common/AST.ma
r1046 r1047 54 54  size_array: nat → abstract_size → abstract_size. 55 55 56 definition abstract_offset ≝ abstract_size × nat. (* nth in size *) 57 56 58 inductive cast: Type[0] ≝ 57 59  cast_int: Byte → cast (* integer constant *) 58 60 (*  cast_float: float → cast (* float constant *) *) 59  cast_addrsymbol of identifier → cast (* address of a global symbol *)61  cast_addrsymbol: Identifier → cast (* address of a global symbol *) 60 62  cast_stack: cast (* address of the stack *) 61 63  cast_offset: abstract_offset → cast (* offset *) … … 119 121  ASTint : intsize → signedness → typ 120 122  ASTptr : region → typ 123  ASToffset: typ 121 124  ASTfloat : floatsize → typ. 122 125 … … 198 201 [ ASTint sz _ ⇒ size_intsize sz 199 202  ASTptr r ⇒ size_pointer r 203  ASToffset ⇒ 1 (* dpm: what!? need this for typesize pos  not sure what correct size of an offset should be? *) 200 204  ASTfloat sz ⇒ size_floatsize sz ]. 201 205 202 206 lemma typesize_pos: ∀ty. typesize ty > 0. 203 * *; try * /2/ qed.207 *; try *; try * /2/ qed. 204 208 205 209 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). 206 * * **; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.210 * *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed. 207 211 208 212 lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2). … … 658 662 659 663 definition Trace ≝ list Identifier. 660 661 (* dpm: how are floats represented? *)662 inductive cast: Type[0] ≝663  cast_int: Byte → cast (* integer constant *)664  cast_float: Byte → cast (* float constant *)665  cast_addr_symbol: ident → cast (* address of a global symbol *)666  cast_stack_offset: Byte → cast.667 664 668 665 inductive op1: Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.