source: src/ASM/ASMCosts.ma @ 1621

Last change on this file since 1621 was 1621, checked in by mulligan, 8 years ago

to prevent conflicts

File size: 15.0 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5include "common/StructuredTraces.ma".
6
7definition current_instruction0 ≝
8  λmem,pc. \fst (\fst (fetch … mem pc)).
9
10definition current_instruction ≝
11 λs:Status. current_instruction0 (code_memory … s) (program_counter … s).
12
13definition ASM_classify0: instruction → status_class ≝
14 λi.
15  match i with
16   [ RealInstruction pre ⇒
17     match pre with
18      [ RET ⇒ cl_return
19      | JZ _ ⇒ cl_jump
20      | JNZ _ ⇒ cl_jump
21      | JC _ ⇒ cl_jump
22      | JNC _ ⇒ cl_jump
23      | JB _ _ ⇒ cl_jump
24      | JNB _ _ ⇒ cl_jump
25      | JBC _ _ ⇒ cl_jump
26      | CJNE _ _ ⇒ cl_jump
27      | DJNZ _ _ ⇒ cl_jump
28      | _ ⇒ cl_other
29      ]
30   | ACALL _ ⇒ cl_call
31   | LCALL _ ⇒ cl_call
32   | JMP _ ⇒ cl_call
33   | AJMP _ ⇒ cl_jump
34   | LJMP _ ⇒ cl_jump
35   | SJMP _ ⇒ cl_jump
36   | _ ⇒ cl_other
37   ].
38
39definition ASM_classify: Status → status_class ≝
40 λs.ASM_classify0 (current_instruction s).
41
42definition current_instruction_is_labelled ≝
43  λcost_labels: BitVectorTrie costlabel 16.
44  λs: Status.
45  let pc ≝ program_counter … s in
46    match lookup_opt … pc cost_labels with
47    [ None ⇒ False
48    | _    ⇒ True
49    ].
50
51definition label_of_current_instruction:
52 BitVectorTrie costlabel 16 → Status → list costlabel
53 ≝
54  λcost_labels,s.
55  let pc ≝ program_counter … s in
56    match lookup_opt … pc cost_labels with
57    [ None ⇒ []
58    | Some l ⇒ [l]
59    ].
60
61definition next_instruction_properly_relates_program_counters ≝
62  λbefore: Status.
63  λafter : Status.
64  let size ≝ current_instruction_cost before in
65  let pc_before ≝ program_counter … before in
66  let pc_after ≝ program_counter … after in
67  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
68    sum = pc_after.
69
70definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
71 λcost_labels.
72  mk_abstract_status
73   Status
74   (λs,s'. (execute_1 s) = s')
75   (λs,class. ASM_classify s = class)
76   (current_instruction_is_labelled cost_labels)
77   next_instruction_properly_relates_program_counters.
78
79(* To be moved in ASM/arithmetic.ma *)
80definition addr16_of_addr11: Word → Word11 → Word ≝
81  λpc: Word.
82  λa: Word11.
83  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
84  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
85  let 〈b123, b〉 ≝ split … 3 8 a in
86  let b1 ≝ get_index_v … b123 0 ? in
87  let b2 ≝ get_index_v … b123 1 ? in
88  let b3 ≝ get_index_v … b123 2 ? in
89  let p5 ≝ get_index_v … n2 0 ? in
90    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
91  //
92qed.
93   
94definition good_program_counter: BitVectorTrie Byte 16 → Word → nat → Prop ≝
95  λcode_memory: BitVectorTrie Byte 16.
96  λprogram_counter: Word.
97  λprogram_size: nat.
98    ∃n: nat.
99      let tail_program_counter ≝ fetch_program_counter_n n code_memory (zero 16) in
100        program_counter = fetch_program_counter_n (S n) code_memory (zero 16) ∧
101          nat_of_bitvector 16 program_counter ≤ program_size ∧
102            nat_of_bitvector 16 tail_program_counter ≤ nat_of_bitvector 16 program_counter.
103
104definition good_program: BitVectorTrie Byte 16 → Word → nat → Prop ≝
105  λcode_memory: BitVectorTrie Byte 16.
106  λprogram_counter: Word.
107  λtotal_program_size: nat.
108  let 〈instruction, program_counter, ticks〉 ≝ fetch code_memory program_counter in
109    match instruction with
110    [ RealInstruction instr ⇒
111      match instr with
112      [ RET                    ⇒ True
113      | JC   relative          ⇒ True (* XXX: see below *)
114      | JNC  relative          ⇒ True (* XXX: see below *)
115      | JB   bit_addr relative ⇒ True
116      | JNB  bit_addr relative ⇒ True
117      | JBC  bit_addr relative ⇒ True
118      | JZ   relative          ⇒ True
119      | JNZ  relative          ⇒ True
120      | CJNE src_trgt relative ⇒ True
121      | DJNZ src_trgt relative ⇒ True
122      | _                      ⇒
123          good_program_counter code_memory program_counter total_program_size
124      ]
125    | LCALL addr         ⇒
126      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
127      [ ADDR16 addr ⇒ λaddr16: True.
128          good_program_counter code_memory addr total_program_size ∧
129            good_program_counter code_memory program_counter total_program_size
130      | _ ⇒ λother: False. ⊥
131      ] (subaddressing_modein … addr)
132    | ACALL addr         ⇒
133      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
134      [ ADDR11 addr ⇒ λaddr11: True.
135        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
136        let 〈thr, eig〉 ≝ split … 3 8 addr in
137        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
138        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
139          good_program_counter code_memory new_program_counter total_program_size ∧
140            good_program_counter code_memory program_counter total_program_size
141      | _ ⇒ λother: False. ⊥
142      ] (subaddressing_modein … addr)
143    | AJMP  addr         ⇒
144      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
145      [ ADDR11 addr ⇒ λaddr11: True.
146        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter in
147        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
148        let bit ≝ get_index' … O ? nl in
149        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
150        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
151        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
152          (good_program_counter code_memory new_program_counter total_program_size) ∧
153            (good_program_counter code_memory program_counter total_program_size)
154      | _ ⇒ λother: False. ⊥
155      ] (subaddressing_modein … addr)
156    | LJMP  addr         ⇒
157      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
158      [ ADDR16 addr ⇒ λaddr16: True.
159          good_program_counter code_memory addr total_program_size ∧
160            good_program_counter code_memory program_counter total_program_size
161      | _ ⇒ λother: False. ⊥
162      ] (subaddressing_modein … addr)
163    | SJMP  addr     ⇒
164      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
165      [ RELATIVE addr ⇒ λrelative: True.
166        let 〈carry, new_program_counter〉 ≝ half_add … program_counter (sign_extension addr) in
167          good_program_counter code_memory new_program_counter total_program_size ∧
168            good_program_counter code_memory program_counter total_program_size
169      | _ ⇒ λother: False. ⊥
170      ] (subaddressing_modein … addr)
171    | JMP   addr     ⇒ True (* XXX: should recurse here, but dptr in JMP ... *)
172    | MOVC  src trgt ⇒
173        good_program_counter code_memory program_counter total_program_size
174    ].
175  cases other
176qed.
177
178axiom dubious:
179  ∀m, n, o, p: nat.
180    1 ≤ p → n ≤ m → m - n ≤ S o → m - (n + p) ≤ o.
181
182lemma subaddressing_mod_elim:
183 ∀T:Type[2].
184 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19,addr,p.
185 ∀Q: addressing_mode → T → Prop.
186 (∀w. Q (ADDR11 w) (P1 w)) →
187  Q addr (match addr
188     in addressing_mode
189     return λx:addressing_mode.(is_in 1 [[addr11]] x→T)
190     with 
191    [ADDR11 (x:Word11) ⇒ λH:True. P1 x
192    |ADDR16 _ ⇒ λH:False. P2 H
193    |DIRECT _ ⇒ λH:False. P3 H
194    |INDIRECT _ ⇒ λH:False. P4 H
195    |EXT_INDIRECT _ ⇒ λH:False. P5 H
196    |ACC_A ⇒ λH:False. P6 H
197    |REGISTER _ ⇒ λH:False. P7 H
198    |ACC_B ⇒ λH:False. P8 H
199    |DPTR ⇒ λH:False. P9 H
200    |DATA _ ⇒ λH:False. P10 H
201    |DATA16 _ ⇒ λH:False. P11 H
202    |ACC_DPTR ⇒ λH:False. P12 H
203    |ACC_PC ⇒ λH:False. P13 H
204    |EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
205    |INDIRECT_DPTR ⇒ λH:False. P15 H
206    |CARRY ⇒ λH:False. P16 H
207    |BIT_ADDR _ ⇒ λH:False. P17 H
208    |N_BIT_ADDR _ ⇒ λH:False. P18 H   
209    |RELATIVE _ ⇒ λH:False. P19 H
210    ] p).
211 #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
212 #P14 #P15 #P16 #P17 #P18 #P19
213 * try #x1 try #x2 try #x3 try #x4
214 try (@⊥ assumption) normalize @x4
215qed.
216
217let rec block_cost
218  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
219    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
220      (good_program_witness: good_program code_memory program_counter total_program_size)
221        on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
222  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
223  [ O ⇒ λbase_case. 0
224  | S program_size' ⇒ λrecursive_case.
225    let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
226      match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with
227      [ None   ⇒
228        match instruction return λx. x = instruction → ? with
229        [ RealInstruction instruction ⇒ λreal_instruction.
230          match instruction return λx. x = instruction → ? with
231          [ RET                    ⇒ λret.  ticks
232          | JC   relative          ⇒ λjc.   ticks
233          | JNC  relative          ⇒ λjnc.  ticks
234          | JB   bit_addr relative ⇒ λjb.   ticks
235          | JNB  bit_addr relative ⇒ λjnb.  ticks
236          | JBC  bit_addr relative ⇒ λjbc.  ticks
237          | JZ   relative          ⇒ λjz.   ticks
238          | JNZ  relative          ⇒ λjnz.  ticks
239          | CJNE src_trgt relative ⇒ λcjne. ticks
240          | DJNZ src_trgt relative ⇒ λdjnz. ticks
241          | _                      ⇒ λalt.
242              ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
243          ] (refl … instruction)
244        | ACALL addr     ⇒ λacall.
245            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
246        | AJMP  addr     ⇒ λajmp. ticks
247        | LCALL addr     ⇒ λlcall.
248            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
249        | LJMP  addr     ⇒ λljmp. ticks
250        | SJMP  addr     ⇒ λsjmp. ticks
251        | JMP   addr     ⇒ λjmp. (* XXX: actually a call due to use with fptrs *)
252            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
253        | MOVC  src trgt ⇒ λmovc.
254            ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? ?
255        ] (refl … instruction)
256      | Some _ ⇒ ticks
257      ]
258  ].
259  [1: -block_cost -eta62747 -program_size
260    generalize in match good_program_witness;
261    whd in match good_program; normalize nodelta
262    cases FETCH normalize nodelta
263    cases acall normalize nodelta
264    @(subaddressing_mod_elim Prop ??????????????????? addr
265       (subaddressing_modein ? [[addr11]] addr)
266       (λ_.λP. P → total_program_size-nat_of_bitvector 16 program_counter'≤program_size'))
267       
268    cases addr #subaddressing_mode cases subaddressing_mode
269    try (#assm #absurd normalize in absurd; cases absurd)
270    try (#absurd normalize in absurd; cases absurd)
271    normalize nodelta
272    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
273    cases (split … 3 8 assm) #thr #eig normalize nodelta
274    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
275    #assm cases assm #ignore
276    whd in match good_program_counter; normalize nodelta * #n * *
277    #program_counter_eq' #program_counter_lt_total_program_size
278    #fetch_n_leq_program_counter'
279    lapply(dubious total_program_size (nat_of_bitvector … program_counter')
280      program_size' ? ? ? ?)
281    [2: assumption ]
282  [2:
283    (* generalize in match good_program_witness; *)
284    whd in match good_program; normalize nodelta
285    cases FETCH normalize nodelta
286    cases (fetch code_memory program_counter') #instruction_program_counter' #ticks' normalize nodelta
287    cases instruction_program_counter' #instruction' #program_counter'' normalize nodelta
288    cases acall normalize nodelta
289    cases addr #subaddressing_mode cases subaddressing_mode
290    try (#assm #absurd normalize in absurd; cases absurd)
291    try (#absurd normalize in absurd; cases absurd)
292    normalize nodelta
293    cases instruction'
294    try (#assm normalize nodelta)
295    [7:
296      #irrelevant
297      whd in match good_program_counter; normalize nodelta
298     
299     
300     
301     
302     
303     
304     
305     
306     
307(* XXX: use memoisation here in the future *)
308let rec block_cost
309  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
310    (program_counter: Word) (program_size: nat) (total_program_size: nat)
311      (size_invariant: total_program_size ≤ code_memory_size)
312        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
313          on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝
314  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with
315  [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *)
316  | S program_size ⇒ λrecursive_case.
317    let 〈instr, newpc, ticks〉 ≝ fetch … code_memory program_counter in
318      match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
319      [ None ⇒
320          let classify ≝ ASM_classify0 instr in
321          match classify return λx. classify = x → ? with
322          [ cl_jump ⇒ λclassify_refl. ticks
323          | cl_call ⇒ λclassify_refl. (* ite here *)
324              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
325          | cl_return ⇒ λclassify_refl. ticks
326          | cl_other ⇒ λclassify_refl. (* ite here *)
327              ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
328          ] (refl … classify)
329        | Some _ ⇒ ticks
330      ]
331  ].
332
333let rec traverse_code_internal
334  (program: list Byte) (mem: BitVectorTrie Byte 16)
335    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
336      on program: identifier_map CostTag nat ≝
337 let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
338 match program with
339 [ nil ⇒ empty_map …
340 | cons hd tl ⇒
341   match lookup_opt … pc cost_labels with
342   [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
343   | Some lbl ⇒
344     let cost ≝ block_cost mem cost_labels pc program_size in
345     let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
346       add … cost_mapping lbl cost ]].
347
348definition traverse_code ≝
349  λprogram: list Byte.
350  λmem: BitVectorTrie Byte 16.
351  λcost_labels.
352  λprogram_size: nat.
353    traverse_code_internal program mem cost_labels (zero …) program_size.
354
355definition compute_costs ≝
356  λprogram: list Byte.
357  λcost_labels: BitVectorTrie costlabel 16.
358  λhas_main: bool.
359  let program_size ≝ |program| + 1 in
360  let memory ≝ load_code_memory program in
361   traverse_code program memory cost_labels program_size.
Note: See TracBrowser for help on using the repository browser.