Changeset 2214 for src/RTL


Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (8 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
Location:
src/RTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall_paolo.ma

    r2162 r2214  
    55  λexit: label.
    66  λlbl: label.
    7   λstmt: rtl_statement globals.
    8   λgraph: codeT rtlntc_params globals.
     7  λstmt: joint_statement RTL globals.
     8  λgraph: codeT RTL_ntc globals.
    99  match stmt with
    1010  [ final fin ⇒
     
    1313         match ext with
    1414          [ rtl_tailcall_id f args ⇒
    15               add … graph lbl (sequential … (CALL_ID rtlntc_params ? f args [ ]) exit)
     15              add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
    1616          | rtl_tailcall_ptr f1 f2 args ⇒
    17               add … graph lbl (sequential rtlntc_params ? (rtl_call_ptr f1 f2 args [ ] : ext_call rtlntc_params) exit)
     17              add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
    1818          ]
    1919      | _ ⇒ graph ]
     
    2323  λglobals.
    2424  λexit: label.
    25   λgraph: codeT rtl_params globals.
     25  λgraph: codeT RTL globals.
    2626    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
    2727
    2828axiom simplify_graph_preserves_labels:
    2929  ∀globals.
    30   ∀g: codeT rtl_params globals.
     30  ∀g: codeT RTL globals.
    3131  ∀exit: label.
    3232  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
     
    3434definition simplify_internal :
    3535 ∀globals.
    36   joint_internal_function globals rtl_params →
    37    joint_internal_function globals rtlntc_params
     36  joint_internal_function RTL globals →
     37   joint_internal_function RTL_ntc globals
    3838
    3939  λglobals,def.
     
    4848qed.
    4949
    50 definition tailcall_simplify : rtl_program → rtlntc_program ≝
     50definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
    5151 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
  • src/RTL/RTLToERTL_paolo.ma

    r2208 r2214  
    88
    99definition save_hdws :
    10   ∀globals.list (register×Register) → list (joint_seq ertl_params globals) ≝
     10  ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝
    1111 λglobals.
    1212  let save_hdws_internal ≝
     
    1515
    1616definition restore_hdws :
    17   ∀globals.list (psd_argument×Register) → list (joint_seq ertl_params globals) ≝
     17  ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
    1818  λglobals.
    1919   let restore_hdws_internal ≝
     
    2222
    2323definition get_params_hdw :
    24   ∀globals.list register → list (joint_seq ertl_params globals) ≝
     24  ∀globals.list register → list (joint_seq ERTL globals) ≝
    2525  λglobals,params.
    2626  save_hdws … (zip_pottier … params RegisterParams).
     
    2828definition get_param_stack :
    2929  ∀globals.register → register → register →
    30   list (joint_seq ertl_params globals) ≝
     30  list (joint_seq ERTL globals) ≝
    3131  λglobals,addr1,addr2,destr.
    3232  (* liveness analysis will erase the last useless ops *)
     
    3838definition get_params_stack :
    3939  ∀globals.list register →
    40   bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
     40  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
    4141  λglobals,params.
    4242  νtmpr,addr1,addr2 in
     
    5959definition prologue :
    6060  ∀globals.list register → register → register → list (register×Register) →
    61   bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
     61  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
    6262  λglobals,params,sral,srah,sregs.
    6363  [ (ertl_new_frame : joint_seq ??) ;
     
    6767
    6868definition save_return :
    69   ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
     69  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
    7070  λglobals,ret_regs.
    7171  match reduce_strong ? ? RegisterSTS ret_regs with
     
    7979  ].
    8080
    81 definition assign_result : ∀globals.list (joint_seq ertl_params globals) ≝
     81definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
    8282  λglobals.
    8383  match reduce_strong ?? RegisterRets RegisterSTS with
     
    9090definition epilogue :
    9191  ∀globals.list register → register → register → list (register × Register) →
    92   list (joint_seq ertl_params globals) ≝
     92  list (joint_seq ERTL globals) ≝
    9393  λglobals,ret_regs,sral,srah,sregs.
    9494  save_return … (map … (Reg ?) ret_regs) @
    9595  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
    96   [ PUSH ertl_params ? srah ;
     96  [ PUSH ERTL ? srah ;
    9797    PUSH … sral ;
    9898    ertl_del_frame ] @
     
    101101definition allocate_regs :
    102102  ∀globals,rs.rs_set rs →
    103   state_monad (joint_internal_function globals ertl_params) (list (register×Register)) ≝
     103  state_monad (joint_internal_function ERTL globals) (list (register×Register)) ≝
    104104  λglobals,rs,saved,def.
    105105   let allocate_regs_internal ≝
     
    112112definition add_pro_and_epilogue :
    113113  ∀globals.list register → list register →
    114   joint_internal_function globals ertl_params →
    115   joint_internal_function globals ertl_params ≝
     114  joint_internal_function ERTL globals →
     115  joint_internal_function ERTL globals ≝
    116116  λglobals,params,ret_regs,def.
    117117  let start_lbl ≝ joint_if_entry … def in
     
    129129
    130130definition set_params_hdw :
    131   ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
     131  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
    132132  λglobals,params.
    133133  restore_hdws globals (zip_pottier ? ? params RegisterParams).
     
    137137definition set_param_stack :
    138138  ∀globals.register → register → psd_argument →
    139   list (joint_seq ertl_params globals) ≝
     139  list (joint_seq ERTL globals) ≝
    140140  λglobals,addr1,addr2,arg.
    141141  [ STORE … addr1 addr2 arg ;
     
    145145
    146146definition set_params_stack :
    147   ∀globals.list psd_argument → bind_new (localsT ertl_params) ? ≝
     147  ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
    148148  λglobals,params.
    149149  νaddr1,addr2 in
     
    166166
    167167definition fetch_result :
    168   ∀globals.list register → list (joint_seq ertl_params globals) ≝
     168  ∀globals.list register → list (joint_seq ERTL globals) ≝
    169169  λglobals,ret_regs.
    170170  match reduce_strong ?? RegisterSTS RegisterRets with
     
    182182
    183183definition translate_step :
    184   ∀globals.label → joint_step rtlntc_params globals →
    185     bind_seq_block ertl_params globals (joint_step ertl_params globals) ≝
     184  ∀globals.label → joint_step RTL_ntc globals →
     185    bind_seq_block ERTL globals (joint_step ERTL globals) ≝
    186186  λglobals.λ_.λs.
    187187  match s return λ_.bind_seq_block ?? (joint_step ??) with
     
    194194      COST_LABEL … lbl
    195195    | ADDRESS x prf r1 r2 ⇒
    196       ADDRESS ertl_params ? x prf r1 r2
     196      ADDRESS ERTL ? x prf r1 r2
    197197    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    198       OPACCS ertl_params ? op destr1 destr2 srcr1 srcr2 
     198      OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 
    199199    | OP1 op1 destr srcr ⇒
    200       OP1 ertl_params ? op1 destr srcr
     200      OP1 ERTL ? op1 destr srcr
    201201    | OP2 op2 destr srcr1 srcr2 ⇒
    202       OP2 ertl_params ? op2 destr srcr1 srcr2
     202      OP2 ERTL ? op2 destr srcr1 srcr2
    203203    | CLEAR_CARRY ⇒
    204204      CLEAR_CARRY …
     
    206206      SET_CARRY …
    207207    | LOAD destr addr1 addr2 ⇒
    208       LOAD ertl_params ? destr addr1 addr2
     208      LOAD ERTL ? destr addr1 addr2
    209209    | STORE addr1 addr2 srcr ⇒
    210       STORE ertl_params ? addr1 addr2 srcr
     210      STORE ERTL ? addr1 addr2 srcr
    211211    | COMMENT msg ⇒
    212212      COMMENT … msg
     
    218218    | CALL_ID f args ret_regs ⇒
    219219      set_params ? args @@
    220       CALL_ID ertl_params ? f (|args|) it :::
     220      CALL_ID ERTL ? f (|args|) it :::
    221221      fetch_result ? ret_regs
    222222    | extension_call c ⇒
     
    227227    ]
    228228  | COND r ltrue ⇒
    229     COND ertl_params ? r ltrue
     229    COND ERTL ? r ltrue
    230230  ]. cases daemon (* pointer call to be ported yet *) qed.
    231231
    232232definition translate_fin_step :
    233   ∀globals.label → joint_fin_step rtlntc_params
    234     bind_seq_block ertl_params globals (joint_fin_step ertl_params) ≝
     233  ∀globals.label → joint_fin_step RTL_ntc
     234    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
    235235  λglobals.λ_.λs.
    236236  match s with
     
    242242(* hack with empty graphs used here *)
    243243definition translate_funct :
    244   ∀globals.joint_internal_function globals rtlntc_params →
    245     joint_internal_function globals ertl_params ≝
     244  ∀globals.joint_internal_function RTL_ntc globals →
     245    joint_internal_function ERTL globals ≝
    246246  λglobals,def.
    247247  let nb_params ≝ |joint_if_params ?? def| in
     
    253253  let graph' ≝ add ? ? graph' exit' (RETURN …) in
    254254  let def' ≝
    255     mk_joint_internal_function globals ertl_params
     255    mk_joint_internal_function ERTL globals
    256256      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
    257257      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
     
    272272  λglobals.
    273273  λstmt.
    274   λdef: joint_internal_function globals ertl_params.
     274  λdef: joint_internal_function globals ERTL.
    275275  let 〈entry, def〉 ≝ fresh_label … def in
    276276  let graph ≝ add … (joint_if_code … def) entry stmt in
    277    set_joint_if_graph … (ertl_params globals) graph def ??.
     277   set_joint_if_graph … (ERTL globals) graph def ??.
    278278  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
    279279  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
     
    295295         match inst with
    296296          [ COST_LABEL cost_lbl ⇒
    297              〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
     297             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
    298298          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    299299      | RETURN ⇒ 〈None …, def〉
     
    310310  match cost_label with
    311311  [ None ⇒ def
    312   | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
     312  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
    313313  ].
    314314
  • src/RTL/RTL_paolo.ma

    r2208 r2214  
    1111  | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    1212
    13 definition rtl_uns_params ≝ mk_unserialized_params
     13definition RTL_uns ≝ mk_unserialized_params
    1414  (mk_step_params
    1515    (* acc_a_reg ≝ *) register
     
    3535      (* localsT ≝ *) register).
    3636
    37 definition rtl_params ≝ mk_graph_params rtl_uns_params.
    38 definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
    39 definition rtl_internal_function ≝
    40   λglobals. joint_internal_function globals rtl_params.
    41 definition rtl_program ≝ joint_program rtl_params.
    42 definition rtl_step ≝ joint_step rtl_params.
    43 definition rtl_seq ≝ joint_seq rtl_params.
    44 definition rtl_statement ≝ joint_statement rtl_params.
     37definition RTL ≝ mk_graph_params RTL_uns.
     38definition rtl_program ≝ joint_program RTL.
    4539
    46 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)).
     40interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
    4741
    4842(* aid unification *)
     
    5044unification hint 0 ≔
    5145(*---------------*) ⊢
    52 acc_a_reg rtl_params ≡ register.
     46acc_a_reg RTL ≡ register.
    5347unification hint 0 ≔
    5448(*---------------*) ⊢
    55 acc_b_reg rtl_params ≡ register.
     49acc_b_reg RTL ≡ register.
    5650unification hint 0 ≔
    5751(*---------------*) ⊢
    58 acc_a_arg rtl_params ≡ psd_argument.
     52acc_a_arg RTL ≡ psd_argument.
    5953unification hint 0 ≔
    6054(*---------------*) ⊢
    61 acc_b_arg rtl_params ≡ psd_argument.
     55acc_b_arg RTL ≡ psd_argument.
    6256unification hint 0 ≔
    6357(*---------------*) ⊢
    64 dpl_reg rtl_params ≡ register.
     58dpl_reg RTL ≡ register.
    6559unification hint 0 ≔
    6660(*---------------*) ⊢
    67 dph_reg rtl_params ≡ register.
     61dph_reg RTL ≡ register.
    6862unification hint 0 ≔
    6963(*---------------*) ⊢
    70 dpl_arg rtl_params ≡ psd_argument.
     64dpl_arg RTL ≡ psd_argument.
    7165unification hint 0 ≔
    7266(*---------------*) ⊢
    73 dph_arg rtl_params ≡ psd_argument.
     67dph_arg RTL ≡ psd_argument.
    7468unification hint 0 ≔
    7569(*---------------*) ⊢
    76 snd_arg rtl_params ≡ psd_argument.
     70snd_arg RTL ≡ psd_argument.
    7771unification hint 0 ≔
    7872(*---------------*) ⊢
    79 pair_move rtl_params ≡ register × psd_argument.
     73pair_move RTL ≡ register × psd_argument.
    8074unification hint 0 ≔
    8175(*---------------*) ⊢
    82 call_args rtl_params ≡ list psd_argument.
     76call_args RTL ≡ list psd_argument.
    8377unification hint 0 ≔
    8478(*---------------*) ⊢
    85 call_dest rtl_params ≡ list register.
     79call_dest RTL ≡ list register.
    8680
    8781unification hint 0 ≔
    8882(*---------------*) ⊢
    89 ext_seq rtl_params ≡ rtl_seq.
     83ext_seq RTL ≡ rtl_seq.
    9084unification hint 0 ≔
    9185(*---------------*) ⊢
    92 ext_call rtl_params ≡ rtl_call.
     86ext_call RTL ≡ rtl_call.
    9387unification hint 0 ≔
    9488(*---------------*) ⊢
    95 ext_tailcall rtl_params ≡ rtl_tailcall.
    96 unification hint 0 ≔ globals
    97 (*---------------*) ⊢
    98 joint_step rtl_params globals ≡ rtl_step globals.
     89ext_tailcall RTL ≡ rtl_tailcall.
    9990
    100 unification hint 0 ≔ globals
    101 (*---------------*) ⊢
    102 joint_seq rtl_params globals ≡ rtl_seq globals.
    103 unification hint 0 ≔ globals
    104 (*---------------*) ⊢
    105 joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    106 
    107 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg
    108   on _r : register to snd_arg rtl_params.
    109 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte
    110   on _b : Byte to snd_arg rtl_params.
     91coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
     92  on _r : register to snd_arg RTL.
     93coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
     94  on _b : Byte to snd_arg RTL.
    11195
    11296
    11397(************ Same without tail calls ****************)
    11498
    115 definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
     99definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
    116100  (mk_step_params
    117101    (* acc_a_reg ≝ *) register
     
    137121      (* localsT ≝ *) register)).
    138122
    139 definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
    140 
    141 definition rtlntc_internal_function ≝
    142   λglobals. joint_internal_function … globals rtlntc_params.
    143 
    144 definition rtlntc_program ≝ joint_program rtlntc_params.
     123definition rtl_ntc_program ≝ joint_program RTL_ntc.
Note: See TracChangeset for help on using the changeset viewer.