Changeset 1709 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Feb 17, 2012, 11:52:36 AM (8 years ago)
Author:
mulligan
Message:

Changes to the execution of the MOVC instruction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1666 r1709  
    11include "ASM/StatusProofs.ma".
     2include "common/StructuredTraces.ma".
    23include "ASM/Fetch.ma".
    34
     
    119120include alias "ASM/BitVectorTrie.ma".
    120121
     122definition ASM_classify0: instruction → status_class ≝
     123  λi: instruction.
     124  match i with
     125   [ RealInstruction pre ⇒
     126     match pre with
     127      [ RET ⇒ cl_return
     128      | JZ _ ⇒ cl_jump
     129      | JNZ _ ⇒ cl_jump
     130      | JC _ ⇒ cl_jump
     131      | JNC _ ⇒ cl_jump
     132      | JB _ _ ⇒ cl_jump
     133      | JNB _ _ ⇒ cl_jump
     134      | JBC _ _ ⇒ cl_jump
     135      | CJNE _ _ ⇒ cl_jump
     136      | DJNZ _ _ ⇒ cl_jump
     137      | _ ⇒ cl_other
     138      ]
     139   | ACALL _ ⇒ cl_call
     140   | LCALL _ ⇒ cl_call
     141   | JMP _ ⇒ cl_call
     142   | AJMP _ ⇒ cl_jump
     143   | LJMP _ ⇒ cl_jump
     144   | SJMP _ ⇒ cl_jump
     145   | _ ⇒ cl_other
     146   ].
     147
     148definition current_instruction0 ≝
     149  λcode_memory: BitVectorTrie Byte 16.
     150  λprogram_counter: Word.
     151    \fst (\fst (fetch … code_memory program_counter)).
     152
     153definition current_instruction ≝
     154  λcode_memory.
     155  λs: Status code_memory.
     156    current_instruction0 code_memory (program_counter … s).
     157   
     158definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
     159  λcode_memory.
     160  λs: Status code_memory.
     161    ASM_classify0 (current_instruction … s).
     162
    121163definition execute_1_preinstruction':
    122164  ∀ticks: nat × nat.
     
    124166  ∀s: PreStatus m cm.
    125167    Σs': PreStatus m cm.
    126       Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) ≝
     168      And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
     169        (ASM_classify cm s' = cl_other → program_counter … s' = \fst (\snd (fetch … s))) ≝
    127170  λticks: nat × nat.
    128171  λa, m: Type[0]. λcm.
     
    132175  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
    133176  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
    134   match instr in preinstruction return λx. Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock ?? s) (clock ?? s' = \snd ticks + clock ?? s) with
     177  match instr in preinstruction return λx. Σs': ?. ? with
    135178        [ ADD addr1 addr2 ⇒
    136179            let s ≝ add_ticks1 s in
     
    554597qed.
    555598
     599discriminator Prod.
     600
    556601definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
    557   Σs': Status cm. clock ?? s' = \snd current + clock … s ≝
     602  Σs': Status cm.
     603    And (clock ?? s' = \snd current + clock … s)
     604      (ASM_classify0 (\fst (\fst current)) = cl_other →
     605        program_counter ? ? s' = \snd (\fst current)) ≝
    558606  λcm,s0,instr_pc_ticks.
    559     let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    560     let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
     607    let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
     608    let 〈instr, pc〉 as INSTR_PC ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    561609    let s ≝ set_program_counter … s0 pc in
    562       match instr return λ_.Status cm with
    563       [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …
     610      match instr return λx. x = instr → Σs:?.? with
     611      [ RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …
    564612        (λx. λs.
    565613        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    566614        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
    567615        | _ ⇒ λabsd. ⊥
    568         ] (subaddressing_modein … x)) instr s
    569       | MOVC addr1 addr2 ⇒
    570           let s ≝ set_clock s (ticks + clock … s) in
    571           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
     616        ] (subaddressing_modein … x)) instr' s
     617      | MOVC addr1 addr2 ⇒ λinstr_refl.
     618          let s ≝ set_clock ?? s (ticks + clock … s) in
     619          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with
    572620            [ ACC_DPTR ⇒ λacc_dptr: True.
    573621              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
     
    578626            | ACC_PC ⇒ λacc_pc: True.
    579627              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    580               let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ?? s) (bitvector_of_nat 16 1) in
    581628              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    582629              (*      addition of the PC with the DPTR? At the moment, no.              *)
    583               let s ≝ set_program_counter … s inc_pc in
    584               let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
     630              let 〈carry, new_addr〉 ≝ half_add ? (program_counter … s) big_acc in
    585631              let result ≝ lookup ? ? new_addr cm (zero ?) in
    586632                set_8051_sfr … s SFR_ACC_A result
    587633            | _ ⇒ λother: False. ⊥
    588634            ] (subaddressing_modein … addr2)
    589       | JMP _ ⇒ (* DPM: always indirect_dptr *)
    590           let s ≝ set_clock s (ticks + clock … s) in
     635      | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
     636          let s ≝ set_clock ?? s (ticks + clock … s) in
    591637          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    592638          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
     
    594640          let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in
    595641            set_program_counter … s new_pc
    596       | LJMP addr ⇒
    597           let s ≝ set_clock s (ticks + clock … s) in
    598           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
     642      | LJMP addr ⇒ λinstr_refl.
     643          let s ≝ set_clock ?? s (ticks + clock … s) in
     644          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
    599645            [ ADDR16 a ⇒ λaddr16: True.
    600646                set_program_counter … s a
    601647            | _ ⇒ λother: False. ⊥
    602648            ] (subaddressing_modein … addr)
    603       | SJMP addr ⇒
    604           let s ≝ set_clock s (ticks + clock … s) in
    605           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
     649      | SJMP addr ⇒ λinstr_refl.
     650          let s ≝ set_clock ?? s (ticks + clock … s) in
     651          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
    606652            [ RELATIVE r ⇒ λrelative: True.
    607653                let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in
     
    609655            | _ ⇒ λother: False. ⊥
    610656            ] (subaddressing_modein … addr)
    611       | AJMP addr ⇒
    612           let s ≝ set_clock s (ticks + clock … s) in
    613           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
     657      | AJMP addr ⇒ λinstr_refl.
     658          let s ≝ set_clock ?? s (ticks + clock … s) in
     659          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    614660            [ ADDR11 a ⇒ λaddr11: True.
    615661              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
     
    622668            | _ ⇒ λother: False. ⊥
    623669            ] (subaddressing_modein … addr)
    624       | ACALL addr ⇒
    625           let s ≝ set_clock s (ticks + clock … s) in
    626           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
     670      | ACALL addr ⇒ λinstr_refl.
     671          let s ≝ set_clock ?? s (ticks + clock … s) in
     672          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    627673            [ ADDR11 a ⇒ λaddr11: True.
    628674              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     
    639685            | _ ⇒ λother: False. ⊥
    640686            ] (subaddressing_modein … addr)
    641         | LCALL addr ⇒
    642           let s ≝ set_clock s (ticks + clock … s) in
    643           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with
     687        | LCALL addr ⇒ λinstr_refl.
     688          let s ≝ set_clock ?? s (ticks + clock … s) in
     689          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
    644690            [ ADDR16 a ⇒ λaddr16: True.
    645691              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     
    653699            | _ ⇒ λother: False. ⊥
    654700            ] (subaddressing_modein … addr)
    655         ]. (*10s*)
    656     [||||||||*:try assumption]
     701        ] (refl … instr). (*10s*)
     702  try assumption
     703  [1,2,3,4,5,6,7,8:
     704    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
     705    try //
     706    destruct(INSTR_PC) <instr_refl
     707    #absurd normalize in absurd; try destruct(absurd) try %
     708  |9:
     709   
    657710    [1,2,3,4,5,7: @pi2 (*35s*)
    658     |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] …
     711    |8: cases daemon (*
     712    lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] …
    659713        (λx. λs.
    660714        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    661715        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
    662716        | _ ⇒ λabsd. ⊥
    663         ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H
     717        ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H *)
     718      (*XXX : propagate further *)
     719    |28,48,68,88,108,128: skip
     720    |*:
     721      try assumption
     722       normalize nodelta
     723       try // >clock_set_program_counter %
     724       try // destruct destruct (* XXX: for wilmer! *) >e1
     725       whd in match ASM_classify; normalize nodelta
     726       whd in match current_instruction; normalize nodelta
     727       whd in match current_instruction0; normalize nodelta
     728    [||||||||*:try assumption]
    664729    |*: normalize nodelta try // (*17s*)
    665730        >clock_set_program_counter // (* Andrea:??*) ]
Note: See TracChangeset for help on using the changeset viewer.