source: src/ASM/ASMCosts.ma @ 1489

Last change on this file since 1489 was 1486, checked in by mulligan, 9 years ago

finished asm costs

File size: 9.9 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5
6inductive instruction_nature: Type[0] ≝
7  | goto: Word → instruction_nature
8  | branch: Word → instruction_nature
9  | direct_fun_call: Word → instruction_nature
10  | ret: instruction_nature
11  | other: instruction_nature.
12
13definition addr16_of_addr11: Word → Word11 → Word ≝
14  λpc: Word.
15  λa: Word11.
16  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
17  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
18  let 〈b123, b〉 ≝ split … 3 8 a in
19  let b1 ≝ get_index_v … b123 0 ? in
20  let b2 ≝ get_index_v … b123 1 ? in
21  let b3 ≝ get_index_v … b123 2 ? in
22  let p5 ≝ get_index_v … n2 0 ? in
23    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
24  //
25qed.
26
27definition instruction_info:
28    BitVectorTrie Byte 16 → Word → ? ≝
29  λmem.
30  λpc.
31  let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in
32  let 〈nature, next_pcs〉 ≝
33    match inst with
34    [ RealInstruction ri ⇒
35      match ri with
36      [ RET ⇒ 〈ret, [ ]〉
37      | RETI ⇒ 〈ret, [ ]〉
38      | JC addr ⇒
39        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
40        [ RELATIVE addr ⇒ λ_.
41          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
42            〈branch addr, [ next_pc; addr ]〉
43        | _ ⇒ λp. match p in False with [ ]
44        ] (subaddressing_modein … addr)
45      | JNC addr ⇒
46        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
47        [ RELATIVE addr ⇒ λ_.
48          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
49            〈branch addr, [ next_pc; addr ]〉
50        | _ ⇒ λp. match p in False with [ ]
51        ] (subaddressing_modein … addr)
52      | JZ addr ⇒
53        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
54        [ RELATIVE addr ⇒ λ_.
55          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
56            〈branch addr, [ next_pc; addr ]〉
57        | _ ⇒ λp. match p in False with [ ]
58        ] (subaddressing_modein … addr)
59      | JNZ addr ⇒
60        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
61        [ RELATIVE addr ⇒ λ_.
62          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
63            〈branch addr, [ next_pc; addr ]〉
64        | _ ⇒ λp. match p in False with [ ]
65        ] (subaddressing_modein … addr)
66      | JB addr1 addr2 ⇒
67        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
68        [ RELATIVE addr ⇒ λ_.
69          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
70            〈branch addr, [ next_pc; addr ]〉
71        | _ ⇒ λp. match p in False with [ ]
72        ] (subaddressing_modein … addr2)
73      | JNB addr1 addr2 ⇒
74        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
75        [ RELATIVE addr ⇒ λ_.
76          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
77            〈branch addr, [ next_pc; addr ]〉
78        | _ ⇒ λp. match p in False with [ ]
79        ] (subaddressing_modein … addr2)
80      | JBC addr1 addr2 ⇒
81        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
82        [ RELATIVE addr ⇒ λ_.
83          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
84            〈branch addr, [ next_pc; addr ]〉
85        | _ ⇒ λp. match p in False with [ ]
86        ] (subaddressing_modein … addr2)
87      | DJNZ addr1 addr2 ⇒
88        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
89        [ RELATIVE addr ⇒ λ_.
90          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
91            〈branch addr, [ next_pc; addr ]〉
92        | _ ⇒ λp. match p in False with [ ]
93        ] (subaddressing_modein … addr2)
94      | CJNE addr1 addr2 ⇒
95        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
96        [ RELATIVE addr ⇒ λ_.
97          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
98            〈branch addr, [ next_pc; addr ]〉
99        | _ ⇒ λp. match p in False with [ ]
100        ] (subaddressing_modein … addr2)
101      | _ ⇒ 〈other, [ next_pc ]〉
102      ]
103    | ACALL addr ⇒
104      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
105      [ ADDR11 addr ⇒ λ_.
106        let addr ≝ addr16_of_addr11 pc addr in
107          〈direct_fun_call addr, [ next_pc ]〉
108      | _ ⇒ λp. match p in False with [ ]
109      ] (subaddressing_modein … addr)
110    | LCALL addr ⇒
111      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
112      [ ADDR16 addr ⇒ λ_. 〈direct_fun_call addr, [ next_pc ]〉
113      | _ ⇒ λp. match p in False with [ ]
114      ] (subaddressing_modein … addr)
115    | AJMP addr ⇒
116      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
117      [ ADDR11 addr ⇒ λ_.
118        let addr ≝ addr16_of_addr11 pc addr in
119          〈goto addr, [ addr ]〉
120      | _ ⇒ λp. match p in False with [ ]
121      ] (subaddressing_modein … addr)
122    | LJMP addr ⇒
123      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
124      [ ADDR16 addr ⇒ λ_. 〈goto addr, [ addr ]〉
125      | _ ⇒ λp. match p in False with [ ]
126      ] (subaddressing_modein … addr)
127    | SJMP addr ⇒
128      match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
129      [ RELATIVE addr ⇒ λ_.
130        let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in
131          〈goto addr, [ addr ]〉
132      | _ ⇒ λp. match p in False with [ ]
133      ] (subaddressing_modein … addr)
134    | JMP addr ⇒ 〈other, [ next_pc ]〉
135    | MOVC acc_a addr ⇒ 〈other, [ next_pc ]〉
136    ]
137  in
138    〈nature, next_pc, next_pcs, inst_cost〉.
139
140let rec compare
141  (a: Type[0]) (the_list: list (a × nat))
142    on the_list: nat ≝
143  match the_list with
144  [ nil ⇒ ⊥ (* XXX: was assert false *)
145  | cons hd tl ⇒
146    match tl with
147    [ nil ⇒
148      let 〈pc, cost〉 ≝ hd in
149        cost
150    | cons hd' tl' ⇒
151      let 〈pc1, cost1〉 ≝ hd in
152      let 〈pc2, cost2〉 ≝ hd' in
153        match eq_nat cost1 cost2 with
154        [ true ⇒ max cost1 (compare … tl)
155        | false ⇒ compare … tl'
156        ]
157    ]
158  ].
159  cases daemon
160qed.
161
162let rec block_cost
163  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
164    (the_list: list Word) (program_size: nat)
165      on program_size: nat ≝
166  match program_size with
167  [ O ⇒ 0 (* XXX: empty program *)
168  | S program_size ⇒
169    match the_list with
170    [ nil ⇒ 0 (* XXX: should be empty program *)
171    | cons pc tl ⇒
172      match tl with
173      [ nil ⇒
174        match lookup_opt … pc cost_labels with
175        [ None ⇒
176          let 〈ignore, ignore, next_pcs, cost〉 ≝ instruction_info mem pc in
177          let tail ≝ block_cost mem cost_labels next_pcs program_size in
178            cost + tail
179        | Some _ ⇒ O
180        ]
181      | _   ⇒ compare ? (map … (λpc. 〈pc, block_cost mem cost_labels [pc] program_size〉) the_list)
182      ]
183    ]
184  ].
185
186let rec traverse_code_internal
187  (program: list Byte) (mem: BitVectorTrie Byte 16)
188    (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat)
189      on program: BitVectorTrie nat 8 ≝
190  let 〈ignore, newpc, ignore, ignore〉 ≝ instruction_info mem pc in
191  match program with
192  [ nil ⇒ Stub …
193  | cons hd tl ⇒
194    match lookup_opt … pc cost_labels with
195    [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
196    | Some lbl ⇒
197      let cost ≝ block_cost mem cost_labels [ pc ] program_size in
198      let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
199        insert … lbl cost cost_mapping
200    ]
201  ].
202
203definition traverse_code ≝
204  λprogram: list Byte.
205  λmem: BitVectorTrie Byte 16.
206  λcost_labels.
207  λprogram_size: nat.
208    traverse_code_internal program mem cost_labels (zero …) program_size.
209
210let rec first_cost_label_internal
211  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
212    (program_size: nat) (oldpc: Word)
213      on program_size: (Byte × nat) ≝
214  match program_size with
215  [ O ⇒ ⊥ (* XXX: ummm ... ? *)
216  | S program_size ⇒
217    match lookup_opt … oldpc cost_labels with
218    [ None ⇒
219      let 〈nature, pc, ignore, inst_cost〉 ≝ instruction_info mem oldpc in
220        match nature with
221        [ direct_fun_call addr ⇒
222          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in
223            〈lbl, inst_cost + cost〉
224        | other ⇒
225          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in
226            〈lbl, inst_cost + cost〉
227        | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)
228        ]
229    | Some cost ⇒ 〈cost, 0〉
230    ]
231  ].
232  cases daemon
233qed.
234
235definition first_cost_label ≝
236  λmem: BitVectorTrie Byte 16.
237  λcost_labels: BitVectorTrie Byte 16.
238  λprogram_size: nat.
239    first_cost_label_internal mem cost_labels program_size (zero …).
240
241definition initialize_costs ≝
242  λmem: BitVectorTrie Byte 16.
243  λcost_labels: BitVectorTrie Byte 16.
244  λcost_mapping: BitVectorTrie nat 8.
245  λprogram_size: nat.
246  let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
247  let old_cost ≝
248    match lookup_opt … lbl cost_mapping with
249    [ None ⇒ 0
250    | Some cost ⇒ cost
251    ]
252  in
253  let new_cost ≝ old_cost + cost in
254    insert … lbl new_cost cost_mapping.
255
256definition compute_costs ≝
257  λprogram: list Byte.
258  λcost_labels: BitVectorTrie Byte 16.
259  λhas_main: bool.
260  let program_size ≝ |program| in
261  let memory ≝ load_code_memory program in
262  let costs_mapping ≝ traverse_code program memory cost_labels program_size in
263    match has_main with
264    [ true ⇒
265      initialize_costs memory cost_labels costs_mapping program_size
266    | false ⇒ costs_mapping
267    ].
Note: See TracBrowser for help on using the repository browser.