Changeset 1245 for src/LIN


Ignore:
Timestamp:
Sep 21, 2011, 10:22:13 PM (8 years ago)
Author:
sacerdot
Message:

RTLtoERTL and LINToASM: porting to new Joint data type in progress.
However, it seems better to go back to a Joint representation where
the "mapping" from label to internal functions is more concrete.
To be done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1179 r1245  
    2828definition statement_labels ≝
    2929  λg: list ident.
    30   λs: lin_statement g.
     30  λs: (option label) × (lin_statement g).
    3131  let 〈label, instr〉 ≝ s in
    3232  let generated ≝
     
    5151  λglobals: list ident.
    5252  λlabels: BitVectorTrieSet ?.
    53   λstatement: lin_statement globals.
     53  λstatement: (option label) × (lin_statement globals).
    5454    set_union ? labels (statement_labels globals statement).
    5555
     56(*
    5657(* dpm: A = Identifier *)
    5758definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
     
    6162  let 〈ignore, fun_def〉 ≝ f in
    6263  match fun_def return λ_. BitVectorTrieSet ? with
    63   [ lin_fu_internal stmts proof
     64  [ Internal stmts
    6465      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
    65   | lin_fu_external _ ⇒ set_empty ?
     66  | External _ ⇒ set_empty ?
    6667  ].
    6768 
     
    7778    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
    7879              (set_empty ?) (lin_pr_funcs program).
    79    
     80*) 
    8081definition data_of_int ≝ λbv. DATA bv.
    8182definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
    8283definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
    83 
    84 axiom ImplementedInRuntime: False.
    8584
    8685definition translate_statements ≝
     
    8887  λglobals_old: list ident.
    8988  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
    90   λstatement: pre_lin_statement globals_old.
     89  λstatement: lin_statement globals_old.
    9190  match statement with
    9291  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
    93   | joint_st_extension ext ⇒ Instruction (NOP ?) (* XXX: NOP or something else? *)
     92  | joint_st_extension ext ⇒
    9493  | joint_st_return ⇒ Instruction (RET ?)
    9594  | joint_st_sequential instr _ ⇒
     
    9796      [ joint_instr_comment comment ⇒ Comment comment
    9897      | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
    99       | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
    100       | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
     98      | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address)
     99      | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address)
    101100      | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    102       | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
    103       | joint_instr_opaccs accs
     101      | joint_instr_call_id f _ ⇒ Call (word_of_identifier ? f)
     102      | joint_instr_opaccs accs _ _
    104103        match accs with
    105104        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    106105        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    107106        ]
    108       | joint_instr_op1 op1
     107      | joint_instr_op1 op1 _
    109108        match op1 with
    110109        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    111110        | Inc ⇒ Instruction (INC ? ACC_A)
    112111        ]
    113       | joint_instr_op2 op2 reg ⇒
     112      | joint_instr_op2 op2 _ reg ⇒
    114113        match op2 with
    115114        [ Add ⇒
     
    205204          | _ ⇒ λother: False. ⊥
    206205          ] (subaddressing_modein … reg')
    207       | joint_instr_from_acc reg ⇒
    208         let reg' ≝ register_address reg in
    209           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    210                                                          direct;
    211                                                          registr ]] x) → ? with
    212           [ REGISTER r ⇒ λregister8: True.
    213             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    214           | ACC_A ⇒ λacc: True.
    215             Instruction (NOP ?)
    216           | DIRECT d ⇒ λdirect8: True.
    217             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
    218           | _ ⇒ λother: False. ⊥
    219           ] (subaddressing_modein … reg')
    220       | joint_instr_to_acc reg ⇒
    221         let reg' ≝ register_address reg in
    222           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    223                                                          direct;
    224                                                          registr ]] x) → ? with
    225           [ REGISTER r ⇒ λregister9: True.
    226             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    227           | DIRECT d ⇒ λdirect9: True.
    228             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    229           | ACC_A ⇒ λacc_a: True.
    230             Instruction (NOP ?)
    231           | _ ⇒ λother: False. ⊥
    232           ] (subaddressing_modein … reg')
    233       | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    234       | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    235       | joint_instr_address addr proof ⇒
     206      | joint_instr_move regs ⇒
     207         match regs with
     208          [ from_acc reg ⇒
     209             let reg' ≝ register_address reg in
     210               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     211                                                              direct;
     212                                                              registr ]] x) → ? with
     213               [ REGISTER r ⇒ λregister8: True.
     214                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
     215               | ACC_A ⇒ λacc: True.
     216                 Instruction (NOP ?)
     217               | DIRECT d ⇒ λdirect8: True.
     218                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
     219               | _ ⇒ λother: False. ⊥
     220               ] (subaddressing_modein … reg')
     221          | to_acc reg ⇒
     222             let reg' ≝ register_address reg in
     223               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     224                                                              direct;
     225                                                              registr ]] x) → ? with
     226               [ REGISTER r ⇒ λregister9: True.
     227                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     228               | DIRECT d ⇒ λdirect9: True.
     229                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     230               | ACC_A ⇒ λacc_a: True.
     231                 Instruction (NOP ?)
     232               | _ ⇒ λother: False. ⊥
     233               ] (subaddressing_modein … reg')]
     234      | joint_instr_load _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     235      | joint_instr_store _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     236      | joint_instr_address addr proof _ _ ⇒
    236237        let look ≝ association addr globals (prf ? proof) in
    237238          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    238       | joint_instr_cond_acc lbl ⇒
     239      | joint_instr_cond _ lbl ⇒
    239240        (* dpm: this should be handled in translate_code! *)
    240241        Instruction (JNZ ? (word_of_identifier ? lbl))
     
    245246  try assumption
    246247  try @ I
    247   cases ImplementedInRuntime
    248248qed.
    249249
     
    252252  λglobals_old.
    253253  λprf.
    254   λstatement: lin_statement globals_old.
     254  λstatement: (option label) × (lin_statement globals_old).
    255255    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
    256256
     
    259259  λglobals_old: list ident.
    260260  λprf.
    261   λcode: list (lin_statement globals_old).
     261  λcode: list ((option label) × (lin_statement globals_old)).
    262262    map ? ? (build_translated_statement globals globals_old prf) code.
    263263   
Note: See TracChangeset for help on using the changeset viewer.