- Timestamp:
- Nov 24, 2011, 7:22:13 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1557 r1560 3 3 include "ASM/Fetch.ma". 4 4 include "ASM/Interpret.ma". 5 include "common/StructuredTraces.ma". 5 6 6 inductive instruction_nature: Type[0] ≝ 7 | goto: Word → instruction_nature 8 | branch: Word → instruction_nature 9 | direct_fun_call: Word → instruction_nature 10 | ret: instruction_nature 11 | other: instruction_nature. 7 definition current_instruction0 ≝ 8 λmem,pc. \fst (\fst (fetch … mem pc)). 12 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 *) 13 80 definition addr16_of_addr11: Word → Word11 → Word ≝ 14 81 λpc: Word. … … 25 92 qed. 26 93 27 definition instruction_nature_next_pc_length ≝ 28 λvariety: instruction_nature. 29 match variety with 30 [ ret ⇒ 0 31 | branch _ ⇒ 2 32 | goto _ ⇒ 1 33 | direct_fun_call _ ⇒ 1 34 | other ⇒ 1 35 ]. 36 37 definition instruction_info: 38 BitVectorTrie Byte 16 → Word → Σprod: (instruction_nature × Word × (list Word) × nat). |\snd (\fst prod)| = instruction_nature_next_pc_length (\fst (\fst (\fst prod))) ≝ 39 λmem. 40 λpc. 41 let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in 42 let nature_next_pcs_proof ≝ 43 match inst return λx. Σpair: (instruction_nature × (list Word)). |(\snd pair)| = instruction_nature_next_pc_length (\fst pair) with 44 [ RealInstruction ri ⇒ 45 match ri with 46 [ RET ⇒ dp … 〈ret, [ ]〉 ? 47 | RETI ⇒ dp … 〈ret, [ ]〉 ? 48 | JC addr ⇒ 49 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 50 [ RELATIVE addr ⇒ λ_. 51 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 52 dp … 〈branch addr, [ next_pc; addr ]〉 ? 53 | _ ⇒ λp. match p in False with [ ] 54 ] (subaddressing_modein … addr) 55 | JNC addr ⇒ 56 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 57 [ RELATIVE addr ⇒ λ_. 58 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 59 dp … 〈branch addr, [ next_pc; addr ]〉 ? 60 | _ ⇒ λp. match p in False with [ ] 61 ] (subaddressing_modein … addr) 62 | JZ addr ⇒ 63 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 64 [ RELATIVE addr ⇒ λ_. 65 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 66 dp … 〈branch addr, [ next_pc; addr ]〉 ? 67 | _ ⇒ λp. match p in False with [ ] 68 ] (subaddressing_modein … addr) 69 | JNZ addr ⇒ 70 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 71 [ RELATIVE addr ⇒ λ_. 72 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 73 dp … 〈branch addr, [ next_pc; addr ]〉 ? 74 | _ ⇒ λp. match p in False with [ ] 75 ] (subaddressing_modein … addr) 76 | JB addr1 addr2 ⇒ 77 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 78 [ RELATIVE addr ⇒ λ_. 79 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 80 dp … 〈branch addr, [ next_pc; addr ]〉 ? 81 | _ ⇒ λp. match p in False with [ ] 82 ] (subaddressing_modein … addr2) 83 | JNB addr1 addr2 ⇒ 84 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 85 [ RELATIVE addr ⇒ λ_. 86 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 87 dp … 〈branch addr, [ next_pc; addr ]〉 ? 88 | _ ⇒ λp. match p in False with [ ] 89 ] (subaddressing_modein … addr2) 90 | JBC addr1 addr2 ⇒ 91 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 92 [ RELATIVE addr ⇒ λ_. 93 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 94 dp … 〈branch addr, [ next_pc; addr ]〉 ? 95 | _ ⇒ λp. match p in False with [ ] 96 ] (subaddressing_modein … addr2) 97 | DJNZ addr1 addr2 ⇒ 98 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 99 [ RELATIVE addr ⇒ λ_. 100 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 101 dp … 〈branch addr, [ next_pc; addr ]〉 ? 102 | _ ⇒ λp. match p in False with [ ] 103 ] (subaddressing_modein … addr2) 104 | CJNE addr1 addr2 ⇒ 105 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 106 [ RELATIVE addr ⇒ λ_. 107 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 108 dp … 〈branch addr, [ next_pc; addr ]〉 ? 109 | _ ⇒ λp. match p in False with [ ] 110 ] (subaddressing_modein … addr2) 111 | _ ⇒ dp … 〈other, [ next_pc ]〉 ? 112 ] 113 | ACALL addr ⇒ 114 match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with 115 [ ADDR11 addr ⇒ λ_. 116 let addr ≝ addr16_of_addr11 pc addr in 117 dp … 〈direct_fun_call addr, [ next_pc ]〉 ? 118 | _ ⇒ λp. match p in False with [ ] 119 ] (subaddressing_modein … addr) 120 | LCALL addr ⇒ 121 match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with 122 [ ADDR16 addr ⇒ λ_. dp … 〈direct_fun_call addr, [ next_pc ]〉 ? 123 | _ ⇒ λp. match p in False with [ ] 124 ] (subaddressing_modein … addr) 125 | AJMP addr ⇒ 126 match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with 127 [ ADDR11 addr ⇒ λ_. 128 let addr ≝ addr16_of_addr11 pc addr in 129 dp … 〈goto addr, [ addr ]〉 ? 130 | _ ⇒ λp. match p in False with [ ] 131 ] (subaddressing_modein … addr) 132 | LJMP addr ⇒ 133 match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with 134 [ ADDR16 addr ⇒ λ_. dp … 〈goto addr, [ addr ]〉 ? 135 | _ ⇒ λp. match p in False with [ ] 136 ] (subaddressing_modein … addr) 137 | SJMP addr ⇒ 138 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 139 [ RELATIVE addr ⇒ λ_. 140 let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in 141 dp … 〈goto addr, [ addr ]〉 ? 142 | _ ⇒ λp. match p in False with [ ] 143 ] (subaddressing_modein … addr) 144 | JMP addr ⇒ dp … 〈other, [ next_pc ]〉 ? 145 | MOVC acc_a addr ⇒ dp … 〈other, [ next_pc ]〉 ? 146 ] 147 in 148 match nature_next_pcs_proof with 149 [ dp nature_next_pcs their_proof ⇒ 150 let nature ≝ \fst nature_next_pcs in 151 let next_pcs ≝ \snd nature_next_pcs in 152 dp … 〈〈〈nature, next_pc〉, next_pcs〉, inst_cost〉 ? 153 ]. 154 [1: >their_proof % 155 |*: % 156 ] 157 qed. 158 159 let rec block_cost' 94 let rec block_cost 160 95 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 161 (program_counter: Word) (program_size: nat) (cost_so_far: nat) 162 on program_size ≝ 96 (pc: Word) (program_size: nat) on program_size : nat ≝ 163 97 match program_size with 164 98 [ O ⇒ 0 165 | S program_size ⇒ 166 let sigma ≝ instruction_info mem program_counter in 167 match sigma with 168 [ dp variety_costs their_proof ⇒ 169 let variety ≝ \fst (\fst (\fst variety_costs)) in 170 let next_pc ≝ \snd (\fst (\fst variety_costs)) in 171 let next_pcs ≝ \snd (\fst variety_costs) in 172 let inst_cost ≝ \snd variety_costs in 173 match variety return λx. |next_pcs| = instruction_nature_next_pc_length x → nat with 174 [ other ⇒ λproof. 175 match next_pcs return λx. |x| = 1 → nat with 176 [ nil ⇒ λabsurd. ⊥ 177 | cons hd tl ⇒ λproof. 178 match lookup_opt … hd cost_labels with 179 [ None ⇒ block_cost' mem cost_labels hd program_size (cost_so_far + inst_cost) 180 | Some _ ⇒ inst_cost + cost_so_far 181 ] 182 ] proof 183 | _ ⇒ λ_. inst_cost + cost_so_far 184 ] their_proof 185 ] 186 ]. 187 normalize in absurd; 188 destruct(absurd) 189 qed. 190 191 definition block_cost ≝ 192 λmem: BitVectorTrie Byte 16. 193 λcost_labels: BitVectorTrie costlabel 16. 194 λprogram_counter: Word. 195 λprogram_size: nat. 196 block_cost' mem cost_labels program_counter program_size 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 ]]. 197 110 198 111 let rec traverse_code_internal … … 200 113 (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat) 201 114 on program: identifier_map CostTag nat ≝ 202 match instruction_info mem pc with 203 [ dp info proof ⇒ 204 let newpc ≝ \snd (\fst (\fst info)) in 205 match program with 206 [ nil ⇒ empty_map … 207 | cons hd tl ⇒ 208 match lookup_opt … pc cost_labels with 209 [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size 210 | Some lbl ⇒ 211 let cost ≝ block_cost mem cost_labels pc program_size in 212 let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in 213 add … cost_mapping lbl cost 214 ] 215 ] 216 ]. 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 ]]. 217 125 218 126 definition traverse_code ≝ … … 223 131 traverse_code_internal program mem cost_labels (zero …) program_size. 224 132 225 let rec first_cost_label_internal226 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)227 (program_size: nat) (oldpc: Word)228 on program_size: (costlabel × nat) ≝229 match program_size with230 [ O ⇒ ⊥ (* XXX: ummm ... ? *)231 | S program_size ⇒232 match lookup_opt … oldpc cost_labels with233 [ None ⇒234 match instruction_info mem oldpc with235 [ dp info proof ⇒236 let nature ≝ \fst (\fst (\fst info)) in237 let pc ≝ \snd (\fst (\fst info)) in238 let inst_cost ≝ \snd info in239 match nature with240 [ direct_fun_call addr ⇒241 let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in242 〈lbl, inst_cost + cost〉243 | other ⇒244 let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in245 〈lbl, inst_cost + cost〉246 | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)247 ]248 ]249 | Some cost ⇒ 〈cost, 0〉250 ]251 ].252 cases daemon253 qed.254 255 definition first_cost_label ≝256 λmem: BitVectorTrie Byte 16.257 λcost_labels: BitVectorTrie costlabel 16.258 λprogram_size: nat.259 first_cost_label_internal mem cost_labels program_size (zero …).260 261 definition initialize_costs ≝262 λmem: BitVectorTrie Byte 16.263 λcost_labels: BitVectorTrie costlabel 16.264 λcost_mapping: identifier_map CostTag nat.265 λprogram_size: nat.266 let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in267 let old_cost ≝268 match lookup ?? cost_mapping lbl with269 [ None ⇒ 0270 | Some cost ⇒ cost271 ]272 in273 let new_cost ≝ old_cost + cost in274 add … cost_mapping lbl new_cost.275 276 133 definition compute_costs ≝ 277 134 λprogram: list Byte. … … 280 137 let program_size ≝ |program| in 281 138 let memory ≝ load_code_memory program in 282 let costs_mapping ≝ traverse_code program memory cost_labels program_size in 283 match has_main with 284 [ true ⇒ initialize_costs memory cost_labels costs_mapping program_size 285 | false ⇒ costs_mapping 286 ]. 139 traverse_code program memory cost_labels program_size.
Note: See TracChangeset
for help on using the changeset viewer.