Changeset 842


Ignore:
Timestamp:
May 25, 2011, 3:57:03 PM (8 years ago)
Author:
sacerdot
Message:

Bug fixed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r840 r842  
    398398qed.
    399399
    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.
     400definition 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
     415definition pseudo_instruction_is_relative_jump: pseudo_instruction → Prop ≝
     416 λi.
     417  match i with
     418   [ Instruction j ⇒ is_relative_jump j
     419   | _ ⇒ False ].
    411420
    412421inductive jump_length: Type[0] ≝
     
    418427  ∀program: pseudo_assembly_program.
    419428  ∀pc: Word.
    420     jump_length.
    421 
    422 definition expand_relative_jump_internal ≝
    423   λjmp_len.
    424   λi.
     429   jump_length.
     430
     431definition 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.
    425436  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 …
    428447  | long_jump ⇒
    429     Some ? [ RealInstruction i;
     448    Some ?
     449    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
    430450      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
    431       LJMP (ADDR16 (bitvector_of_nat ? 0)) (* fill in *)
     451      LJMP (ADDR16 (lookup_labels jmp))
    432452    ]
    433453  ].
     
    435455qed.
    436456
    437 definition expand_relative_jump: jump_length → preinstruction Identifier → option (list instruction) ≝
     457definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
     458  λlookup_labels.
    438459  λjmp_len: jump_length.
     460  λpc.
    439461  λi: preinstruction Identifier.
    440462  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
    441463  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)
    451473  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
    452474  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
     
    478500  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
    479501  ].
    480   @ I
    481 qed.
    482502
    483503definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
     
    508528    let address ≝ DATA16 (lookup_datalabels trgt) in
    509529      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
    510   | Instruction instr ⇒ expand_relative_jump jmp_len instr
     530  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
    511531  | Jmp jmp ⇒
    512532    match jmp_len with
     
    562582        〈insert ? ? name addr_16 datalabels, addr + size〉)
    563583          〈(Stub ? ?), 0〉 preamble).
    564 
    565 definition is_jump ≝
    566   λi: preinstruction Identifier.
    567   match i with
    568   [ JC _ ⇒ true
    569   | JNC _ ⇒ true
    570   | JB _ _ ⇒ true
    571   | JNB _ _ ⇒ true
    572   | JBC _ _ ⇒ true
    573   | JZ _ ⇒ true
    574   | JNZ _ ⇒ true
    575   | CJNE _ _ ⇒ true
    576   | DJNZ _ _ ⇒ true
    577   | _ ⇒ false
    578   ].
    579584
    580585definition construct_costs ≝
Note: See TracChangeset for help on using the changeset viewer.