Changeset 2705 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Feb 22, 2013, 5:56:31 PM (7 years ago)
Author:
sacerdot
Message:

More progress in ASM towards implementing the new pseudoinstructions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2504 r2705  
    184184              | _ ⇒ λother: False. ⊥
    185185              ] (subaddressing_modein … addr)
     186        | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
     187          let s ≝ add_ticks1 s in
     188          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
     189          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
     190          let jmp_addr ≝ add … big_acc dptr in
     191          let new_pc ≝ add … (program_counter … s) jmp_addr in
     192            set_program_counter … s new_pc
    186193        | NOP ⇒ λinstr_refl.
    187            let s ≝ add_ticks2 s in
     194           let s ≝ add_ticks1 s in
    188195            s
    189196        | DEC addr ⇒ λinstr_refl.
     
    604611              | _ ⇒ λother: False. ⊥
    605612              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
     613        | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
     614          let s ≝ add_ticks1 s in
     615          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
     616          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
     617          let jmp_addr ≝ add … big_acc dptr in
     618          let new_pc ≝ add … (program_counter … s) jmp_addr in
     619            set_program_counter … s new_pc
    606620        | NOP ⇒ λinstr_refl.
    607621           let s ≝ add_ticks2 s in
     
    938952    try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
    939953    try (change with (cl_return = cl_other → ?) #absurd destruct(absurd))
     954    try (change with (cl_call = cl_other → ?) #absurd destruct(absurd))
    940955    try (@or_introl //)
    941956    try (@or_intror //)
     
    10451060            | _ ⇒ λother: False. ⊥
    10461061            ] (subaddressing_modein … addr2)
    1047       | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
    1048           let s ≝ set_clock ?? s (ticks + clock … s) in
    1049           let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    1050           let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    1051           let jmp_addr ≝ add … big_acc dptr in
    1052           let new_pc ≝ add … (program_counter … s) jmp_addr in
    1053             set_program_counter … s new_pc
    10541062      | LJMP addr ⇒ λinstr_refl.
    10551063          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
     
    10981106        ] (refl … instr). (*10s*)
    10991107  try assumption
    1100   [1,2,3,4,5,6,7,8:
     1108  [1,2,3,4,5,6,7:
    11011109    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
    11021110    try //
     
    11101118      /demod by clock_set_program_counter/ /demod nohyps/ %
    11111119    ]
    1112   |9:
     1120  |8:
    11131121    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
    11141122        (λx. λs.
     
    11901198       let s ≝ set_clock … s (\fst ticks + clock … s) in
    11911199        set_program_counter … s (address_of_word_labels (\snd cm) jmp)
     1200    | Jnz acc dst1 dst2 ⇒
     1201       if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
     1202        let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     1203         set_program_counter … s (address_of_word_labels (\snd cm) dst1)
     1204       else
     1205        let s ≝ set_clock ?? s (\snd ticks + clock … s) in
     1206         set_program_counter … s (address_of_word_labels (\snd cm) dst2)
     1207    | MovSuccessor dst ws lbl ⇒
     1208      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     1209      let addr ≝ address_of_word_labels (\snd cm) lbl in
     1210      let 〈high, low〉 ≝ vsplit ? 8 8 addr in
     1211      let v ≝ match ws with [ HIGH ⇒ high | LOW ⇒ low ] in
     1212       set_arg_8 … s dst v     
    11921213    | Call call ⇒
    11931214      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
     
    12091230  in
    12101231    s.
    1211   normalize
    1212   @I
     1232  [2: % | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    12131233qed.
    12141234
Note: See TracChangeset for help on using the changeset viewer.