Changeset 1709


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

Changes to the execution of the MOVC instruction

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1697 r1709  
    331331qed.
    332332
     333(* XXX: todo *)
    333334lemma subaddressing_mode_elim':
    334335  ∀T: Type[2].
     
    349350qed.
    350351
     352(* XXX: todo *)
    351353axiom subaddressing_mode_elim:
    352354  ∀T: Type[2].
     
    360362    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    361363      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    362 
    363 definition current_instruction0 ≝
    364   λcode_memory: BitVectorTrie Byte 16.
    365   λprogram_counter: Word.
    366     \fst (\fst (fetch … code_memory program_counter)).
    367 
    368 definition current_instruction ≝
    369   λcode_memory.
    370   λs: Status code_memory.
    371     current_instruction0 code_memory (program_counter … s).
    372 
    373 definition ASM_classify0: instruction → status_class ≝
    374   λi: instruction.
    375   match i with
    376    [ RealInstruction pre ⇒
    377      match pre with
    378       [ RET ⇒ cl_return
    379       | JZ _ ⇒ cl_jump
    380       | JNZ _ ⇒ cl_jump
    381       | JC _ ⇒ cl_jump
    382       | JNC _ ⇒ cl_jump
    383       | JB _ _ ⇒ cl_jump
    384       | JNB _ _ ⇒ cl_jump
    385       | JBC _ _ ⇒ cl_jump
    386       | CJNE _ _ ⇒ cl_jump
    387       | DJNZ _ _ ⇒ cl_jump
    388       | _ ⇒ cl_other
    389       ]
    390    | ACALL _ ⇒ cl_call
    391    | LCALL _ ⇒ cl_call
    392    | JMP _ ⇒ cl_call
    393    | AJMP _ ⇒ cl_jump
    394    | LJMP _ ⇒ cl_jump
    395    | SJMP _ ⇒ cl_jump
    396    | _ ⇒ cl_other
    397    ].
    398 
    399 definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
    400   λcode_memory.
    401   λs: Status code_memory.
    402     ASM_classify0 (current_instruction … s).
    403364
    404365definition current_instruction_is_labelled ≝
     
    505466
    506467(* XXX: indexing bug *)
    507 example fetch_twice_fetch_execute_1:
     468lemma fetch_twice_fetch_execute_1:
    508469  ∀code_memory: BitVectorTrie Byte 16.
    509470  ∀start_status: Status code_memory.
     471    ASM_classify code_memory start_status = cl_other →
    510472    \snd (\fst (fetch code_memory (program_counter … start_status))) =
    511473      program_counter … (execute_1 … start_status).
    512   cases daemon
    513 qed.
     474  #code_memory #start_status #classify_assm
     475  whd in match execute_1; normalize nodelta
     476  whd in match execute_1'; normalize nodelta
     477  whd in match execute_1_0; normalize nodelta
     478  generalize in match (refl … (fetch code_memory
     479    (program_counter (BitVectorTrie Byte 16) code_memory start_status)));
     480  cases (fetch code_memory
     481    (program_counter (BitVectorTrie Byte 16) code_memory start_status)) in ⊢ (??%? → ?);
     482  #instr_pc #ticks #fetch_rewrite <fetch_rewrite
     483  cases
     484qed-.
    514485
    515486lemma reachable_program_counter_to_0_lt_total_program_size:
  • 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:??*) ]
  • src/common/StructuredTraces.ma

    r1658 r1709  
    77| cl_jump   : status_class
    88| cl_call   : status_class
    9 | cl_other : status_class
    10 .
     9| cl_other : status_class.
    1110
    1211record abstract_status : Type[1] ≝ {
  • src/joint/semantics_paolo.ma

    r1643 r1709  
    177177  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    178178  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    179   OK … (set_m … m (set_sp … isp st)).
     179  OK … (set_m … m (set_isp … isp st)).
    180180
    181181definition pop: ∀p. state p → res (state p × beval) ≝
     
    183183  let isp ≝ isp ? st in
    184184  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    185   let ist ≝ set_sp … isp st in
     185  let ist ≝ set_isp … isp st in
    186186  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    187187  OK ? 〈st,v〉.
Note: See TracChangeset for help on using the changeset viewer.