Changeset 2490 for src/RTL


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/RTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.