source: src/ASM/ASMCosts.ma @ 1591

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

work from today

File size: 8.1 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 
94axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o:
95  ∀m, n, o: nat.
96    m - n ≤ m - S o → S m - n ≤ m - o.
97
98lemma strengthened_invariant:
99  ∀code_memory: BitVectorTrie Byte 16.
100  ∀total_program_size: nat.
101  ∀new_program_counter: Word.
102  ∀program_counter: Word.
103    total_program_size ≤ code_memory_size →
104      let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
105        Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) →
106          new_program_counter = \snd (\fst (fetch … code_memory program_counter)) →
107            nat_of_bitvector … program_counter ≤ total_program_size →
108              nat_of_bitvector … new_program_counter ≤ total_program_size.
109  #code_memory #total_program_size #new_program_counter #program_counter
110  #relation_total_program_code_memory_size #end_instruction_is_ok
111  #new_program_counter_from_fetch #program_counter_within_program
112  >new_program_counter_from_fetch
113  lapply (sig2 ? ? (fetch code_memory program_counter)) #assm
114   
115       
116(* XXX: use memoisation here in the future *)
117let rec block_cost
118  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
119    (program_counter: Word) (program_size: nat) (total_program_size: nat)
120      (size_invariant: total_program_size ≤ code_memory_size)
121        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
122          (final_instr_invariant:
123            let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
124              Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return))
125                on program_size: total_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
126  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter < program_size → nat with
127  [ O ⇒ λabsurd. ⊥
128  | S program_size ⇒ λrecursive_case.
129    let ticks ≝ \snd (fetch … code_memory program_counter) in
130    let instr ≝ \fst (\fst (fetch … code_memory program_counter)) in
131    let newpc ≝ \snd (\fst (fetch … code_memory program_counter)) in
132    match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
133    [ None ⇒
134        let classify ≝ ASM_classify0 instr in
135        match classify return λx. ∀classify_refl: x = classify. nat with
136        [ cl_jump ⇒ λclassify_refl. ticks
137        | cl_call ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
138        | cl_return ⇒ λclassify_refl. ticks
139        | cl_other ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
140        ] (refl … classify)
141    | Some _ ⇒ ticks
142    ]
143  ].
144  [1:
145    cases(lt_to_not_zero … absurd)
146  |2,4:
147    cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc)
148    [1,3:
149      @fetch_pc_lt_new_pc (* XXX: now @sig2 from fetch's russell type *)
150      lapply(transitive_lt
151        (nat_of_bitvector 16 pc)
152        initial_program_size
153        (size Byte 16 mem) ? ?)
154      [1,2,4,5:
155        assumption
156      |3,6:
157        #assm assumption
158      ]
159    |2,4:
160      change with (
161        S (nat_of_bitvector … 16 pc) ≤ nat_of_bitvector … newpc
162      ) in ⊢ (% → ?);
163      #first_le_assm
164      normalize in recursive_case;
165      change with (
166        S (initial_program_size - nat_of_bitvector … newpc) ≤ program_size)
167      lapply (le_S_S_to_le … recursive_case)
168      change with (
169        initial_program_size - (nat_of_bitvector … pc) ≤ program_size
170      ) in ⊢ (% → ?);
171      #second_le_assm
172      @(transitive_le
173        (S (initial_program_size-nat_of_bitvector 16 newpc))
174        (initial_program_size-nat_of_bitvector_aux 16 O pc)
175        program_size ? second_le_assm)
176      change with (
177        initial_program_size - nat_of_bitvector … pc
178      ) in ⊢ (??%);
179      lapply (minus_Sn_m (nat_of_bitvector … newpc) initial_program_size)
180      #assm <assm in ⊢ (?%?);
181      [1,3:
182        @minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o
183        @monotonic_le_minus_r
184        assumption
185      |2,4:
186        @(strengthened_invariant mem initial_program_size newpc pc size_invariant final_instr_invariant)
187        [1,3:
188          %
189        |2,4:
190          assumption
191        ]
192      ]
193    ]
194  |3,5:
195  ]
196qed.
197
198let rec traverse_code_internal
199  (program: list Byte) (mem: BitVectorTrie Byte 16)
200    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
201      on program: identifier_map CostTag nat ≝
202 let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
203 match program with
204 [ nil ⇒ empty_map …
205 | cons hd tl ⇒
206   match lookup_opt … pc cost_labels with
207   [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
208   | Some lbl ⇒
209     let cost ≝ block_cost mem cost_labels pc program_size in
210     let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
211       add … cost_mapping lbl cost ]].
212
213definition traverse_code ≝
214  λprogram: list Byte.
215  λmem: BitVectorTrie Byte 16.
216  λcost_labels.
217  λprogram_size: nat.
218    traverse_code_internal program mem cost_labels (zero …) program_size.
219
220definition compute_costs ≝
221  λprogram: list Byte.
222  λcost_labels: BitVectorTrie costlabel 16.
223  λhas_main: bool.
224  let program_size ≝ |program| + 1 in
225  let memory ≝ load_code_memory program in
226   traverse_code program memory cost_labels program_size.
Note: See TracBrowser for help on using the repository browser.