Changeset 1082 for src/ERTL/Uses.ma


Ignore:
Timestamp:
Jul 20, 2011, 5:17:38 PM (9 years ago)
Author:
mulligan
Message:

work from today on ertl -> ltl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Uses.ma

    r777 r1082  
    11include "ERTL/ERTL.ma".
    2 include "utilities/BitVectorTrieSet.ma".
    3 include "ASM/Arithmetic.ma".
    4 include "ASM/I8051.ma".
    52include "common/Registers.ma".
    6 
    7 definition count ≝
    8   λr: register.
    9   λuses.
    10     let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
    11       insert ? 16 l uses.
    12      
    13 definition examine_statement ≝
    14   λstatement: ertl_statement.
    15   λuses.
    16   match statement with
    17   [ ertl_st_skip _ ⇒ uses
    18   | ertl_st_comment _ _ ⇒ uses
    19   | ertl_st_cost _ _ ⇒ uses
    20   | ertl_st_hdw_to_hdw _ _ _ ⇒ uses
    21   | ertl_st_new_frame _ ⇒ uses
    22   | ertl_st_del_frame _ ⇒ uses
    23   | ertl_st_clear_carry _ ⇒ uses
    24   | ertl_st_call_id _ _ _ ⇒ uses
    25   | ertl_st_return _ ⇒ uses
    26   | ertl_st_get_hdw r _ _ ⇒ count (word_of_register r) uses
    27   | ertl_st_set_hdw _ r _ ⇒ count (word_of_register r) uses
    28   | ertl_st_frame_size ar _ ⇒
    29     match ar with [
    30       mk_abstract_register r ⇒
    31         (* dpm: shift the abstract registers above the physical registers *)
    32         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    33           count offset uses
    34     ]
    35   | ertl_st_pop ar _ ⇒
    36     match ar with [
    37       mk_abstract_register r ⇒
    38         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    39           count offset uses
    40     ]
    41   | ertl_st_push ar _ ⇒
    42     match ar with [
    43       mk_abstract_register r ⇒
    44         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    45           count offset uses
    46     ]
    47   | ertl_st_int ar _ _ ⇒
    48     match ar with [
    49       mk_abstract_register r ⇒
    50         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    51           count offset uses
    52     ]
    53   | ertl_st_addr_h ar _ _ ⇒
    54     match ar with [
    55       mk_abstract_register r ⇒
    56         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    57           count offset uses
    58     ]
    59   | ertl_st_addr_l ar _ _ ⇒
    60     match ar with [
    61       mk_abstract_register r ⇒
    62         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    63           count offset uses
    64     ]
    65   | ertl_st_cond_acc ar _ _ ⇒
    66     match ar with [
    67       mk_abstract_register r ⇒
    68         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    69           count offset uses
    70     ]
    71   | ertl_st_move ar1 ar2 _ ⇒
    72     match ar1 with [
    73       mk_abstract_register r1 ⇒
    74       match ar2 with [
    75         mk_abstract_register r2 ⇒
    76           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    77           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    78             count offset1 (count offset2 uses)
    79       ]
    80     ]
    81   | ertl_st_op1 op1 ar1 ar2 _ ⇒
    82     match ar1 with [
    83       mk_abstract_register r1 ⇒
    84       match ar2 with [
    85         mk_abstract_register r2 ⇒
    86           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    87           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    88             count offset1 (count offset2 uses)
    89       ]
    90     ]
    91   | ertl_st_op2 op2 ar1 ar2 ar3 _ ⇒
    92     match ar1 with [
    93       mk_abstract_register r1 ⇒
    94       match ar2 with [
    95         mk_abstract_register r2 ⇒
    96         match ar3 with [
    97           mk_abstract_register r3 ⇒
    98           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    99           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    100           let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
    101             count offset1 (count offset2 (count offset3 uses))
    102         ]
    103       ]
    104     ]
    105   | ertl_st_opaccs opaccs ar1 ar2 ar3 _ ⇒
    106     match ar1 with [
    107       mk_abstract_register r1 ⇒
    108       match ar2 with [
    109         mk_abstract_register r2 ⇒
    110         match ar3 with [
    111           mk_abstract_register r3 ⇒
    112           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    113           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    114           let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
    115             count offset1 (count offset2 (count offset3 uses))
    116         ]
    117       ]
    118     ]
    119   | ertl_st_load ar1 ar2 ar3 _ ⇒
    120     match ar1 with [
    121       mk_abstract_register r1 ⇒
    122       match ar2 with [
    123         mk_abstract_register r2 ⇒
    124         match ar3 with [
    125           mk_abstract_register r3 ⇒
    126           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    127           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    128           let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
    129             count offset1 (count offset2 (count offset3 uses))
    130         ]
    131       ]
    132     ]
    133   | ertl_st_store ar1 ar2 ar3 _ ⇒
    134     match ar1 with [
    135       mk_abstract_register r1 ⇒
    136       match ar2 with [
    137         mk_abstract_register r2 ⇒
    138         match ar3 with [
    139           mk_abstract_register r3 ⇒
    140           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    141           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    142           let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
    143             count offset1 (count offset2 (count offset3 uses))
    144         ]
    145       ]
    146     ]
    147   ].
    148   [*: normalize
    149       @ le_S @ le_S @ le_S @ le_S @ le_S @ le_S
    150       @ le_S @ le_S @ le_S @ le_S @ le_S @ le_n ]
    151 qed.
    152 
    153 (*
    154 definition examine_internal ≝
    155   λint_fun.
    156     let uses ≝ foldr ? ? examine_statement (Stub ? ?) (ERTL_IF_Graph int_fun) in
    157       lookup uses.
    158 *)
Note: See TracChangeset for help on using the changeset viewer.