Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/LIN/LINToASM.ma

    r757 r1153  
    3333    match instr with
    3434    [ joint_st_sequential instr' _ ⇒
    35         match instr' with
    36         [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37         | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    38         | _ ⇒ set_empty ?
    39         ]
     35      match instr' with
     36      [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     37      | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     38      | _ ⇒ set_empty ?
     39      ]
     40    | joint_st_return ⇒ set_empty ?
    4041    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    41     | joint_st_return ⇒ set_empty ?
    42     ] in
     42    ]
     43  in
    4344  match label with
    4445  [ None ⇒ generated
     
    8889  λstatement: pre_lin_statement globals_old.
    8990  match statement with
    90   [ joint_st_return ⇒ Instruction (RET ?)
    91   | joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     91  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     92  | joint_st_return ⇒ Instruction (RET ?)
    9293  | 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      match instr with
     95      [ joint_instr_comment comment ⇒ Comment comment
     96      | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
     97      | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
     98      | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
     99      | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
     100      | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
     101      | joint_instr_opaccs accs ⇒
     102        match accs with
     103        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
     104        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
     105        ]
     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 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 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 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 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 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 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 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 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 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        Instruction (JNZ ? (word_of_identifier ? lbl))
     239      | joint_instr_set_carry ⇒
     240        Instruction (SETB ? CARRY)
    105241      ]
    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))
    239     ]
    240   ].
     242    ].
    241243  try assumption
    242244  try @ I
     
    312314definition globals_addr_internal ≝
    313315  λres_offset.
    314   λx_size: Identifier × nat.
     316  λx_size: ident × nat.
    315317    let 〈res, offset〉 ≝ res_offset in
    316318    let 〈x, size〉 ≝ x_size in
Note: See TracChangeset for help on using the changeset viewer.