Changeset 1486 for src/ASM/ASMCosts.ma
- Timestamp:
- Nov 3, 2011, 2:36:37 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1474 r1486 1 include "ASM/ASM.ma". 2 include "ASM/Arithmetic.ma". 3 include "ASM/Fetch.ma". 4 include "ASM/Interpret.ma". 5 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. 12 13 definition addr16_of_addr11: Word → Word11 → Word ≝ 14 λpc: Word. 15 λa: Word11. 16 let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in 17 let 〈n1, n2〉 ≝ split … 4 4 pc_upper in 18 let 〈b123, b〉 ≝ split … 3 8 a in 19 let b1 ≝ get_index_v … b123 0 ? in 20 let b2 ≝ get_index_v … b123 1 ? in 21 let b3 ≝ get_index_v … b123 2 ? in 22 let p5 ≝ get_index_v … n2 0 ? in 23 (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b. 24 // 25 qed. 26 27 definition instruction_info: 28 BitVectorTrie Byte 16 → Word → ? ≝ 29 λmem. 30 λpc. 31 let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in 32 let 〈nature, next_pcs〉 ≝ 33 match inst with 34 [ RealInstruction ri ⇒ 35 match ri with 36 [ RET ⇒ 〈ret, [ ]〉 37 | RETI ⇒ 〈ret, [ ]〉 38 | JC addr ⇒ 39 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 40 [ RELATIVE addr ⇒ λ_. 41 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 42 〈branch addr, [ next_pc; addr ]〉 43 | _ ⇒ λp. match p in False with [ ] 44 ] (subaddressing_modein … addr) 45 | JNC addr ⇒ 46 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 47 [ RELATIVE addr ⇒ λ_. 48 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 49 〈branch addr, [ next_pc; addr ]〉 50 | _ ⇒ λp. match p in False with [ ] 51 ] (subaddressing_modein … addr) 52 | JZ addr ⇒ 53 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 54 [ RELATIVE addr ⇒ λ_. 55 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 56 〈branch addr, [ next_pc; addr ]〉 57 | _ ⇒ λp. match p in False with [ ] 58 ] (subaddressing_modein … addr) 59 | JNZ addr ⇒ 60 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 61 [ RELATIVE addr ⇒ λ_. 62 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 63 〈branch addr, [ next_pc; addr ]〉 64 | _ ⇒ λp. match p in False with [ ] 65 ] (subaddressing_modein … addr) 66 | JB addr1 addr2 ⇒ 67 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 68 [ RELATIVE addr ⇒ λ_. 69 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 70 〈branch addr, [ next_pc; addr ]〉 71 | _ ⇒ λp. match p in False with [ ] 72 ] (subaddressing_modein … addr2) 73 | JNB addr1 addr2 ⇒ 74 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 75 [ RELATIVE addr ⇒ λ_. 76 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 77 〈branch addr, [ next_pc; addr ]〉 78 | _ ⇒ λp. match p in False with [ ] 79 ] (subaddressing_modein … addr2) 80 | JBC addr1 addr2 ⇒ 81 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 82 [ RELATIVE addr ⇒ λ_. 83 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 84 〈branch addr, [ next_pc; addr ]〉 85 | _ ⇒ λp. match p in False with [ ] 86 ] (subaddressing_modein … addr2) 87 | DJNZ addr1 addr2 ⇒ 88 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 89 [ RELATIVE addr ⇒ λ_. 90 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 91 〈branch addr, [ next_pc; addr ]〉 92 | _ ⇒ λp. match p in False with [ ] 93 ] (subaddressing_modein … addr2) 94 | CJNE addr1 addr2 ⇒ 95 match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 96 [ RELATIVE addr ⇒ λ_. 97 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 98 〈branch addr, [ next_pc; addr ]〉 99 | _ ⇒ λp. match p in False with [ ] 100 ] (subaddressing_modein … addr2) 101 | _ ⇒ 〈other, [ next_pc ]〉 102 ] 103 | ACALL addr ⇒ 104 match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with 105 [ ADDR11 addr ⇒ λ_. 106 let addr ≝ addr16_of_addr11 pc addr in 107 〈direct_fun_call addr, [ next_pc ]〉 108 | _ ⇒ λp. match p in False with [ ] 109 ] (subaddressing_modein … addr) 110 | LCALL addr ⇒ 111 match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with 112 [ ADDR16 addr ⇒ λ_. 〈direct_fun_call addr, [ next_pc ]〉 113 | _ ⇒ λp. match p in False with [ ] 114 ] (subaddressing_modein … addr) 115 | AJMP addr ⇒ 116 match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with 117 [ ADDR11 addr ⇒ λ_. 118 let addr ≝ addr16_of_addr11 pc addr in 119 〈goto addr, [ addr ]〉 120 | _ ⇒ λp. match p in False with [ ] 121 ] (subaddressing_modein … addr) 122 | LJMP addr ⇒ 123 match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with 124 [ ADDR16 addr ⇒ λ_. 〈goto addr, [ addr ]〉 125 | _ ⇒ λp. match p in False with [ ] 126 ] (subaddressing_modein … addr) 127 | SJMP addr ⇒ 128 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 129 [ RELATIVE addr ⇒ λ_. 130 let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in 131 〈goto addr, [ addr ]〉 132 | _ ⇒ λp. match p in False with [ ] 133 ] (subaddressing_modein … addr) 134 | JMP addr ⇒ 〈other, [ next_pc ]〉 135 | MOVC acc_a addr ⇒ 〈other, [ next_pc ]〉 136 ] 137 in 138 〈nature, next_pc, next_pcs, inst_cost〉. 139 140 let rec compare 141 (a: Type[0]) (the_list: list (a × nat)) 142 on the_list: nat ≝ 143 match the_list with 144 [ nil ⇒ ⊥ (* XXX: was assert false *) 145 | cons hd tl ⇒ 146 match tl with 147 [ nil ⇒ 148 let 〈pc, cost〉 ≝ hd in 149 cost 150 | cons hd' tl' ⇒ 151 let 〈pc1, cost1〉 ≝ hd in 152 let 〈pc2, cost2〉 ≝ hd' in 153 match eq_nat cost1 cost2 with 154 [ true ⇒ max cost1 (compare … tl) 155 | false ⇒ compare … tl' 156 ] 157 ] 158 ]. 159 cases daemon 160 qed. 161 162 let rec block_cost 163 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16) 164 (the_list: list Word) (program_size: nat) 165 on program_size: nat ≝ 166 match program_size with 167 [ O ⇒ 0 (* XXX: empty program *) 168 | S program_size ⇒ 169 match the_list with 170 [ nil ⇒ 0 (* XXX: should be empty program *) 171 | cons pc tl ⇒ 172 match tl with 173 [ nil ⇒ 174 match lookup_opt … pc cost_labels with 175 [ None ⇒ 176 let 〈ignore, ignore, next_pcs, cost〉 ≝ instruction_info mem pc in 177 let tail ≝ block_cost mem cost_labels next_pcs program_size in 178 cost + tail 179 | Some _ ⇒ O 180 ] 181 | _ ⇒ compare ? (map … (λpc. 〈pc, block_cost mem cost_labels [pc] program_size〉) the_list) 182 ] 183 ] 184 ]. 185 186 let rec traverse_code_internal 187 (program: list Byte) (mem: BitVectorTrie Byte 16) 188 (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat) 189 on program: BitVectorTrie nat 8 ≝ 190 let 〈ignore, newpc, ignore, ignore〉 ≝ instruction_info mem pc in 191 match program with 192 [ nil ⇒ Stub … 193 | cons hd tl ⇒ 194 match lookup_opt … pc cost_labels with 195 [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size 196 | Some lbl ⇒ 197 let cost ≝ block_cost mem cost_labels [ pc ] program_size in 198 let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in 199 insert … lbl cost cost_mapping 200 ] 201 ]. 202 203 definition traverse_code ≝ 204 λprogram: list Byte. 205 λmem: BitVectorTrie Byte 16. 206 λcost_labels. 207 λprogram_size: nat. 208 traverse_code_internal program mem cost_labels (zero …) program_size. 209 210 let rec first_cost_label_internal 211 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16) 212 (program_size: nat) (oldpc: Word) 213 on program_size: (Byte × nat) ≝ 214 match program_size with 215 [ O ⇒ ⊥ (* XXX: ummm ... ? *) 216 | S program_size ⇒ 217 match lookup_opt … oldpc cost_labels with 218 [ None ⇒ 219 let 〈nature, pc, ignore, inst_cost〉 ≝ instruction_info mem oldpc in 220 match nature with 221 [ direct_fun_call addr ⇒ 222 let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in 223 〈lbl, inst_cost + cost〉 224 | other ⇒ 225 let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in 226 〈lbl, inst_cost + cost〉 227 | _ ⇒ ⊥ (* XXX: was assert false in o'caml *) 228 ] 229 | Some cost ⇒ 〈cost, 0〉 230 ] 231 ]. 232 cases daemon 233 qed. 234 235 definition first_cost_label ≝ 236 λmem: BitVectorTrie Byte 16. 237 λcost_labels: BitVectorTrie Byte 16. 238 λprogram_size: nat. 239 first_cost_label_internal mem cost_labels program_size (zero …). 240 241 definition initialize_costs ≝ 242 λmem: BitVectorTrie Byte 16. 243 λcost_labels: BitVectorTrie Byte 16. 244 λcost_mapping: BitVectorTrie nat 8. 245 λprogram_size: nat. 246 let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in 247 let old_cost ≝ 248 match lookup_opt … lbl cost_mapping with 249 [ None ⇒ 0 250 | Some cost ⇒ cost 251 ] 252 in 253 let new_cost ≝ old_cost + cost in 254 insert … lbl new_cost cost_mapping. 255 256 definition compute_costs ≝ 257 λprogram: list Byte. 258 λcost_labels: BitVectorTrie Byte 16. 259 λhas_main: bool. 260 let program_size ≝ |program| in 261 let memory ≝ load_code_memory program in 262 let costs_mapping ≝ traverse_code program memory cost_labels program_size in 263 match has_main with 264 [ true ⇒ 265 initialize_costs memory cost_labels costs_mapping program_size 266 | false ⇒ costs_mapping 267 ].
Note: See TracChangeset
for help on using the changeset viewer.