source: src/ASM/ASMCosts.ma @ 1560

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

Complete re-implementation that:

1) assumes no code before the first cost label of main

Note: the preamble of the program is no longer paid by anyone;
but before it was paid every time main was recursively called

2) assumes a cost label as the target of every call/jmp

File size: 4.3 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'. 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 *)
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
94let 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
111let 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
126definition 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
133definition 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.
Note: See TracBrowser for help on using the repository browser.