Changeset 1948 for src/ASM/Assembly.ma
 Timestamp:
 May 15, 2012, 11:13:14 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1946 r1948 5 5 include alias "basics/logic.ma". 6 6 include alias "arithmetics/nat.ma". 7 include "utilities/extralib.ma". 7 include "utilities/extralib.ma". 8 8 9 9 (**************************************** START OF POLICY ABSTRACTION ********************) … … 419 419 420 420 definition expand_relative_jump_internal: 421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word × bool.421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word. 422 422 Identifier → Word → ([[relative]] → preinstruction [[relative]]) → 423 423 list instruction 424 424 ≝ 425 425 λlookup_labels.λsigma.λlbl.λppc,i. 426 let lookup_address ≝ \fst (sigma (lookup_labels lbl)) in427 let pc ≝ \fst (sigma ppc)in426 let lookup_address ≝ sigma (lookup_labels lbl) in 427 let pc ≝ sigma ppc in 428 428 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 429 429 let 〈upper, lower〉 ≝ split ? 8 8 result in … … 436 436 LJMP (ADDR16 lookup_address) 437 437 ]. 438 @ I438 % 439 439 qed. 440 440 … … 471 471 preinstruction Identifier → list instruction ≝ 472 472 λlookup_labels: Identifier → Word. 473 λsigma:Word → Word × bool.473 λsigma:Word → Word. 474 474 λppc: Word. 475 475 (*λjmp_len: jump_length.*) … … 517 517 518 518 definition expand_pseudo_instruction: 519 ∀lookup_labels.∀sigma.Word → ? → pseudo_instruction → list instruction ≝ 520 λlookup_labels:Identifier → Word. 521 λsigma:Word → Word × bool. 519 ∀lookup_labels. 520 ∀sigma: Word → Word. 521 ∀policy: Word → bool. 522 Word → ? → pseudo_instruction → list instruction ≝ 523 λlookup_labels: Identifier → Word. 524 λsigma: Word → Word. 525 λpolicy: Word → bool. 522 526 λppc. 523 527 λlookup_datalabels:Identifier → Word. … … 527 531  Comment comment ⇒ [ ] 528 532  Call call ⇒ 529 let 〈addr_5, resta〉 ≝ split ? 5 11 (\fst (sigma (lookup_labels call))) in 530 let 〈pc, do_a_long〉 ≝ sigma ppc in 533 let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in 534 let pc ≝ sigma ppc in 535 let do_a_long ≝ policy ppc in 531 536 let 〈pc_5, restp〉 ≝ split ? 5 11 pc in 532 537 if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then … … 534 539 [ ACALL address ] 535 540 else 536 let address ≝ ADDR16 ( \fst (sigma (lookup_labels call))) in541 let address ≝ ADDR16 (sigma (lookup_labels call)) in 537 542 [ LCALL address ] 538 543  Mov d trgt ⇒ … … 541 546  Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr 542 547  Jmp jmp ⇒ 543 let 〈pc, do_a_long〉 ≝ sigma ppc in 544 let lookup_address ≝ \fst (sigma (lookup_labels jmp)) in 548 let pc ≝ sigma ppc in 549 let do_a_long ≝ policy ppc in 550 let lookup_address ≝ sigma (lookup_labels jmp) in 545 551 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 546 552 let 〈upper, lower〉 ≝ split ? 8 8 result in … … 558 564 [ LJMP address ] 559 565 ]. 560 @ I566 % 561 567 qed. 562 568 … … 607 613 definition assembly_1_pseudoinstruction ≝ 608 614 λlookup_labels. 609 λsigma. 615 λsigma: Word → Word. 616 λpolicy: Word → bool. 610 617 λppc: Word. 611 618 λlookup_datalabels. 612 619 λi. 613 let pseudos ≝ expand_pseudo_instruction lookup_labels sigma p pc lookup_datalabels i in620 let pseudos ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels i in 614 621 let mapped ≝ map ? ? assembly1 pseudos in 615 622 let flattened ≝ flatten ? mapped in … … 618 625 619 626 definition instruction_size ≝ 620 λlookup_labels.λsigma.λppc.λi. 621 \fst (assembly_1_pseudoinstruction lookup_labels sigma ppc (λx.zero …) i). 627 λlookup_labels. 628 λsigma: Word → Word. 629 λpolicy: Word → bool. 630 λppc. 631 λi. 632 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i). 622 633 623 634 (* Jaap: never used … … 1136 1147 1137 1148 (* The function that creates the labeltoaddress map *) 1138 definition create_label_cost_map : ∀program:list labelled_instruction.1149 definition create_label_cost_map0: ∀program:list labelled_instruction. 1139 1150 (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *) 1140 1151 let 〈labels,costs〉 ≝ labels_costs in 1141 (*∀i:ℕ.lt i (program) → *)1142 1152 ∀l.occurs_exactly_once ?? l program → 1143 (*is_label (nth i ? program 〈None ?, Comment [ ]〉) l →1144 lookup ?? labels l = Some ? i*)1145 1153 bitvector_of_nat ? (lookup_def ?? labels l 0) = 1146 1154 address_of_word_labels_code_mem program l … … 1153 1161 ∀l.occurs_exactly_once ?? l prefix → 1154 1162 bitvector_of_nat ? (lookup_def ?? labels l 0) = 1155 address_of_word_labels_code_mem prefix l 1156 (* 1157 ∀i:ℕ.lt i (prefix) → 1158 ∀l.occurs_exactly_once ?? l prefix → 1159 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 1160 lookup … labels l = Some ? i *) 1161 ) 1163 address_of_word_labels_code_mem prefix l) 1162 1164 program 1163 1165 (λprefix.λx.λtl.λprf.λlabels_costs_ppc. … … 1197 1199 ] 1198 1200 ] 1199 (* 1200 [ @Hocc1201  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /1202 ]1203 [1,2: normalize nodelta1204 (* #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi;1205 [3: #Hi *) #lbl #Hocc (*#Hlbl*) lapply (occurs_exactly_once_Some_stronger ?????? Hocc) Hocc1206 @eq_identifier_elim1207 [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl1208 @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/1209  #Heq #Hocc normalize in Hocc; >lookup_add_miss1210 [ @(IH2 … i (le_S_S_to_le … Hi))1211 [ @Hocc1212  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /1213 ]1214  @sym_neq @Heq1215 ]1216 ]1217 4: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second1218 [ <minus_n_n #Hl normalize in Hl; >Hl >IH1 @lookup_add_hit1219  @le_n1220 ]1221 1: #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl1222 @(IH2 … i (le_S_S_to_le … Hi))1223 [ @Hocc1224  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /1225 ]1226 2: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second1227 [ <minus_n_n #Hl cases Hl1228  @le_n1229 ]1230 ]1231 ] *)1232 1201  @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try % 1233 1202 #l #abs cases (abs) … … 1237 1206 qed. 1238 1207 1208 (* The function that creates the labeltoaddress map *) 1209 definition create_label_cost_map: ∀program:list labelled_instruction. 1210 label_map × (BitVectorTrie costlabel 16) ≝ 1211 λprogram. 1212 pi1 … (create_label_cost_map0 program). 1213 1239 1214 theorem create_label_cost_map_ok: 1240 1215 ∀pseudo_program: pseudo_assembly_program. … … 1242 1217 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 1243 1218 bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id. 1244 #p @pi21219 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2 1245 1220 qed. 1246 1221 1247 1222 definition assembly: 1248 ∀p:pseudo_assembly_program.∀sigma:Word → Word × bool.list Byte × (BitVectorTrie costlabel 16) ≝ 1249 λp.let 〈preamble, instr_list〉 ≝ p in 1250 λsigma. 1251 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1252 let datalabels ≝ construct_datalabels preamble in 1253 let lookup_labels ≝ λx. \fst (sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0))) in 1254 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1255 let result ≝ 1223 ∀p: pseudo_assembly_program. 1224 ∀sigma: Word → Word. 1225 ∀policy: Word → bool. 1226 list Byte × (BitVectorTrie costlabel 16) ≝ 1227 λp. 1228 let 〈preamble, instr_list〉 ≝ p in 1229 λsigma. 1230 λpolicy. 1231 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1232 let datalabels ≝ construct_datalabels preamble in 1233 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in 1234 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1235 let result ≝ 1256 1236 foldl_strong 1257 1237 (option Identifier × pseudo_instruction) … … 1262 1242 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in 1263 1243 let 〈len,assembledi〉 ≝ 1264 assembly_1_pseudoinstruction lookup_labels sigma p pc' lookup_datalabels pi in1244 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 1265 1245 True) 1266 1246 instr_list … … 1268 1248 let 〈pc, ppc_code〉 ≝ pc_ppc_code in 1269 1249 let 〈ppc, code〉 ≝ ppc_code in 1270 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma p pc lookup_datalabels (\snd hd) in1250 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in 1271 1251 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 1272 1252 let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in … … 1275 1255 in 1276 1256 〈\snd (\snd result), 1277 fold … (λppc.λcost.λpc_to_costs. insert … (\fst (sigma ppc)) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 1278 @pair_elim normalize nodelta #x #y #z @pair_elim normalize nodelta #w1 #w2 #w3 #w4 @pair_elim // 1279 qed. 1280 1281 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 1282 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉). 1257 fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 1258 @pair_elim normalize nodelta #x #y #z 1259 @pair_elim normalize nodelta #w1 #w2 #w3 #w4 1260 @pair_elim // 1261 qed. 1262 1263 definition assembly_unlabelled_program: 1264 assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 1265 λp. 1266 Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracChangeset
for help on using the changeset viewer.