Changeset 712 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Mar 28, 2011, 5:40:51 PM (9 years ago)
Author:
mulligan
Message:

Changes to get things to typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r698 r712  
    154154 ]
    155155qed.
    156    
     156
     157include alias "arithmetics/nat.ma".
     158
    157159definition execute_1: Status → Status ≝
    158160  λs: Status.
     
    170172            let ov_flag ≝ get_index' ? 2 ? flags in
    171173            let s ≝ set_arg_8 s ACC_A result in
    172               set_flags s cy_flag (Some Bit ac_flag) ov_flag
     174              set_flags s cy_flag (Some Bit ac_flag) ov_flag   
    173175        | ADDC addr1 addr2 ⇒
    174176            let old_cy_flag ≝ get_cy_flag s in
     
    394396            let new_pc ≝ high_bits @@ low_bits in
    395397              set_program_counter s new_pc
    396         | Jump j ⇒
    397           match j with
    398             [ JC addr ⇒
    399               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    400                 [ RELATIVE r ⇒ λrel: True.
    401                   if get_cy_flag s then
    402                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    403                       set_program_counter s new_pc
    404                   else
    405                     s
    406                 | _ ⇒ λother: False. ⊥
    407                 ] (subaddressing_modein … addr)
    408             | JNC addr ⇒
    409               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    410                 [ RELATIVE r ⇒ λrel: True.
    411                   if ¬(get_cy_flag s) then
    412                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    413                       set_program_counter s new_pc
    414                   else
    415                     s
    416                 | _ ⇒ λother: False. ⊥
    417                 ] (subaddressing_modein … addr)
    418             | JB addr1 addr2 ⇒
    419               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    420                 [ RELATIVE r ⇒ λrel: True.
    421                   if get_arg_1 s addr1 false then
    422                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    423                       set_program_counter s new_pc
    424                   else
    425                     s
    426                 | _ ⇒ λother: False. ⊥
    427                 ] (subaddressing_modein … addr2)
    428             | JNB addr1 addr2 ⇒
    429               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    430                 [ RELATIVE r ⇒ λrel: True.
    431                   if ¬(get_arg_1 s addr1 false) then
    432                     let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    433                       set_program_counter s new_pc
    434                   else
    435                     s
    436                 | _ ⇒ λother: False. ⊥
    437                 ] (subaddressing_modein … addr2)
    438             | JBC addr1 addr2 ⇒
    439               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    440                 [ RELATIVE r ⇒ λrel: True.
    441                   let s ≝ set_arg_1 s addr1 false in
    442                     if get_arg_1 s addr1 false then
    443                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    444                         set_program_counter s new_pc
    445                     else
    446                       s
    447                 | _ ⇒ λother: False. ⊥
    448                 ] (subaddressing_modein … addr2)
    449             | JZ addr ⇒
    450               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    451                 [ RELATIVE r ⇒ λrel: True.
    452                     if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
    453                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    454                         set_program_counter s new_pc
    455                     else
    456                       s
    457                 | _ ⇒ λother: False. ⊥
    458                 ] (subaddressing_modein … addr)
    459             | JNZ addr ⇒
    460               match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    461                 [ RELATIVE r ⇒ λrel: True.
    462                     if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
    463                       let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    464                         set_program_counter s new_pc
    465                     else
    466                       s
    467                 | _ ⇒ λother: False. ⊥
    468                 ] (subaddressing_modein … addr)
    469             | CJNE addr1 addr2 ⇒
    470               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    471                 [ RELATIVE r ⇒ λrelative: True.
    472                   match addr1 with
    473                     [ inl l ⇒
    474                         let 〈addr1, addr2〉 ≝ l in
    475                         let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
    476                                                  (nat_of_bitvector ? (get_arg_8 s false addr2)) in
    477                           if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
    478                             let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    479                             let s ≝ set_program_counter s new_pc in
    480                               set_flags s new_cy (None ?) (get_ov_flag s)
    481                           else
    482                             (set_flags s new_cy (None ?) (get_ov_flag s))
    483                     | inr r' ⇒
    484                         let 〈addr1, addr2〉 ≝ r' in
    485                         let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
    486                                                  (nat_of_bitvector ? (get_arg_8 s false addr2)) in
    487                           if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
    488                             let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    489                             let s ≝ set_program_counter s new_pc in
    490                               set_flags s new_cy (None ?) (get_ov_flag s)
    491                           else
    492                             (set_flags s new_cy (None ?) (get_ov_flag s))
    493                     ]
    494                 | _ ⇒ λother: False. ⊥
    495                 ] (subaddressing_modein … addr2)
    496             | DJNZ addr1 addr2 ⇒
    497               match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    498                 [ RELATIVE r ⇒ λrel: True.
    499                     let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
    500                     let s ≝ set_arg_8 s addr1 result in
    501                       if ¬(eq_bv ? result (zero 8)) then
    502                         let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    503                           set_program_counter s new_pc
    504                       else
    505                         s
    506                 | _ ⇒ λother: False. ⊥
    507                 ] (subaddressing_modein … addr2)
    508             ]
    509398        | JMP _ ⇒ (* DPM: always indirect_dptr *)
    510399          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     
    629518            | _ ⇒ λother: False. ⊥
    630519            ] (subaddressing_modein … addr)
     520        | Jump j ⇒
     521          match j with
     522            [ JC addr ⇒
     523              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     524                [ RELATIVE r ⇒ λrel: True.
     525                  if get_cy_flag s then
     526                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     527                      set_program_counter s new_pc
     528                  else
     529                    s
     530                | _ ⇒ λother: False. ⊥
     531                ] (subaddressing_modein … addr)
     532            | JNC addr ⇒
     533              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     534                [ RELATIVE r ⇒ λrel: True.
     535                  if ¬(get_cy_flag s) then
     536                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     537                      set_program_counter s new_pc
     538                  else
     539                    s
     540                | _ ⇒ λother: False. ⊥
     541                ] (subaddressing_modein … addr)
     542            | JB addr1 addr2 ⇒
     543              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     544                [ RELATIVE r ⇒ λrel: True.
     545                  if get_arg_1 s addr1 false then
     546                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     547                      set_program_counter s new_pc
     548                  else
     549                    s
     550                | _ ⇒ λother: False. ⊥
     551                ] (subaddressing_modein … addr2)
     552            | JNB addr1 addr2 ⇒
     553              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     554                [ RELATIVE r ⇒ λrel: True.
     555                  if ¬(get_arg_1 s addr1 false) then
     556                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     557                      set_program_counter s new_pc
     558                  else
     559                    s
     560                | _ ⇒ λother: False. ⊥
     561                ] (subaddressing_modein … addr2)
     562            | JBC addr1 addr2 ⇒
     563              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     564                [ RELATIVE r ⇒ λrel: True.
     565                  let s ≝ set_arg_1 s addr1 false in
     566                    if get_arg_1 s addr1 false then
     567                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     568                        set_program_counter s new_pc
     569                    else
     570                      s
     571                | _ ⇒ λother: False. ⊥
     572                ] (subaddressing_modein … addr2)
     573            | JZ addr ⇒
     574              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     575                [ RELATIVE r ⇒ λrel: True.
     576                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
     577                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     578                        set_program_counter s new_pc
     579                    else
     580                      s
     581                | _ ⇒ λother: False. ⊥
     582                ] (subaddressing_modein … addr)
     583            | JNZ addr ⇒
     584              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     585                [ RELATIVE r ⇒ λrel: True.
     586                    if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
     587                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     588                        set_program_counter s new_pc
     589                    else
     590                      s
     591                | _ ⇒ λother: False. ⊥
     592                ] (subaddressing_modein … addr)
     593            | CJNE addr1 addr2 ⇒
     594              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     595                [ RELATIVE r ⇒ λrelative: True.
     596                  match addr1 with
     597                    [ inl l ⇒
     598                        let 〈addr1, addr2〉 ≝ l in
     599                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
     600                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
     601                          if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
     602                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     603                            let s ≝ set_program_counter s new_pc in
     604                              set_flags s new_cy (None ?) (get_ov_flag s)
     605                          else
     606                            (set_flags s new_cy (None ?) (get_ov_flag s))
     607                    | inr r' ⇒
     608                        let 〈addr1, addr2〉 ≝ r' in
     609                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 s false addr1))
     610                                                 (nat_of_bitvector ? (get_arg_8 s false addr2)) in
     611                          if ¬(eq_bv ? (get_arg_8 s false addr1) (get_arg_8 s false addr2)) then
     612                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     613                            let s ≝ set_program_counter s new_pc in
     614                              set_flags s new_cy (None ?) (get_ov_flag s)
     615                          else
     616                            (set_flags s new_cy (None ?) (get_ov_flag s))
     617                    ]
     618                | _ ⇒ λother: False. ⊥
     619                ] (subaddressing_modein … addr2)
     620            | DJNZ addr1 addr2 ⇒
     621              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
     622                [ RELATIVE r ⇒ λrel: True.
     623                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
     624                    let s ≝ set_arg_8 s addr1 result in
     625                      if ¬(eq_bv ? result (zero 8)) then
     626                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
     627                          set_program_counter s new_pc
     628                      else
     629                        s
     630                | _ ⇒ λother: False. ⊥
     631                ] (subaddressing_modein … addr2)
     632            ]
    631633        | NOP ⇒ s
    632634        ]
Note: See TracChangeset for help on using the changeset viewer.