Changeset 465 for Deliverables/D4.1/Matita/Assembly.ma
 Timestamp:
 Jan 20, 2011, 6:10:07 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Assembly.ma
r437 r465 10 10 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 11 11 [ ADDR11 w ⇒ λ_. 12 let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in12 let 〈v1,v2〉 ≝ split ? (S (S (S O))) (S (S (S (S (S (S (S (S O)))))))) w in 13 13 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 14 14  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 30 30 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 31 31 [ ADDR11 w ⇒ λ_. 32 let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in32 let 〈v1,v2〉 ≝ split ? (S (S (S O))) (S (S (S (S (S (S (S (S O)))))))) w in 33 33 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] 34 34  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 35 35  ANL addrs ⇒ 36 36 match addrs with 37 [ Leftaddrs ⇒ match addrs with38 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in37 [ inl addrs ⇒ match addrs with 38 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 39 39 match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with 40 40 [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ] … … 43 43  DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ] 44 44  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 45  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in45  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 46 46 let b1 ≝ 47 47 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with … … 53 53  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 54 54 ] 55  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in55  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 56 56 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with 57 57 [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ] … … 157 157  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in 158 158 match addrs with 159 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in159 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 160 160 match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with 161 161 [ DIRECT b1 ⇒ λ_. … … 164 164 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ] 165 165  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 166  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in166  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 167 167 let b2 ≝ 168 168 match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with 169 169 [ DATA b2 ⇒ λ_. b2 170 170  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 171 match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with171 match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → list Byte with 172 172 [ REGISTER r⇒ λ_. 173 173 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ] … … 193 193 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 194 194 [ ADDR16 w ⇒ λ_. 195 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in195 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in 196 196 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ] 197 197  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 199 199 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 200 200 [ ADDR16 w ⇒ λ_. 201 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in201 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in 202 202 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ] 203 203  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 204 204  MOV addrs ⇒ 205 205 match addrs with 206 [ Leftaddrs ⇒206 [ inl addrs ⇒ 207 207 match addrs with 208 [ Leftaddrs ⇒208 [ inl addrs ⇒ 209 209 match addrs with 210 [ Leftaddrs ⇒210 [ inl addrs ⇒ 211 211 match addrs with 212 [ Leftaddrs ⇒212 [ inl addrs ⇒ 213 213 match addrs with 214 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in214 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 215 215 match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with 216 216 [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ] … … 219 219  DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ] 220 220  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 221  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in221  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 222 222 match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with 223 223 [ REGISTER r ⇒ λ_. … … 234 234  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 235 235  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] 236  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in236  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 237 237 let b1 ≝ 238 238 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with … … 246 246  DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ] 247 247  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 248  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in248  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 249 249 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with 250 250 [ DATA16 w ⇒ λ_. 251 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in251 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in 252 252 [ ([[true;false;false;true;false;false;false;false]]); b1; b2] 253 253  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 254  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in254  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 255 255 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 256 256 [ BIT_ADDR b1 ⇒ λ_. 257 257 [ ([[true;false;true;false;false;false;true;false]]); b1 ] 258 258  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 259  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in259  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 260 260 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 261 261 [ BIT_ADDR b1 ⇒ λ_. … … 271 271  MOVX addrs ⇒ 272 272 match addrs with 273 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in273 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 274 274 match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with 275 275 [ EXT_INDIRECT i1 ⇒ λ_. … … 278 278 [ ([[true;true;true;false;false;false;false;false]]) ] 279 279  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 280  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in280  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 281 281 match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with 282 282 [ EXT_INDIRECT i1 ⇒ λ_. … … 291 291  ORL addrs ⇒ 292 292 match addrs with 293 [ Leftaddrs ⇒293 [ inl addrs ⇒ 294 294 match addrs with 295 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in295 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 296 296 match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with 297 297 [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ] … … 300 300  DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ] 301 301  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 302  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in302  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 303 303 let b1 ≝ 304 304 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with … … 311 311 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ] 312 312  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 313  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in313  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 314 314 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with 315 315 [ BIT_ADDR b1 ⇒ λ_. … … 381 381  XRL addrs ⇒ 382 382 match addrs with 383 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in383 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 384 384 match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with 385 385 [ REGISTER r ⇒ λ_. … … 392 392 [ ([[false;true;true;false;false;true;false;false]]); b1] 393 393  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 394  Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in394  inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 395 395 let b1 ≝ 396 396 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with … … 419 419 ]. 420 420 421 ndefinition address_of: BitVectorTrie (BitVector eight) eight→ String → addressing_mode ≝422 λmap: BitVectorTrie (BitVector eight) eight.421 ndefinition address_of: BitVectorTrie (BitVector 8) 8 → String → addressing_mode ≝ 422 λmap: BitVectorTrie (BitVector 8) 8. 423 423 λstring: String. 424 424 let address ≝ lookup … (bitvector_of_string … string) map (zero ?) in 425 425 let address_bv ≝ nat_of_bitvector ? address in 426 if le ss_than_b address_bv two_hundred_and_fifty_sixthen426 if leb address_bv 256 then 427 427 RELATIVE address 428 428 else … … 431 431 nqed. 432 432 433 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝433 ndefinition assembly: assembly_program → option (list Byte × (BitVectorTrie String 16)) ≝ 434 434 λp. 435 435 let 〈preamble, instr_list〉 ≝ p in 436 436 let 〈datalabels, ignore〉 ≝ 437 fold _left ((BitVectorTrie (BitVector sixteen) sixteen) × Nat) ? (437 foldl ((BitVectorTrie (BitVector 16) 16) × nat) ? ( 438 438 λt. λpreamble. 439 439 let 〈datalabels, addr〉 ≝ t in 440 440 let 〈name, size〉 ≝ preamble in 441 let addr_sixteen ≝ bitvector_of_nat sixteenaddr in441 let addr_sixteen ≝ bitvector_of_nat 16 addr in 442 442 〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉) 443 〈(Stub ? ?), Z〉 preamble in443 〈(Stub ? ?), O〉 preamble in 444 444 let 〈pc_labels, costs〉 ≝ 445 fold _left ((Nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? (445 foldl ((nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? ( 446 446 λt. λi. 447 447 let 〈pc_labels, costs〉 ≝ t in … … 450 450 [ Instruction instr ⇒ 451 451 let code_memory ≝ load_code_memory (assembly1 instr) in 452 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in452 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in 453 453 let 〈instr', program_counter'〉 ≝ instr_pc' in 454 454 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in … … 456 456  Label label ⇒ 457 457 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 458 〈〈program_counter, (insert ? ? (bitvector_of_string eightlabel) program_counter_bv labels)〉, costs〉458 〈〈program_counter, (insert ? ? (bitvector_of_string 8 label) program_counter_bv labels)〉, costs〉 459 459  Cost cost ⇒ 460 460 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 461 461 〈pc_labels, (insert ? ? program_counter_bv cost costs)〉 462 462  Jmp jmp ⇒ 463 〈〈program_counter + three, labels〉, costs〉463 〈〈program_counter + 3, labels〉, costs〉 464 464  Call call ⇒ 465 〈〈program_counter + three, labels〉, costs〉465 〈〈program_counter + 3, labels〉, costs〉 466 466  Mov dptr trgt ⇒ t 467 467  WithLabel jmp ⇒ 468 let fake_addr ≝ RELATIVE (zero eight) in468 let fake_addr ≝ RELATIVE (zero 8) in 469 469 let fake_jump ≝ assembly_jump jmp (λx: String. fake_addr) in 470 470 let code_memory ≝ load_code_memory (assembly1 fake_jump) in 471 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in471 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in 472 472 let 〈instr', program_counter'〉 ≝ instr_pc' in 473 let program_counter_n' ≝ nat_of_bitvector sixteenprogram_counter' in473 let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in 474 474 〈〈program_counter + program_counter_n', labels〉, costs〉 475 475 ] 476 ) 〈〈 Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in476 ) 〈〈O, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in 477 477 let 〈program_counter, labels〉 ≝ pc_labels in 478 if greater_than_b program_counter 479 sixty_five_thousand_five_hundred_and_thirty_six then 480 Nothing ? 478 if gtb program_counter (2^16) then 479 None ? 481 480 else 482 481 let flat_list ≝ … … 489 488  Call call ⇒ 490 489 let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in 491 let pc_offset_pad ≝ (zero eight) @@ pc_offset in490 let pc_offset_pad ≝ (zero 8) @@ pc_offset in 492 491 let address ≝ ADDR16 pc_offset_pad in 493 492 assembly1 (LCALL ? address) … … 495 494 let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in 496 495 let address ≝ DATA16 pc_offset in 497 assembly1 (MOV ? ( Left ? ? (Left ? ? (Right? ? 〈DPTR, address〉))))496 assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉)))) 498 497  Instruction instr ⇒ assembly1 instr 499 498  Jmp jmp ⇒ 500 499 let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in 501 let pc_offset_pad ≝ (zero eight) @@ pc_offset in500 let pc_offset_pad ≝ (zero 8) @@ pc_offset in 502 501 let address ≝ ADDR16 pc_offset_pad in 503 502 assembly1 (LJMP ? address) … … 507 506 ) instr_list 508 507 ) in 509 Just (List ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.508 Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉. 510 509 ##[##2,3,4,5,6: nnormalize; @; 511 510 ## nwhd in ⊢ (? (? ? ? %)); 512 ncases (le ss_than_b (nat_of_bitvector eight ?) two_hundred_and_fifty_six)511 ncases (leb (nat_of_bitvector 8 ?) 256) 513 512 [ nnormalize; @; 514 513 ## nnormalize; … … 518 517 nqed. 519 518 520 ndefinition assembly_unlabelled_program: List instruction → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝521 λp. Just ? (〈fold_right?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).519 ndefinition assembly_unlabelled_program: list instruction → option (list Byte × (BitVectorTrie String 16)) ≝ 520 λp.Some ? (〈foldr ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracChangeset
for help on using the changeset viewer.