Changeset 822 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 23, 2011, 4:22:13 PM (9 years ago)
Author:
mulligan
Message:

removed all axioms

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r821 r822  
    158158include alias "ASM/BitVectorTrie.ma".
    159159
    160 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → Byte) → preinstruction A → PreStatus M → PreStatus M ≝
     160definition execute_1_preinstruction: ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
    161161  λA, M: Type[0].
    162   λaddr_of: A → Byte.
     162  λaddr_of: A → (PreStatus M) → Word.
    163163  λinstr: preinstruction A.
    164164  λs: PreStatus M.
     
    205205            | inr r ⇒
    206206              let 〈addr1, addr2〉 ≝ r in
    207               let and_val ≝ (get_cy_flag ? s) ∧ (get_arg_1 ? s addr2 true) in
     207              let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in
    208208                set_flags ? s and_val (None ?) (get_ov_flag ? s)
    209209            ]
     
    439439            ]
    440440          | JC addr ⇒
    441               let r ≝ addr_of addr in
    442441                  if get_cy_flag ? s then
    443                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    444                       set_program_counter ? s new_pc
     442                      set_program_counter ? s (addr_of addr s)
    445443                  else
    446444                    s
    447445            | JNC addr ⇒
    448               let r ≝ addr_of addr in
    449446                  if ¬(get_cy_flag ? s) then
    450                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    451                       set_program_counter ? s new_pc
     447                      set_program_counter ? s (addr_of addr s)
    452448                  else
    453449                    s
    454450            | JB addr1 addr2 ⇒
    455               let r ≝ addr_of addr2 in
    456451                  if get_arg_1 ? s addr1 false then
    457                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    458                       set_program_counter ? s new_pc
     452                      set_program_counter ? s (addr_of addr2 s)
    459453                  else
    460454                    s
    461455            | JNB addr1 addr2 ⇒
    462               let r ≝ addr_of addr2 in
    463456                  if ¬(get_arg_1 ? s addr1 false) then
    464                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    465                       set_program_counter ? s new_pc
     457                      set_program_counter ? s (addr_of addr2 s)
    466458                  else
    467459                    s
    468460            | JBC addr1 addr2 ⇒
    469               let r ≝ addr_of addr2 in
    470461                  let s ≝ set_arg_1 ? s addr1 false in
    471462                    if get_arg_1 ? s addr1 false then
    472                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    473                         set_program_counter ? s new_pc
     463                        set_program_counter ? s (addr_of addr2 s)
    474464                    else
    475465                      s
    476466            | JZ addr ⇒
    477               let r ≝ addr_of addr in
    478467                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
    479                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    480                         set_program_counter ? s new_pc
     468                        set_program_counter ? s (addr_of addr s)
    481469                    else
    482470                      s
    483471            | JNZ addr ⇒
    484               let r ≝ addr_of addr in
    485472                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
    486                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    487                         set_program_counter ? s new_pc
     473                        set_program_counter ? s (addr_of addr s)
    488474                    else
    489475                      s
    490476            | CJNE addr1 addr2 ⇒
    491               let r ≝ addr_of addr2 in
    492477                  match addr1 with
    493478                    [ inl l ⇒
    494                         let 〈addr1, addr2〉 ≝ l in
     479                        let 〈addr1, addr2'〉 ≝ l in
    495480                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
    496                                                  (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in
    497                           if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then
    498                             let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    499                             let s ≝ set_program_counter ? s new_pc in
     481                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
     482                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     483                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    500484                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    501485                          else
    502486                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    503487                    | inr r' ⇒
    504                         let 〈addr1, addr2〉 ≝ r' in
     488                        let 〈addr1, addr2'〉 ≝ r' in
    505489                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1))
    506                                                  (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in
    507                           if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then
    508                             let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    509                             let s ≝ set_program_counter ? s new_pc in
     490                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
     491                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     492                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    510493                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    511494                          else
     
    513496                    ]
    514497            | DJNZ addr1 addr2 ⇒
    515               let r ≝ addr_of addr2 in
    516498              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in
    517499              let s ≝ set_arg_8 ? s addr1 result in
    518500                if ¬(eq_bv ? result (zero 8)) then
    519                   let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
    520                     set_program_counter ? s new_pc
     501                    set_program_counter ? s (addr_of addr2 s)
    521502                else
    522503                  s
     
    548529      match instr with
    549530      [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ?
    550         (λx.
     531        (λx. λs.
    551532        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
    552         [ RELATIVE r ⇒ λ_. r
     533        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
    553534        | _ ⇒ λabsd. ⊥
    554535        ] (subaddressing_modein … x)) instr s
     
    651632qed.
    652633
    653 axiom fetch_pseudo_instruction:
    654   ∀ps: PseudoStatus.
    655   ∀pc: Word.
    656     (pseudo_instruction × Word) × nat.
    657 
    658 axiom address_of_labels: Identifier → Byte.
    659 axiom address_of_word_labels: Identifier → Word.
    660 
    661 definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus ≝
     634definition fetch_pseudo_instruction: PseudoStatus → Word → (Word → nat) → ((pseudo_instruction × Word) × nat) ≝
     635  λps: PseudoStatus.
     636  λpc: Word.
     637  λticks_of: Word → nat.
     638    let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … (code_memory ? ps) ? in
     639    let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
     640      〈〈instr, new_pc〉, ticks_of pc〉.
     641    cases not_implemented.
     642qed.
     643
     644let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
     645  match l with
     646  [ nil ⇒ ?
     647  | cons hd tl ⇒
     648    if pred hd then
     649      acc
     650    else
     651      index_of_internal A pred tl (S acc)
     652  ].
     653  cases not_implemented.
     654qed.
     655
     656definition index_of ≝
     657  λA.
     658  λeq.
     659  λl.
     660    index_of_internal A eq l 0.
     661
     662definition address_of_word_labels_internal ≝
     663  λy: Identifier.
     664  λx: labelled_instruction.
     665    match \fst x with
     666    [ None ⇒ false
     667    | Some x ⇒ eq_bv ? x y
     668    ].
     669
     670definition address_of_word_labels ≝
     671  λps: PseudoStatus.
     672  λid: Identifier.
     673    bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) (code_memory ? ps)).
     674
     675definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
     676  λticks_of.
    662677  λs.
    663   let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) in
     678  let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) ticks_of in
    664679  let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    665680  let s ≝ set_clock ? s (clock ? s + ticks) in
     
    667682  let s ≝
    668683    match instr with
    669     [ Instruction instr ⇒ execute_1_preinstruction … address_of_labels instr s
     684    [ Instruction instr ⇒ execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
    670685    | Comment cmt ⇒ s
    671686    | Cost cst ⇒ s
    672     | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels jmp)
     687    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
    673688    | Call call ⇒
    674       let a ≝ address_of_word_labels call in
     689      let a ≝ address_of_word_labels s call in
    675690      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    676691      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     
    681696      let s ≝ write_at_stack_pointer ? s pc_bu in
    682697        set_program_counter ? s a
    683     | Mov dptr ident ⇒ set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels ident))) dptr
     698    | Mov dptr ident ⇒ set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
    684699    ]
    685700  in
     
    695710    ].
    696711
    697 let rec execute_pseudo_instruction (n: nat) (s: PseudoStatus) on n: PseudoStatus ≝
     712let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat) (s: PseudoStatus) on n: PseudoStatus ≝
    698713  match n with
    699714    [ O ⇒ s
    700     | S o ⇒ execute_pseudo_instruction o (execute_1_pseudo_instruction s)
     715    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
    701716    ].
Note: See TracChangeset for help on using the changeset viewer.