Changeset 2760 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Mar 2, 2013, 1:29:41 AM (8 years ago)
Author:
sacerdot
Message:
  1. Many files repaired.
  2. 3 new daemons: 2 in Assembly.ma, 1 in StructuredTraces?.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2756 r2760  
    11931193  let s ≝
    11941194    match instr with
    1195     [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (\snd cm) x) instr s
     1195    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (code cm) x) instr s
    11961196    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    11971197    | Cost cst ⇒ s
    11981198    | Jmp jmp ⇒
    11991199       let s ≝ set_clock … s (\fst ticks + clock … s) in
    1200         set_program_counter … s (address_of_word_labels (\snd cm) jmp)
     1200        set_program_counter … s (address_of_word_labels (code cm) jmp)
    12011201    | Jnz acc dst1 dst2 ⇒
    12021202       if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
    12031203        let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1204          set_program_counter … s (address_of_word_labels (\snd cm) dst1)
     1204         set_program_counter … s (address_of_word_labels (code cm) dst1)
    12051205       else
    12061206        let s ≝ set_clock ?? s (\snd ticks + clock … s) in
    1207          set_program_counter … s (address_of_word_labels (\snd cm) dst2)
     1207         set_program_counter … s (address_of_word_labels (code cm) dst2)
    12081208    | MovSuccessor dst ws lbl ⇒
    12091209      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1210       let addr ≝ address_of_word_labels (\snd cm) lbl in
     1210      let addr ≝ address_of_word_labels (code cm) lbl in
    12111211      let 〈high, low〉 ≝ vsplit ? 8 8 addr in
    12121212      let v ≝ match ws with [ HIGH ⇒ high | LOW ⇒ low ] in
     
    12141214    | Call call ⇒
    12151215      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1216       let a ≝ address_of_word_labels (\snd cm) call in
     1216      let a ≝ address_of_word_labels (code cm) call in
    12171217      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    12181218      let s ≝ set_8051_sfr … s SFR_SP new_sp in
     
    12251225    | Mov dptr ident ⇒
    12261226      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1227       let the_preamble ≝ \fst cm in
     1227      let the_preamble ≝ preamble cm in
    12281228      let data_labels ≝ construct_datalabels the_preamble in
    12291229        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
     
    12351235
    12361236definition execute_1_pseudo_instruction:
    1237  ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |\snd cm| → nat × nat) → ∀s:PseudoStatus cm.
    1238    nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
     1237 ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |code cm| → nat × nat) → ∀s:PseudoStatus cm.
     1238   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|code cm| →
    12391239    PseudoStatus cm
    12401240
    12411241  λcm,ticks_of,s,pc_ok.
    1242   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
     1242  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (code cm) (program_counter … s) pc_ok in
    12431243  let ticks ≝ ticks_of (program_counter … s) pc_ok in
    12441244   execute_1_pseudo_instruction0 ticks cm s instr pc.
Note: See TracChangeset for help on using the changeset viewer.