Changeset 2283 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jul 31, 2012, 6:11:27 PM (8 years ago)
Author:
mulligan
Message:

Work from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2280 r2283  
    162162              [ ACC_A ⇒ λacc_a: True.
    163163                let s' ≝ add_ticks1 s in
    164                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
     164                let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
    165165                 set_arg_8 … s' ACC_A result
    166166              | REGISTER r ⇒ λregister: True.
    167167                let s' ≝ add_ticks1 s in
    168                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     168                let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    169169                 set_arg_8 … s' (REGISTER r) result
    170170              | DIRECT d ⇒ λdirect: True.
    171171                let s' ≝ add_ticks1 s in
    172                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     172                let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    173173                 set_arg_8 … s' (DIRECT d) result
    174174              | INDIRECT i ⇒ λindirect: True.
    175175                let s' ≝ add_ticks1 s in
    176                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     176                let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    177177                 set_arg_8 … s' (INDIRECT i) result
    178178              | DPTR ⇒ λdptr: True.
    179179                let s' ≝ add_ticks1 s in
    180                 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
    181                 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
     180                let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
     181                let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
    182182                let s ≝ set_8051_sfr … s' SFR_DPL bl in
    183183                 set_8051_sfr … s' SFR_DPH bu
     
    222222                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    223223                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    224                     let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     224                    let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in
    225225                    let new_acc ≝ nu @@ acc_nl' in
    226226                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
     
    582582              [ ACC_A ⇒ λacc_a: True. λEQaddr.
    583583                let s' ≝ add_ticks1 s in
    584                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
     584                let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
    585585                 set_arg_8 … s' ACC_A result
    586586              | REGISTER r ⇒ λregister: True. λEQaddr.
    587587                let s' ≝ add_ticks1 s in
    588                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
     588                let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
    589589                 set_arg_8 … s' (REGISTER r) result
    590590              | DIRECT d ⇒ λdirect: True. λEQaddr.
    591591                let s' ≝ add_ticks1 s in
    592                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
     592                let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
    593593                 set_arg_8 … s' (DIRECT d) result
    594594              | INDIRECT i ⇒ λindirect: True. λEQaddr.
    595595                let s' ≝ add_ticks1 s in
    596                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
     596                let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
    597597                 set_arg_8 … s' (INDIRECT i) result
    598598              | DPTR ⇒ λdptr: True. λEQaddr.
    599599                let s' ≝ add_ticks1 s in
    600                 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
    601                 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
     600                let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
     601                let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
    602602                let s ≝ set_8051_sfr … s' SFR_DPL bl in
    603603                 set_8051_sfr … s' SFR_DPH bu
     
    642642                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    643643                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    644                     let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     644                    let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in
    645645                    let new_acc ≝ nu @@ acc_nl' in
    646646                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
     
    721721              [ DIRECT d ⇒ λdirect: True. λEQaddr.
    722722                let s ≝ add_ticks1 s in
    723                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     723                let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    724724                let s ≝ set_8051_sfr … s SFR_SP new_sp in
    725725                  write_at_stack_pointer ?? s (get_arg_8 ?? s false (DIRECT … d))
     
    969969        match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
    970970        [ RELATIVE r ⇒ λrelative: True.
    971           let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in
    972             new_pc
     971            add … program_counter (sign_extension r)
    973972        | _ ⇒ λother: False. ⊥
    974973        ] (subaddressing_modein … addr)
     
    10341033              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    10351034              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    1036               let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
     1035              let new_addr ≝ add … dptr big_acc in
    10371036              let result ≝ lookup ? ? new_addr cm (zero ?) in
    10381037                set_8051_sfr … s SFR_ACC_A result
     
    10411040              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    10421041              (*      addition of the PC with the DPTR? At the moment, no.              *)
    1043               let 〈carry, new_addr〉 ≝ half_add ? (program_counter … s) big_acc in
     1042              let new_addr ≝ add … (program_counter … s) big_acc in
    10441043              let result ≝ lookup ? ? new_addr cm (zero ?) in
    10451044                set_8051_sfr … s SFR_ACC_A result
     
    10501049          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    10511050          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
    1052           let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    1053           let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in
     1051          let jmp_addr ≝ add … big_acc dptr in
     1052          let new_pc ≝ add … (program_counter … s) jmp_addr in
    10541053            set_program_counter … s new_pc
    10551054      | LJMP addr ⇒ λinstr_refl.
     
    10691068          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    10701069            [ ADDR11 a ⇒ λaddr11: True.
    1071               «let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1070              «let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10721071              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10731072              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    10741073              let s ≝ write_at_stack_pointer … s pc_bl in
    1075               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1074              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10761075              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10771076              let s ≝ write_at_stack_pointer … s pc_bu in
     
    10871086            [ ADDR16 a ⇒ λaddr16: True.
    10881087              «
    1089               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1088              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10901089              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10911090              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    10921091              let s ≝ write_at_stack_pointer … s pc_bl in
    1093               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1092              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10941093              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10951094              let s ≝ write_at_stack_pointer … s pc_bu in
     
    11051104    try (#absurd normalize in absurd; try destruct(absurd) try %)
    11061105    @pair_elim #carry #new_sp #carry_new_sp_refl
    1107     @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl
    1108     @pair_elim #carry' #new_sp' #carry_new_sp_refl'
    11091106    [2:
    11101107      /demod nohyps/ %
     
    11961193      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    11971194      let a ≝ address_of_word_labels (\snd cm) call in
    1198       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1195      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    11991196      let s ≝ set_8051_sfr … s SFR_SP new_sp in
    12001197      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    12011198      let s ≝ write_at_stack_pointer … s pc_bl in
    1202       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1199      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    12031200      let s ≝ set_8051_sfr … s SFR_SP new_sp in
    12041201      let s ≝ write_at_stack_pointer … s pc_bu in
Note: See TracChangeset for help on using the changeset viewer.