Changeset 1270


Ignore:
Timestamp:
Sep 26, 2011, 3:59:28 PM (8 years ago)
Author:
sacerdot
Message:

Making RTL syntax an instance of Joint.

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1269 r1270  
    1313 mk_params_
    1414  (mk_params__ register register register register
    15     (move_registers × move_registers) register
     15    (move_registers × move_registers) register nat unit
    1616      ertl_statement_extension unit (list register) nat) label.
    1717
  • src/LIN/LIN.ma

    r1264 r1270  
    33
    44definition lin_params_: params_ ≝
    5  mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) unit.
     5 mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) unit.
    66
    77definition pre_lin_statement ≝ joint_statement lin_params_.
  • src/LIN/LINToASM.ma

    r1268 r1270  
    9797      | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address)
    9898      | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    99       | joint_instr_call_id f _ ⇒ Call (word_of_identifier ? f)
     99      | joint_instr_call_id f _ _ ⇒ Call (word_of_identifier ? f)
    100100      | joint_instr_opaccs accs _ _ ⇒
    101101        match accs with
  • src/LTL/LTL.ma

    r1269 r1270  
    22
    33definition ltl_params_: params_ ≝
    4  mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) label.
     4 mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) label.
    55
    66definition ltl_statement ≝ joint_statement ltl_params_.
  • src/RTL/RTL.ma

    r1239 r1270  
    1 include "basics/list.ma".
    2 include "common/Registers.ma".
    3 include "common/AST.ma".
    4 include "common/Graphs.ma".
    5 include "common/CostLabel.ma".
     1include "joint/Joint.ma".
    62
    7 definition registers ≝ list register.
     3(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
     4  are not sequential. Thus there is a dummy label at the moment in the code.
     5  To be fixed once we understand exactly what to do with tail calls. *)
     6inductive rtl_statement_extension: Type[0] ≝
     7  | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
     8  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
     9  | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
    810
    9 inductive rtl_statement: Type[0] ≝
    10   | rtl_st_skip: label → rtl_statement
    11   | rtl_st_cost: costlabel → label → rtl_statement
    12                 (* ldest, hdest, symbol, next *)
    13   | rtl_st_addr: register → register → ident → label → rtl_statement
    14                 (* ldest, hdest, next *)
    15   | rtl_st_stack_addr: register → register → label → rtl_statement
    16   | rtl_st_int: register → Byte → label → rtl_statement
    17                 (* dest, src, next *)
    18   | rtl_st_move: register → register → label → rtl_statement
    19   | rtl_st_clear_carry: label → rtl_statement
    20                 (* op, acc dest, bacc dest, acc src, bacc src, next *)
    21   | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
    22                 (* op, dest, src, next *)
    23   | rtl_st_op1: Op1 → register → register → label → rtl_statement
    24                 (* op, dest, src1, src2, next *)
    25   | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
    26   | rtl_st_load: register → register → register → label → rtl_statement
    27   | rtl_st_store: register → register → register → label → rtl_statement
    28   | rtl_st_call_id: ident → registers → registers → label → rtl_statement
    29   | rtl_st_call_ptr: register → register → registers → registers → label → rtl_statement
    30   | rtl_st_tailcall_id: ident → registers → rtl_statement
    31   | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
    32   | rtl_st_cond: register → label → label → rtl_statement
    33   | rtl_st_set_carry: label → rtl_statement
    34   | rtl_st_return: rtl_statement.
    35  
    36 definition rtl_statement_graph ≝ graph rtl_statement.
     11definition rtl_params_: params_ ≝
     12 mk_params_
     13  (mk_params__ register register register register
     14    (register × register) register (list register) (list register)
     15      rtl_statement_extension unit (list register) (list register)) label.
    3716
    38 record rtl_internal_function: Type[0] ≝
    39 {
    40   rtl_if_luniverse: universe LabelTag;
    41   rtl_if_runiverse: universe RegisterTag;
    42 (*  rtl_if_sig: signature;  -- dropped in front end *)
    43   rtl_if_result   : registers;
    44   rtl_if_params   : registers;
    45   rtl_if_locals   : registers;
    46   rtl_if_stacksize: nat;
    47   rtl_if_graph    : rtl_statement_graph;
    48   rtl_if_entry    : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?;
    49   rtl_if_exit     : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?
    50 }.
     17definition rtl_statement ≝ joint_statement rtl_params_.
    5118
    52 definition rtl_function_definition ≝ fundef rtl_internal_function.
     19definition rtl_params: ∀globals. params globals ≝ graph_params rtl_params_.
    5320
    54 definition rtl_program: Type[0] ≝ program (λ_.rtl_function_definition) nat.
     21definition rtl_internal_function ≝
     22  λglobals.
     23    joint_internal_function globals (rtl_params globals).
     24
     25definition rtl_program ≝ joint_program rtl_params.
  • src/RTL/RTLTailcall.ma

    r1240 r1270  
    22
    33definition simplify_stmt ≝
     4  λglobals.
    45  λexit: label.
    56  λlbl: label.
    6   λstmt.
    7   λgraph: rtl_statement_graph.
     7  λstmt: rtl_statement globals.
     8  λgraph: codeT … (rtl_params globals).
    89  match stmt with
    9   [ rtl_st_tailcall_id f args ⇒
    10       add ? ? graph lbl (rtl_st_call_id f args [ ] exit)
    11   | rtl_st_tailcall_ptr f1 f2 args ⇒
    12       add ? ? graph lbl (rtl_st_call_ptr f1 f2 args [ ] exit)
    13   | _ ⇒ graph
    14   ].
     10  [ joint_st_sequential seq DUMMY ⇒
     11     match seq with
     12      [ joint_instr_extension ext ⇒
     13         match ext with
     14          [ rtl_st_ext_tailcall_id f args ⇒
     15              add ? ? graph lbl (joint_st_sequential … (joint_instr_call_id … f args [ ]) exit)
     16          | 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)
     18          | _ ⇒ graph ]
     19      | _ ⇒ graph ]
     20  | _ ⇒ graph ].
    1521
    1622definition simplify_graph ≝
     23  λglobals.
    1724  λexit: label.
    18   λgraph: rtl_statement_graph.
    19     foldi ? ? ? (simplify_stmt exit) graph graph.
     25  λgraph: codeT … (rtl_params globals).
     26    foldi ? ? ? (simplify_stmt globals exit) graph graph.
    2027
    2128axiom simplify_graph_preserves_labels:
    22   ∀g: rtl_statement_graph.
     29  ∀globals.
     30  ∀g: codeT … (rtl_params globals).
    2331  ∀l: label.
    2432  ∀exit: label.
    25     lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?.
     33    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
    2634   
    27 definition simplify_internal ≝
    28   λdef.
    29     let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    30     let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    31     let rtl_if_result' ≝ rtl_if_result def in
    32     let rtl_if_params' ≝ rtl_if_params def in
    33     let rtl_if_locals' ≝ rtl_if_locals def in
    34     let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    35     let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in
    36     let rtl_if_entry' ≝ rtl_if_entry def in
    37     let rtl_if_exit' ≝ rtl_if_exit def in
    38       mk_rtl_internal_function
    39         rtl_if_luniverse' rtl_if_runiverse'
    40         rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
    41         rtl_if_graph' ? ?.
    42   normalize nodelta
    43   [1: cases rtl_if_entry'
    44       #ENTRY #ENTRY_PRF
    45       %
    46       [1: @ENTRY
    47       |2: @simplify_graph_preserves_labels
    48           @ENTRY_PRF
    49       ]
    50   |2: cases rtl_if_exit'
    51       #EXIT #EXIT_PRF
    52       %
    53       [1: @EXIT
    54       |2: @simplify_graph_preserves_labels
    55           @EXIT_PRF
    56       ]
    57   ]
     35definition simplify_internal :
     36 ∀globals.
     37  joint_internal_function … (rtl_params globals) →
     38   joint_internal_function … (rtl_params globals)
     39
     40  λglobals,def.
     41    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
     42      mk_joint_internal_function …
     43       (joint_if_luniverse … def) (joint_if_runiverse … def)
     44       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
     45       (joint_if_stacksize … def) graph
     46       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
     47 [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
     48 #l #IH @simplify_graph_preserves_labels @IH
    5849qed.
    5950
    6051definition tailcall_simplify : rtl_program → rtl_program ≝
    61  λp. transform_program … p (transf_fundef … simplify_internal).
     52 λp. transform_program … p (transf_fundef … (simplify_internal …)).
  • src/RTL/RTLtoERTL.ma

    r1262 r1270  
    364364    add_translates globals (
    365365      set_params … args @ [
    366       adds_graph … [ joint_st_sequential … (joint_instr_call_id … f nb_args) start_lbl ];
     366      adds_graph … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];
    367367      fetch_result … ret_regs
    368368      ]
     
    370370
    371371axiom translate_stmt :
    372  ∀globals: list ident. label → rtl_statement → ertl_internal_function globals → ertl_internal_function globals.
     372 ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals.
    373373(*
    374374 ≝
     
    415415(* hack with empty graphs used here *)
    416416definition translate_funct_internal ≝
    417   λglobals,def.
    418   let nb_params ≝ |rtl_if_params def| in
     417  λglobals.λdef:rtl_internal_function globals.
     418  let nb_params ≝ |joint_if_params ?? def| in
    419419  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
    420   let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
    421   let entry' ≝ rtl_if_entry def in
    422   let exit' ≝ rtl_if_exit def in
     420  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
     421  let entry' ≝ joint_if_entry … def in
     422  let exit' ≝ joint_if_exit … def in
    423423  let graph' ≝ add ? ? (empty_map ? ?) entry' (joint_st_goto … entry') in
    424424  let graph' ≝ add ? ? graph' exit' (joint_st_goto … exit') in
    425425  let def' ≝
    426426    mk_joint_internal_function globals (ertl_params globals)
    427       (rtl_if_luniverse def) (rtl_if_runiverse … def) it
    428       nb_params new_locals ((rtl_if_stacksize … def) + added_stacksize)
     427      (joint_if_luniverse … def) (joint_if_runiverse … def) it
     428      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    429429      graph' ? ? in
    430   let def' ≝ foldi ? ? ? (translate_stmt globals) (rtl_if_graph def) def' in
    431   let def' ≝ add_pro_and_epilogue … (rtl_if_params def) (rtl_if_result def) def' in
     430  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
    432432    def'.
    433433whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
  • src/joint/Joint.ma

    r1260 r1270  
    1313 ; pair_reg: Type[0]
    1414 ; generic_reg: Type[0]
     15 ; call_args: Type[0]
     16 ; call_dest: Type[0]
    1517 
    1618 ; extend_statements: Type[0]
     
    4143  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
    4244  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    43   | joint_instr_call_id: ident → nat → joint_instruction p globals
     45  | joint_instr_call_id: ident → call_args p → call_dest p → joint_instruction p globals
    4446  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals
    4547  | joint_instr_extension: extend_statements p → joint_instruction p globals.
Note: See TracChangeset for help on using the changeset viewer.