Changeset 2286 for src/LIN


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (7 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

Location:
src/LIN
Files:
4 deleted
5 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r1601 r2286  
    11include "LIN/joint_LTL_LIN.ma".
    2 include "basics/lists/list.ma".
    32
    4 definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.
     3definition LIN ≝ mk_lin_params LTL_LIN.
    54
    6 definition pre_lin_statement ≝ joint_statement lin_params_.
    7 definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals).
     5(* aid unification *)
     6unification hint 0 ≔
     7(*---------------*) ⊢
     8acc_a_reg LIN ≡ unit.
     9unification hint 0 ≔
     10(*---------------*) ⊢
     11acc_a_arg LIN ≡ unit.
     12unification hint 0 ≔
     13(*---------------*) ⊢
     14acc_b_reg LIN ≡ unit.
     15unification hint 0 ≔
     16(*---------------*) ⊢
     17acc_a_arg LIN ≡ unit.
     18unification hint 0 ≔
     19(*---------------*) ⊢
     20snd_arg LIN ≡ hdw_argument.
     21unification hint 0 ≔
     22(*---------------*) ⊢
     23ext_seq LIN ≡ ltl_lin_seq.
     24unification hint 0 ≔
     25(*---------------*) ⊢
     26pair_move LIN ≡ registers_move.
    827
    9 definition lin_params: ∀globals. params globals ≝
    10  λglobals.
    11   mk_params globals unit ltl_lin_params1 (list (lin_statement globals))
    12    (λcode. λl.
    13     find ?? (λs. let 〈l',x〉 ≝ s in
    14      match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
    15 
    16 definition lin_function ≝ λglobals. joint_function … (lin_params globals).
    17 definition lin_program ≝ joint_program lin_params.
     28definition lin_program ≝ joint_program LIN.
  • src/LIN/LINToASM.ma

    r1995 r2286  
    22include "utilities/BitVectorTrieSet.ma".
    33include "LIN/LIN.ma".
     4include "ASM/ASM.ma".
     5
     6definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     7  λr: Register.
     8    match r with
     9    [ Register00 ⇒ REGISTER [[ false; false; false ]]
     10    | Register01 ⇒ REGISTER [[ false; false; true ]]
     11    | Register02 ⇒ REGISTER [[ false; true; false ]]
     12    | Register03 ⇒ REGISTER [[ false; true; true ]]
     13    | Register04 ⇒ REGISTER [[ true; false; false ]]
     14    | Register05 ⇒ REGISTER [[ true; false; true ]]
     15    | Register06 ⇒ REGISTER [[ true; true; false ]]
     16    | Register07 ⇒ REGISTER [[ true; true; true ]]
     17    | RegisterA ⇒ ACC_A
     18    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
     19    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
     20    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
     21    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
     22    ]. @I qed.
     23
     24(* TODO:
     25  this should translate back end immediates (which rely on beval) to ASM
     26  byte immediates. How should it work? surely needs arguments for instantiation
     27  of blocks. If it's too much a fuss, we can go back to byte immediates in the
     28  back end. *)
     29definition asm_byte_of_beval : beval → Byte ≝
     30  λb.match b with
     31    [ BVByte b ⇒ b
     32    | BVundef ⇒ (* any will do *) zero_byte
     33    | BVnonzero ⇒ (* any will do *) maximum 7 @@ [[ true ]]
     34    | BVnull _ ⇒ zero_byte (* is it correct? *)
     35    | BVptr b p o ⇒ ?
     36    ].
     37  cases daemon qed.
     38
     39definition arg_address : hdw_argument → [[ acc_a ; direct ; registr ; data ]] ≝
     40  λa.match a with
     41  [ Reg r ⇒ register_address r
     42  | Imm bv ⇒ DATA (asm_byte_of_beval bv)
     43  ].
     44  cases a #x [2: normalize //] normalize nodelta
     45  elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
     46qed.
    447
    548let rec association (i: ident) (l: list (ident × nat))
     
    2568qed.
    2669
     70definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
     71 
    2772definition statement_labels ≝
    2873  λg: list ident.
     
    3378    [ sequential instr' _ ⇒
    3479      match instr' with
    35       [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
     80      [ step_seq instr'' ⇒
     81        match instr'' with
     82        [ COST_LABEL lbl ⇒ { (toASM_ident ? lbl) }
     83        | _ ⇒ ∅
     84        ]
    3685      | COND acc_a_reg lbl ⇒ { (toASM_ident ? lbl) }
     86      ]
     87    | final instr' ⇒
     88      match instr' with
     89      [ GOTO lbl ⇒ {(toASM_ident ? lbl)}
    3790      | _ ⇒ ∅
    3891      ]
    39     | RETURN ⇒ ∅
    40     | GOTO lbl ⇒ {(toASM_ident ? lbl)} ]
     92    ]
    4193  in
    4294  match label with
     
    55107  λA: Type[0].
    56108  λglobals: list ident.
    57   λf: A × (lin_function globals).
     109  λf: A × (joint_function LIN globals).
    58110  let 〈ignore, fun_def〉 ≝ f in
    59111  match fun_def return λ_. identifier_set ? with
     
    67119  λglobals: list ident.
    68120  λlabels: identifier_set ?.
    69   λfunct: A × (lin_function globals).
     121  λfunct: A × (joint_function LIN globals).
    70122    labels ∪ (function_labels ? globals funct).
    71123
     
    80132definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
    81133
     134(* TODO: check and change to free bit *)
     135definition asm_other_bit ≝ BIT_ADDR (zero_byte).
     136
    82137definition translate_statements ≝
    83138  λglobals: list (ident × nat).
    84139  λglobals_old: list ident.
    85140  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
    86   λstatement: pre_lin_statement globals_old.
     141  λstatement: joint_statement LIN globals_old.
    87142  match statement with
    88   [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    89   | RETURN ⇒ Instruction (RET ?)
     143  [ final instr ⇒
     144    match instr with
     145    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
     146    | RETURN ⇒ Instruction (RET ?)
     147    | tailcall abs ⇒ match abs in void with [ ]
     148    ]
    90149  | sequential instr _ ⇒
    91150      match instr with
    92       [ extension ext ⇒ ⊥
    93       | COMMENT comment ⇒ Comment comment
    94       | COST_LABEL lbl ⇒ Cost lbl
    95       | POP _ ⇒ Instruction (POP ? accumulator_address)
    96       | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
    97       | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
    98       | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
    99       | OPACCS accs _ _ _ _ ⇒
    100         match accs with
    101         [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    102         | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    103         ]
    104       | OP1 op1 _ _ ⇒
    105         match op1 with
    106         [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    107         | Inc ⇒ Instruction (INC ? ACC_A)
    108         | Rl ⇒ Instruction (RL ? ACC_A)
    109         ]
    110       | OP2 op2 _ _ reg ⇒
    111         match op2 with
    112         [ Add ⇒
    113           let reg' ≝ register_address reg in
    114           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    115                                                          direct;
    116                                                          registr ]] x) → ? with
    117           [ ACC_A ⇒ λacc_a: True.
    118             Instruction (ADD ? ACC_A accumulator_address)
    119           | DIRECT d ⇒ λdirect1: True.
    120             Instruction (ADD ? ACC_A (DIRECT d))
    121           | REGISTER r ⇒ λregister1: True.
    122             Instruction (ADD ? ACC_A (REGISTER r))
    123           | _ ⇒ λother: False. ⊥
    124           ] (subaddressing_modein … reg')
    125         | Addc ⇒
    126           let reg' ≝ register_address reg in
    127           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    128                                                          direct;
    129                                                          registr ]] x) → ? with
    130           [ ACC_A ⇒ λacc_a: True.
    131             Instruction (ADDC ? ACC_A accumulator_address)
    132           | DIRECT d ⇒ λdirect2: True.
    133             Instruction (ADDC ? ACC_A (DIRECT d))
    134           | REGISTER r ⇒ λregister2: True.
    135             Instruction (ADDC ? ACC_A (REGISTER r))
    136           | _ ⇒ λother: False. ⊥
    137           ] (subaddressing_modein … reg')
    138         | Sub ⇒
    139           let reg' ≝ register_address reg in
    140           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    141                                                          direct;
    142                                                          registr ]] x) → ? with
    143           [ ACC_A ⇒ λacc_a: True.
    144             Instruction (SUBB ? ACC_A accumulator_address)
    145           | DIRECT d ⇒ λdirect3: True.
    146             Instruction (SUBB ? ACC_A (DIRECT d))
    147           | REGISTER r ⇒ λregister3: True.
    148             Instruction (SUBB ? ACC_A (REGISTER r))
    149           | _ ⇒ λother: False. ⊥
    150           ] (subaddressing_modein … reg')
    151         | And ⇒
    152           let reg' ≝ register_address reg in
    153           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    154                                                          direct;
    155                                                          registr ]] x) → ? with
    156           [ ACC_A ⇒ λacc_a: True.
    157             Instruction (NOP ?)
    158           | DIRECT d ⇒ λdirect4: True.
    159             Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    160           | REGISTER r ⇒ λregister4: True.
    161             Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    162           | _ ⇒ λother: False. ⊥
    163           ] (subaddressing_modein … reg')
    164         | Or ⇒
    165           let reg' ≝ register_address reg in
    166           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    167                                                          direct;
    168                                                          registr ]] x) → ? with
    169           [ ACC_A ⇒ λacc_a: True.
    170             Instruction (NOP ?)
    171           | DIRECT d ⇒ λdirect5: True.
    172             Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    173           | REGISTER r ⇒ λregister5: True.
    174             Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    175           | _ ⇒ λother: False. ⊥
    176           ] (subaddressing_modein … reg')
    177         | Xor ⇒
    178           let reg' ≝ register_address reg in
    179           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    180                                                          direct;
    181                                                          registr ]] x) → ? with
    182           [ ACC_A ⇒ λacc_a: True.
    183             Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
    184           | DIRECT d ⇒ λdirect6: True.
    185             Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
    186           | REGISTER r ⇒ λregister6: True.
    187             Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
    188           | _ ⇒ λother: False. ⊥
    189           ] (subaddressing_modein … reg')
    190         ]
    191       | INT reg byte ⇒
    192         let reg' ≝ register_address reg in
    193           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    194                                                          direct;
    195                                                          registr ]] x) → ? with
    196           [ REGISTER r ⇒ λregister7: True.
    197             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
    198           | ACC_A ⇒ λacc: True.
    199             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
    200           | DIRECT d ⇒ λdirect7: True.
    201             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
    202           | _ ⇒ λother: False. ⊥
    203           ] (subaddressing_modein … reg')
    204       | MOVE regs ⇒
    205          match regs with
    206           [ from_acc reg ⇒
     151      [ step_seq instr' ⇒
     152        match instr' with
     153        [ extension_seq ext ⇒
     154          match ext with
     155          [ SAVE_CARRY ⇒
     156            Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
     157          | RESTORE_CARRY ⇒
     158            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
     159          ]
     160        | COMMENT comment ⇒ Comment comment
     161        | COST_LABEL lbl ⇒ Cost lbl
     162        | POP _ ⇒ Instruction (POP ? accumulator_address)
     163        | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
     164        | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
     165        | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
     166        | extension_call abs ⇒ match abs in void with [ ]
     167        | OPACCS accs _ _ _ _ ⇒
     168          match accs with
     169          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
     170          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
     171          ]
     172        | OP1 op1 _ _ ⇒
     173          match op1 with
     174          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     175          | Inc ⇒ Instruction (INC ? ACC_A)
     176          | Rl ⇒ Instruction (RL ? ACC_A)
     177          ]
     178        | OP2 op2 _ _ reg ⇒
     179          match op2 with
     180          [ Add ⇒
     181            let reg' ≝ arg_address reg in
     182            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     183                                                           direct;
     184                                                           registr;
     185                                                           data ]] x) → ? with
     186            [ ACC_A ⇒ λacc_a: True.
     187              Instruction (ADD ? ACC_A accumulator_address)
     188            | DIRECT d ⇒ λdirect1: True.
     189              Instruction (ADD ? ACC_A (DIRECT d))
     190            | REGISTER r ⇒ λregister1: True.
     191              Instruction (ADD ? ACC_A (REGISTER r))
     192            | DATA b ⇒ λdata : True.
     193              Instruction (ADD ? ACC_A (DATA b))
     194            | _ ⇒ Ⓧ
     195            ] (subaddressing_modein … reg')
     196          | Addc ⇒
     197            let reg' ≝ arg_address reg in
     198            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     199                                                           direct;
     200                                                           registr;
     201                                                           data ]] x) → ? with
     202            [ ACC_A ⇒ λacc_a: True.
     203              Instruction (ADDC ? ACC_A accumulator_address)
     204            | DIRECT d ⇒ λdirect2: True.
     205              Instruction (ADDC ? ACC_A (DIRECT d))
     206            | REGISTER r ⇒ λregister2: True.
     207              Instruction (ADDC ? ACC_A (REGISTER r))
     208            | DATA b ⇒ λdata : True.
     209              Instruction (ADDC ? ACC_A (DATA b))
     210            | _ ⇒ Ⓧ
     211            ] (subaddressing_modein … reg')
     212          | Sub ⇒
     213            let reg' ≝ arg_address reg in
     214            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     215                                                           direct;
     216                                                           registr;
     217                                                           data ]] x) → ? with
     218            [ ACC_A ⇒ λacc_a: True.
     219              Instruction (SUBB ? ACC_A accumulator_address)
     220            | DIRECT d ⇒ λdirect3: True.
     221              Instruction (SUBB ? ACC_A (DIRECT d))
     222            | REGISTER r ⇒ λregister3: True.
     223              Instruction (SUBB ? ACC_A (REGISTER r))
     224            | DATA b ⇒ λdata : True.
     225              Instruction (SUBB ? ACC_A (DATA b))
     226            | _ ⇒ Ⓧ
     227            ] (subaddressing_modein … reg')
     228          | And ⇒
     229            let reg' ≝ arg_address reg in
     230            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     231                                                           direct;
     232                                                           registr;
     233                                                           data ]] x) → ? with
     234            [ ACC_A ⇒ λacc_a: True.
     235              Instruction (NOP ?)
     236            | DIRECT d ⇒ λdirect4: True.
     237              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     238            | REGISTER r ⇒ λregister4: True.
     239              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     240            | DATA b ⇒ λdata : True.
     241              Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
     242            | _ ⇒ Ⓧ
     243            ] (subaddressing_modein … reg')
     244          | Or ⇒
     245            let reg' ≝ arg_address reg in
     246            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     247                                                           direct;
     248                                                           registr ; data ]] x) → ? with
     249            [ ACC_A ⇒ λacc_a: True.
     250              Instruction (NOP ?)
     251            | DIRECT d ⇒ λdirect5: True.
     252              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     253            | REGISTER r ⇒ λregister5: True.
     254              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     255            | DATA b ⇒ λdata : True.
     256              Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
     257            | _ ⇒ Ⓧ
     258            ] (subaddressing_modein … reg')
     259          | Xor ⇒
     260            let reg' ≝ arg_address reg in
     261            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     262                                                           direct;
     263                                                           registr ; data ]] x) → ? with
     264            [ ACC_A ⇒ λacc_a: True.
     265              Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
     266            | DIRECT d ⇒ λdirect6: True.
     267              Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
     268            | REGISTER r ⇒ λregister6: True.
     269              Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
     270            | DATA b ⇒ λdata : True.
     271              Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
     272            | _ ⇒ Ⓧ
     273            ] (subaddressing_modein … reg')
     274          ]
     275        | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     276        | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     277        | ADDRESS addr proof _ _ ⇒
     278          let look ≝ association addr globals (prf ? proof) in
     279            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     280        | SET_CARRY ⇒
     281          Instruction (SETB ? CARRY)
     282        | MOVE regs ⇒
     283          match regs with
     284          [ to_acc _ reg ⇒
     285             let reg' ≝ register_address reg in
     286               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     287                                                              direct;
     288                                                              registr ]] x) → ? with
     289               [ REGISTER r ⇒ λregister9: True.
     290                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     291               | DIRECT d ⇒ λdirect9: True.
     292                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     293               | ACC_A ⇒ λacc_a: True.
     294                 Instruction (NOP ?)
     295               | _ ⇒ λother: False. ⊥
     296               ] (subaddressing_modein … reg')
     297          | from_acc reg _ ⇒
    207298             let reg' ≝ register_address reg in
    208299               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    217308               | _ ⇒ λother: False. ⊥
    218309               ] (subaddressing_modein … reg')
    219           | to_acc reg ⇒
    220              let reg' ≝ register_address reg in
    221                match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    222                                                               direct;
    223                                                               registr ]] x) → ? with
    224                [ REGISTER r ⇒ λregister9: True.
    225                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    226                | DIRECT d ⇒ λdirect9: True.
    227                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    228                | ACC_A ⇒ λacc_a: True.
    229                  Instruction (NOP ?)
    230                | _ ⇒ λother: False. ⊥
    231                ] (subaddressing_modein … reg')]
    232       | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    233       | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    234       | ADDRESS addr proof _ _ ⇒
    235         let look ≝ association addr globals (prf ? proof) in
    236           Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     310          | int_to_reg reg bv ⇒
     311            let b ≝ asm_byte_of_beval bv in
     312            let reg' ≝ register_address reg in
     313              match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     314                                                             direct;
     315                                                             registr ]] x) → ? with
     316              [ REGISTER r ⇒ λregister7: True.
     317                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
     318              | ACC_A ⇒ λacc: True.
     319                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
     320              | DIRECT d ⇒ λdirect7: True.
     321                Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
     322              | _ ⇒ λother: False. ⊥
     323              ] (subaddressing_modein … reg')
     324          | int_to_acc _ bv ⇒
     325            let b ≝ asm_byte_of_beval bv in
     326            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
     327          ]
     328        ]
    237329      | COND _ lbl ⇒
    238330        (* dpm: this should be handled in translate_code! *)
    239331        Instruction (JNZ ? (toASM_ident ? lbl))
    240       | SET_CARRY ⇒
    241         Instruction (SETB ? CARRY)
    242332      ]
    243333    ].
     
    272362    match def with
    273363    [ Internal int ⇒
    274       let code ≝ joint_if_code … (lin_params globals_old) int in
     364      let code ≝ joint_if_code LIN globals_old int in
    275365      match translate_code globals globals_old prf code with
    276366      [ nil ⇒ ⊥
     
    293383let rec flatten_fun_defs
    294384  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
    295     (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function globals_old (lin_params globals_old)))))
     385    (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function LIN globals_old))))
    296386      on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
    297387  match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
  • src/LIN/joint_LTL_LIN.ma

    r1378 r2286  
    22
    33inductive registers_move: Type[0] ≝
    4  | from_acc: Register → registers_move
    5  | to_acc: Register → registers_move.
     4 | from_acc: Register → unit → registers_move
     5 | to_acc: unit → Register → registers_move
     6 | int_to_reg : Register → beval → registers_move
     7 | int_to_acc : unit → beval → registers_move.
     8(* the last is redudant, but kept for notation's sake *)
    69
    7 definition ltl_lin_params__: params__ ≝
    8  mk_params__ unit unit unit unit registers_move Register nat unit False.
    9 definition ltl_lin_params0 : params0 ≝ mk_params0 ltl_lin_params__ unit unit.
    10 definition ltl_lin_params1 : params1 ≝ mk_params1 ltl_lin_params0 unit.
     10inductive ltl_lin_seq : Type[0] ≝
     11| SAVE_CARRY : ltl_lin_seq
     12| RESTORE_CARRY : ltl_lin_seq.
     13
     14definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
     15    (* acc_a_reg ≝ *) unit
     16    (* acc_b_reg ≝ *) unit
     17    (* acc_a_arg ≝ *) unit
     18    (* acc_b_arg ≝ *) unit
     19    (* dpl_reg   ≝ *) unit
     20    (* dph_reg   ≝ *) unit
     21    (* dpl_arg   ≝ *) unit
     22    (* dph_arg   ≝ *) unit
     23    (* snd_arg   ≝ *) hdw_argument
     24    (* pair_move ≝ *) registers_move
     25    (* call_args ≝ *) ℕ
     26    (* call_dest ≝ *) unit
     27    (* ext_seq ≝ *) ltl_lin_seq
     28    (* ext_call ≝ *) void
     29    (* ext_tailcall ≝ *) void
     30    (* paramsT ≝ *) unit
     31    (* localsT ≝ *) void.
     32
     33interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
     34interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
     35interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
     36interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1451 r2286  
    44definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
    55definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
     6definition hw_arg_retrieve ≝
     7  λl,a.match a with
     8  [ Reg r ⇒ hw_reg_retrieve l r
     9  | Imm b ⇒ OK … b
     10  ].
    611
    7 definition ltl_lin_more_sem_params: ∀succT. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
    8  λsuccT.
    9  mk_more_sem_params ?
    10   unit it hw_register_env init_hw_register_env 0 it
    11    hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA)
    12     (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB)
    13     (λ_.hw_reg_store RegisterDPL) (λe.λ_.hw_reg_retrieve e RegisterDPL)
    14     (λ_.hw_reg_store RegisterDPH) (λe.λ_.hw_reg_retrieve e RegisterDPH)
    15      (λlocals,dest_src.
    16        match dest_src with
    17        [ from_acc reg ⇒
    18           do v ← hw_reg_retrieve locals RegisterA ;
    19           hw_reg_store reg v locals
    20        | to_acc reg ⇒
    21           do v ← hw_reg_retrieve locals reg ;
    22           hw_reg_store RegisterA v locals ]).
     12definition eval_registers_move ≝ λe,m.
     13match m with
     14[ from_acc r _ ⇒
     15  hw_reg_store r (hwreg_retrieve e RegisterA) e
     16| to_acc _ r ⇒
     17  hw_reg_store RegisterA (hwreg_retrieve e r) e
     18| int_to_reg r v ⇒
     19  hw_reg_store r v e
     20| int_to_acc _ v ⇒
     21  hw_reg_store RegisterA v e
     22].
    2323
    24 definition ltl_lin_sem_params: ∀succT. sem_params ≝
    25  λsuccT.mk_sem_params … (ltl_lin_more_sem_params succT).
    26 
    27 
    28 definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    29 definition ltl_lin_pop_frame:
    30  ∀succT,codeT,lookup.
    31  ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    32  state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
    33  λ_.λ_.λ_.λ_.λ_.λt.OK … t.
    34 definition ltl_lin_save_frame:
    35  ∀succT. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
    36  λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    37 
    38 (* The following implementation only works for functions that return 32 bits *)
    39 definition ltl_lin_result_regs:
    40  ∀succT,codeT,lookup.
    41  ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    42  state (ltl_lin_sem_params succT) → res (list Register) ≝
    43  λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
     24definition LTL_LIN_state : sem_state_params ≝
     25  mk_sem_state_params
     26 (* framesT ≝ *) unit
     27 (* empty_framesT ≝ *) it
     28 (* regsT ≝ *) hw_register_env
     29 (* empty_regsT ≝ *) init_hw_register_env.
    4430
    4531(*CSC: XXXX, for external functions only*)
    46 axiom ltl_lin_fetch_external_args: ∀succT.external_function → state (ltl_lin_sem_params succT) → res (list val).
    47 axiom ltl_lin_set_result: ∀succT.list val → state (ltl_lin_sem_params succT) → res (state (ltl_lin_sem_params succT)).
     32axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → res (list val).
     33axiom ltl_lin_set_result: list val → unit → state LTL_LIN_state → res (state LTL_LIN_state).
    4834
    49 definition ltl_lin_exec_extended: ∀succT.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT) → IO io_out io_in (trace × (state (ltl_lin_sem_params succT)))
    50  ≝ λsuccT,p,globals,ge,abs. ⊥.
    51 @abs qed.
     35(* TODO (needs another bit to be added to hdw) *)
     36axiom eval_ltl_lin_seq : ltl_lin_seq → state LTL_LIN_state → IO io_out io_in (state LTL_LIN_state).
    5237
    53 definition ltl_lin_more_sem_params2:
    54  ∀succT,codeT,lookup.∀succ: succT → address → res address.∀fetch.
    55  ∀pointer_of_label: ∀globals. genv globals
    56   (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals))
    57   →pointer→label→res (Σp0:pointer.ptype p0=Code).
    58  ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    59  λsuccT,codeT,lookup,succ,fetch,pointer_of_label,globals.
    60   mk_more_sem_params2 …
    61    (mk_more_sem_params1 … (ltl_lin_more_sem_params …)
    62     succ (pointer_of_label …) (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    63     ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    64     (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …).
    65 
    66 definition ltl_lin_fullexec ≝
    67  λsuccT,codeT,lookup,succ,fetch,pointer_of_label.
    68   joint_fullexec … (λp. ltl_lin_more_sem_params2 succT codeT lookup succ fetch pointer_of_label (prog_var_names … p)).
     38definition LTL_LIN_semantics ≝
     39  λF.mk_more_sem_unserialized_params LTL_LIN F
     40  (* st_pars            ≝ *) LTL_LIN_state
     41  (* acca_store_        ≝ *) (λ_.hw_reg_store RegisterA)
     42  (* acca_retrieve_     ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA)
     43  (* acca_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA)
     44  (* accb_store_        ≝ *) (λ_.hw_reg_store RegisterB)
     45  (* accb_retrieve_     ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB)
     46  (* accb_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB)
     47  (* dpl_store_         ≝ *) (λ_.hw_reg_store RegisterDPL)
     48  (* dpl_retrieve_      ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL)
     49  (* dpl_arg_retrieve_  ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL)
     50  (* dph_store_         ≝ *) (λ_.hw_reg_store RegisterDPH)
     51  (* dph_retrieve_      ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH)
     52  (* dph_arg_retrieve_  ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH)
     53  (* snd_arg_retrieve_  ≝ *) hw_arg_retrieve
     54  (* pair_reg_move_     ≝ *) eval_registers_move
     55  (* fetch_ra           ≝ *) (load_ra …)
     56  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
     57  (* save_frame         ≝ *) (λp.λ_.λst.save_ra … st p)
     58  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
     59  (* fetch_external_args≝ *) ltl_lin_fetch_external_args
     60  (* set_result         ≝ *) ltl_lin_set_result
     61  (* call_args_for_main ≝ *) 0
     62  (* call_dest_for_main ≝ *) it
     63  (* read_result        ≝ *) (λ_.λ_.λ_.
     64  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
     65  (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
     66  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     67  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     68  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
     69  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).
  • src/LIN/semantics.ma

    r1601 r2286  
    22include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition lin_succ_pc: unit → address → res address :=
    5  λ_.λaddr. addr_add addr 1.
    6 
    7 axiom BadOldPointer: String.
    8 (*CSC: XXX factorize the code with graph_fetch_function!!! *)
    9 definition lin_fetch_function:
    10  ∀globals. genv … (lin_params globals) → pointer → res (joint_internal_function globals (lin_params globals)) ≝
    11  λglobals,ge,old.
    12   let b ≝ pblock old in
    13   do def ← opt_to_res ? [MSG BadOldPointer] (find_funct_ptr … ge b);
    14   match def with
    15   [ Internal fn ⇒ OK … fn
    16   | External _ ⇒ Error … [MSG BadOldPointer]].
    17 
    18 axiom BadLabel: String.
    19 definition lin_pointer_of_label:
    20  ∀globals. genv … (lin_params globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
    21  λglobals,ge,old,l.
    22   do fn ← lin_fetch_function … ge old ;
    23   do pos ←
    24    opt_to_res ? [MSG BadLabel]
    25     (position_of ?
    26       (λs. let 〈l',x〉 ≝ s in
    27         match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
    28      (joint_if_code … (lin_params …) fn)) ;
    29   OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
    30 // qed.
    31 
    32 (*CSC: XXX factorize code with graph_fetch_statement?*)
    33 axiom BadProgramCounter: String.
    34 definition lin_fetch_statement:
    35  ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params unit) → res (pre_lin_statement globals) ≝
    36  λglobals,ge,st.
    37   do ppc ← pointer_of_address (pc … st) ;
    38   do fn ← lin_fetch_function … ge ppc ;
    39   let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
    40   do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
    41   OK … (\snd found).
    42 
    43 definition lin_fullexec: fullexec io_out io_in ≝
    44  ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label.
     4definition LIN_semantics : sem_params ≝
     5  make_sem_lin_params LIN (LTL_LIN_semantics ?).
Note: See TracChangeset for help on using the changeset viewer.