source: src/ASM/ASMCosts.ma @ 1606

Last change on this file since 1606 was 1606, checked in by sacerdot, 8 years ago

Porting to last library of Matita.

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