Changeset 1934 for src/ASM/Assembly.ma
 Timestamp:
 May 10, 2012, 3:37:07 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1925 r1934 419 419 420 420 definition expand_relative_jump_internal: 421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word .421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word × bool. 422 422 Identifier → Word → ([[relative]] → preinstruction [[relative]]) → 423 423 list instruction 424 424 ≝ 425 λlookup_labels.λsigma.λlbl.λpc,i. 426 let lookup_address ≝ sigma (lookup_labels lbl) in 425 λlookup_labels.λsigma.λlbl.λppc,i. 426 let lookup_address ≝ \fst (sigma (lookup_labels lbl)) in 427 let pc ≝ \fst (sigma ppc) in 427 428 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 428 429 let 〈upper, lower〉 ≝ split ? 8 8 result in … … 470 471 preinstruction Identifier → list instruction ≝ 471 472 λlookup_labels: Identifier → Word. 472 λsigma:Word → Word .473 λp c: Word.473 λsigma:Word → Word × bool. 474 λppc: Word. 474 475 (*λjmp_len: jump_length.*) 475 476 λi: preinstruction Identifier. 476 let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in477 (*let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in*) 477 478 match i with 478 [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (JC ?)479  JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (JNC ?)480  JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (JB ? baddr)481  JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (JZ ?)482  JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (JNZ ?)483  JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (JBC ? baddr)484  JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (JNB ? baddr)485  CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (CJNE ? addr)486  DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp p c (DJNZ ? addr)479 [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JC ?) 480  JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNC ?) 481  JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JB ? baddr) 482  JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JZ ?) 483  JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNZ ?) 484  JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JBC ? baddr) 485  JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (JNB ? baddr) 486  CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (CJNE ? addr) 487  DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp ppc (DJNZ ? addr) 487 488  ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ] 488 489  ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ] … … 518 519 ∀lookup_labels.∀sigma.Word → ? → pseudo_instruction → list instruction ≝ 519 520 λlookup_labels:Identifier → Word. 520 λsigma:Word → Word .521 λp c.521 λsigma:Word → Word × bool. 522 λppc. 522 523 λlookup_datalabels:Identifier → Word. 523 524 λi. … … 526 527  Comment comment ⇒ [ ] 527 528  Call call ⇒ 528 let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in 529 let 〈fst_5, rest〉 ≝ split ? 5 11 pc in 530 if eq_bv ? ignore fst_5 then 531 let address ≝ ADDR11 address in 529 let 〈addr_5, resta〉 ≝ split ? 5 11 (\fst (sigma (lookup_labels call))) in 530 let 〈pc, do_a_long〉 ≝ sigma ppc in 531 let 〈pc_5, restp〉 ≝ split ? 5 11 pc in 532 if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then 533 let address ≝ ADDR11 resta in 532 534 [ ACALL address ] 533 535 else 534 let address ≝ ADDR16 ( lookup_labels call) in536 let address ≝ ADDR16 (\fst (sigma (lookup_labels call))) in 535 537 [ LCALL address ] 536 538  Mov d trgt ⇒ 537 539 let address ≝ DATA16 (lookup_datalabels trgt) in 538 540 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))] 539  Instruction instr ⇒ expand_relative_jump lookup_labels sigma p c instr541  Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr 540 542  Jmp jmp ⇒ 541 let 〈result, flags〉 ≝ sub_16_with_carry pc (lookup_labels jmp) false in 543 let 〈pc, do_a_long〉 ≝ sigma ppc in 544 let lookup_address ≝ \fst (sigma (lookup_labels jmp)) in 545 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 542 546 let 〈upper, lower〉 ≝ split ? 8 8 result in 543 if eq_bv ? upper (zero 8) then547 if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then 544 548 let address ≝ RELATIVE lower in 545 549 [ SJMP address ] … … 547 551 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in 548 552 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 549 if eq_bv ? fst_5_addr fst_5_pc then553 if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then 550 554 let address ≝ ADDR11 rest_addr in 551 555 [ AJMP address ] 552 556 else 553 let address ≝ ADDR16 (lookup_labels jmp)in557 let address ≝ ADDR16 lookup_address in 554 558 [ LJMP address ] 555 559 ]. … … 604 608 λlookup_labels. 605 609 λsigma. 606 (*λppc: Word.*) 607 λpc: Word. 610 λppc: Word. 608 611 λlookup_datalabels. 609 612 λi. 610 let pseudos ≝ expand_pseudo_instruction lookup_labels sigma p c lookup_datalabels i in613 let pseudos ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels i in 611 614 let mapped ≝ map ? ? assembly1 pseudos in 612 615 let flattened ≝ flatten ? mapped in … … 614 617 〈pc_len, flattened〉. 615 618 616 definition construct_costs ≝ 617 (*X?*)λlookup_labels. 618 λsigma. 619 λprogram_counter: nat. 620 λpseudo_program_counter: nat. 621 λcosts: BitVectorTrie costlabel 16. 622 λi. 623 match i with 624 [ Cost cost ⇒ 625 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 626 〈program_counter, (insert … program_counter_bv cost costs)〉 627  _ ⇒ 628 let pc_bv ≝ bitvector_of_nat ? program_counter in 629 (*let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in*) 630 let lookup_datalabels ≝ λx.zero ? in 631 let pc_delta_assembled ≝ 632 assembly_1_pseudoinstruction (*X?(λx.pc_bv)*) lookup_labels 633 sigma (*ppc_bv*) pc_bv lookup_datalabels i in 634 let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in 635 〈pc_delta + program_counter, costs〉 636 ]. 637 638 axiom nat_of_bitvector_bitvector_of_nat: 639 ∀n,v.n < 2^v → nat_of_bitvector v (bitvector_of_nat v n) = n. 640 641 axiom bitvector_of_nat_nat_of_bitvector: 642 ∀n,v.bitvector_of_nat n (nat_of_bitvector n v) = v. 643 644 lemma nth_cons: 645 ∀n,A,h,t,y. 646 nth (S n) A (h::t) y = nth n A t y. 647 #n #A #h #t #y /2 by refl/ 648 qed. 649 619 definition instruction_size ≝ 620 λlookup_labels.λsigma.λppc.λi. 621 \fst (assembly_1_pseudoinstruction lookup_labels sigma ppc (λx.zero …) i). 622 623 (* Jaap: never used 650 624 lemma fetch_pseudo_instruction_prefix: 651 625 ∀prefix.∀x.∀ppc.ppc < (prefix) → … … 665 639 ] 666 640 qed. 641 *) 667 642 668 643 (* … … 834 809 qed.*) 835 810 836 example half_add_SO:837 ∀pc.838 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).839 cases daemon.840 qed.841 842 811 (*CSC: Main axiom here, needs to be proved soon! *) 843 812 (*lemma snd_assembly_1_pseudoinstruction_ok: … … 881 850 qed.*) 882 851 852 (*CSC: FALSE!!!*) 883 853 axiom fetch_pseudo_instruction_split: 884 854 ∀instr_list,ppc. … … 1081 1051 *) 1082 1052 1083 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.1084 #A #a #b #EQ destruct //1085 qed.1086 1087 1053 (* 1088 1054 lemma tech_pc_sigma00_append_Some: … … 1121 1087 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. *) 1122 1088 1123 axiom eq_identifier_eq:1089 (*axiom eq_identifier_eq: 1124 1090 ∀tag: String. 1125 1091 ∀l. … … 1131 1097 ∀l, r: identifier tag. 1132 1098 eq_identifier tag l r = false → (l = r → False). 1133 1134 definition build_maps0: 1135 ∀pseudo_program:pseudo_assembly_program.∀sigma:Word → Word. 1136 Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)). 1137 let 〈labels, costs〉 ≝ res in 1138 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 1139 lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝ 1140 λpseudo_program. 1141 λsigma. 1142 let result ≝ 1143 foldl_strong 1144 (option Identifier × pseudo_instruction) 1145 (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))). 1146 let 〈labels,ppc_pc_costs〉 ≝ res in 1147 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in 1148 let 〈pc',costs〉 ≝ pc_costs in 1149 And ( And ( 1150 And (bitvector_of_nat ? pc' = sigma (bitvector_of_nat ? ppc')) (*∧*) 1151 (ppc' = length … pre)) (*∧ *) 1152 (*(tech_pc_sigma00 pseudo_program (pi1 … pol) pre = 〈ppc',pc'〉)*) True) (*∧*) 1153 (∀id. occurs_exactly_once ?? id pre → 1154 lookup_def … labels id (zero …) = sigma (address_of_word_labels_code_mem pre id))) 1155 (\snd pseudo_program) 1156 (λprefix,i,tl,prf,t. 1157 let 〈labels, ppc_pc_costs〉 ≝ t in 1158 let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in 1159 let 〈pc,costs〉 ≝ pc_costs in 1160 let 〈label, i'〉 ≝ i in 1161 let labels ≝ 1162 match label with 1163 [ None ⇒ labels 1164  Some label ⇒ 1165 let program_counter_bv ≝ bitvector_of_nat ? pc in 1166 add ? ? labels label program_counter_bv 1167 ] 1168 in 1169 let construct ≝ construct_costs (λid.lookup_def … labels id (zero ?)) sigma 1170 pc ppc costs i' in 1171 〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉 1172 in 1173 let 〈labels, ppc_pc_costs〉 ≝ result in 1174 let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in 1175 let 〈pc, costs〉 ≝ pc_costs in 1176 〈labels, costs〉. 1177 (* [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 1178 generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]] 1179 [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ % 1180  >append_length <IH0 normalize; IHn1; (*CSC: otherwise it diverges!*) // 1181  >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ % 1182  #id normalize nodelta; labels1; cases label; normalize nodelta 1183 [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 IHn1; (*CSC: otherwise it diverges!*) // 1184  #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?; 1185 generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %); 1186 [ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit 1187 <IH0 [@IHn1  <(eq_identifier_eq … EQ) in H; #H @H] 1188  #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: IHn1; 1189 (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL) 1190 lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ] 1191 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]] 1192 3: whd % [% [%]] [>sigma_0 %  %  %  #id normalize in ⊢ (% → ?); #abs @⊥ // ] 1193  generalize in match (pi2 … result) in ⊢ ?; 1194 normalize nodelta in p ⊢ %; result; >p in ⊢ (match % with [_ ⇒ ?] → ?); 1195 normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H] *) 1196 cases daemon 1197 qed. 1198 1199 definition build_maps: 1200 ∀pseudo_program.∀sigma. 1201 (identifier_map ASMTag Word) × (BitVectorTrie costlabel 16) 1202 ≝ λpseudo_program,sigma. build_maps0 pseudo_program sigma. 1203 1204 theorem build_maps_ok: 1099 *) 1100 1101 (* label_map: identifier ↦ pseudo program counter *) 1102 definition label_map ≝ identifier_map ASMTag ℕ. 1103 1104 (* Labels *) 1105 definition is_label ≝ 1106 λx:labelled_instruction.λl:Identifier. 1107 let 〈lbl,instr〉 ≝ x in 1108 match lbl with 1109 [ Some l' ⇒ l' = l 1110  _ ⇒ False 1111 ]. 1112 1113 lemma label_does_not_occur: 1114 ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier. 1115 is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false. 1116 #i #p #l generalize in match i; elim p 1117 [ #i >nth_nil #H cases H 1118  #h #t #IH #i cases i i 1119 [ cases h #hi #hp cases hi 1120 [ normalize #H cases H 1121  #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????); 1122 whd in Heq; >Heq 1123 >eq_identifier_refl / by refl/ 1124 ] 1125  #i #H whd in match (does_not_occur ????); 1126 whd in match (instruction_matches_identifier ????); 1127 cases h #hi #hp cases hi normalize nodelta 1128 [ @(IH i) @H 1129  #l' @eq_identifier_elim 1130 [ normalize / by / 1131  normalize #_ @(IH i) @H 1132 ] 1133 ] 1134 ] 1135 ] 1136 qed. 1137 1138 (* The function that creates the labeltoaddress map *) 1139 definition create_label_cost_map: ∀program:list labelled_instruction. 1140 (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *) 1141 let 〈labels,costs〉 ≝ labels_costs in 1142 ∀i:ℕ.lt i (program) → 1143 ∀l.occurs_exactly_once ?? l program → 1144 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 1145 lookup ?? labels l = Some ? i 1146 ) ≝ 1147 λprogram. 1148 \fst (foldl_strong (option Identifier × pseudo_instruction) 1149 (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × nat. 1150 let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in 1151 ppc = prefix ∧ 1152 ∀i:ℕ.lt i (prefix) → 1153 ∀l.occurs_exactly_once ?? l prefix → 1154 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 1155 lookup … labels l = Some ? i 1156 ) 1157 program 1158 (λprefix.λx.λtl.λprf.λlabels_costs_ppc. 1159 let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in 1160 let 〈label,instr〉 ≝ x in 1161 let labels ≝ 1162 match label with 1163 [ None ⇒ labels 1164  Some l ⇒ add … labels l ppc 1165 ] in 1166 let costs ≝ 1167 match instr with 1168 [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs 1169  _ ⇒ costs ] in 1170 〈labels,costs,S ppc〉 1171 ) 〈(empty_map …),(Stub ??),0〉). 1172 [2: normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2 1173 labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %] 1174 inversion label [#EQ  #l #EQ] 1175 [1,2: normalize nodelta 1176 #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 1177 [3: #Hi #lbl #Hocc #Hlbl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) Hocc 1178 @eq_identifier_elim 1179 [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl 1180 @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/ 1181  #Heq #Hocc normalize in Hocc; >lookup_add_miss 1182 [ @(IH2 … i (le_S_S_to_le … Hi)) 1183 [ @Hocc 1184  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by / 1185 ] 1186  @sym_neq @Heq 1187 ] 1188 ] 1189 4: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second 1190 [ <minus_n_n #Hl normalize in Hl; >Hl >IH1 @lookup_add_hit 1191  @le_n 1192 ] 1193 1: #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl 1194 @(IH2 … i (le_S_S_to_le … Hi)) 1195 [ @Hocc 1196  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by / 1197 ] 1198 2: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second 1199 [ <minus_n_n #Hl cases Hl 1200  @le_n 1201 ] 1202 ] 1203 ] 1204  @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try % 1205 #i #Hi normalize in Hi; cases (not_le_Sn_O i) #abs cases (abs Hi) 1206  cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta * 1207 #_ #H @H 1208 ] 1209 qed. 1210 1211 (*theorem build_maps_ok: 1205 1212 ∀pseudo_program.∀sigma:Word → Word. 1206 1213 let 〈labels, costs〉 ≝ build_maps pseudo_program sigma in … … 1208 1215 lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id). 1209 1216 #pseudo_program #sigma @(pi2 … (build_maps0 … sigma)) 1210 qed. 1217 qed.*) 1211 1218 1212 1219 definition assembly: 1213 ∀p:pseudo_assembly_program.∀sigma:Word → Word .list Byte × (BitVectorTrie costlabel 16) ≝1220 ∀p:pseudo_assembly_program.∀sigma:Word → Word × bool.list Byte × (BitVectorTrie costlabel 16) ≝ 1214 1221 λp.let 〈preamble, instr_list〉 ≝ p in 1215 1222 λsigma. 1216 let 〈labels ,costs〉 ≝ build_maps 〈preamble,instr_list〉 sigmain1223 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1217 1224 let datalabels ≝ construct_datalabels preamble in 1218 let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in1225 let lookup_labels ≝ λx. \fst (sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0))) in 1219 1226 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1220 1227 let result ≝ … … 1239 1246 〈(zero ?), 〈(zero ?), [ ]〉〉 1240 1247 in 1241 〈\snd (\snd result), costs〉. 1242 cases daemon 1248 〈\snd (\snd result), 1249 fold … (λppc.λcost.λpc_to_costs. insert … (\fst (sigma ppc)) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 1250 @pair_elim normalize nodelta #x #y #z @pair_elim normalize nodelta #w1 #w2 #w3 #w4 @pair_elim // 1243 1251 qed. 1244 1252
Note: See TracChangeset
for help on using the changeset viewer.