Changeset 842 for src/ASM/Assembly.ma
 Timestamp:
 May 25, 2011, 3:57:03 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r840 r842 398 398 qed. 399 399 400 definition address_of: BitVectorTrie Word 16 → Identifier → Byte ≝ 401 λmap. 402 λid: Identifier. 403 let address ≝ lookup … id map (zero ?) in 404 let 〈high, low〉 ≝ split ? 8 8 address in 405 if eq_bv ? high (zero ?) then 406 low 407 else 408 ?. 409 elim not_implemented. 410 qed. 400 definition is_relative_jump ≝ 401 λi: preinstruction Identifier. 402 match i with 403 [ JC _ ⇒ True 404  JNC _ ⇒ True 405  JB _ _ ⇒ True 406  JNB _ _ ⇒ True 407  JBC _ _ ⇒ True 408  JZ _ ⇒ True 409  JNZ _ ⇒ True 410  CJNE _ _ ⇒ True 411  DJNZ _ _ ⇒ True 412  _ ⇒ False 413 ]. 414 415 definition pseudo_instruction_is_relative_jump: pseudo_instruction → Prop ≝ 416 λi. 417 match i with 418 [ Instruction j ⇒ is_relative_jump j 419  _ ⇒ False ]. 411 420 412 421 inductive jump_length: Type[0] ≝ … … 418 427 ∀program: pseudo_assembly_program. 419 428 ∀pc: Word. 420 jump_length. 421 422 definition expand_relative_jump_internal ≝ 423 λjmp_len. 424 λi. 429 jump_length. 430 431 definition expand_relative_jump_internal: 432 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) → 433 option (list instruction) 434 ≝ 435 λlookup_labels,jmp_len.λjmp:Identifier.λpc,i. 425 436 match jmp_len with 426 [ short_jump ⇒ Some ? [ i ] 427  medium_jump ⇒ None ? 437 [ short_jump ⇒ 438 let lookup_address ≝ lookup_labels jmp in 439 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 440 let 〈upper, lower〉 ≝ split ? 8 8 result in 441 if eq_bv ? upper (zero 8) then 442 let address ≝ RELATIVE lower in 443 Some ? [ RealInstruction (i address) ] 444 else 445 None ? 446  medium_jump ⇒ None … 428 447  long_jump ⇒ 429 Some ? [ RealInstruction i; 448 Some ? 449 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); 430 450 SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) 431 LJMP (ADDR16 ( bitvector_of_nat ? 0)) (* fill in *)451 LJMP (ADDR16 (lookup_labels jmp)) 432 452 ] 433 453 ]. … … 435 455 qed. 436 456 437 definition expand_relative_jump: jump_length → preinstruction Identifier → option (list instruction) ≝ 457 definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝ 458 λlookup_labels. 438 459 λjmp_len: jump_length. 460 λpc. 439 461 λi: preinstruction Identifier. 440 462 let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in 441 463 match i with 442 [ JC jmp ⇒ expand_relative_jump_internal jmp_len (JC ? rel_jmp)443  JNC jmp ⇒ expand_relative_jump_internal jmp_len (JNC ? rel_jmp)444  JB baddr jmp ⇒ expand_relative_jump_internal jmp_len (JB ? baddr rel_jmp)445  JZ jmp ⇒ expand_relative_jump_internal jmp_len (JZ ? rel_jmp)446  JNZ jmp ⇒ expand_relative_jump_internal jmp_len (JNZ ? rel_jmp)447  JBC baddr jmp ⇒ expand_relative_jump_internal jmp_len (JBC ? baddr rel_jmp)448  JNB baddr jmp ⇒ expand_relative_jump_internal jmp_len (JNB ? baddr rel_jmp)449  CJNE addr jmp ⇒ expand_relative_jump_internal jmp_len (CJNE ? addr rel_jmp)450  DJNZ addr jmp ⇒ expand_relative_jump_internal jmp_len (DJNZ ? addr rel_jmp)464 [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?) 465  JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?) 466  JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr) 467  JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?) 468  JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?) 469  JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr) 470  JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr) 471  CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr) 472  DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr) 451 473  ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ] 452 474  ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ] … … 478 500  NOP ⇒ Some ? [ RealInstruction (NOP ?) ] 479 501 ]. 480 @ I481 qed.482 502 483 503 definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝ … … 508 528 let address ≝ DATA16 (lookup_datalabels trgt) in 509 529 Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))] 510  Instruction instr ⇒ expand_relative_jump jmp_leninstr530  Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr 511 531  Jmp jmp ⇒ 512 532 match jmp_len with … … 562 582 〈insert ? ? name addr_16 datalabels, addr + size〉) 563 583 〈(Stub ? ?), 0〉 preamble). 564 565 definition is_jump ≝566 λi: preinstruction Identifier.567 match i with568 [ JC _ ⇒ true569  JNC _ ⇒ true570  JB _ _ ⇒ true571  JNB _ _ ⇒ true572  JBC _ _ ⇒ true573  JZ _ ⇒ true574  JNZ _ ⇒ true575  CJNE _ _ ⇒ true576  DJNZ _ _ ⇒ true577  _ ⇒ false578 ].579 584 580 585 definition construct_costs ≝
Note: See TracChangeset
for help on using the changeset viewer.