1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Interpret.ma". |
---|
5 | include "common/StructuredTraces.ma". |
---|
6 | |
---|
7 | definition current_instruction0 ≝ |
---|
8 | λmem,pc. \fst (\fst (fetch … mem pc)). |
---|
9 | |
---|
10 | definition current_instruction ≝ |
---|
11 | λs:Status. current_instruction0 (code_memory … s) (program_counter … s). |
---|
12 | |
---|
13 | definition 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 | |
---|
39 | definition ASM_classify: Status → status_class ≝ |
---|
40 | λs.ASM_classify0 (current_instruction s). |
---|
41 | |
---|
42 | definition 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 | |
---|
51 | definition 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 | |
---|
61 | definition 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 | |
---|
70 | definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝ |
---|
71 | λcost_labels. |
---|
72 | mk_abstract_status |
---|
73 | Status |
---|
74 | (λs,s'. eject … (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 *) |
---|
80 | definition 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 | // |
---|
92 | qed. |
---|
93 | |
---|
94 | let rec block_cost |
---|
95 | (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) |
---|
96 | (pc: Word) (program_size: nat) on program_size : nat ≝ |
---|
97 | match program_size with |
---|
98 | [ O ⇒ 0 |
---|
99 | | S program_size ⇒ |
---|
100 | let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in |
---|
101 | match lookup_opt … newpc cost_labels with |
---|
102 | [ None ⇒ |
---|
103 | match ASM_classify0 instr with |
---|
104 | [ cl_jump ⇒ ticks |
---|
105 | | cl_call ⇒ ticks + block_cost mem cost_labels newpc program_size |
---|
106 | | cl_return ⇒ ticks |
---|
107 | | cl_other ⇒ ticks + block_cost mem cost_labels newpc program_size |
---|
108 | ] |
---|
109 | | Some _ ⇒ ticks ]]. |
---|
110 | |
---|
111 | let rec traverse_code_internal |
---|
112 | (program: list Byte) (mem: BitVectorTrie Byte 16) |
---|
113 | (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat) |
---|
114 | on program: identifier_map CostTag nat ≝ |
---|
115 | let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in |
---|
116 | match program with |
---|
117 | [ nil ⇒ empty_map … |
---|
118 | | cons hd tl ⇒ |
---|
119 | match lookup_opt … pc cost_labels with |
---|
120 | [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size |
---|
121 | | Some lbl ⇒ |
---|
122 | let cost ≝ block_cost mem cost_labels pc program_size in |
---|
123 | let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in |
---|
124 | add … cost_mapping lbl cost ]]. |
---|
125 | |
---|
126 | definition traverse_code ≝ |
---|
127 | λprogram: list Byte. |
---|
128 | λmem: BitVectorTrie Byte 16. |
---|
129 | λcost_labels. |
---|
130 | λprogram_size: nat. |
---|
131 | traverse_code_internal program mem cost_labels (zero …) program_size. |
---|
132 | |
---|
133 | definition compute_costs ≝ |
---|
134 | λprogram: list Byte. |
---|
135 | λcost_labels: BitVectorTrie costlabel 16. |
---|
136 | λhas_main: bool. |
---|
137 | let program_size ≝ |program| in |
---|
138 | let memory ≝ load_code_memory program in |
---|
139 | traverse_code program memory cost_labels program_size. |
---|