1 | include "ERTL/ERTL.ma". |
---|
2 | include "utilities/BitVectorTrieSet.ma". |
---|
3 | include "ASM/Arithmetic.ma". |
---|
4 | include "ASM/I8051.ma". |
---|
5 | |
---|
6 | definition count ≝ |
---|
7 | λregister. |
---|
8 | λuses. |
---|
9 | let l ≝ increment ? (lookup ? ? register uses (zero 16)) in |
---|
10 | insert ? 16 register l uses. |
---|
11 | |
---|
12 | definition examine_statement ≝ |
---|
13 | λstatement: ERTLStatement. |
---|
14 | λuses. |
---|
15 | match statement with |
---|
16 | [ ERTL_St_Skip _ ⇒ uses |
---|
17 | | ERTL_St_Comment _ _ ⇒ uses |
---|
18 | | ERTL_St_Cost _ _ ⇒ uses |
---|
19 | | ERTL_St_Hdw_To_Hdw _ _ _ ⇒ uses |
---|
20 | | ERTL_St_NewFrame _ ⇒ uses |
---|
21 | | ERTL_St_DelFrame _ ⇒ uses |
---|
22 | | ERTL_St_ClearCarry _ ⇒ uses |
---|
23 | | ERTL_St_Call_Id _ _ _ ⇒ uses |
---|
24 | | ERTL_St_Return _ ⇒ uses |
---|
25 | | ERTL_St_Get_Hdw r _ _ ⇒ count (word_of_register r) uses |
---|
26 | | ERTL_St_Set_Hdw _ r _ ⇒ count (word_of_register r) uses |
---|
27 | | ERTL_St_FrameSize ar _ ⇒ |
---|
28 | match ar with [ |
---|
29 | mkAbstractRegister r ⇒ |
---|
30 | (* dpm: shift the abstract registers above the physical registers *) |
---|
31 | let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in |
---|
32 | count offset uses |
---|
33 | ] |
---|
34 | | ERTL_St_Pop ar _ ⇒ |
---|
35 | match ar with [ |
---|
36 | mkAbstractRegister r ⇒ |
---|
37 | let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in |
---|
38 | count offset uses |
---|
39 | ] |
---|
40 | | ERTL_St_Push ar _ ⇒ |
---|
41 | match ar with [ |
---|
42 | mkAbstractRegister r ⇒ |
---|
43 | let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in |
---|
44 | count offset uses |
---|
45 | ] |
---|
46 | | ERTL_St_Int ar _ _ ⇒ |
---|
47 | match ar with [ |
---|
48 | mkAbstractRegister r ⇒ |
---|
49 | let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in |
---|
50 | count offset uses |
---|
51 | ] |
---|
52 | | ERTL_St_AddrH ar _ _ ⇒ |
---|
53 | match ar with [ |
---|
54 | mkAbstractRegister r ⇒ |
---|
55 | let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in |
---|
56 | count offset uses |
---|
57 | ] |
---|
58 | | ERTL_St_AddrL ar _ _ ⇒ |
---|
59 | match ar with [ |
---|
60 | mkAbstractRegister r ⇒ |
---|
61 | let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in |
---|
62 | count offset uses |
---|
63 | ] |
---|
64 | | ERTL_St_CondAcc ar _ _ ⇒ |
---|
65 | match ar with [ |
---|
66 | mkAbstractRegister r ⇒ |
---|
67 | let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in |
---|
68 | count offset uses |
---|
69 | ] |
---|
70 | | ERTL_St_Move ar1 ar2 _ ⇒ |
---|
71 | match ar1 with [ |
---|
72 | mkAbstractRegister r1 ⇒ |
---|
73 | match ar2 with [ |
---|
74 | mkAbstractRegister r2 ⇒ |
---|
75 | let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in |
---|
76 | let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in |
---|
77 | count offset1 (count offset2 uses) |
---|
78 | ] |
---|
79 | ] |
---|
80 | | ERTL_St_Op1 op1 ar1 ar2 _ ⇒ |
---|
81 | match ar1 with [ |
---|
82 | mkAbstractRegister r1 ⇒ |
---|
83 | match ar2 with [ |
---|
84 | mkAbstractRegister r2 ⇒ |
---|
85 | let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in |
---|
86 | let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in |
---|
87 | count offset1 (count offset2 uses) |
---|
88 | ] |
---|
89 | ] |
---|
90 | | ERTL_St_Op2 op2 ar1 ar2 ar3 _ ⇒ |
---|
91 | match ar1 with [ |
---|
92 | mkAbstractRegister r1 ⇒ |
---|
93 | match ar2 with [ |
---|
94 | mkAbstractRegister r2 ⇒ |
---|
95 | match ar3 with [ |
---|
96 | mkAbstractRegister r3 ⇒ |
---|
97 | let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in |
---|
98 | let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in |
---|
99 | let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in |
---|
100 | count offset1 (count offset2 (count offset3 uses)) |
---|
101 | ] |
---|
102 | ] |
---|
103 | ] |
---|
104 | | ERTL_St_Opaccs opaccs ar1 ar2 ar3 _ ⇒ |
---|
105 | match ar1 with [ |
---|
106 | mkAbstractRegister r1 ⇒ |
---|
107 | match ar2 with [ |
---|
108 | mkAbstractRegister r2 ⇒ |
---|
109 | match ar3 with [ |
---|
110 | mkAbstractRegister r3 ⇒ |
---|
111 | let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in |
---|
112 | let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in |
---|
113 | let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in |
---|
114 | count offset1 (count offset2 (count offset3 uses)) |
---|
115 | ] |
---|
116 | ] |
---|
117 | ] |
---|
118 | | ERTL_St_Load ar1 ar2 ar3 _ ⇒ |
---|
119 | match ar1 with [ |
---|
120 | mkAbstractRegister r1 ⇒ |
---|
121 | match ar2 with [ |
---|
122 | mkAbstractRegister r2 ⇒ |
---|
123 | match ar3 with [ |
---|
124 | mkAbstractRegister r3 ⇒ |
---|
125 | let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in |
---|
126 | let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in |
---|
127 | let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in |
---|
128 | count offset1 (count offset2 (count offset3 uses)) |
---|
129 | ] |
---|
130 | ] |
---|
131 | ] |
---|
132 | | ERTL_St_Store ar1 ar2 ar3 _ ⇒ |
---|
133 | match ar1 with [ |
---|
134 | mkAbstractRegister r1 ⇒ |
---|
135 | match ar2 with [ |
---|
136 | mkAbstractRegister r2 ⇒ |
---|
137 | match ar3 with [ |
---|
138 | mkAbstractRegister r3 ⇒ |
---|
139 | let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in |
---|
140 | let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in |
---|
141 | let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in |
---|
142 | count offset1 (count offset2 (count offset3 uses)) |
---|
143 | ] |
---|
144 | ] |
---|
145 | ] |
---|
146 | ]. |
---|
147 | [*: normalize |
---|
148 | @ le_S @ le_S @ le_S @ le_S @ le_S @ le_S |
---|
149 | @ le_S @ le_S @ le_S @ le_S @ le_S @ le_n ] |
---|
150 | qed. |
---|
151 | |
---|
152 | (* |
---|
153 | definition examine_internal ≝ |
---|
154 | λint_fun. |
---|
155 | let uses ≝ foldr ? ? examine_statement (Stub ? ?) (ERTL_IF_Graph int_fun) in |
---|
156 | lookup uses. |
---|
157 | *) |
---|