Changeset 1275


Ignore:
Timestamp:
Sep 26, 2011, 6:07:47 PM (8 years ago)
Author:
sacerdot
Message:

RTL ported to joint syntax, but:

  1. bug discovered: opaccs should have taken four registers
  2. push/pop should not be present in RTL :-(

ERTLToLTL and RTLtoERTL not working ATM

Location:
src
Files:
1 deleted
7 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1274 r1275  
    22include "LTL/LTL.ma".
    33include "ERTL/spill.ma".
    4 include "ERTL/uses.ma".
    54include "ASM/Arithmetic.ma".
    65
     
    396395          〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
    397396      ]
    398     | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
     397    | joint_instr_opaccs opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    399398      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    400399      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
  • src/ERTL/liveness.ma

    r1271 r1275  
    8989    | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
    9090    | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
    91     | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     91    | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     92       lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2)
    9293    | joint_instr_op1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    9394    | joint_instr_pop r ⇒ lattice_psingleton r
     
    135136    | joint_instr_set_carry ⇒ lattice_bottom
    136137    (* acc_a and acc_b *)
    137     | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     138    | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     139       lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2)
    138140    | joint_instr_op1 op1 r1 r2 ⇒ lattice_psingleton r2
    139141    | joint_instr_pop r ⇒ lattice_bottom
     
    181183    | joint_instr_clear_carry ⇒ None ?
    182184    | joint_instr_set_carry ⇒ None ?
    183     | joint_instr_opaccs opaccs r1 r2 ⇒
    184       if set_member … (eq_identifier …) r1 pliveafter ∨
    185          set_member … (eq_identifier …) r2 pliveafter ∨
     185    | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     186      if set_member … (eq_identifier …) dr1 pliveafter ∨
     187         set_member … (eq_identifier …) dr2 pliveafter ∨
    186188         set_member … eq_Register RegisterCarry hliveafter then
    187189        None ?
  • src/LIN/LINToASM.ma

    r1270 r1275  
    9898      | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    9999      | joint_instr_call_id f _ _ ⇒ Call (word_of_identifier ? f)
    100       | joint_instr_opaccs accs _ _
     100      | joint_instr_opaccs accs _ _ _ _
    101101        match accs with
    102102        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
  • src/RTL/RTL.ma

    r1270 r1275  
    55  To be fixed once we understand exactly what to do with tail calls. *)
    66inductive rtl_statement_extension: Type[0] ≝
     7  | rtl_st_ext_address: register → register → rtl_statement_extension
    78  | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
    89  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
     
    2425
    2526definition rtl_program ≝ joint_program rtl_params.
     27
     28(************ Same without tail calls ****************)
     29
     30(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
     31  are not sequential. Thus there is a dummy label at the moment in the code.
     32  To be fixed once we understand exactly what to do with tail calls. *)
     33inductive rtlntc_statement_extension: Type[0] ≝
     34  | rtlntc_st_ext_address: register → register → rtlntc_statement_extension
     35  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension
     36  | rtlntc_st_ext_tailcall_id: ident → list register → rtlntc_statement_extension
     37  | rtlntc_st_ext_tailcall_ptr: register → register → list register → rtlntc_statement_extension.
     38
     39definition rtlntc_params_: params_ ≝
     40 mk_params_
     41  (mk_params__ register register register register
     42    (register × register) register (list register) (list register)
     43      rtlntc_statement_extension unit (list register) (list register)) label.
     44
     45definition rtlntc_statement ≝ joint_statement rtlntc_params_.
     46
     47definition rtlntc_params: ∀globals. params globals ≝ graph_params rtlntc_params_.
     48
     49definition rtlntc_internal_function ≝
     50  λglobals.
     51    joint_internal_function globals (rtlntc_params globals).
     52
     53definition rtlntc_program ≝ joint_program rtlntc_params.
  • src/RTL/RTLTailcall.ma

    r1270 r1275  
    66  λlbl: label.
    77  λstmt: rtl_statement globals.
    8   λgraph: codeT … (rtl_params globals).
     8  λgraph: codeT … (rtlntc_params globals).
    99  match stmt with
    1010  [ joint_st_sequential seq DUMMY ⇒
     
    1515              add ? ? graph lbl (joint_st_sequential … (joint_instr_call_id … f args [ ]) exit)
    1616          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
    17               add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtl_st_ext_call_ptr f1 f2 args [ ])) exit)
     17              add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
    1818          | _ ⇒ graph ]
    1919      | _ ⇒ graph ]
     
    2424  λexit: label.
    2525  λgraph: codeT … (rtl_params globals).
    26     foldi ? ? ? (simplify_stmt globals exit) graph graph.
     26    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
    2727
    2828axiom simplify_graph_preserves_labels:
     
    3636 ∀globals.
    3737  joint_internal_function … (rtl_params globals) →
    38    joint_internal_function … (rtl_params globals)
     38   joint_internal_function … (rtlntc_params globals)
    3939
    4040  λglobals,def.
     
    4949qed.
    5050
    51 definition tailcall_simplify : rtl_program → rtl_program ≝
     51definition tailcall_simplify : rtl_program → rtlntc_program ≝
    5252 λp. transform_program … p (transf_fundef … (simplify_internal …)).
  • src/RTL/RTLtoERTL.ma

    r1270 r1275  
    369369    ) start_lbl dest_lbl def.
    370370
    371 axiom translate_stmt :
    372  ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals.
    373 (*
     371definition translate_stmt :
     372 ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals
    374373 ≝
    375374  λglobals.
     
    378377  λdef.
    379378  match stmt with
    380   [ rtl_st_skip lbl' ⇒ add_graph … lbl (ertl_st_skip lbl') def
    381   | rtl_st_cost cost_lbl lbl' ⇒ add_graph … lbl (ertl_st_cost cost_lbl lbl') def
    382   | rtl_st_addr r1 r2 x lbl' ⇒ add_graph … lbl (ertl_st_addr r1 r2 x lbl') def
    383   | rtl_st_stack_addr r1 r2 lbl' ⇒
    384     adds_graph … [
    385       ertl_st_get_hdw r1 RegisterSPL lbl;
    386       ertl_st_get_hdw r2 RegisterSPH lbl
    387     ] lbl lbl' def
    388   | rtl_st_int r i lbl' ⇒  add_graph … lbl (ertl_st_int r i lbl') def
    389   | rtl_st_move r1 r2 lbl' ⇒ add_graph … lbl (ertl_st_move r1 r2 lbl') def
    390   | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
    391       add_graph … lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
    392   | rtl_st_op1 op1 destr srcr lbl' ⇒
    393     add_graph … lbl (ertl_st_op1 op1 destr srcr lbl') def
    394   | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
    395     add_graph … lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
    396   | rtl_st_clear_carry lbl' ⇒
    397     add_graph … lbl (ertl_st_clear_carry lbl') def
    398   | rtl_st_set_carry lbl' ⇒
    399     add_graph … lbl (ertl_st_set_carry lbl') def
    400   | rtl_st_load destr addr1 addr2 lbl' ⇒
    401     add_graph … lbl (ertl_st_load destr addr1 addr2 lbl') def
    402   | rtl_st_store addr1 addr2 srcr lbl' ⇒
    403     add_graph … lbl (ertl_st_store addr1 addr2 srcr lbl') def
    404   | rtl_st_call_id f args ret_regs lbl' ⇒
    405     translate_call_id … f args ret_regs lbl lbl' def
    406   | rtl_st_cond srcr lbl_true lbl_false ⇒
    407     add_graph … lbl (ertl_st_cond srcr lbl_true lbl_false) def
    408   | rtl_st_return ⇒
    409     add_graph … lbl ertl_st_return def
    410   | _ ⇒ ? (* assert false: not implemented or should not happen *)
    411   ].
     379  [ joint_st_goto lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
     380  | joint_st_return ⇒ add_graph … lbl (joint_st_return …) def
     381  | joint_st_sequential seq lbl' ⇒
     382     match seq with
     383      [ joint_instr_call_id f args ret_regs ⇒
     384         translate_call_id … f args ret_regs lbl lbl' def
     385      | joint_instr_move rs ⇒
     386         let 〈r1,r2〉 ≝ rs in
     387         let rs ≝ 〈pseudo r1, pseudo r2〉 in
     388          add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_move … rs) lbl') def
     389      | joint_instr_extension ext ⇒
     390         match ext with
     391          [ rtl_st_ext_call_ptr _ _ _ _ ⇒ ? (*CSC: XXXX not implemented in OCaml too *)
     392          | rtl_st_ext_address r1 r2 ⇒
     393             adds_graph … [
     394              joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
     395              joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
     396             ] lbl lbl' def
     397          (*| _ ⇒ ? (* assert false: not implemented or should not happen *)*)
     398          ]
     399      (*CSC: everything is just copied to re-type it from now on;
     400        the problem is call_id that takes different parameters, but that is pattern-matched
     401        above. It could be made nicer at the cost of making all the rest of the code uglier *)
     402      | joint_instr_cost_label cost_lbl ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cost_label … cost_lbl) lbl') def
     403      | joint_instr_address x prf r1 r2 ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_address … x prf r1 r2) lbl') def
     404      | joint_instr_int r i ⇒  add_graph … lbl (joint_st_sequential ertl_params_ globals (joint_instr_int … r i) lbl') def
     405      | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒
     406          add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
     407      | joint_instr_op1 op1 destr srcr ⇒
     408        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op1 … op1 destr srcr) lbl') def
     409      | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
     410        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
     411      | joint_instr_clear_carry ⇒
     412        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_clear_carry …) lbl') def
     413      | joint_instr_set_carry ⇒
     414        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_set_carry …) lbl') def
     415      | joint_instr_load destr addr1 addr2 ⇒
     416        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_load … destr addr1 addr2) lbl') def
     417      | joint_instr_store addr1 addr2 srcr ⇒
     418        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_store … addr1 addr2 srcr) lbl') def
     419      | joint_instr_cond srcr lbl_true ⇒
     420        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cond … srcr lbl_true) lbl') def
     421      | joint_instr_comment msg ⇒
     422        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_comment … msg) lbl') def
     423      | joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     424      | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     425      ]].
    412426  cases not_implemented
    413 qed.*) 
     427qed.
    414428
    415429(* hack with empty graphs used here *)
     
    429443      graph' ? ? in
    430444  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
    431   let def' ≝ add_pro_and_epilogue … (joint_if_params … def) (joint_if_result … def) def' in
    432     def'.
     445   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
    433446whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
    434447                                 makes the next application fail. Why? *)   
     
    485498definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
    486499
    487 (*
    488 definition move_first_cost_label_up ≝
    489   λglobals.
    490   λA: Type[0].
    491   λid_def: A × ?.
    492   let 〈id, def〉 ≝ id_def in
    493   let def' ≝
    494     match def with
    495     [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal … (translate_funct_internal globals int_fun))
    496     | External ext ⇒ External … ext
    497     ]
    498   in
    499     〈id, def'〉.
    500 
    501 definition translate ≝
    502   λp.
    503   let p ≝ tailcall_simplify p in (* tailcall simplification here *)
    504   let f ≝ λfunct. move_first_cost_label_up ? funct in
    505   let vars ≝ map ? ? f (rtl_pr_functs p) in
    506     mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
    507 *)
    508 
    509500definition translate : rtl_program → ertl_program ≝
    510501 λp.
    511502  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
    512     transform_program ??? p (transf_fundef ?? translate_funct).
     503    transform_program ??? p (transf_fundef ?? (translate_funct …)).
  • src/joint/Joint.ma

    r1271 r1275  
    3636  | joint_instr_push: acc_a_reg p → joint_instruction p globals
    3737  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    38   | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
     38  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
    3939  | joint_instr_op1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    4040  | joint_instr_op2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
Note: See TracChangeset for help on using the changeset viewer.