Changeset 1112 for src/LIN


Ignore:
Timestamp:
Aug 24, 2011, 7:08:49 PM (8 years ago)
Author:
mulligan
Message:

got lin > asm stuff working

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r757 r1112  
    3232  let generated ≝
    3333    match instr with
    34     [ joint_st_sequential instr' _ ⇒
     34    [ lin_st_lift l ⇒
     35      match l with
     36      [ joint_st_sequential instr' _ ⇒
    3537        match instr' with
    3638        [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     
    3840        | _ ⇒ set_empty ?
    3941        ]
    40     | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    41     | joint_st_return ⇒ set_empty ?
    42     ] in
     42      | joint_st_return ⇒ set_empty ?
     43      ]
     44    | lin_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     45    ]
     46  in
    4347  match label with
    4448  [ None ⇒ generated
     
    8892  λstatement: pre_lin_statement globals_old.
    8993  match statement with
    90   [ joint_st_return ⇒ Instruction (RET ?)
    91   | joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
    92   | joint_st_sequential instr _ ⇒
    93     match instr with
    94     [ joint_instr_comment comment ⇒ Comment comment
    95     | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
    96     | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
    97     | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
    98     | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    99     | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
    100     | joint_instr_opaccs accs ⇒
    101       match accs with
    102       [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    103       | Divu ⇒ Instruction (DIV ? ACC_A ACC_B)
    104       | Modu ⇒ ?
     94  [ lin_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     95  | lin_st_lift l ⇒
     96    match l with
     97    [ joint_st_return ⇒ Instruction (RET ?)
     98    | joint_st_sequential instr _ ⇒
     99      match instr with
     100      [ joint_instr_comment comment ⇒ Comment comment
     101      | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
     102      | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
     103      | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
     104      | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
     105      | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
     106      | joint_instr_opaccs accs ⇒
     107        match accs with
     108        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
     109        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
     110        ]
     111      | joint_instr_op1 op1 ⇒
     112        match op1 with
     113        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     114        | Inc ⇒ Instruction (INC ? ACC_A)
     115        ]
     116      | joint_instr_op2 op2 reg ⇒
     117        match op2 with
     118        [ Add ⇒
     119          let reg' ≝ register_address reg in
     120          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     121                                                         direct;
     122                                                         registr ]] x) → ? with
     123          [ ACC_A ⇒ λacc_a: True.
     124            Instruction (ADD ? ACC_A accumulator_address)
     125          | DIRECT d ⇒ λdirect1: True.
     126            Instruction (ADD ? ACC_A (DIRECT d))
     127          | REGISTER r ⇒ λregister1: True.
     128            Instruction (ADD ? ACC_A (REGISTER r))
     129          | _ ⇒ λother: False. ⊥
     130          ] (subaddressing_modein … reg')
     131        | Addc ⇒
     132          let reg' ≝ register_address reg in
     133          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     134                                                         direct;
     135                                                         registr ]] x) → ? with
     136          [ ACC_A ⇒ λacc_a: True.
     137            Instruction (ADDC ? ACC_A accumulator_address)
     138          | DIRECT d ⇒ λdirect2: True.
     139            Instruction (ADDC ? ACC_A (DIRECT d))
     140          | REGISTER r ⇒ λregister2: True.
     141            Instruction (ADDC ? ACC_A (REGISTER r))
     142          | _ ⇒ λother: False. ⊥
     143          ] (subaddressing_modein … reg')
     144        | Sub ⇒
     145          let reg' ≝ register_address reg in
     146          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     147                                                         direct;
     148                                                         registr ]] x) → ? with
     149          [ ACC_A ⇒ λacc_a: True.
     150            Instruction (SUBB ? ACC_A accumulator_address)
     151          | DIRECT d ⇒ λdirect3: True.
     152            Instruction (SUBB ? ACC_A (DIRECT d))
     153          | REGISTER r ⇒ λregister3: True.
     154            Instruction (SUBB ? ACC_A (REGISTER r))
     155          | _ ⇒ λother: False. ⊥
     156          ] (subaddressing_modein … reg')
     157        | And ⇒
     158          let reg' ≝ register_address reg in
     159          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     160                                                         direct;
     161                                                         registr ]] x) → ? with
     162          [ ACC_A ⇒ λacc_a: True.
     163            Instruction (NOP ?)
     164          | DIRECT d ⇒ λdirect4: True.
     165            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     166          | REGISTER r ⇒ λregister4: True.
     167            Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     168          | _ ⇒ λother: False. ⊥
     169          ] (subaddressing_modein … reg')
     170        | Or ⇒
     171          let reg' ≝ register_address reg in
     172          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     173                                                         direct;
     174                                                         registr ]] x) → ? with
     175          [ ACC_A ⇒ λacc_a: True.
     176            Instruction (NOP ?)
     177          | DIRECT d ⇒ λdirect5: True.
     178            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     179          | REGISTER r ⇒ λregister5: True.
     180            Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     181          | _ ⇒ λother: False. ⊥
     182          ] (subaddressing_modein … reg')
     183        | Xor ⇒
     184          let reg' ≝ register_address reg in
     185          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     186                                                         direct;
     187                                                         registr ]] x) → ? with
     188          [ ACC_A ⇒ λacc_a: True.
     189            Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
     190          | DIRECT d ⇒ λdirect6: True.
     191            Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
     192          | REGISTER r ⇒ λregister6: True.
     193            Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
     194          | _ ⇒ λother: False. ⊥
     195          ] (subaddressing_modein … reg')
     196        ]
     197      | joint_instr_int reg byte ⇒
     198        let reg' ≝ register_address reg in
     199          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     200                                                         direct;
     201                                                         registr ]] x) → ? with
     202          [ REGISTER r ⇒ λregister7: True.
     203            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
     204          | ACC_A ⇒ λacc: True.
     205            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
     206          | DIRECT d ⇒ λdirect7: True.
     207            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
     208          | _ ⇒ λother: False. ⊥
     209          ] (subaddressing_modein … reg')
     210      | joint_instr_from_acc reg ⇒
     211        let reg' ≝ register_address reg in
     212          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     213                                                         direct;
     214                                                         registr ]] x) → ? with
     215          [ REGISTER r ⇒ λregister8: True.
     216            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
     217          | ACC_A ⇒ λacc: True.
     218            Instruction (NOP ?)
     219          | DIRECT d ⇒ λdirect8: True.
     220            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
     221          | _ ⇒ λother: False. ⊥
     222          ] (subaddressing_modein … reg')
     223      | joint_instr_to_acc reg ⇒
     224        let reg' ≝ register_address reg in
     225          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     226                                                         direct;
     227                                                         registr ]] x) → ? with
     228          [ REGISTER r ⇒ λregister9: True.
     229            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     230          | DIRECT d ⇒ λdirect9: True.
     231            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     232          | ACC_A ⇒ λacc_a: True.
     233            Instruction (NOP ?)
     234          | _ ⇒ λother: False. ⊥
     235          ] (subaddressing_modein … reg')
     236      | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     237      | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     238      | joint_instr_address addr proof ⇒
     239        let look ≝ association addr globals (prf ? proof) in
     240          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     241      | joint_instr_cond_acc lbl ⇒
     242        (* dpm: this should be handled in translate_code! *)
     243        Instruction (JNZ ? (word_of_identifier ? lbl))
     244      | joint_instr_set_carry ⇒
     245        Instruction (SETB ? CARRY)
    105246      ]
    106     | joint_instr_op1 op1 ⇒
    107       match op1 with
    108       [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    109       | Inc ⇒ Instruction (INC ? ACC_A)
    110       ]
    111     | joint_instr_op2 op2 reg ⇒
    112       match op2 with
    113       [ Add ⇒
    114         let reg' ≝ register_address (Register_of_register reg) in
    115         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    116                                                        direct;
    117                                                        registr ]] x) → ? with
    118         [ ACC_A ⇒ λacc_a: True.
    119           Instruction (ADD ? ACC_A accumulator_address)
    120         | DIRECT d ⇒ λdirect1: True.
    121           Instruction (ADD ? ACC_A (DIRECT d))
    122         | REGISTER r ⇒ λregister1: True.
    123           Instruction (ADD ? ACC_A (REGISTER r))
    124         | _ ⇒ λother: False. ⊥
    125         ] (subaddressing_modein … reg')
    126       | Addc ⇒
    127         let reg' ≝ register_address (Register_of_register reg) in
    128         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    129                                                        direct;
    130                                                        registr ]] x) → ? with
    131         [ ACC_A ⇒ λacc_a: True.
    132           Instruction (ADDC ? ACC_A accumulator_address)
    133         | DIRECT d ⇒ λdirect2: True.
    134           Instruction (ADDC ? ACC_A (DIRECT d))
    135         | REGISTER r ⇒ λregister2: True.
    136           Instruction (ADDC ? ACC_A (REGISTER r))
    137         | _ ⇒ λother: False. ⊥
    138         ] (subaddressing_modein … reg')
    139       | Sub ⇒
    140         let reg' ≝ register_address (Register_of_register reg) in
    141         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    142                                                        direct;
    143                                                        registr ]] x) → ? with
    144         [ ACC_A ⇒ λacc_a: True.
    145           Instruction (SUBB ? ACC_A accumulator_address)
    146         | DIRECT d ⇒ λdirect3: True.
    147           Instruction (SUBB ? ACC_A (DIRECT d))
    148         | REGISTER r ⇒ λregister3: True.
    149           Instruction (SUBB ? ACC_A (REGISTER r))
    150         | _ ⇒ λother: False. ⊥
    151         ] (subaddressing_modein … reg')
    152       | And ⇒
    153         let reg' ≝ register_address (Register_of_register reg) in
    154         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    155                                                        direct;
    156                                                        registr ]] x) → ? with
    157         [ ACC_A ⇒ λacc_a: True.
    158           Instruction (NOP ?)
    159         | DIRECT d ⇒ λdirect4: True.
    160           Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    161         | REGISTER r ⇒ λregister4: True.
    162           Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    163         | _ ⇒ λother: False. ⊥
    164         ] (subaddressing_modein … reg')
    165       | Or ⇒
    166         let reg' ≝ register_address (Register_of_register reg) in
    167         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    168                                                        direct;
    169                                                        registr ]] x) → ? with
    170         [ ACC_A ⇒ λacc_a: True.
    171           Instruction (NOP ?)
    172         | DIRECT d ⇒ λdirect5: True.
    173           Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    174         | REGISTER r ⇒ λregister5: True.
    175           Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    176         | _ ⇒ λother: False. ⊥
    177         ] (subaddressing_modein … reg')
    178       | Xor ⇒
    179         let reg' ≝ register_address (Register_of_register reg) in
    180         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    181                                                        direct;
    182                                                        registr ]] x) → ? with
    183         [ ACC_A ⇒ λacc_a: True.
    184           Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
    185         | DIRECT d ⇒ λdirect6: True.
    186           Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
    187         | REGISTER r ⇒ λregister6: True.
    188           Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
    189         | _ ⇒ λother: False. ⊥
    190         ] (subaddressing_modein … reg')
    191       ]
    192     | joint_instr_int reg byte ⇒
    193       let reg' ≝ register_address (Register_of_register reg) in
    194         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    195                                                        direct;
    196                                                        registr ]] x) → ? with
    197         [ REGISTER r ⇒ λregister7: True.
    198           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
    199         | ACC_A ⇒ λacc: True.
    200           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
    201         | DIRECT d ⇒ λdirect7: True.
    202           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
    203         | _ ⇒ λother: False. ⊥
    204         ] (subaddressing_modein … reg')
    205     | joint_instr_from_acc reg ⇒
    206       let reg' ≝ register_address (Register_of_register reg) in
    207         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    208                                                        direct;
    209                                                        registr ]] x) → ? with
    210         [ REGISTER r ⇒ λregister8: True.
    211           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    212         | ACC_A ⇒ λacc: True.
    213           Instruction (NOP ?)
    214         | DIRECT d ⇒ λdirect8: True.
    215           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
    216         | _ ⇒ λother: False. ⊥
    217         ] (subaddressing_modein … reg')
    218     | joint_instr_to_acc reg ⇒
    219       let reg' ≝ register_address (Register_of_register reg) in
    220         match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    221                                                        direct;
    222                                                        registr ]] x) → ? with
    223         [ REGISTER r ⇒ λregister9: True.
    224           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    225         | DIRECT d ⇒ λdirect9: True.
    226           Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    227         | ACC_A ⇒ λacc_a: True.
    228           Instruction (NOP ?)
    229         | _ ⇒ λother: False. ⊥
    230         ] (subaddressing_modein … reg')
    231     | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    232     | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    233     | joint_instr_address addr proof ⇒
    234       let look ≝ association addr globals (prf ? proof) in
    235         Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    236     | joint_instr_cond_acc lbl ⇒
    237       (* dpm: this should be handled in translate_code! *)
    238       WithLabel (JNZ ? (word_of_identifier ? lbl))
    239247    ]
    240248  ].
     
    312320definition globals_addr_internal ≝
    313321  λres_offset.
    314   λx_size: Identifier × nat.
     322  λx_size: ident × nat.
    315323    let 〈res, offset〉 ≝ res_offset in
    316324    let 〈x, size〉 ≝ x_size in
Note: See TracChangeset for help on using the changeset viewer.