Changeset 686


Ignore:
Timestamp:
Mar 18, 2011, 11:22:49 AM (9 years ago)
Author:
mulligan
Message:

Most of LIN completed.

Location:
Deliverables/D4.2-4.3
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/ASM/I8051.ma

    r683 r686  
    11include "arithmetics/nat.ma".
     2include "basics/jmeq.ma".
    23
    34include "cerco/String.ma".
     
    132133definition RegisterSPH ≝ Register07.
    133134
    134 definition register_address: Register → addressing_mode
     135definition register_address: Register → [[ acc_a; direct; register ]]
    135136  λr: Register.
    136137    match r with
     
    144145    | Register07 ⇒ REGISTER [[ true; true; true ]]
    145146    | RegisterA ⇒ ACC_A
    146     | RegisterB ⇒ ACC_B
     147    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
    147148    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
    148149    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
    149     | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
     150    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) 
    150151    ].
     152    [*: normalize
     153        @ I
     154    ]
     155qed.
    151156   
    152157definition registers: list Register ≝
  • Deliverables/D4.2-4.3/LIN/LIN.ma

    r683 r686  
    1414  [ nil ⇒ False
    1515  | cons hd tl ⇒
    16     let 〈id, n〉 ≝ hd in
    17     match eq_i i id with
    18     [ true ⇒ True
    19     | false ⇒ member i eq_i tl
    20     ]
     16      bool_to_Prop (eq_i (fst ? ? hd) i) ∨ member i eq_i tl
    2117  ].
    2218
  • Deliverables/D4.2-4.3/LIN/LinToAsm.ma

    r683 r686  
    22include "cerco-intermediate-languages/utilities/BitVectorTrieSet.ma".
    33include "cerco-intermediate-languages/LIN/LIN.ma".
     4 
     5let rec association (i: Identifier) (l: list (Identifier × nat))
     6                    on l: member i (eq_bv ?) l → nat ≝
     7  match l return λl. member i (eq_bv ?) l → nat with
     8  [ nil ⇒ λabsd. ?
     9  | cons hd tl ⇒
     10    λprf: member i (eq_bv ?) (cons ? hd tl).
     11      (match eq_bv ? (\fst hd) i return λb. eq_bv ? (\fst hd) i = b → nat with
     12      [ true ⇒ λeq_prf. \snd hd
     13      | false ⇒ λeq_prf. association i tl ?
     14      ]) (refl ? (eq_bv ? (\fst hd) i))
     15  ].
     16  [ cases absd
     17  | cases prf
     18    [ > eq_prf
     19      # H
     20      cases H
     21    | # H
     22      assumption
     23    ]
     24  ]
     25qed.
    426
    527definition statement_labels ≝
     
    4668   
    4769definition data_of_int ≝ λbv. DATA bv.
    48 definition data16_of_int ≝ λbv. DATA16 bv.
    49 definition accumulator_address ≝ register_address RegisterA.
     70definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
     71definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
    5072
    5173axiom ImplementedInRuntime: False.
     
    5577  λlin_statement: LINStatement globals.
    5678  match lin_statement with
    57   [ LIN_St_Goto lbl ⇒ Some ? [ Jmp lbl ]
    58   | LIN_St_Label lbl ⇒ Some ? [ Label lbl ]
    59   | LIN_St_Comment _ ⇒ Some ? [ ]
    60   | LIN_St_CostLabel lbl ⇒ Some ? [ Cost lbl ]
    61   | LIN_St_Pop ⇒ Some ? [ Instruction (POP ? accumulator_address) ]
    62   | LIN_St_Push ⇒ Some ? [ Instruction (PUSH ? accumulator_address) ]
    63   | LIN_St_ClearCarry ⇒ Some ? [ Instruction (CLR ? CARRY) ]
    64   | LIN_St_Return ⇒ Some ? [ Instruction (RET ?) ]
    65   | LIN_St_CallId f ⇒ Some ? [ Call f ]
     79  [ LIN_St_Goto lbl ⇒ [ Jmp lbl ]
     80  | LIN_St_Label lbl ⇒ [ Label lbl ]
     81  | LIN_St_Comment _ ⇒ [ ]
     82  | LIN_St_CostLabel lbl ⇒ [ Cost lbl ]
     83  | LIN_St_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
     84  | LIN_St_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
     85  | LIN_St_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
     86  | LIN_St_Return ⇒ [ Instruction (RET ?) ]
     87  | LIN_St_CallId f ⇒ [ Call f ]
    6688  | LIN_St_OpAccs accs ⇒
    6789    match accs with
    68     [ Mul ⇒ Some ? [ Instruction (MUL ? ACC_A ACC_B) ]
    69     | Divu ⇒ Some ? [ Instruction (DIV ? ACC_A ACC_B) ]
     90    [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
     91    | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
    7092    | Modu ⇒ ?
    7193    ]
    7294  | LIN_St_Op1 op1 ⇒
    7395    match op1 with
    74     [ Cmpl ⇒ Some ? [ Instruction (CPL ? ACC_A) ]
    75     | Inc ⇒ Some ? [ Instruction (INC ? ACC_A) ]
     96    [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
     97    | Inc ⇒ [ Instruction (INC ? ACC_A) ]
    7698    ]
    7799  | LIN_St_Op2 op2 reg ⇒
    78100    match op2 with
    79     [ Add ⇒ Some ? [ Instruction (ADD ? ACC_A (register_address reg)) ]
    80     | Addc ⇒ Some ? [ Instruction (ADDC ? ACC_A (register_address reg)) ]
    81     | Sub ⇒ Some ? [ Instruction (SUBB ? ACC_A (register_address reg)) ]
    82     | And ⇒ Some ? [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
    83     | Or ⇒ Some ? [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, (register_address reg)〉))) ]
    84     | Xor ⇒ Some ? [ Instruction (XRL ? (inl ? ? 〈ACC_A, (register_address reg)〉)) ]
     101    [ Add ⇒
     102      let reg' ≝ register_address reg in
     103      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     104                                                     direct;
     105                                                     register ]] x) → ? with
     106      [ ACC_A ⇒ λacc_a: True.
     107        [ Instruction (ADD ? ACC_A accumulator_address) ]
     108      | DIRECT d ⇒ λdirect1: True.
     109        [ Instruction (ADD ? ACC_A (DIRECT d)) ]
     110      | REGISTER r ⇒ λregister1: True.
     111        [ Instruction (ADD ? ACC_A (REGISTER r)) ]
     112      | _ ⇒ λother: False. ⊥
     113      ] (subaddressing_modein … reg')
     114    | Addc ⇒
     115      let reg' ≝ register_address reg in
     116      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     117                                                     direct;
     118                                                     register ]] x) → ? with
     119      [ ACC_A ⇒ λacc_a: True.
     120        [ Instruction (ADDC ? ACC_A accumulator_address) ]
     121      | DIRECT d ⇒ λdirect2: True.
     122        [ Instruction (ADDC ? ACC_A (DIRECT d)) ]
     123      | REGISTER r ⇒ λregister2: True.
     124        [ Instruction (ADDC ? ACC_A (REGISTER r)) ]
     125      | _ ⇒ λother: False. ⊥
     126      ] (subaddressing_modein … reg')
     127    | Sub ⇒
     128      let reg' ≝ register_address reg in
     129      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     130                                                     direct;
     131                                                     register ]] x) → ? with
     132      [ ACC_A ⇒ λacc_a: True.
     133        [ Instruction (SUBB ? ACC_A accumulator_address) ]
     134      | DIRECT d ⇒ λdirect3: True.
     135        [ Instruction (SUBB ? ACC_A (DIRECT d)) ]
     136      | REGISTER r ⇒ λregister3: True.
     137        [ Instruction (SUBB ? ACC_A (REGISTER r)) ]
     138      | _ ⇒ λother: False. ⊥
     139      ] (subaddressing_modein … reg')
     140    | And ⇒
     141      let reg' ≝ register_address reg in
     142      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     143                                                     direct;
     144                                                     register ]] x) → ? with
     145      [ ACC_A ⇒ λacc_a: True.
     146        [ Instruction (NOP ?) ]
     147      | DIRECT d ⇒ λdirect4: True.
     148        [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
     149      | REGISTER r ⇒ λregister4: True.
     150        [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
     151      | _ ⇒ λother: False. ⊥
     152      ] (subaddressing_modein … reg')
     153    | Or ⇒
     154      let reg' ≝ register_address reg in
     155      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     156                                                     direct;
     157                                                     register ]] x) → ? with
     158      [ ACC_A ⇒ λacc_a: True.
     159        [ Instruction (NOP ?) ]
     160      | DIRECT d ⇒ λdirect5: True.
     161        [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
     162      | REGISTER r ⇒ λregister5: True.
     163        [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
     164      | _ ⇒ λother: False. ⊥
     165      ] (subaddressing_modein … reg')
     166    | Xor ⇒
     167      let reg' ≝ register_address reg in
     168      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     169                                                     direct;
     170                                                     register ]] x) → ? with
     171      [ ACC_A ⇒ λacc_a: True.
     172        [ Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) ]
     173      | DIRECT d ⇒ λdirect6: True.
     174        [ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) ]
     175      | REGISTER r ⇒ λregister6: True.
     176        [ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) ]
     177      | _ ⇒ λother: False. ⊥
     178      ] (subaddressing_modein … reg')
    85179    ]
    86180  | LIN_St_Int reg byte ⇒
    87181    let reg' ≝ register_address reg in
    88182      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    89                                                     register;
    90                                                     direct ]] x) → ? with
    91       [ REGISTER _ ⇒ λreg: True.
    92         Some ? [ Instruction (MOV ? (inl ? ? 〈register, (data_of_int byte)〉)) ]
    93       | _ ⇒ ?
    94       ] (subaddressing_modein … reg')
    95   | _ ⇒ ?
    96   ].
    97 
    98       | DIRECT _ ⇒ λdirect: True.
    99         Some ? [ Instruction (MOV ? (inr ? ? (inr ? ? 〈register, (data_of_int byte)〉))) ]
     183                                                     direct;
     184                                                     register ]] x) → ? with
     185      [ REGISTER r ⇒ λregister7: True.
     186        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) ]
     187      | ACC_A ⇒ λacc: True.
     188        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) ]
     189      | DIRECT d ⇒ λdirect7: True.
     190        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) ]
     191      | _ ⇒ λother: False. ⊥
     192      ] (subaddressing_modein … reg')
     193  | LIN_St_FromAcc reg ⇒
     194    let reg' ≝ register_address reg in
     195      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     196                                                     direct;
     197                                                     register ]] x) → ? with
     198      [ REGISTER r ⇒ λregister8: True.
     199        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) ]
     200      | ACC_A ⇒ λacc: True.
     201        [ Instruction (NOP ?) ]
     202      | DIRECT d ⇒ λdirect8: True.
     203        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) ]
     204      | _ ⇒ λother: False. ⊥
     205      ] (subaddressing_modein … reg')
     206  | LIN_St_ToAcc reg ⇒
     207    let reg' ≝ register_address reg in
     208      match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     209                                                     direct;
     210                                                     register ]] x) → ? with
     211      [ REGISTER r ⇒ λregister9: True.
     212        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) ]
     213      | DIRECT d ⇒ λdirect9: True.
     214        [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) ]
    100215      | ACC_A ⇒ λacc_a: True.
    101         Some ? [ Instruction (MOV ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)) ]
    102       | _ ⇒ λother: False. ⊥
    103       ] (subaddressing_modein … reg')
    104 
    105   | LIN_St_FromAcc reg ⇒ ? (*
    106     let reg' ≝ register_address reg in
    107       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    108                                                     register;
    109                                                     direct ]] x) → ? with
    110       [ REGISTER _ ⇒ λreg: True.
    111         Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
    112       | DIRECT _ ⇒ λdirect: True.
    113         Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
    114       | ACC_A ⇒ λacc_a: True.
    115         Some ? [ Instruction (MOV ? (inr ? ? 〈reg', ACC_A〉)) ]
    116       | _ ⇒ λother: False. ⊥
    117       ] (subaddressing_modein … reg') *)
    118   | LIN_St_ToAcc reg ⇒ ? (*
    119     let reg' ≝ register_address reg in
    120       match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    121                                                     register;
    122                                                     direct ]] x) → ? with
    123       [ REGISTER _ ⇒ λreg: True.
    124         Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
    125       | DIRECT _ ⇒ λdirect: True.
    126         Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
    127       | ACC_A ⇒ λacc_a: True.
    128         Some ? [ Instruction (MOV ? (inr ? ? 〈ACC_A, reg'〉)) ]
    129       | _ ⇒ λother: False. ⊥
    130       ] (subaddressing_modein … reg') *)
    131   | LIN_St_Address addr ⇒ ? (*
    132     let look ≝ association ? ? eq_v addr global_addresses in
    133     match look with
    134     [ None ⇒ None
    135     | Some look' ⇒
    136       Some ? [ Instruction (MOV ? (inr ? ? (inr ? ? 〈DPTR, (data16_of_int look')〉))) ]
    137     ] *)
    138   | LIN_St_Load ⇒ Some ? [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
    139   | LIN_St_Store ⇒ Some ? [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
    140   | LIN_St_CondAcc lbl ⇒ ?
    141   ].
     216        [ Instruction (NOP ?) ]
     217      | _ ⇒ λother: False. ⊥
     218      ] (subaddressing_modein … reg')
     219  | LIN_St_Load ⇒ [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
     220  | LIN_St_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
     221  | LIN_St_Address addr proof ⇒
     222    let look ≝ association addr globals proof in
     223      [ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ]
     224  | LIN_St_CondAcc lbl ⇒
     225    (* dpm: this should be handled in translate_code! *)
     226    [ WithLabel (JNZ ? lbl) ]
     227  ].
     228  try assumption
     229  try @ I
     230  cases ImplementedInRuntime
     231qed.
     232
     233definition translate_code ≝
     234  λglobals: list (Identifier × nat).
     235  λcode: list (LINStatement globals).
     236    flatten ? (map ? ? (translate_statements globals) code).
Note: See TracChangeset for help on using the changeset viewer.