Changeset 2490


Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (7 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

Location:
src
Files:
11 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r2286 r2490  
    3737    (* call_dest ≝ *) unit
    3838    (* ext_seq ≝ *) ertl_seq
    39     (* ext_call ≝ *) void
    40     (* ext_tailcall ≝ *) void
     39    (* has_tailcall ≝ *) false
    4140    (* paramsT ≝ *) ℕ
    4241    (* localsT ≝ *) register.
     
    8887(*---------------*) ⊢
    8988ext_seq ERTL ≡ ertl_seq.
    90 unification hint 0 ≔
    91 (*---------------*) ⊢
    92 ext_call ERTL ≡ void.
    93 unification hint 0 ≔
    94 (*---------------*) ⊢
    95 ext_tailcall ERTL ≡ void.
    9689
    9790coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝
  • src/ERTL/ERTLToLTL.ma

    r2443 r2490  
    1515  | arg_decision_colour : Register → arg_decision
    1616  | arg_decision_spill : ℕ → arg_decision
    17   | arg_decision_imm : beval → arg_decision.
     17  | arg_decision_imm : Byte → arg_decision.
    1818
    1919coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
     
    7575 
    7676definition set_stack_int :
    77   ∀globals.nat → beval →  list (joint_seq LTL globals) ≝
     77  ∀globals.nat → Byte →  list (joint_seq LTL globals) ≝
    7878  λglobals,off,int.
    7979  set_dp_by_offset ? off @
     
    289289
    290290definition translate_address :
    291   ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision →
     291  ∀globals.bool → ∀i.member ? (eq_identifier ?) i globals → decision → decision →
    292292  list (joint_seq LTL globals) ≝
    293293  λglobals,carry_lives_after,id,prf,addr1,addr2.
     
    367367        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    368368      ]
    369     | CALL_ID f n_args _ ⇒ CALL_ID LTL ? f n_args it
    370     | extension_call abs ⇒ match abs in void with [ ]
     369    | CALL f n_args _ ⇒
     370      match f with
     371      [ inl f ⇒ [ CALL LTL ? (inl … f) n_args it ]
     372      | inr dp ⇒
     373        let 〈dpl, dph〉 ≝ dp in
     374        move_to_dp … (lookup_arg dpl) (lookup_arg dph) @
     375        [ CALL LTL ? (inr … 〈it, it〉) n_args it ]
     376      ]
    371377    ]
    372378  | COND r ltrue ⇒
     
    380386  [ RETURN ⇒ RETURN ?
    381387  | GOTO l ⇒ GOTO ? l
    382   | tailcall abs ⇒ match abs in void with [ ]
     388  | TAILCALL abs _ _ ⇒ Ⓧabs
    383389  ].
    384390
    385391definition translate_internal: ∀globals: list ident.
    386   joint_internal_function ERTL globals →
    387   joint_internal_function LTL globals ≝
    388   λglobals: list ident.
    389   λint_fun: joint_internal_function ERTL globals.
     392  joint_closed_internal_function ERTL globals →
     393  joint_closed_internal_function LTL globals ≝
     394  λglobals,int_fun.
    390395  (* initialize graph *)
    391396  let entry ≝ pi1 … (joint_if_entry … int_fun) in
     
    406411    (translate_fin_step …)
    407412    int_fun.
     413cases daemon (* TODO *) qed.
    408414
    409415definition ertl_to_ltl: ertl_program → ltl_program ≝
  • src/ERTL/liveness.ma

    r2286 r2490  
    8383        ]
    8484      (* Potentially destroys all caller-save hardware registers. *)
    85       | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    86       | extension_call abs ⇒ match abs in void with [ ]
     85      | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    8786      ]
    8887    | COND r lbl_true ⇒ rl_bottom
     
    139138        ]
    140139      (* Reads the hardware registers that are used to pass parameters. *)
    141       | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    142       | extension_call abs ⇒ match abs in void with [ ]
     140      | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    143141      | _ ⇒ rl_bottom
    144142      ]
     
    149147    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    150148    | GOTO l ⇒ rl_bottom
    151     | tailcall abs ⇒ match abs in void with [ ]
     149    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
    152150    ]
    153151  ].
  • src/LIN/LINToASM.ma

    r2443 r2490  
    4141definition association_block ≝ association block Word eq_block.
    4242
    43 definition asm_cst_well_def :
    44   list (block × Word) → beval → bool ≝
    45 λglobals,bv.match bv with
    46 [ BVptr b _ _ ⇒ member ? eq_block b (map ?? \fst globals)
    47 | _ ⇒ true
    48 ].
    49 
    5043definition vector_cast :
    5144∀A,n,m.A → Vector A n → Vector A m ≝
     
    6255qed.
    6356
    64 definition asm_byte_of_beval :
    65   ∀globals,bv.asm_cst_well_def globals bv → Byte ≝
    66   λglobals,bv.match bv return λbv.asm_cst_well_def globals bv → Byte with
    67     [ BVByte b ⇒ λ_.b
    68     | BVundef ⇒ λ_.(* any will do *) zero_byte
    69     | BVnonzero ⇒ λ_.(* any will do *) maximum 7 @@ [[ true ]]
    70     | BVnull _ ⇒ λ_.zero_byte (* is it correct? *)
    71     | BVptr b p o ⇒ λprf.
    72       let b_inst ≝ vector_cast … (S p) zero_byte (rvsplit … 2 8 (association_block … prf)) in
    73       let 〈inst, ignore〉 ≝ op2_bytes Add … false b_inst o in
    74       head' … inst
    75     ].
    76 
    77 definition asm_arg_well_def :
    78   list (block × Word) → hdw_argument → bool ≝
    79 λglobals,a.match a with
    80 [ Imm bv ⇒ asm_cst_well_def globals bv
    81 | _ ⇒ true
    82 ].
    83 
    84 definition arg_address : ∀globals,arg.asm_arg_well_def globals arg →
     57definition arg_address : hdw_argument →
    8558  [[ acc_a ; direct ; registr ; data ]] ≝
    86   λglobals,a.
     59  λa.
    8760  match a
    88   return λa.asm_arg_well_def globals a → [[ acc_a ; direct ; registr ; data ]]
    8961  with
    90   [ Reg r ⇒ λ_.register_address r
    91   | Imm bv ⇒ λprf.DATA (asm_byte_of_beval … prf)
    92   ].
    93   [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
    94   | @I
    95   ]
     62  [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
     63  | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
     64  ].
     65  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
    9666qed.
    9767
    9868definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
    9969
    100 definition asm_stmt_well_def :
    101   list (block × Word) → ∀old_globals.joint_statement LIN old_globals → bool ≝
    102   λblocks,old_globals,stmt.
    103   match stmt with
    104   [ sequential instr _ ⇒
    105     match instr with
    106     [ step_seq instr' ⇒
    107       match instr' with
    108       [ OP2 _ _ _ arg ⇒ asm_arg_well_def blocks arg
    109       | MOVE regs ⇒
    110         match regs with
    111         [ int_to_reg _ bv ⇒ asm_cst_well_def blocks bv
    112         | int_to_acc _ bv ⇒ asm_cst_well_def blocks bv
    113         | _ ⇒ true
    114         ]
    115       | _ ⇒ true
    116       ]
    117     | _ ⇒ true
    118     ]
    119   | _ ⇒ true
    120   ].
    121  
    12270definition statement_labels ≝
    12371  λg: list ident.
     
    187135definition translate_statements ≝
    188136  λglobals: list (ident × nat).
    189   λblocks: list (block × Word).
    190137  λglobals_old: list ident.
    191138  λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
    192139  λstatement: joint_statement LIN globals_old.
    193   match statement return λstmt.asm_stmt_well_def blocks ? stmt → ? with
    194   [ final instr ⇒ λ_.
     140  match statement with
     141  [ final instr ⇒
    195142    match instr with
    196143    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    197144    | RETURN ⇒ Instruction (RET ?)
    198     | tailcall abs ⇒ match abs in void with [ ]
     145    | TAILCALL abs _ _ ⇒ Ⓧabs
    199146    ]
    200147  | sequential instr _ ⇒
    201       match instr return λinstr.asm_stmt_well_def blocks ? (sequential ?? instr ?) → ? with
     148      match instr with
    202149      [ step_seq instr' ⇒
    203         match instr' return λinstr'.asm_stmt_well_def ?? (sequential ?? (step_seq ?? instr') ?) → ? with
    204         [ extension_seq ext ⇒ λ_.
     150        match instr' with
     151        [ extension_seq ext ⇒
    205152          match ext with
    206153          [ SAVE_CARRY ⇒
     
    209156            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
    210157          ]
    211         | COMMENT comment ⇒ λ_.Comment comment
    212         | COST_LABEL lbl ⇒ λ_.Cost lbl
    213         | POP _ ⇒ λ_.Instruction (POP ? accumulator_address)
    214         | PUSH _ ⇒ λ_.Instruction (PUSH ? accumulator_address)
    215         | CLEAR_CARRY ⇒ λ_.Instruction (CLR ? CARRY)
    216         | CALL_ID f _ _ ⇒ λ_.Call (toASM_ident ? f)
    217         | extension_call abs ⇒ λ_.match abs in void with [ ]
    218         | OPACCS accs _ _ _ _ ⇒ λ_.
     158        | COMMENT comment ⇒ Comment comment
     159        | COST_LABEL lbl ⇒ Cost lbl
     160        | POP _ ⇒ Instruction (POP ? accumulator_address)
     161        | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
     162        | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
     163        | CALL f _ _ ⇒
     164          match f with
     165          [ inl f_id ⇒ Call (toASM_ident ? f_id)
     166          | inr _ ⇒ (* TODO call from ptr in DPTR *)
     167            match not_implemented in False with [ ]
     168          ]
     169        | OPACCS accs _ _ _ _ ⇒
    219170          match accs with
    220171          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    221172          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    222173          ]
    223         | OP1 op1 _ _ ⇒ λ_.
     174        | OP1 op1 _ _ ⇒
    224175          match op1 with
    225176          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     
    227178          | Rl ⇒ Instruction (RL ? ACC_A)
    228179          ]
    229         | OP2 op2 _ _ reg ⇒ λprf'.?
    230           | _ ⇒ ?] | _ ⇒ ? ]].[12: whd in prf : (?%);
    231 
    232           match op2 with
    233           [ Add ⇒
    234             let reg' ≝ arg_address … prf' in
    235             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    236                                                            direct;
    237                                                            registr;
    238                                                            data ]] x) → ? with
    239             [ ACC_A ⇒ λacc_a: True.
    240               Instruction (ADD ? ACC_A accumulator_address)
    241             | DIRECT d ⇒ λdirect1: True.
    242               Instruction (ADD ? ACC_A (DIRECT d))
    243             | REGISTER r ⇒ λregister1: True.
    244               Instruction (ADD ? ACC_A (REGISTER r))
    245             | DATA b ⇒ λdata : True.
    246               Instruction (ADD ? ACC_A (DATA b))
    247             | _ ⇒ Ⓧ
    248             ] (subaddressing_modein … reg')
    249           | Addc ⇒
    250             let reg' ≝ arg_address … prf' in
    251             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    252                                                            direct;
    253                                                            registr;
    254                                                            data ]] x) → ? with
    255             [ ACC_A ⇒ λacc_a: True.
    256               Instruction (ADDC ? ACC_A accumulator_address)
    257             | DIRECT d ⇒ λdirect2: True.
    258               Instruction (ADDC ? ACC_A (DIRECT d))
    259             | REGISTER r ⇒ λregister2: True.
    260               Instruction (ADDC ? ACC_A (REGISTER r))
    261             | DATA b ⇒ λdata : True.
    262               Instruction (ADDC ? ACC_A (DATA b))
    263             | _ ⇒ Ⓧ
    264             ] (subaddressing_modein … reg')
    265           | Sub ⇒
    266             let reg' ≝ arg_address … prf' in
    267             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    268                                                            direct;
    269                                                            registr;
    270                                                            data ]] x) → ? with
    271             [ ACC_A ⇒ λacc_a: True.
    272               Instruction (SUBB ? ACC_A accumulator_address)
    273             | DIRECT d ⇒ λdirect3: True.
    274               Instruction (SUBB ? ACC_A (DIRECT d))
    275             | REGISTER r ⇒ λregister3: True.
    276               Instruction (SUBB ? ACC_A (REGISTER r))
    277             | DATA b ⇒ λdata : True.
    278               Instruction (SUBB ? ACC_A (DATA b))
    279             | _ ⇒ Ⓧ
    280             ] (subaddressing_modein … reg')
    281           | And ⇒
    282             let reg' ≝ arg_address … prf' in
    283             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    284                                                            direct;
    285                                                            registr;
    286                                                            data ]] x) → ? with
    287             [ ACC_A ⇒ λacc_a: True.
    288               Instruction (NOP ?)
    289             | DIRECT d ⇒ λdirect4: True.
    290               Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    291             | REGISTER r ⇒ λregister4: True.
    292               Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    293             | DATA b ⇒ λdata : True.
    294               Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
    295             | _ ⇒ Ⓧ
    296             ] (subaddressing_modein … reg')
    297           | Or ⇒
    298             let reg' ≝ arg_address … prf' in
    299             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    300                                                            direct;
    301                                                            registr ; data ]] x) → ? with
    302             [ ACC_A ⇒ λacc_a: True.
    303               Instruction (NOP ?)
    304             | DIRECT d ⇒ λdirect5: True.
    305               Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    306             | REGISTER r ⇒ λregister5: True.
    307               Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    308             | DATA b ⇒ λdata : True.
    309               Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
    310             | _ ⇒ Ⓧ
    311             ] (subaddressing_modein … reg')
    312           | Xor ⇒
    313             let reg' ≝ arg_address … prf' in
    314             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    315                                                            direct;
    316                                                            registr ; data ]] x) → ? with
    317             [ ACC_A ⇒ λacc_a: True.
    318               Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
    319             | DIRECT d ⇒ λdirect6: True.
    320               Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
    321             | REGISTER r ⇒ λregister6: True.
    322               Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
    323             | DATA b ⇒ λdata : True.
    324               Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
    325             | _ ⇒ Ⓧ
    326             ] (subaddressing_modein … reg')
    327           ]
    328         | LOAD _ _ _ ⇒ λ_.Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    329         | STORE _ _ _ ⇒ λ_.Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    330         | ADDRESS addr proof _ _ ⇒ λ_.
     180        | OP2 op2 _ _ reg ⇒
     181          match arg_address … reg
     182          return λx.is_in … [[ acc_a;
     183                                 direct;
     184                                 registr;
     185                                 data ]] x → ? with
     186          [ ACC_A ⇒ λacc_a: True.
     187            match op2 with
     188            [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address)
     189            | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address)
     190            | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address)
     191            | Xor ⇒ Instruction (CLR ? ACC_A)
     192            | _ ⇒ Instruction (NOP ?)
     193            ]
     194          | DIRECT d ⇒ λdirect1: True.
     195            match op2 with
     196            [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d))
     197            | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d))
     198            | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d))
     199            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     200            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     201            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
     202            ]
     203          | REGISTER r ⇒ λregister1: True.
     204            match op2 with
     205            [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r))
     206            | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r))
     207            | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r))
     208            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     209            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     210            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
     211            ]
     212          | DATA b ⇒ λdata : True.
     213            match op2 with
     214            [ Add ⇒ Instruction (ADD ? ACC_A (DATA b))
     215            | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b))
     216            | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b))
     217            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
     218            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
     219            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
     220            ]
     221          | _ ⇒ Ⓧ
     222          ] (subaddressing_modein …)
     223        | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     224        | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     225        | ADDRESS addr proof _ _ ⇒
    331226          let look ≝ association_ident addr globals (prf ? proof) in
    332227            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    333         | SET_CARRY ⇒ λ_.
     228        | SET_CARRY ⇒
    334229          Instruction (SETB ? CARRY)
    335230        | MOVE regs ⇒
    336           match regs return λregs.asm_stmt_well_def ?? (sequential ?? (step_seq ?? (MOVE regs)) ?) → ? with
    337           [ to_acc _ reg ⇒ λ_.
    338              let reg' ≝ register_address reg in
    339                match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     231          match regs with
     232          [ to_acc _ reg ⇒
     233            match register_address reg return λx.is_in … [[ acc_a;
    340234                                                              direct;
    341                                                               registr ]] x) → ? with
    342                [ REGISTER r ⇒ λregister9: True.
    343                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    344                | DIRECT d ⇒ λdirect9: True.
    345                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    346                | ACC_A ⇒ λacc_a: True.
    347                  Instruction (NOP ?)
    348                | _ ⇒ λother: False. ⊥
    349                ] (subaddressing_modein … reg')
    350           | from_acc reg _ ⇒ λ_.
    351              let reg' ≝ register_address reg in
    352                match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     235                                                              registr]] x → ? with
     236           [ REGISTER r ⇒ λregister9: True.
     237             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     238           | DIRECT d ⇒ λdirect9: True.
     239             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     240           | ACC_A ⇒ λacc_a: True.
     241             Instruction (NOP ?)
     242           | _ ⇒ Ⓧ
     243           ] (subaddressing_modein …)
     244         | from_acc reg _ ⇒
     245            match register_address reg return λx.is_in … [[ acc_a;
    353246                                                              direct;
    354                                                               registr ]] x) → ? with
    355                [ REGISTER r ⇒ λregister8: True.
    356                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    357                | ACC_A ⇒ λacc: True.
    358                  Instruction (NOP ?)
    359                | DIRECT d ⇒ λdirect8: True.
    360                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
    361                | _ ⇒ λother: False. ⊥
    362                ] (subaddressing_modein … reg')
    363           | int_to_reg reg bv ⇒ λprf'.
    364             let b ≝ asm_byte_of_beval … prf' in
    365             let reg' ≝ register_address reg in
    366               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    367                                                              direct;
    368                                                              registr ]] x) → ? with
    369               [ REGISTER r ⇒ λregister7: True.
    370                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
    371               | ACC_A ⇒ λacc: True.
    372                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
    373               | DIRECT d ⇒ λdirect7: True.
    374                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
    375               | _ ⇒ λother: False. ⊥
    376               ] (subaddressing_modein … reg')
    377           | int_to_acc _ bv ⇒ λprf'.
    378             let b ≝ asm_byte_of_beval … prf' in
    379             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
     247                                                              registr ]] x → ? with
     248            [ REGISTER r ⇒ λregister8: True.
     249             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
     250            | ACC_A ⇒ λacc: True.
     251             Instruction (NOP ?)
     252            | DIRECT d ⇒ λdirect8: True.
     253             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
     254            | _ ⇒ Ⓧ
     255            ] (subaddressing_modein …)
     256          | int_to_reg reg b ⇒
     257            match register_address reg return λx.is_in … [[ acc_a;
     258                                                              direct;
     259                                                              registr ]] x → ? with
     260            [ REGISTER r ⇒ λregister7: True.
     261              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
     262            | ACC_A ⇒ λacc: True.
     263               if eq_bv … (bv_zero …) b then
     264                  Instruction (CLR ? ACC_A)
     265               else
     266                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
     267            | DIRECT d ⇒ λdirect7: True.
     268              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
     269            | _ ⇒ Ⓧ
     270            ] (subaddressing_modein …)
     271          | int_to_acc _ b ⇒
     272            if eq_bv … (bv_zero …) b then
     273              Instruction (CLR ? ACC_A)
     274            else
     275              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
    380276          ]
    381277        ]
    382       | COND _ lbl ⇒ λ_.
     278      | COND _ lbl ⇒
    383279        (* dpm: this should be handled in translate_code! *)
    384280        Instruction (JNZ ? (toASM_ident ? lbl))
     
    386282    ].
    387283  try @I
    388   assumption
    389284qed.
    390285
     
    411306  λglobals_old.
    412307  λprf.
    413   λid_def.
     308  λid_def : ident × (joint_function LIN globals_old).
    414309    let 〈id, def〉 ≝ id_def in
    415310    match def with
     
    436331let rec flatten_fun_defs
    437332  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
    438     (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function LIN globals_old))))
     333    (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old)))
    439334      on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
    440335  match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
     
    457352  λexit_label.
    458353  λmain.
    459   λfuncts.
     354  λfuncts : list (ident × (joint_function LIN ?)).
    460355  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
    461356  let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
     
    487382  let global_addr ≝ globals_addr (prog_vars … p) in
    488383  let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
    489   let 〈translated, funct_map〉 ≝ translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p) in
     384  let 〈translated, funct_map〉 ≝
     385    translate_functs global_addr (prog_var_names … p) ? exit_label
     386    (toASM_ident … (prog_main … p)) (prog_funct ?? p) in
    490387    〈〈funct_map, global_addr'〉, translated〉.
    491388 #i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
  • src/LIN/joint_LTL_LIN.ma

    r2286 r2490  
    44 | from_acc: Register → unit → registers_move
    55 | to_acc: unit → Register → registers_move
    6  | int_to_reg : Register → beval → registers_move
    7  | int_to_acc : unit → beval → registers_move.
     6 | int_to_reg : Register → Byte → registers_move
     7 | int_to_acc : unit → Byte → registers_move.
    88(* the last is redudant, but kept for notation's sake *)
    99
     
    2626    (* call_dest ≝ *) unit
    2727    (* ext_seq ≝ *) ltl_lin_seq
    28     (* ext_call ≝ *) void
    29     (* ext_tailcall ≝ *) void
     28    (* has_tailcalls ≝ *) false
    3029    (* paramsT ≝ *) unit
    3130    (* localsT ≝ *) void.
  • src/LTL/LTLToLIN.ma

    r2286 r2490  
    44
    55definition ltl_to_lin : ltl_program → lin_program ≝
    6  λp. transform_program … p (λvarnames. transf_fundef … (linearise_int_fun LTL_LIN varnames)).
     6  linearise ….
  • src/RTL/RTL.ma

    r2286 r2490  
    44  | rtl_stack_address: register → register → rtl_seq.
    55 
    6 inductive rtl_call : Type[0] ≝
    7   | rtl_call_ptr: register → register → list psd_argument → list register → rtl_call.
    8 
    9 inductive rtl_tailcall : Type[0] ≝
    10   | rtl_tailcall_id: ident → list psd_argument → rtl_tailcall
    11   | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    12 
    13 definition RTL_uns ≝ mk_unserialized_params
     6definition RTL_uns ≝ λhas_tailcalls.mk_unserialized_params
    147    (* acc_a_reg ≝ *) register
    158    (* acc_b_reg ≝ *) register
     
    2518    (* call_dest ≝ *) (list register)
    2619    (* ext_seq ≝ *) rtl_seq
    27     (* ext_call ≝ *) rtl_call
    28     (* ext_tailcall ≝ *) rtl_tailcall
     20    (* has_tailcalls ≝ *) has_tailcalls
    2921    (* paramsT ≝ *) (list register)
    3022    (* localsT ≝ *) register.
    3123
    32 definition RTL ≝ mk_graph_params RTL_uns.
     24definition RTL ≝ mk_graph_params (RTL_uns true).
    3325definition rtl_program ≝ joint_program RTL.
    3426
     
    7769(*---------------*) ⊢
    7870ext_seq RTL ≡ rtl_seq.
    79 unification hint 0 ≔
    80 (*---------------*) ⊢
    81 ext_call RTL ≡ rtl_call.
    82 unification hint 0 ≔
    83 (*---------------*) ⊢
    84 ext_tailcall RTL ≡ rtl_tailcall.
    8571
    8672coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
     
    9278(************ Same without tail calls ****************)
    9379
    94 definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
    95     (* acc_a_reg ≝ *) register
    96     (* acc_b_reg ≝ *) register
    97     (* acc_a_arg ≝ *) psd_argument
    98     (* acc_b_arg ≝ *) psd_argument
    99     (* dpl_reg   ≝ *) register
    100     (* dph_reg   ≝ *) register
    101     (* dpl_arg   ≝ *) psd_argument
    102     (* dph_arg   ≝ *) psd_argument
    103     (* snd_arg   ≝ *) psd_argument
    104     (* pair_move ≝ *) (register × psd_argument)
    105     (* call_args ≝ *) (list psd_argument)
    106     (* call_dest ≝ *) (list register)
    107     (* ext_seq ≝ *) rtl_seq
    108     (* ext_call ≝ *) rtl_call
    109     (* ext_tailcall ≝ *) void
    110     (* paramsT ≝ *) (list register)
    111     (* localsT ≝ *) register).
    112 
     80definition RTL_ntc ≝ mk_graph_params (RTL_uns false).
    11381definition rtl_ntc_program ≝ joint_program RTL_ntc.
  • src/RTL/RTLTailcall.ma

    r2286 r2490  
    44  λglobals.
    55  λexit: label.
    6   λlbl: label.
    76  λstmt: joint_statement RTL globals.
    8   λgraph: codeT RTL_ntc globals.
    97  match stmt with
    108  [ final fin ⇒
    119     match fin with
    12       [ tailcall ext ⇒
    13          match ext with
    14           [ rtl_tailcall_id f args ⇒
    15               add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
    16           | rtl_tailcall_ptr f1 f2 args ⇒
    17               add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
    18           ]
    19       | _ ⇒ graph ]
    20   | _ ⇒ graph ].
     10      [ TAILCALL _ f args ⇒ sequential … (CALL RTL_ntc ? f args [ ]) exit
     11      | RETURN ⇒ RETURN RTL_ntc
     12      | GOTO l ⇒ GOTO RTL_ntc l
     13      ]
     14  | sequential s next ⇒
     15    sequential RTL_ntc ?
     16    (match s return λ_.joint_step RTL_ntc globals with
     17    [ step_seq s ⇒
     18      match s return λ_.joint_seq RTL_ntc globals with
     19      [ COMMENT s ⇒ COMMENT … s
     20      | COST_LABEL l ⇒ COST_LABEL … l
     21      | MOVE m ⇒ MOVE … m
     22      | POP a ⇒ POP … a
     23      | PUSH a ⇒ PUSH … a
     24      | ADDRESS i prf dpl dph ⇒ ADDRESS … i prf dpl dph
     25      | OPACCS op a b arg1 arg2 ⇒ OPACCS … op a b arg1 arg2
     26      | OP1 op a arg ⇒ OP1 … op a arg
     27      | OP2 op a arg1 arg2 ⇒ OP2 … op a arg1 arg2
     28      | CLEAR_CARRY ⇒ CLEAR_CARRY ??
     29      | SET_CARRY ⇒ SET_CARRY ??
     30      | LOAD a dpl dph ⇒ LOAD … a dpl dph
     31      | STORE dpl dph a ⇒ STORE … dpl dph a
     32      | CALL f args dest ⇒ CALL … f args dest
     33      | extension_seq s ⇒ extension_seq … s
     34      ]
     35    | COND a ltrue ⇒ COND … a ltrue
     36    ]) next
     37  ].
     38
     39definition id_map_map : ∀tag,A,B.(A → B) → identifier_map tag A → identifier_map tag B ≝
     40λtag,A,B,f,m.
     41match m with
     42[ an_id_map m ⇒ an_id_map … (map … f m)
     43].
    2144
    2245definition simplify_graph ≝
     
    2447  λexit: label.
    2548  λgraph: codeT RTL globals.
    26     foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
     49  id_map_map … (simplify_stmt globals exit) graph.
    2750
    2851axiom simplify_graph_preserves_labels:
     
    3457definition simplify_internal :
    3558 ∀globals.
    36   joint_internal_function RTL globals →
    37    joint_internal_function RTL_ntc globals
     59  joint_closed_internal_function RTL globals →
     60   joint_closed_internal_function RTL_ntc globals
    3861
    3962  λglobals,def.
    4063    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
    41       mk_joint_internal_function …
     64    «mk_joint_internal_function …
    4265       (joint_if_luniverse … def) (joint_if_runiverse … def)
    4366       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
    4467       (joint_if_stacksize … def) graph
    45        (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
    46  [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
     68       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)), ?».
     69 [3: cases daemon (* TODO *)
     70 | cases (joint_if_exit … def) | cases (joint_if_entry … def) ]
    4771 #l #IH @simplify_graph_preserves_labels @IH
    4872qed.
  • src/RTL/RTLToERTL.ma

    r2286 r2490  
    222222        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
    223223      ]
    224     | CALL_ID f args ret_regs ⇒
     224    | CALL f args ret_regs ⇒
    225225      set_params ? args @@
    226       CALL_ID ERTL ? f (|args|) it :::
     226      CALL ERTL ? f (|args|) it :::
    227227      fetch_result ? ret_regs
    228     | extension_call c ⇒
    229       match c with
    230       [ rtl_call_ptr f1 f2 args dest ⇒
    231         ?
    232       ]
    233228    ]
    234229  | COND r ltrue ⇒
    235230    COND ERTL ? r ltrue
    236   ]. cases daemon (* pointer call to be ported yet *) qed.
     231  ].
    237232
    238233definition translate_fin_step :
     
    243238  [ GOTO lbl' ⇒ GOTO … lbl'
    244239  | RETURN ⇒ RETURN ?
    245   | tailcall abs ⇒ match abs in void with [ ]
     240  | TAILCALL abs _ _ ⇒ match abs in False with [ ]
    246241  ].
    247242
    248243(* hack with empty graphs used here *)
    249244definition translate_funct :
    250   ∀globals.joint_internal_function RTL_ntc globals →
    251     joint_internal_function ERTL globals ≝
     245  ∀globals.joint_closed_internal_function RTL_ntc globals →
     246    joint_closed_internal_function ERTL globals ≝
    252247  λglobals,def.
    253248  let nb_params ≝ |joint_if_params ?? def| in
     
    267262    def in
    268263  add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
     264 cases daemon (* TODO *) qed.
    269265
    270266(* removing this because of how insert_prologue is now defined
  • src/RTLabs/RTLabsToRTL.ma

    r2290 r2490  
    2626  [ ASTint isize sign ⇒
    2727    match isize with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    28   | ASTfloat _ ⇒ ? (* dpm: not implemented *)
    2928  | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *)
    3029  ].
    31   cases not_implemented
    32 qed.
    3330
    3431inductive register_type: Type[0] ≝
     
    161158  λr,lenv,prf. make_addr ? (find_local_env r lenv prf).
    162159
     160definition find_and_addr_arg ≝
     161  λr,lenv,prf. make_addr ? (find_local_env_arg r lenv prf).
     162
    163163include alias "common/Identifiers.ma".
    164164let rec rtl_args (args : list register) (env : local_env) on args :
     
    270270definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
    271271  [ Ointconst size _ _ ⇒ size_intsize size
    272   | Ofloatconst _ _ ⇒ ? (* not implemented *)
    273272  | _ ⇒ 2
    274273  ].
    275   cases not_implemented qed.
    276274
    277275definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
     
    296294      map2 … (λr.λb : Byte.r ← b) destrs
    297295        (split_into_bytes size const) ?
    298   | Ofloatconst _ _ ⇒ ?
    299296  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    300297    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     
    304301    [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
    305302  ] (pi2 … cst_sig).
    306   [2: cases not_implemented
    307   |1: cases (split_into_bytes ??) #lst
     303  [ cases (split_into_bytes ??) #lst
    308304    #EQ >EQ >prf whd in ⊢ (??%?); cases size %
    309   |3: @cst_prf
     305  | @cst_prf
    310306  |*: >prf %
    311307  ]
     
    337333     destr ← .Inc. destr ;
    338334     destr ← .Cmpl. destr ]
    339   | Imm by ⇒
    340     match by with
    341     [ BVByte b ⇒
    342       if sign_bit … b then
    343         [ destr ← (maximum … : Byte) ]
    344       else
    345         [ destr ← zero_byte ]
    346     | _ ⇒ (* should not happend ... *) [ ]
    347     ]
     335  | Imm b ⇒
     336    if sign_bit … b then
     337      [ destr ← (maximum … : Byte) ]
     338    else
     339      [ destr ← zero_byte ]
    348340  ].
    349341
     
    531523  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
    532524  ] (refl …) (refl …).
    533   [3,4,5,6,7,8,9: (* floats *)  cases not_implemented
    534   |*: destruct >prf1 >prf2 [3: >length_map ] //
    535   ]
     525  destruct >prf1 >prf2 [3: >length_map ] //
    536526qed.
    537527
    538528include alias "arithmetics/nat.ma".
    539 
    540 let rec range_strong_internal (start : ℕ) (count : ℕ)
    541   (* Paolo: no notation to avoid ambiguity *)
    542   on count : list (Σn : ℕ.lt n (plus start count)) ≝
    543 match count return λx.count = x → list (Σn : ℕ. n < start + count)
    544   with
    545 [ O ⇒ λ_.[ ]
    546 | S count' ⇒ λEQ.
    547   let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝
    548     λsig.match sig with [mk_Sig n prf ⇒ n] in
    549   start :: map … f (range_strong_internal (S start) count')
    550 ] (refl …).
    551 destruct(EQ) // qed.
    552 
    553 definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
    554   λend.range_strong_internal 0 end.
    555529
    556530definition translate_mul_i :
     
    1009983      (find_local_env_arg srcr lenv ?), lbl'❭
    1010984  | St_call_id f args retr lbl' ⇒ λstmt_typed.
    1011     ❬(match retr with
    1012       [ Some retr ⇒
    1013         CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
    1014       | None ⇒
    1015         CALL_ID RTL ? f (rtl_args args lenv ?) [ ]
    1016       ] : bind_seq_block ???), lbl'❭
     985    ❬(CALL RTL ? (inl … f) (rtl_args args lenv ?)
     986      (match retr with
     987      [ Some retr ⇒ find_local_env retr lenv ?
     988      | None ⇒ [ ]
     989      ]) : bind_seq_block ???), lbl'❭
    1017990  | St_call_ptr f args retr lbl' ⇒ λstmt_typed.
    1018     let fs ≝ find_and_addr f lenv ?? in
    1019     ❬(rtl_call_ptr (\fst fs) (\snd fs) (rtl_args args lenv ?)
     991    let fs ≝ find_and_addr_arg f lenv ?? in
     992    ❬(CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
    1020993      (match retr with
    1021994       [ Some retr ⇒
     
    10441017    | @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf)
    10451018    ]
    1046   |*: whd in stmt_typed; cases daemon (* TODO need more stringent statement_typed *)
     1019  |*: cases daemon (* TODO *)
    10471020  ]
    10481021qed.
     
    10521025   the start and end nodes to ensure that they are in, and place dummy
    10531026   skip instructions at these nodes. *)
    1054 definition translate_internal ≝
     1027definition translate_internal :
     1028  ∀globals.internal_function → (* insert here more properties *)
     1029  joint_closed_internal_function RTL globals ≝
    10551030  λglobals: list ident.
    10561031  λdef.
  • src/joint/Joint.ma

    r2462 r2490  
    1111   the ↓ edges are the only explicitly defined coercions). lin_params and
    1212   graph_params are simple wrappers of unserialized_params, and the coercions
    13    from them to params instantiate the missing bits with values for linarized
     13   from them to params instantate the missing bits with values for linarized
    1414   programs and graph programs respectively.
    1515
     
    3636inductive argument (T : Type[0]) : Type[0] ≝
    3737| Reg : T → argument T
    38 | Imm : beval → argument T.
     38| Imm : Byte → argument T.
    3939
    4040definition psd_argument ≝ argument register.
     
    4343coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg
    4444  on _r : register to psd_argument.
    45 
     45(*
    4646definition psd_argument_from_beval : beval → psd_argument ≝ Imm register.
    4747coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval
    4848  on _b : beval to psd_argument.
    49 
    50 definition psd_argument_from_byte : Byte → psd_argument ≝ λb.Imm ? (BVByte b).
     49*)
     50definition psd_argument_from_byte : Byte → psd_argument ≝ Imm ?.
    5151coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
    5252  on _b : Byte to psd_argument.
     
    5757coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg
    5858  on _r : Register to hdw_argument.
    59 
     59(*
    6060definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register.
    6161coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval
    6262  on _b : beval to hdw_argument.
    63 
    64 definition hdw_argument_from_byte : Byte → hdw_argument ≝ λb.Imm ? (BVByte b).
     63*)
     64definition hdw_argument_from_byte : Byte → hdw_argument ≝ Imm ?.
    6565coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
    6666  on _b : Byte to hdw_argument.
     
    9696  | POP: acc_a_reg p → joint_seq p globals
    9797  | PUSH: acc_a_arg p → joint_seq p globals
    98   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals
     98  | ADDRESS: ∀i: ident. (member ? (eq_identifier ?) i globals) → dpl_reg p → dph_reg p → joint_seq p globals
    9999  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
    100100  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
Note: See TracChangeset for help on using the changeset viewer.