Changeset 2681 for src/RTL/RTLToERTL.ma


Ignore:
Timestamp:
Feb 19, 2013, 6:48:32 PM (7 years ago)
Author:
tranquil
Message:
  • improvements to the graph translation function
  • fixed passes up to LTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r2659 r2681  
    11include "utilities/RegisterSet.ma".
    22include "common/Identifiers.ma".
     3include "RTL/RTL.ma".
    34include "ERTL/ERTL.ma".
    45include "joint/TranslateUtils.ma".
    56
    67include alias "basics/lists/list.ma".
    7 
    8 definition ertl_fresh_reg:
    9  ∀globals.freshT ERTL globals register ≝
    10   λglobals,def.
    11     let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    12     〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
    138
    149definition save_hdws :
     
    4338definition get_params_stack :
    4439  ∀globals.list register →
    45   bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
     40  bind_new register (list (joint_seq ERTL globals)) ≝
    4641  λglobals,params.
    4742  νtmpr,addr1,addr2 in
     
    6156  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
    6257  get_params_hdw globals hdw_params @@ get_params_stack … stack_params.
    63 
    64 definition prologue :
    65   ∀globals.list register → register → register → list (register×Register) →
    66   bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
    67   λglobals,params,sral,srah,sregs.
    68   [ (ertl_new_frame : joint_seq ??) ;
    69     POP … sral ;
    70     POP … srah
    71   ] @@ save_hdws … sregs @@ get_params … params.
    7258
    7359definition save_return :
     
    9379  ].
    9480
     81lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf.
     82 All2 A B P l1 l2 →
     83 (∀x,y.P x y → R (f x y)) →
     84 All C R (map2 A B C f l1 l2 prf).
     85#A #B #C #P #R #f #l1 elim l1 -l1
     86[ * [ #prf * #H % ] #hd' #tl'
     87| #hd #tl #IH * [2: #hd' #tl' ]
     88] #prf normalize in prf; destruct
     89* #H1 #H2 #H % [ @H @H1 | @IH assumption ] qed.
     90
     91lemma All2_True : ∀A,B,l1,l2.|l1| = |l2| → All2 A B (λ_.λ_.True) l1 l2.
     92#A #B #l1 elim l1 -l1
     93[ * [ #prf % ] #hd' #tl'
     94| #hd #tl #IH * [2: #hd' #tl' ]
     95] #prf normalize in prf; destruct %{I} @IH assumption
     96qed.
     97
     98lemma All_True : ∀A,l.All A (λ_.True) l.
     99#A #l elim l -l [ % | #hd #tl #IH %{I IH} ] qed.
     100
    95101definition epilogue :
    96102  ∀globals.list register → register → register → list (register × Register) →
    97   list (joint_seq ERTL globals) ≝
     103  Σl : list (joint_seq ERTL globals).
     104  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
    98105  λglobals,ret_regs,sral,srah,sregs.
    99106  save_return … (map … (Reg ?) ret_regs) @
     
    103110    ertl_del_frame ] @
    104111  assign_result globals.
    105 
    106 definition allocate_regs :
    107   ∀globals,rs.rs_set rs →
    108   freshT ERTL globals (list (register×Register)) ≝
    109   λglobals,rs,saved,def.
    110    let allocate_regs_internal ≝
    111     λr: Register.
    112     λdef_sregs.
    113     let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in
    114     〈def, 〈r', r〉::\snd def_sregs〉 in
    115   rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉.
    116 
    117 definition add_pro_and_epilogue :
    118   ∀globals.list register → list register →
    119   joint_internal_function ERTL globals →
    120   joint_internal_function ERTL globals ≝
    121   λglobals,params,ret_regs,def.
    122   let start_lbl ≝ joint_if_entry … def in
    123   let end_lbl ≝ joint_if_exit … def in
    124   state_run … def (
    125     ! sral ← ertl_fresh_reg … ;
    126     ! srah ← ertl_fresh_reg … ;
    127     ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ;
    128     ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ;
    129     let epilogue' ≝ epilogue … ret_regs sral srah sregs in
    130     ! def' ← state_get … ;
    131     let def'' ≝ insert_prologue … prologue' def' in
    132     return insert_epilogue … epilogue' def''
    133   ).
     112@hide_prf
     113@All_append
     114[ whd in match save_return; normalize nodelta
     115  cases (reduce_strong ????) ** #a #b * #c #d #prf normalize nodelta
     116  @All_append
     117  [ @(All_map2 … (All2_True … prf)) #x #y #_ %
     118  | @(All_map … (All_True …)) #x #_ %
     119  ]
     120| @All_append
     121  [ @(All_map … (All_True …)) #x #_ %
     122  | %{(refl …)} %{(refl …)} %{(refl …)}
     123    whd in match assign_result;
     124    generalize in match reduce_strong; #f normalize nodelta
     125    cases (f ????) #l #prf normalize nodelta
     126    @(All_map2 … (All2_True … prf)) #x #y #_ %
     127  ]
     128]
     129qed.
     130
     131definition prologue :
     132  ∀globals.list register → register → register → list (register×Register) →
     133  bind_new register (list (joint_seq ERTL globals)) ≝
     134  λglobals,params,sral,srah,sregs.
     135  [ (ertl_new_frame : joint_seq ??) ;
     136    POP … sral ;
     137    POP … srah
     138  ] @@ save_hdws … sregs @@ get_params … params.
    134139
    135140definition set_params_hdw :
     
    150155
    151156definition set_params_stack :
    152   ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
     157  ∀globals.list psd_argument → bind_new register ? ≝
    153158  λglobals,params.
    154159  νaddr1,addr2 in
     
    162167  flatten … (map … (set_param_stack globals addr1 addr2) params).
    163168
    164 definition set_params ≝
     169definition set_params :
     170  ∀globals.list psd_argument →
     171  Σb : bind_new register (list (joint_seq ERTL globals)).
     172  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
    165173  λglobals,params.
    166174  let n ≝ min (|params|) (|RegisterParams|) in
     
    169177  let stack_params ≝ \snd hdw_stack_params in
    170178  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
     179@hide_prf
     180  @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:]
     181  [ #r1 #r2
     182    %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)}
     183    @All_append [ % ]
     184    elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta
     185    whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH
     186  | whd whd in match set_params_hdw; normalize nodelta
     187    whd in match restore_hdws; normalize nodelta @(All_map … (All_True …))
     188    #a #_ %
     189  ]
     190qed.
    171191
    172192definition fetch_result :
    173   ∀globals.list register → list (joint_seq ERTL globals) ≝
     193  ∀globals.list register →
     194  Σl : list (joint_seq ERTL globals).
     195  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
    174196  λglobals,ret_regs.
    175197  match reduce_strong ?? RegisterSTS RegisterRets with
     
    185207    ]
    186208  ].
     209@hide_prf
     210@All_append
     211[ @(All_map2 … (All2_True … crl_proof)) #x #y #_ %
     212| cases (reduce_strong ????) #l #prf normalize nodelta
     213  @(All_map2 … (All2_True … prf)) #x #y #_ %
     214]
     215qed.
    187216
    188217definition translate_step :
    189   ∀globals.label → joint_step RTL_ntc globals →
    190     bind_seq_block ERTL globals (joint_step ERTL globals)
     218  ∀globals.label → joint_step RTL globals →
     219    bind_step_block ERTL globals
    191220  λglobals.λ_.λs.
    192   match s return λ_.bind_seq_block ?? (joint_step ??) with
     221  match s return λ_.bind_step_block ?? with
    193222  [ step_seq s ⇒
    194     match s return λ_.bind_seq_block ?? (joint_step ??) with
    195     [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *)
    196     | POP _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *)
    197     | MOVE rs ⇒ PSD (\fst rs) ← \snd rs
     223    match s return λ_.bind_step_block ?? with
     224    [ PUSH _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
     225    | POP _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
     226    | MOVE rs ⇒ bret … [PSD (\fst rs) ← \snd rs]
    198227    | COST_LABEL lbl ⇒
    199       COST_LABEL … lbl
     228      bret … [COST_LABEL … lbl]
    200229    | ADDRESS x prf r1 r2 ⇒
    201       ADDRESS ERTL ? x prf r1 r2
     230      bret … [ADDRESS ERTL ? x prf r1 r2]
    202231    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    203       OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 
     232      bret … [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
    204233    | OP1 op1 destr srcr ⇒
    205       OP1 ERTL ? op1 destr srcr
     234      bret … [OP1 ERTL ? op1 destr srcr]
    206235    | OP2 op2 destr srcr1 srcr2 ⇒
    207       OP2 ERTL ? op2 destr srcr1 srcr2
     236      bret … [OP2 ERTL ? op2 destr srcr1 srcr2]
    208237    | CLEAR_CARRY ⇒
    209       CLEAR_CARRY …
     238      bret … [CLEAR_CARRY ??]
    210239    | SET_CARRY ⇒
    211       SET_CARRY …
     240      bret … [SET_CARRY ??]
    212241    | LOAD destr addr1 addr2 ⇒
    213       LOAD ERTL ? destr addr1 addr2
     242      bret … [LOAD ERTL ? destr addr1 addr2]
    214243    | STORE addr1 addr2 srcr ⇒
    215       STORE ERTL ? addr1 addr2 srcr
     244      bret … [STORE ERTL ? addr1 addr2 srcr]
    216245    | COMMENT msg ⇒
    217       COMMENT … msg
     246      bret … [COMMENT … msg]
    218247    | extension_seq ext ⇒
    219       match ext with
     248      match ext return λ_.bind_step_block ?? with
    220249      [ rtl_stack_address addr1 addr2 ⇒
    221         [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
     250        bret … [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
    222251      ]
    223     | CALL f args ret_regs ⇒
    224       set_params ? args @@
    225       CALL ERTL ? f (|args|) it :::
    226       fetch_result ? ret_regs
    227252    ]
     253  | CALL f args ret_regs ⇒
     254    ! pref ← pi1 … (set_params ? args) ;
     255    bret ? (step_block ??) 〈add_dummy_variance … pref,
     256             λ_.CALL ERTL ? f (|args|) it,
     257             fetch_result ? ret_regs〉
    228258  | COND r ltrue ⇒
    229     COND ERTL ? r ltrue
     259    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
    230260  ].
    231261
    232262definition translate_fin_step :
    233   ∀globals.label → joint_fin_step RTL_ntc →
    234     bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
    235   λglobals.λ_.λs.
    236   match s with
    237   [ GOTO lbl' ⇒ GOTO … lbl'
    238   | RETURN ⇒ RETURN ?
    239   | TAILCALL abs _ _ ⇒ match abs in False with [ ]
    240   ].
    241 
    242 (* hack with empty graphs used here *)
    243 definition translate_funct :
    244   ∀globals.joint_closed_internal_function RTL_ntc globals →
    245     joint_closed_internal_function ERTL globals ≝
    246   λglobals,def.
    247   let nb_params ≝ |joint_if_params ?? def| in
    248   let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
    249   let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
    250   let entry' ≝ pi1 … (joint_if_entry … def) in
    251   let exit' ≝ pi1 … (joint_if_exit … def) in
    252   let def' ≝ init_graph_if ERTL globals
    253       (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
    254       nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    255       entry' exit' in
    256   let def'' ≝ b_graph_translate …
    257     (ertl_fresh_reg …)
    258     def'
    259     (translate_step globals)
    260     (translate_fin_step globals)
    261     def in
    262   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
    263  cases daemon (* TODO *) qed.
     263  ∀globals.list register → register → register → list (register × Register) →
     264    label → joint_fin_step RTL →
     265    bind_fin_block ERTL globals ≝
     266  λglobals.λret_regs,ral,rah,to_restore.λ_.λs.
     267  match s return λ_.bind_fin_block ERTL ? with
     268  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
     269  | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉
     270  | TAILCALL b _ _ ⇒ match b in False with [ ]
     271  ].
     272
     273definition allocate_regs :
     274  ∀X : Type[0].
     275  (register → register → list (register×Register) → bind_new register X) →
     276  bind_new register X ≝
     277  λX,f.
     278  νral,rah in
     279  let allocate_regs_internal ≝
     280    λacc : bind_new register (list (register × Register)).
     281    λr: Register.
     282    ! tl ← acc ;
     283    νr' in return (〈r', r〉 :: tl) in
     284  ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ;
     285  f ral rah to_save.
     286
     287definition translate_data :
     288 ∀globals.joint_closed_internal_function RTL globals →
     289 bind_new register (b_graph_translate_data RTL ERTL globals) ≝
     290λglobals,def.
     291let params ≝ joint_if_params … def in
     292let new_stacksize ≝
     293  joint_if_stacksize … def + (|params| - |RegisterParams|) in
     294allocate_regs …
     295  (λral,rah,to_save.
     296    ! prologue ← prologue globals params ral rah to_save ;
     297    return mk_b_graph_translate_data RTL ERTL globals
     298    (* init_ret ≝ *) it
     299    (* init_params ≝ *) (|params|)
     300    (* init_stack_size ≝ *) new_stacksize
     301    (* added_prologue ≝ *) prologue
     302    (* f_step ≝ *) (translate_step globals)
     303    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
     304    ???).
     305@hide_prf
     306[ #l #c % ]
     307#l *
     308[ #l whd %{I} %{I} %1 %
     309| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
     310| *
     311| #called #args #dest @(mp_bind … (BindNewP …))
     312  [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%]
     313    [ @(All_map … H1) #a #EQ #l whd >EQ %
     314    | #l %
     315    | cases (fetch_result ??) @All_mp #s #EQ whd >EQ %
     316    ]
     317| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
     318| * try #a try #b try #c try #d try #e whd
     319  try (%{I} %{I} #l %)
     320  cases a -a #a #b whd %{I} % [ %{I} ] #l %
     321]
     322qed.
    264323
    265324(* removing this because of how insert_prologue is now defined
     
    312371
    313372definition rtl_to_ertl : rtl_program → ertl_program ≝
    314  λp.
    315   transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)).
     373  b_graph_transform_program … translate_data.
Note: See TracChangeset for help on using the changeset viewer.