source: src/ERTL/Uses.ma @ 756

Last change on this file since 756 was 756, checked in by mulligan, 10 years ago

Made a start on RTL. Renaming in ERTL and below to move closer to Brian's naming convention and datatypes.

File size: 6.2 KB
Line 
1include "ERTL/ERTL.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "ASM/Arithmetic.ma".
4include "ASM/I8051.ma".
5include "common/Registers.ma".
6
7definition count ≝
8  λr: register.
9  λuses.
10    let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
11      insert ? 16 register l uses.
12     
13definition 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 ]
151qed.
152
153(*
154definition examine_internal ≝
155  λint_fun.
156    let uses ≝ foldr ? ? examine_statement (Stub ? ?) (ERTL_IF_Graph int_fun) in
157      lookup uses.
158*)
Note: See TracBrowser for help on using the repository browser.