Changeset 936 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 10, 2011, 4:20:47 PM (9 years ago)
Author:
sacerdot
Message:

Ticks are now handled correctly everywhere and the main proof takes care of
them.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r928 r936  
    159159include alias "ASM/BitVectorTrie.ma".
    160160
    161 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
     161definition execute_1_preinstruction:
     162 ∀ticks: nat × nat.
     163 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝
     164  λticks.
    162165  λA, M: Type[0].
    163166  λaddr_of: A → (PreStatus M) → Word.
    164167  λinstr: preinstruction A.
    165168  λs: PreStatus M.
     169  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
     170  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
    166171  match instr with
    167172        [ ADD addr1 addr2 ⇒
     173            let s ≝ add_ticks1 s in
    168174            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
    169175                                                   (get_arg_8 ? s false addr2) false in
     
    174180              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    175181        | ADDC addr1 addr2 ⇒
     182            let s ≝ add_ticks1 s in
    176183            let old_cy_flag ≝ get_cy_flag ? s in
    177184            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1)
     
    183190              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    184191        | SUBB addr1 addr2 ⇒
     192            let s ≝ add_ticks1 s in
    185193            let old_cy_flag ≝ get_cy_flag ? s in
    186194            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1)
     
    192200              set_flags ? s cy_flag (Some Bit ac_flag) ov_flag
    193201        | ANL addr ⇒
     202          let s ≝ add_ticks1 s in
    194203          match addr with
    195204            [ inl l ⇒
     
    210219            ]
    211220        | ORL addr ⇒
     221          let s ≝ add_ticks1 s in
    212222          match addr with
    213223            [ inl l ⇒
     
    228238            ]
    229239        | XRL addr ⇒
     240          let s ≝ add_ticks1 s in
    230241          match addr with
    231242            [ inl l' ⇒
     
    239250            ]
    240251        | INC addr ⇒
     252            let s ≝ add_ticks1 s in
    241253            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
    242254                                                           registr;
     
    264276              ] (subaddressing_modein … addr)
    265277        | DEC addr ⇒
     278           let s ≝ add_ticks1 s in
    266279           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in
    267280             set_arg_8 ? s addr result
    268281        | MUL addr1 addr2 ⇒
     282           let s ≝ add_ticks1 s in
    269283           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
    270284           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
     
    276290             set_8051_sfr ? s SFR_ACC_B high
    277291        | DIV addr1 addr2 ⇒
     292           let s ≝ add_ticks1 s in
    278293           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in
    279294           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in
     
    288303               ]
    289304        | DA addr ⇒
     305            let s ≝ add_ticks1 s in
    290306            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    291307              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then
     
    303319                s
    304320        | CLR addr ⇒
     321          let s ≝ add_ticks1 s in
    305322          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    306323            [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8)
     
    310327            ] (subaddressing_modein … addr)
    311328        | CPL addr ⇒
     329          let s ≝ add_ticks1 s in
    312330          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    313331            [ ACC_A ⇒ λacc_a: True.
     
    325343            | _ ⇒ λother: False. ?
    326344            ] (subaddressing_modein … addr)
    327         | SETB b ⇒ set_arg_1 ? s b false
     345        | SETB b ⇒
     346            let s ≝ add_ticks1 s in
     347            set_arg_1 ? s b false
    328348        | RL _ ⇒ (* DPM: always ACC_A *)
     349            let s ≝ add_ticks1 s in
    329350            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    330351            let new_acc ≝ rotate_left … 1 old_acc in
    331352              set_8051_sfr ? s SFR_ACC_A new_acc
    332353        | RR _ ⇒ (* DPM: always ACC_A *)
     354            let s ≝ add_ticks1 s in
    333355            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    334356            let new_acc ≝ rotate_right … 1 old_acc in
    335357              set_8051_sfr ? s SFR_ACC_A new_acc
    336358        | RLC _ ⇒ (* DPM: always ACC_A *)
     359            let s ≝ add_ticks1 s in
    337360            let old_cy_flag ≝ get_cy_flag ? s in
    338361            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     
    342365              set_8051_sfr ? s SFR_ACC_A new_acc
    343366        | RRC _ ⇒ (* DPM: always ACC_A *)
     367            let s ≝ add_ticks1 s in
    344368            let old_cy_flag ≝ get_cy_flag ? s in
    345369            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     
    349373              set_8051_sfr ? s SFR_ACC_A new_acc
    350374        | SWAP _ ⇒ (* DPM: always ACC_A *)
     375            let s ≝ add_ticks1 s in
    351376            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    352377            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     
    354379              set_8051_sfr ? s SFR_ACC_A new_acc
    355380        | PUSH addr ⇒
     381            let s ≝ add_ticks1 s in
    356382            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
    357383              [ DIRECT d ⇒ λdirect: True.
     
    362388              ] (subaddressing_modein … addr)
    363389        | POP addr ⇒
     390            let s ≝ add_ticks1 s in
    364391            let contents ≝ read_at_stack_pointer ? s in
    365392            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
     
    367394              set_arg_8 ? s addr contents
    368395        | XCH addr1 addr2 ⇒
     396            let s ≝ add_ticks1 s in
    369397            let old_addr ≝ get_arg_8 ? s false addr2 in
    370398            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
     
    372400              set_arg_8 ? s addr2 old_acc
    373401        | XCHD addr1 addr2 ⇒
     402            let s ≝ add_ticks1 s in
    374403            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
    375404            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in
     
    379408              set_arg_8 ? s addr2 new_arg
    380409        | RET ⇒
     410            let s ≝ add_ticks1 s in
    381411            let high_bits ≝ read_at_stack_pointer ? s in
    382412            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
     
    388418              set_program_counter ? s new_pc
    389419        | RETI ⇒
     420            let s ≝ add_ticks1 s in
    390421            let high_bits ≝ read_at_stack_pointer ? s in
    391422            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in
     
    397428              set_program_counter ? s new_pc
    398429        | MOVX addr ⇒
     430          let s ≝ add_ticks1 s in
    399431          (* DPM: only copies --- doesn't affect I/O *)
    400432          match addr with
     
    407439            ]
    408440        | MOV addr ⇒
     441          let s ≝ add_ticks1 s in
    409442          match addr with
    410443            [ inl l ⇒
     
    441474          | JC addr ⇒
    442475                  if get_cy_flag ? s then
    443                       set_program_counter ? s (addr_of addr s)
     476                   let s ≝ add_ticks1 s in
     477                    set_program_counter ? s (addr_of addr s)
    444478                  else
     479                   let s ≝ add_ticks2 s in
    445480                    s
    446481            | JNC addr ⇒
    447482                  if ¬(get_cy_flag ? s) then
    448                       set_program_counter ? s (addr_of addr s)
     483                   let s ≝ add_ticks1 s in
     484                    set_program_counter ? s (addr_of addr s)
    449485                  else
     486                   let s ≝ add_ticks2 s in
    450487                    s
    451488            | JB addr1 addr2 ⇒
    452489                  if get_arg_1 ? s addr1 false then
    453                       set_program_counter ? s (addr_of addr2 s)
     490                   let s ≝ add_ticks1 s in
     491                    set_program_counter ? s (addr_of addr2 s)
    454492                  else
     493                   let s ≝ add_ticks2 s in
    455494                    s
    456495            | JNB addr1 addr2 ⇒
    457496                  if ¬(get_arg_1 ? s addr1 false) then
    458                       set_program_counter ? s (addr_of addr2 s)
     497                   let s ≝ add_ticks1 s in
     498                    set_program_counter ? s (addr_of addr2 s)
    459499                  else
     500                   let s ≝ add_ticks2 s in
    460501                    s
    461502            | JBC addr1 addr2 ⇒
    462503                  let s ≝ set_arg_1 ? s addr1 false in
    463504                    if get_arg_1 ? s addr1 false then
    464                         set_program_counter ? s (addr_of addr2 s)
     505                     let s ≝ add_ticks1 s in
     506                      set_program_counter ? s (addr_of addr2 s)
    465507                    else
     508                     let s ≝ add_ticks2 s in
    466509                      s
    467510            | JZ addr ⇒
    468511                    if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then
    469                         set_program_counter ? s (addr_of addr s)
     512                     let s ≝ add_ticks1 s in
     513                      set_program_counter ? s (addr_of addr s)
    470514                    else
     515                     let s ≝ add_ticks2 s in
    471516                      s
    472517            | JNZ addr ⇒
    473518                    if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then
    474                         set_program_counter ? s (addr_of addr s)
     519                     let s ≝ add_ticks1 s in
     520                      set_program_counter ? s (addr_of addr s)
    475521                    else
     522                     let s ≝ add_ticks2 s in
    476523                      s
    477524            | CJNE addr1 addr2 ⇒
     
    482529                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
    483530                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     531                            let s ≝ add_ticks1 s in
    484532                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    485533                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    486534                          else
     535                            let s ≝ add_ticks2 s in
    487536                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    488537                    | inr r' ⇒
     
    491540                                                 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in
    492541                          if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then
     542                            let s ≝ add_ticks1 s in
    493543                            let s ≝ set_program_counter ? s (addr_of addr2 s) in
    494544                              set_flags ? s new_cy (None ?) (get_ov_flag ? s)
    495545                          else
     546                            let s ≝ add_ticks2 s in
    496547                            (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
    497548                    ]
     
    500551              let s ≝ set_arg_8 ? s addr1 result in
    501552                if ¬(eq_bv ? result (zero 8)) then
    502                     set_program_counter ? s (addr_of addr2 s)
     553                 let s ≝ add_ticks1 s in
     554                  set_program_counter ? s (addr_of addr2 s)
    503555                else
     556                 let s ≝ add_ticks2 s in
    504557                  s
    505         | NOP ⇒ s
     558        | NOP ⇒
     559           let s ≝ add_ticks2 s in
     560            s
    506561        ].
    507562    try assumption
     
    517572    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    518573    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    519     let s ≝ set_clock ? s (clock ? s + ticks) in
    520574    let s ≝ set_program_counter ? s pc in
    521575    let s ≝
    522576      match instr with
    523       [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ?
     577      [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
    524578        (λx. λs.
    525579        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
     
    528582        ] (subaddressing_modein … x)) instr s
    529583      | ACALL addr ⇒
     584          let s ≝ set_clock ? s (ticks + clock ? s) in
    530585          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    531586            [ ADDR11 a ⇒ λaddr11: True.
     
    544599            ] (subaddressing_modein … addr)
    545600        | LCALL addr ⇒
     601          let s ≝ set_clock ? s (ticks + clock ? s) in
    546602          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    547603            [ ADDR16 a ⇒ λaddr16: True.
     
    557613            ] (subaddressing_modein … addr)
    558614        | MOVC addr1 addr2 ⇒
     615          let s ≝ set_clock ? s (ticks + clock ? s) in
    559616          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
    560617            [ ACC_DPTR ⇒ λacc_dptr: True.
     
    576633            ] (subaddressing_modein … addr2)
    577634        | JMP _ ⇒ (* DPM: always indirect_dptr *)
     635          let s ≝ set_clock ? s (ticks + clock ? s) in
    578636          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    579637          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
     
    582640            set_program_counter ? s new_pc
    583641        | LJMP addr ⇒
     642          let s ≝ set_clock ? s (ticks + clock ? s) in
    584643          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    585644            [ ADDR16 a ⇒ λaddr16: True.
     
    588647            ] (subaddressing_modein … addr)
    589648        | SJMP addr ⇒
     649          let s ≝ set_clock ? s (ticks + clock ? s) in
    590650          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    591651            [ RELATIVE r ⇒ λrelative: True.
     
    595655            ] (subaddressing_modein … addr)
    596656        | AJMP addr ⇒
     657          let s ≝ set_clock ? s (ticks + clock ? s) in
    597658          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    598659            [ ADDR11 a ⇒ λaddr11: True.
     
    666727    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
    667728
    668 definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
     729definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
    669730  λticks_of.
    670731  λs.
    671732  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    672733  let ticks ≝ ticks_of (program_counter ? s) in
    673   let s ≝ set_clock ? s (clock ? s + ticks) in
    674734  let s ≝ set_program_counter ? s pc in
    675735  let s ≝
    676736    match instr with
    677     [ Instruction instr ⇒ execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
    678     | Comment cmt ⇒ s
     737    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s
     738    | Comment cmt ⇒
     739       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
     740        s
    679741    | Cost cst ⇒ s
    680     | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
     742    | Jmp jmp ⇒
     743       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
     744        set_program_counter ? s (address_of_word_labels s jmp)
    681745    | Call call ⇒
     746      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    682747      let a ≝ address_of_word_labels s call in
    683748      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     
    690755        set_program_counter ? s a
    691756    | Mov dptr ident ⇒
     757      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
    692758      let preamble ≝ \fst (code_memory ? s) in
    693759      let data_labels ≝ construct_datalabels preamble in
     
    706772    ].
    707773
    708 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat) (s: PseudoStatus) on n: PseudoStatus ≝
     774let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
    709775  match n with
    710776    [ O ⇒ s
Note: See TracChangeset for help on using the changeset viewer.