Changeset 757 for src/ASM


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (10 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

Location:
src/ASM
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r722 r757  
    2222| ADDR16: Word → addressing_mode.
    2323
     24(* dpm: renamed register to registr to avoid clash with brian's types *)
    2425inductive addressing_mode_tag : Type[0] ≝
    2526  direct: addressing_mode_tag
    2627| indirect: addressing_mode_tag
    2728| ext_indirect: addressing_mode_tag
    28 | register: addressing_mode_tag
     29| registr: addressing_mode_tag
    2930| acc_a: addressing_mode_tag
    3031| acc_b: addressing_mode_tag
     
    4950      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
    5051      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
    51       | register ⇒ match b with [ register ⇒ true | _ ⇒ false ]
     52      | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
    5253      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
    5354      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
     
    7374   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
    7475   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
    75    | register ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
     76   | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
    7677   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
    7778   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
     
    120121| JNZ: A → jump A
    121122| CJNE:
    122    [[acc_a]] × [[direct; data]] ⊎ [[register; indirect]] × [[data]] → A → jump A
    123 | DJNZ: [[register ; direct]] → A → jump A.
     123   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → jump A
     124| DJNZ: [[registr ; direct]] → A → jump A.
    124125
    125126inductive preinstruction (A: Type[0]) : Type[0] ≝
    126   ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    127 | ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    128 | SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    129 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] → preinstruction A
    130 | DEC: [[ acc_a ; register ; direct ; indirect ]] → preinstruction A
     127  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     128| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     129| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     130| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
     131| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
    131132| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
    132133| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
     
    135136 (* logical operations *)
    136137| ANL:
    137    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
     138   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
    138139   [[direct]] × [[ acc_a ; data ]] ⊎
    139140   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
    140141| ORL:
    141    [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
     142   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
    142143   [[direct]] × [[ acc_a ; data ]] ⊎
    143144   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
    144145| XRL:
    145    [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
     146   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
    146147   [[direct]] × [[ acc_a ; data ]] → preinstruction A
    147148| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
     
    155156 (* data transfer *)
    156157| MOV:
    157     [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
    158     [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
    159     [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
     158    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
     159    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
     160    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
    160161    [[dptr]] × [[data16]] ⊎
    161162    [[carry]] × [[bit_addr]] ⊎
     
    168169| PUSH: [[direct]] → preinstruction A
    169170| POP: [[direct]] → preinstruction A
    170 | XCH: [[acc_a]] → [[ register ; direct ; indirect ]] → preinstruction A
     171| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
    171172| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
    172173
  • src/ASM/Assembly.ma

    r719 r757  
    1515      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    1616  | ADD addr1 addr2 ⇒
    17      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     17     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    1818      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
    1919      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
     
    2222      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    2323  | ADDC addr1 addr2 ⇒
    24      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     24     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    2525      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
    2626      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
     
    3838      [ inl addrs ⇒ match addrs with
    3939         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    40            match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     40           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    4141            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
    4242            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
     
    8080     [ ([[true; true; false; true; false; true; false; false]]) ]
    8181  | DEC addr ⇒
    82      match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
     82     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
    8383      [ ACC_A ⇒ λ_.
    8484         [ ([[false; false; false; true; false; true; false; false]]) ]
     
    9999           [ RELATIVE b2 ⇒ λ_. b2
    100100           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    101          match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
     101         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
    102102          [ REGISTER r ⇒ λ_.
    103103             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
     
    170170               [ DATA b2 ⇒ λ_. b2
    171171               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    172              match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → list Byte with
     172             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
    173173              [ REGISTER r⇒ λ_.
    174174                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
     
    177177              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
    178178  | INC addr ⇒
    179      match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
     179     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
    180180      [ ACC_A ⇒ λ_.
    181181         [ ([[false;false;false;false;false;true;false;false]]) ]         
     
    214214                     match addrs with
    215215                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    216                          match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     216                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    217217                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
    218218                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
     
    221221                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    222222                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    223                          match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
     223                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
    224224                          [ REGISTER r ⇒ λ_.
    225225                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
     
    240240                       [ DIRECT b1 ⇒ λ_. b1
    241241                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
    242                      match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
     242                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
    243243                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
    244244                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
     
    295295         match addrs with
    296296          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    297              match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
     297             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
    298298             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
    299299             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
     
    354354      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    355355  | SUBB addr1 addr2 ⇒
    356      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     356     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    357357      [ REGISTER r ⇒ λ_.
    358358         [ ([[true;false;false;true;true]]) @@ r ]
     
    367367     [ ([[true;true;false;false;false;true;false;false]]) ]
    368368  | XCH addr1 addr2 ⇒
    369      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
     369     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
    370370      [ REGISTER r ⇒ λ_.
    371371         [ ([[true;true;false;false;true]]) @@ r ]
     
    383383     match addrs with
    384384      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    385          match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
     385         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
    386386          [ REGISTER r ⇒ λ_.
    387387             [ ([[false;true;true;false;true]]) @@ r ]
  • src/ASM/I8051.ma

    r746 r757  
    140140definition RegisterSPH ≝ Register07.
    141141
    142 definition register_address: Register → [[ acc_a; direct; register ]] ≝
     142definition register_address: Register → [[ acc_a; direct; registr ]] ≝
    143143  λr: Register.
    144144    match r with
  • src/ASM/Interpret.ma

    r712 r757  
    156156
    157157include alias "arithmetics/nat.ma".
     158include alias "ASM/BitVectorTrie.ma".
    158159
    159160definition execute_1: Status → Status ≝
     
    172173            let ov_flag ≝ get_index' ? 2 ? flags in
    173174            let s ≝ set_arg_8 s ACC_A result in
    174               set_flags s cy_flag (Some Bit ac_flag) ov_flag   
     175              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    175176        | ADDC addr1 addr2 ⇒
    176177            let old_cy_flag ≝ get_cy_flag s in
     
    240241        | INC addr ⇒
    241242            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
    242                                                            register;
     243                                                           registr;
    243244                                                           direct;
    244245                                                           indirect;
     
    427428            | _ ⇒ λother: False. ⊥
    428429            ] (subaddressing_modein … addr)
    429         | MOVC addr1 addr2 ⇒
    430           match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
    431             [ ACC_DPTR ⇒ λacc_dptr: True.
    432               let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    433               let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    434               let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
    435               let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    436                 set_8051_sfr s SFR_ACC_A result
    437             | ACC_PC ⇒ λacc_pc: True.
    438               let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    439               let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
    440               (* DPM: Under specified: does the carry from PC incrementation affect the *)
    441               (*      addition of the PC with the DPTR? At the moment, no.              *)
    442               let s ≝ set_program_counter s inc_pc in
    443               let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
    444               let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    445                 set_8051_sfr s SFR_ACC_A result
    446             | _ ⇒ λother: False. ⊥
    447             ] (subaddressing_modein … addr2)
    448430        | MOVX addr ⇒
    449431          (* DPM: only copies --- doesn't affect I/O *)
     
    631613                ] (subaddressing_modein … addr2)
    632614            ]
     615        | MOVC addr1 addr2 ⇒
     616          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
     617            [ ACC_DPTR ⇒ λacc_dptr: True.
     618              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     619              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     620              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
     621              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
     622                set_8051_sfr s SFR_ACC_A result
     623            | ACC_PC ⇒ λacc_pc: True.
     624              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     625              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
     626              (* DPM: Under specified: does the carry from PC incrementation affect the *)
     627              (*      addition of the PC with the DPTR? At the moment, no.              *)
     628              let s ≝ set_program_counter s inc_pc in
     629              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
     630              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
     631                set_8051_sfr s SFR_ACC_A result
     632            | _ ⇒ λother: False. ⊥
     633            ] (subaddressing_modein … addr2)
    633634        | NOP ⇒ s
    634635        ]
  • src/ASM/Status.ma

    r705 r757  
    755755      ] (subaddressing_modein … a).
    756756     
    757 definition get_arg_8: Status → bool → [[ direct ; indirect ; register ;
     757definition get_arg_8: Status → bool → [[ direct ; indirect ; registr ;
    758758                                          acc_a ; acc_b ; data ; acc_dptr ;
    759759                                          acc_pc ; ext_indirect ;
    760760                                          ext_indirect_dptr ]] → Byte ≝
    761761  λs, l, a.
    762     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
     762    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    763763                                                acc_a ; acc_b ; data ; acc_dptr ;
    764764                                                acc_pc ; ext_indirect ;
     
    820820qed.
    821821
    822 definition set_arg_8: Status → [[ direct ; indirect ; register ;
     822definition set_arg_8: Status → [[ direct ; indirect ; registr ;
    823823                                   acc_a ; acc_b ; ext_indirect ;
    824824                                   ext_indirect_dptr ]] → Byte → Status ≝
    825825  λs, a, v.
    826     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
     826    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    827827                                                acc_a ; acc_b ; ext_indirect ;
    828828                                                ext_indirect_dptr ]] x) → ? with
Note: See TracChangeset for help on using the changeset viewer.