Changeset 820 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 20, 2011, 6:09:00 PM (9 years ago)
Author:
mulligan
Message:

changes to get the semantics of pseudoassembly working

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r757 r820  
    158158include alias "ASM/BitVectorTrie.ma".
    159159
    160 definition execute_1: Status → Status ≝
     160definition execute_1_preinstruction: ∀A: Type[0]. (A → Byte) → preinstruction A → Status → Status ≝
     161  λA: Type[0].
     162  λaddr_of: A → Byte.
     163  λinstr: preinstruction A.
    161164  λs: Status.
    162     let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in
    163     let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    164     let s ≝ set_clock s (clock s + ticks) in
    165     let s ≝ set_program_counter s pc in
    166     let s ≝
    167       match instr with
     165  match instr with
    168166        [ ADD addr1 addr2 ⇒
    169167            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
     
    397395            let new_pc ≝ high_bits @@ low_bits in
    398396              set_program_counter s new_pc
    399         | JMP _ ⇒ (* DPM: always indirect_dptr *)
    400           let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    401           let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    402           let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    403           let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
    404             set_program_counter s new_pc
    405         | LJMP addr ⇒
    406           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    407             [ ADDR16 a ⇒ λaddr16: True.
    408                 set_program_counter s a
    409             | _ ⇒ λother: False. ⊥
    410             ] (subaddressing_modein … addr)
    411         | SJMP addr ⇒
    412           match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    413             [ RELATIVE r ⇒ λrelative: True.
    414                 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    415                   set_program_counter s new_pc
    416             | _ ⇒ λother: False. ⊥
    417             ] (subaddressing_modein … addr)
    418         | AJMP addr ⇒
    419           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    420             [ ADDR11 a ⇒ λaddr11: True.
    421               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    422               let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
    423               let bit ≝ get_index' ? O ? nl in
    424               let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
    425               let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    426               let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
    427                 set_program_counter s new_pc
    428             | _ ⇒ λother: False. ⊥
    429             ] (subaddressing_modein … addr)
    430397        | MOVX addr ⇒
    431398          (* DPM: only copies --- doesn't affect I/O *)
     
    471438                set_arg_1 s addr1 (get_arg_1 s addr2 false)
    472439            ]
    473         | LCALL addr ⇒
    474           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    475             [ ADDR16 a ⇒ λaddr16: True.
    476               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    477               let s ≝ set_8051_sfr s SFR_SP new_sp in
    478               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    479               let s ≝ write_at_stack_pointer s pc_bl in
    480               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    481               let s ≝ set_8051_sfr s SFR_SP new_sp in
    482               let s ≝ write_at_stack_pointer s pc_bu in
    483                 set_program_counter s a
    484             | _ ⇒ λother: False. ⊥
    485             ] (subaddressing_modein … addr)
    486         | ACALL addr ⇒
    487           match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    488             [ ADDR11 a ⇒ λaddr11: True.
    489               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    490               let s ≝ set_8051_sfr s SFR_SP new_sp in
    491               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    492               let s ≝ write_at_stack_pointer s pc_bl in
    493               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    494               let s ≝ set_8051_sfr s SFR_SP new_sp in
    495               let s ≝ write_at_stack_pointer s pc_bu in
    496               let 〈thr, eig〉 ≝ split ? 3 8 a in
    497               let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
    498               let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    499                 set_program_counter s new_addr
    500             | _ ⇒ λother: False. ⊥
    501             ] (subaddressing_modein … addr)
    502         | Jump j ⇒
    503           match j with
    504             [ JC addr ⇒
    505               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    506                 [ RELATIVE r ⇒ λrel: True.
     440          | JC addr ⇒
     441              let r ≝ addr_of addr in
    507442                  if get_cy_flag s then
    508443                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    510445                  else
    511446                    s
    512                 | _ ⇒ λother: False. ⊥
    513                 ] (subaddressing_modein … addr)
    514447            | JNC addr ⇒
    515               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    516                 [ RELATIVE r ⇒ λrel: True.
     448              let r ≝ addr_of addr in
    517449                  if ¬(get_cy_flag s) then
    518450                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    520452                  else
    521453                    s
    522                 | _ ⇒ λother: False. ⊥
    523                 ] (subaddressing_modein … addr)
    524454            | JB addr1 addr2 ⇒
    525               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    526                 [ RELATIVE r ⇒ λrel: True.
     455              let r ≝ addr_of addr2 in
    527456                  if get_arg_1 s addr1 false then
    528457                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    530459                  else
    531460                    s
    532                 | _ ⇒ λother: False. ⊥
    533                 ] (subaddressing_modein … addr2)
    534461            | JNB addr1 addr2 ⇒
    535               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    536                 [ RELATIVE r ⇒ λrel: True.
     462              let r ≝ addr_of addr2 in
    537463                  if ¬(get_arg_1 s addr1 false) then
    538464                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    540466                  else
    541467                    s
    542                 | _ ⇒ λother: False. ⊥
    543                 ] (subaddressing_modein … addr2)
    544468            | JBC addr1 addr2 ⇒
    545               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    546                 [ RELATIVE r ⇒ λrel: True.
     469              let r ≝ addr_of addr2 in
    547470                  let s ≝ set_arg_1 s addr1 false in
    548471                    if get_arg_1 s addr1 false then
     
    551474                    else
    552475                      s
    553                 | _ ⇒ λother: False. ⊥
    554                 ] (subaddressing_modein … addr2)
    555476            | JZ addr ⇒
    556               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    557                 [ RELATIVE r ⇒ λrel: True.
     477              let r ≝ addr_of addr in
    558478                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
    559479                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    561481                    else
    562482                      s
    563                 | _ ⇒ λother: False. ⊥
    564                 ] (subaddressing_modein … addr)
    565483            | JNZ addr ⇒
    566               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    567                 [ RELATIVE r ⇒ λrel: True.
     484              let r ≝ addr_of addr in
    568485                    if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
    569486                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     
    571488                    else
    572489                      s
    573                 | _ ⇒ λother: False. ⊥
    574                 ] (subaddressing_modein … addr)
    575490            | CJNE addr1 addr2 ⇒
    576               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    577                 [ RELATIVE r ⇒ λrelative: True.
     491              let r ≝ addr_of addr2 in
    578492                  match addr1 with
    579493                    [ inl l ⇒
     
    598512                            (set_flags s new_cy (None ?) (get_ov_flag s))
    599513                    ]
    600                 | _ ⇒ λother: False. ⊥
    601                 ] (subaddressing_modein … addr2)
    602514            | DJNZ addr1 addr2 ⇒
    603               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    604                 [ RELATIVE r ⇒ λrel: True.
    605                     let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
    606                     let s ≝ set_arg_8 s addr1 result in
    607                       if ¬(eq_bv ? result (zero 8)) then
    608                         let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    609                           set_program_counter s new_pc
    610                       else
    611                         s
    612                 | _ ⇒ λother: False. ⊥
    613                 ] (subaddressing_modein … addr2)
    614             ]
     515              let r ≝ addr_of addr2 in
     516              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
     517              let s ≝ set_arg_8 s addr1 result in
     518                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
     521                else
     522                  s
     523        | NOP ⇒ s
     524        ].
     525    try assumption
     526    try (
     527      normalize
     528      repeat (@ (le_S_S))
     529      @ (le_O_n)
     530    )
     531    try (
     532      @ (execute_1_technical … (subaddressing_modein …))
     533      @ I
     534    )
     535    try (
     536      normalize
     537      @ I
     538    )
     539qed.
     540
     541definition execute_1: Status → Status ≝
     542  λs: Status.
     543    let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in
     544    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
     545    let s ≝ set_clock s (clock s + ticks) in
     546    let s ≝ set_program_counter s pc in
     547    let s ≝
     548      match instr with
     549      [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]]
     550        (λx.
     551        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
     552        [ RELATIVE r ⇒ λ_. r
     553        | _ ⇒ λabsd. ⊥
     554        ] (subaddressing_modein … x)) instr s
     555      | ACALL addr ⇒
     556          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     557            [ ADDR11 a ⇒ λaddr11: True.
     558              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     559              let s ≝ set_8051_sfr s SFR_SP new_sp in
     560              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     561              let s ≝ write_at_stack_pointer s pc_bl in
     562              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     563              let s ≝ set_8051_sfr s SFR_SP new_sp in
     564              let s ≝ write_at_stack_pointer s pc_bu in
     565              let 〈thr, eig〉 ≝ split ? 3 8 a in
     566              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
     567              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
     568                set_program_counter s new_addr
     569            | _ ⇒ λother: False. ⊥
     570            ] (subaddressing_modein … addr)
     571        | LCALL addr ⇒
     572          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     573            [ ADDR16 a ⇒ λaddr16: True.
     574              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     575              let s ≝ set_8051_sfr s SFR_SP new_sp in
     576              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     577              let s ≝ write_at_stack_pointer s pc_bl in
     578              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     579              let s ≝ set_8051_sfr s SFR_SP new_sp in
     580              let s ≝ write_at_stack_pointer s pc_bu in
     581                set_program_counter s a
     582            | _ ⇒ λother: False. ⊥
     583            ] (subaddressing_modein … addr)
    615584        | MOVC addr1 addr2 ⇒
    616585          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
     
    632601            | _ ⇒ λother: False. ⊥
    633602            ] (subaddressing_modein … addr2)
    634         | NOP ⇒ s
    635         ]
     603        | JMP _ ⇒ (* DPM: always indirect_dptr *)
     604          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     605          let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     606          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
     607          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
     608            set_program_counter s new_pc
     609        | LJMP addr ⇒
     610          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
     611            [ ADDR16 a ⇒ λaddr16: True.
     612                set_program_counter s a
     613            | _ ⇒ λother: False. ⊥
     614            ] (subaddressing_modein … addr)
     615        | SJMP addr ⇒
     616          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     617            [ RELATIVE r ⇒ λrelative: True.
     618                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     619                  set_program_counter s new_pc
     620            | _ ⇒ λother: False. ⊥
     621            ] (subaddressing_modein … addr)
     622        | AJMP addr ⇒
     623          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
     624            [ ADDR11 a ⇒ λaddr11: True.
     625              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     626              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
     627              let bit ≝ get_index' ? O ? nl in
     628              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
     629              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
     630              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
     631                set_program_counter s new_pc
     632            | _ ⇒ λother: False. ⊥
     633            ] (subaddressing_modein … addr)
     634      ]
    636635    in
    637636      s.
     
    652651qed.
    653652
     653axiom fetch_pseudo_instruction:
     654  ∀p: list labelled_instruction.
     655  ∀pc: Word.
     656    (pseudo_instruction × Word) × nat.
     657
     658axiom address_of_labels: Identifier → Byte.
     659axiom address_of_word_labels: Identifier → Word.
     660
     661definition execute_1_pseudo_instruction: pseudo_assembly_program → Status → Status ≝
     662  λp.
     663  λs.
     664  let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction (\snd p) (program_counter s) in
     665  let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
     666  let s ≝ set_clock s (clock s + ticks) in
     667  let s ≝ set_program_counter s pc in
     668  let s ≝
     669    match instr with
     670    [ Instruction instr ⇒ execute_1_preinstruction ? address_of_labels instr s
     671    | Comment cmt ⇒ s
     672    | Cost cst ⇒ s
     673    | Jmp jmp ⇒ set_program_counter s (address_of_word_labels jmp)
     674    | Call call ⇒
     675      let a ≝ address_of_word_labels call in
     676      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     677      let s ≝ set_8051_sfr s SFR_SP new_sp in
     678      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     679      let s ≝ write_at_stack_pointer s pc_bl in
     680      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
     681      let s ≝ set_8051_sfr s SFR_SP new_sp in
     682      let s ≝ write_at_stack_pointer s pc_bu in
     683        set_program_counter s a
     684    | Mov dptr ident ⇒ set_arg_16 s (get_arg_16 s (DATA16 (address_of_word_labels ident))) dptr
     685    ]
     686  in
     687    s.
     688  normalize
     689  @ I
     690qed.
     691
    654692let rec execute (n: nat) (s: Status) on n: Status ≝
    655693  match n with
     
    657695    | S o ⇒ execute o (execute_1 s)
    658696    ].
     697
     698let rec execute_pseudo_instruction (n: nat) (p: pseudo_assembly_program) (s: Status) on n: Status ≝
     699  match n with
     700    [ O ⇒ s
     701    | S o ⇒ execute_pseudo_instruction o p (execute_1_pseudo_instruction p s)
     702    ].
Note: See TracChangeset for help on using the changeset viewer.