- Timestamp:
- Nov 18, 2011, 1:03:14 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 7 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASM.ma
r1493 r1515 1 1 include "ASM/BitVector.ma". 2 3 definition Identifier ≝ Word. 2 include "common/Identifiers.ma". 3 include "common/CostLabel.ma". 4 5 axiom ASMTag : String. 6 definition Identifier ≝ identifier ASMTag. 7 definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ]. 4 8 5 9 inductive addressing_mode: Type[0] ≝ … … 194 198 | Instruction: preinstruction Identifier → pseudo_instruction 195 199 | Comment: String → pseudo_instruction 196 | Cost: Identifier→ pseudo_instruction200 | Cost: costlabel → pseudo_instruction 197 201 | Jmp: Identifier → pseudo_instruction 198 202 | Call: Identifier → pseudo_instruction -
src/ASM/Erase.ma
r1463 r1515 1 1 include "ASM/ASM.ma". 2 include "ASM/BitVectorTrie.ma". 3 2 4 3 let rec pre_erase 5 4 (the_program: list labelled_instruction) (labels: list Identifier) 6 on the_program: (( BitVectorTrie Identifier 16) × (list labelled_instruction)) ≝5 on the_program: ((identifier_map ASMTag Identifier) × (list labelled_instruction)) ≝ 7 6 match the_program with 8 7 [ nil ⇒ 9 8 match labels with 10 [ nil ⇒ 〈 Stub Identifier 16, [ ]〉 (* XXX: labels should be empty *)9 [ nil ⇒ 〈empty_map ??, [ ]〉 (* XXX: labels should be empty *) 11 10 | _ ⇒ ⊥ 12 11 ] … … 25 24 | _ ⇒ 26 25 let 〈maps, the_program〉 ≝ pre_erase tl [ ] in 27 let maps ≝ foldr … (λl. λmap. insert … l label map) maps (label::labels) in26 let maps ≝ foldr ?? (λl. λmap. add … map l label) maps (label::labels) in 28 27 〈maps, the_program〉 29 28 ] … … 33 32 qed. 34 33 35 definition relabel_instruction: preinstruction Identifier → BitVectorTrie Identifier 16→ preinstruction Identifier ≝34 definition relabel_instruction: preinstruction Identifier → identifier_map ASMTag Identifier → preinstruction Identifier ≝ 36 35 λpre. 37 36 λmap. 38 37 match pre with 39 38 [ JC ident ⇒ 40 let located ≝ lookup … ident mapident in39 let located ≝ lookup_def … map ident ident in 41 40 JC … located 42 41 | JNC ident ⇒ 43 let located ≝ lookup … ident mapident in42 let located ≝ lookup_def … map ident ident in 44 43 JNC … located 45 44 | JB bit ident ⇒ 46 let located ≝ lookup … ident mapident in45 let located ≝ lookup_def … map ident ident in 47 46 JB … bit located 48 47 | JNB bit ident ⇒ 49 let located ≝ lookup … ident mapident in48 let located ≝ lookup_def … map ident ident in 50 49 JNB … bit located 51 50 | JBC bit ident ⇒ 52 let located ≝ lookup … ident mapident in51 let located ≝ lookup_def … map ident ident in 53 52 JBC … bit located 54 53 | JZ ident ⇒ 55 let located ≝ lookup … ident mapident in54 let located ≝ lookup_def … map ident ident in 56 55 JZ … located 57 56 | JNZ ident ⇒ 58 let located ≝ lookup … ident mapident in57 let located ≝ lookup_def … map ident ident in 59 58 JNZ … located 60 59 | CJNE src ident ⇒ 61 let located ≝ lookup … ident mapident in60 let located ≝ lookup_def … map ident ident in 62 61 CJNE … src located 63 62 | DJNZ src ident ⇒ 64 let located ≝ lookup … ident mapident in63 let located ≝ lookup_def … map ident ident in 65 64 DJNZ … src located 66 65 (* XXX: no identifiers in rest of instructions *) … … 68 67 ]. 69 68 70 definition relabel_pseudo_instruction: pseudo_instruction → BitVectorTrie Identifier 16→ pseudo_instruction ≝69 definition relabel_pseudo_instruction: pseudo_instruction → identifier_map ASMTag Identifier → pseudo_instruction ≝ 71 70 λpseudo. 72 71 λmap. … … 76 75 | Comment comment ⇒ Comment comment 77 76 | Jmp ident ⇒ 78 let located ≝ lookup … ident mapident in77 let located ≝ lookup_def … map ident ident in 79 78 Jmp located 80 79 | Call ident ⇒ 81 let located ≝ lookup … ident mapident in80 let located ≝ lookup_def … map ident ident in 82 81 Call located 83 82 | Mov dptr ident ⇒ 84 let located ≝ lookup … ident mapident in83 let located ≝ lookup_def … map ident ident in 85 84 Mov dptr located 86 85 ]. 87 86 88 87 let rec relabel 89 (the_program: list labelled_instruction) (map: BitVectorTrie Identifier 16)88 (the_program: list labelled_instruction) (map: identifier_map ASMTag Identifier) 90 89 on the_program: list labelled_instruction ≝ 91 90 match the_program with … … 97 96 match label with 98 97 [ None ⇒ None … 99 | Some label ⇒ Some … (lookup … ident mapident)98 | Some label ⇒ Some … (lookup_def … map ident ident) 100 99 ] 101 100 in -
src/ASM/I8051.ma
r1416 r1515 7 7 include "utilities/Compare.ma". 8 8 include "joint/BEValues.ma". 9 include "ASM/BitVectorTrie.ma". 9 10 10 11 definition int_size ≝ bitvector_of_nat 8 1. -
src/ASM/Interpret.ma
r1514 r1515 686 686 let preamble ≝ \fst (code_memory ? s) in 687 687 let data_labels ≝ construct_datalabels (map … (fst …) preamble) in 688 set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup ? ? ident data_labels(zero ?)))) dptr688 set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr 689 689 ] 690 690 in -
src/ASM/Interpret2.ma
r1478 r1515 23 23 let s ≝ execute_1_pseudo_instruction ticks_of s in 24 24 match instr with 25 [ Cost cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉25 [ Cost cst ⇒ ret … 〈Echarge cst, s〉 26 26 | _ ⇒ ret ? 〈E0, s〉 ]. 27 27 … … 37 37 38 38 (*CSC: move this definition elsewhere *) 39 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie Identifier16).39 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16). 40 40 41 definition make_global: object_code → BitVectorTrie Identifier16 ≝ \snd.41 definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd. 42 42 43 43 definition execute_1_instruction: 44 BitVectorTrie Identifier16 → Status → IO io_out io_in (trace × Status) ≝44 BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝ 45 45 λcosts,s. 46 46 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in … … 49 49 match lookup_opt … pc costs with 50 50 [ None ⇒ ret … 〈E0, s〉 51 | Some cst ⇒ ret … 〈Echarge (an_identifier … cst), s〉 ].51 | Some cst ⇒ ret … 〈Echarge cst, s〉 ]. 52 52 53 axiom is_final: BitVectorTrie Identifier16 → Status → option int.53 axiom is_final: BitVectorTrie costlabel 16 → Status → option int. 54 54 55 55 definition exec: trans_system io_out io_in ≝ -
src/ASM/Status.ma
r1459 r1515 702 702 λr: BitVector 3. 703 703 let address ≝ bit_address_of_register ? s r in 704 lookup …address (low_internal_ram ? s) (zero 8).704 lookup ?? address (low_internal_ram ? s) (zero 8). 705 705 706 706 definition set_register ≝ … … 717 717 λM: Type[0]. 718 718 λs: PreStatus M. 719 let 〈 nu, nl 〉 ≝ split …4 4 (get_8051_sfr ? s SFR_SP) in719 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_SP) in 720 720 let m ≝ get_index_v … nu O ? in 721 721 let r1 ≝ get_index_v … nu 1 ? in … … 804 804 λext_indirect_dptr: True. 805 805 let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 806 lookup …16 address (external_ram ? s) (zero 8)806 lookup ? 16 address (external_ram ? s) (zero 8) 807 807 | EXT_INDIRECT e ⇒ 808 808 λext_indirect: True. 809 809 let address ≝ get_register ? s [[ false; false; e ]] in 810 810 let padded_address ≝ pad 8 8 address in 811 lookup …16 padded_address (external_ram ? s) (zero 8)811 lookup ? 16 padded_address (external_ram ? s) (zero 8) 812 812 | ACC_DPTR ⇒ 813 813 λacc_dptr: True. … … 815 815 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in 816 816 let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in 817 lookup …16 address (external_ram ? s) (zero 8)817 lookup ? 16 address (external_ram ? s) (zero 8) 818 818 | ACC_PC ⇒ 819 819 λacc_pc: True. 820 820 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in 821 821 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in 822 lookup …16 address (external_ram ? s) (zero 8)822 lookup ? 16 address (external_ram ? s) (zero 8) 823 823 | DIRECT d ⇒ 824 824 λdirect: True. 825 let 〈 nu, nl 〉 ≝ split …4 4 d in825 let 〈 nu, nl 〉 ≝ split ? 4 4 d in 826 826 let bit_one ≝ get_index_v ? ? nu 0 ? in 827 827 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in … … 836 836 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in 837 837 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 838 let bit_1 ≝ get_index_v …bit_one_v O ? in838 let bit_1 ≝ get_index_v ?? bit_one_v O ? in 839 839 match bit_1 with 840 840 [ false ⇒ … … 1002 1002 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1003 1003 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1004 let trans ≝ lookup …7 address' (low_internal_ram ? s) (zero 8) in1004 let trans ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in 1005 1005 ¬(get_index_v … trans (modulus address 8) ?) 1006 1006 ] … … 1038 1038 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1039 1039 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1040 let t ≝ lookup …7 address' (low_internal_ram ? s) (zero 8) in1040 let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in 1041 1041 let n_bit ≝ set_index … t (modulus address 8) v ? in 1042 1042 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in … … 1096 1096 match \fst x with 1097 1097 [ None ⇒ false 1098 | Some x ⇒ eq_ bv? x y1098 | Some x ⇒ eq_identifier ? x y 1099 1099 ]. 1100 1100 … … 1114 1114 lemma does_not_occur_Some: 1115 1115 ∀id,id',i,list_instr. 1116 eq_ bv? id' id = false →1116 eq_identifier ? id' id = false → 1117 1117 does_not_occur id (list_instr@[〈Some ? id',i〉]) = 1118 1118 does_not_occur id list_instr. … … 1126 1126 does_not_occur id (list_instr@[〈Some ? id,i〉]) = false. 1127 1127 #id #i #list_instr elim list_instr 1128 [ normalize change with (if (if eq_ bv??? then ? else ?) then ? else ? = ?)1129 >eq_ bv_refl %1128 [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?) 1129 >eq_identifier_refl % 1130 1130 | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %] 1131 1131 qed. … … 1151 1151 lemma occurs_exactly_once_Some: 1152 1152 ∀id,id',i,prefix. 1153 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_ bv? id' id ∨ occurs_exactly_once id prefix.1153 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix. 1154 1154 #id #id' #i #prefix elim prefix 1155 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) 1156 change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/ 1155 [ whd in ⊢ (?% → ?) 1156 change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) with (eq_identifier ? id' id) 1157 @eq_identifier_elim normalize nodelta; /2/ 1157 1158 | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) 1158 1159 cases he; normalize nodelta 1159 1160 [ #H @ (IH H) 1160 | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)1161 change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;1162 [ generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)normalize nodelta;1163 /2/ #H >does_not_occur_Some / /1161 | #x whd in ⊢ (? → ?(??%)) change in match (instruction_matches_identifier ??) with (eq_identifier ? x id) 1162 @eq_identifier_elim #E normalize nodelta 1163 [ destruct @eq_identifier_elim normalize nodelta; 1164 /2/ #H >does_not_occur_Some /2/ 1164 1165 | #H @IH @H]]] 1165 1166 qed. … … 1168 1169 ∀id,id',i,prefix. 1169 1170 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → 1170 (eq_ bv? id' id ∧ does_not_occur id prefix) ∨1171 (¬eq_ bv? id' id ∧ occurs_exactly_once id prefix).1171 (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨ 1172 (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix). 1172 1173 #id #id' #i #prefix elim prefix 1173 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) →?)1174 change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)1174 [ whd in ⊢ (?% → ?) change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?) with (eq_identifier ???) 1175 @eq_identifier_elim #E 1175 1176 [ normalize // 1176 1177 | normalize #H @⊥ @H … … 1179 1180 cases he; normalize nodelta 1180 1181 [ #H @ (IH H) 1181 | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??) 1182 generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id) 1183 cases (eq_bv ???) in ⊢ (???% → %) #Heq 1184 [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta 1185 [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf 1182 | #x @eq_identifier_elim #Heq 1183 [ @eq_identifier_elim normalize nodelta 1184 [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf 1186 1185 | #H >(does_not_occur_Some) 1187 [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??) 1188 change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta 1189 @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??) 1190 change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 1191 | @(sym_eq … H) 1186 [ #H2 whd in match (does_not_occur ??) 1187 change in match (instruction_matches_identifier ??) with (eq_identifier ???) 1188 >Heq >eq_identifier_refl normalize nodelta 1189 @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) 1190 change in match (instruction_matches_identifier ??) with (eq_identifier ???) 1191 >eq_identifier_refl 1192 normalize nodelta @H2 1193 | /2/ 1192 1194 ] 1193 1195 ] 1194 | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim1195 generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)1196 #H eq21197 [ normalize nodelta<Heq2 in Hor; #Hor normalize in Hor;1198 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier??)1199 change in match (eq_v ???x id) with (eq_bv ? x id) >Heqnormalize nodelta1200 cases (does_not_occur id tl) in Hor; normalize nodelta //1196 | normalize nodelta #H lapply (IH H) -IH -H; 1197 @eq_identifier_elim #Heq2 1198 #Hor @orb_elim 1199 [ <Heq2 in Hor; #Hor normalize in Hor; 1200 whd in match (does_not_occur ??) change in match (instruction_matches_identifier ??) with (eq_identifier ???) 1201 >eq_identifier_false // normalize nodelta 1202 cases (does_not_occur id' tl) in Hor; normalize nodelta // 1201 1203 | normalize nodelta whd in match (occurs_exactly_once ??) 1202 whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)1203 > Heq normalize nodelta <Heq2 in Hor; normalize //1204 change in match (instruction_matches_identifier ??) with (eq_identifier ???) 1205 >eq_identifier_false // 1204 1206 ] 1205 1207 ] … … 1241 1243 1242 1244 lemma index_of_internal_Some_miss: ∀i,id,id'. 1243 eq_ bv? id' id = false →1245 eq_identifier ? id' id = false → 1244 1246 ∀instr_list,n. 1245 1247 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) → … … 1259 1261 = |instr_list| + n. 1260 1262 #i #id #instr_list elim instr_list 1261 [ #n #_ whd in ⊢ (??%%) change with (if eq_ bv … id id then ? else ? = ?) >eq_bv_refl %1263 [ #n #_ whd in ⊢ (??%%) change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl % 1262 1264 | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta; 1263 [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]1265 [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]] 1264 1266 qed. 1265 1267 … … 1278 1280 1279 1281 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list. 1280 eq_ bv? id' id = false →1282 eq_identifier ? id' id = false → 1281 1283 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) → 1282 1284 address_of_word_labels_code_mem instr_list id = 1283 1285 address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id. 1284 1286 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?)) 1285 >(index_of_internal_Some_miss … H) //1287 >(index_of_internal_Some_miss … H) [ @refl | // ] 1286 1288 qed. 1287 1289 … … 1291 1293 = bitvector_of_nat … (|instr_list|). 1292 1294 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?) 1293 >(index_of_internal_Some_hit … H) //1295 >(index_of_internal_Some_hit … H) <plus_n_O @refl 1294 1296 qed. 1295 1297 … … 1301 1303 definition construct_datalabels ≝ 1302 1304 λpreamble. 1303 \fst (foldl (( BitVectorTrie Identifier 16) × nat) ? (1305 \fst (foldl ((identifier_map ASMTag Word) × nat) ? ( 1304 1306 λt. λpreamble. 1305 1307 let 〈datalabels, addr〉 ≝ t in 1306 1308 let 〈name, size〉 ≝ preamble in 1307 1309 let addr_16 ≝ bitvector_of_nat 16 addr in 1308 〈 insert ? ? name addr_16 datalabels, addr + size〉)1309 〈 (Stub ? ?), 0〉 preamble).1310 〈add ? ? datalabels name addr_16, addr + size〉) 1311 〈empty_map …, 0〉 preamble). -
src/ASM/StatusProofs.ma
r1014 r1515 182 182 lemma get_8051_sfr_write_at_stack_pointer: 183 183 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y. 184 #T #s #x #y whd in ⊢ (??%%) //184 #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl 185 185 qed. 186 186
Note: See TracChangeset
for help on using the changeset viewer.