Changeset 712


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

Changes to get things to typecheck.

Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r698 r712  
    7575qed.
    7676
    77 definition add_8_with_carry ≝ add_n_with_carry 8.
    78 definition add_16_with_carry ≝ add_n_with_carry 16.
    79 definition sub_8_with_carry ≝ sub_n_with_carry 8.
    80 definition sub_16_with_carry ≝ sub_n_with_carry 16.
     77definition add_8_with_carry ≝
     78  λb, c: BitVector 8.
     79  λcarry: bool.
     80  add_n_with_carry 8 b c carry ?.
     81  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
     82qed.
     83
     84definition add_16_with_carry ≝
     85  λb, c: BitVector 16.
     86  λcarry: bool.
     87  add_n_with_carry 16 b c carry ?.
     88  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
     89  @le_S @le_S @le_n (* ugly: fix using tacticals *)
     90qed.
     91
     92definition sub_8_with_carry ≝
     93  λb, c: BitVector 8.
     94  λcarry: bool.
     95  sub_n_with_carry 8 b c carry ?.
     96  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
     97qed.
     98
     99definition sub_16_with_carry ≝
     100  λb, c: BitVector 16.
     101  λcarry: bool.
     102  sub_n_with_carry 16 b c carry ?.
     103  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
     104  @le_S @le_S @le_n (* ugly: fix using tacticals *)
     105qed.
    81106
    82107definition increment ≝
  • src/ASM/Fetch.ma

    r706 r712  
    22include "ASM/Arithmetic.ma".
    33include "ASM/ASM.ma".
    4 
    5 include "basics/types.ma".
    64
    75definition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝
  • 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        ]
  • src/ASM/Util.ma

    r704 r712  
    1 include "arithmetics/nat.ma".
    21include "basics/list.ma".
    32include "basics/types.ma".
     3include "arithmetics/nat.ma".
    44
    55let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
     
    4343definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
    4444
    45 let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝
    46 match l with
    47 [ nil ⇒ r
    48 | cons h t ⇒ revapp T t (h::r)
    49 ].
    50 
    51 definition rev ≝ λT:Type[0].λl. revapp T l [ ].
    52 
    5345lemma eq_rect_Type0_r :
    5446  ∀A: Type[0].
     
    10597        ]
    10698    ].
    107 
     99   
    108100definition ltb ≝
    109101  λm, n: nat.
     
    118110    leb n m.
    119111
     112(* dpm: conflicts with library definitions
    120113interpretation "Nat less than" 'lt m n = (ltb m n).
    121114interpretation "Nat greater than" 'gt m n = (gtb m n).
    122115interpretation "Nat greater than eq" 'geq m n = (geb m n).
     116*)
    123117
    124118let rec division_aux (m: nat) (n : nat) (p: nat) ≝
Note: See TracChangeset for help on using the changeset viewer.