Changeset 419
 Timestamp:
 Dec 14, 2010, 2:13:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Assembly.ma
r418 r419 405 405 include "Status.ma". 406 406 407 ndefinition assembly_jump ≝408 λA , B: Type[0].409 λj .410 λaddr_of: A → B.407 ndefinition assembly_jump: ? → (jump ?) → (? → [[relative]]) → instruction ≝ 408 λA: Type[0]. 409 λj: jump A. 410 λaddr_of: A → [[relative]]. 411 411 match j with 412 [ JC jmp ⇒ J C ? (addr_of jmp)413  JNC jmp ⇒ J NC ? (addr_of jmp)414  JZ jmp ⇒ J Z ? (addr_of jmp)415  JNZ jmp ⇒ J NZ ? (addr_of jmp)416  JB jmp jmp' ⇒ J B ? jmp (addr_of jmp')417  JNB jmp jmp' ⇒ J NB ? jmp (addr_of jmp')418  JBC jmp jmp' ⇒ J BC ? jmp (addr_of jmp')419  CJNE jmp jmp' ⇒ CJNE ? jmp (addr_of jmp')420  DJNZ jmp jmp' ⇒ DJNZ ? jmp (addr_of jmp')412 [ JC jmp ⇒ Jump [[relative]] (JC ? (addr_of jmp)) 413  JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp)) 414  JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp)) 415  JNZ jmp ⇒ Jump ? (JNZ ? (addr_of jmp)) 416  JB jmp jmp' ⇒ Jump ? (JB ? jmp (addr_of jmp')) 417  JNB jmp jmp' ⇒ Jump ? (JNB ? jmp (addr_of jmp')) 418  JBC jmp jmp' ⇒ Jump ? (JBC ? jmp (addr_of jmp')) 419  CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp')) 420  DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp')) 421 421 ]. 422 422 423 ndefinition address_of: BitVectorTrie ? ?→ String → addressing_mode ≝424 λmap .425 λstring .423 ndefinition address_of: BitVectorTrie (BitVector eight) eight → String → addressing_mode ≝ 424 λmap: BitVectorTrie (BitVector eight) eight. 425 λstring: String. 426 426 let address ≝ lookup … (bitvector_of_string … string) map (zero ?) in 427 427 let address_bv ≝ nat_of_bitvector ? address in … … 457 457 〈〈program_counter + program_counter_n', labels〉, costs〉 458 458  Label label ⇒ 459 let program_counter_bv ≝ bitvector_of_nat sixteenprogram_counter in460 〈〈program_counter, (insert ? ? (bitvector_of_string ?label) program_counter_bv labels)〉, costs〉459 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 460 〈〈program_counter, (insert ? ? (bitvector_of_string eight label) program_counter_bv labels)〉, costs〉 461 461  Cost cost ⇒ 462 let program_counter_bv ≝ bitvector_of_nat sixteenprogram_counter in462 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 463 463 〈pc_labels, (insert ? ? program_counter_bv cost costs)〉 464 464  Jmp jmp ⇒ … … 467 467 〈〈program_counter + three, labels〉, costs〉 468 468  Mov dptr trgt ⇒ t 469  WithLabel jmp ⇒ ? (*469  WithLabel jmp ⇒ 470 470 let fake_addr ≝ RELATIVE (zero eight) in 471 let fake_jump ≝ assembly_jump ? ?jmp (λx. fake_addr) in472 let code_memory ≝ load_code_memory (assembly1 (Jump relative fake_jump)) in473 let 〈instr_pc', ignore〉 471 let fake_jump ≝ assembly_jump ? jmp (λx. fake_addr) in 472 let code_memory ≝ load_code_memory (assembly1 fake_jump) in 473 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in 474 474 let 〈instr', program_counter'〉 ≝ instr_pc' in 475 475 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in 476 〈〈program_counter + program_counter_n', labels〉, costs〉 *)476 〈〈program_counter + program_counter_n', labels〉, costs〉 477 477 ] 478 478 ) 〈〈Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in … … 491 491  Call call ⇒ 492 492 let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in 493 let address ≝ ADDR16 pc_offset in 493 let pc_offset_pad ≝ (zero eight) @@ pc_offset in 494 let address ≝ ADDR16 pc_offset_pad in 494 495 assembly1 (LCALL ? address) 495 496  Mov d trgt ⇒ … … 500 501  Jmp jmp ⇒ 501 502 let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in 502 let address ≝ ADDR16 pc_offset in 503 let pc_offset_pad ≝ (zero eight) @@ pc_offset in 504 let address ≝ ADDR16 pc_offset_pad in 503 505 assembly1 (LJMP ? address) 504  WithLabel jmp ⇒ ? (*505 assembly1 ( Jump ? (assembly_jump ? ? jmp (address_of labels))) *)506  WithLabel jmp ⇒ 507 assembly1 (assembly_jump ? jmp (address_of labels)) 506 508 ] 507 509 ) instr_list
Note: See TracChangeset
for help on using the changeset viewer.