Changeset 2681


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

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r2490 r2681  
    289289
    290290definition translate_address :
    291   ∀globals.bool → ∀i.member ? (eq_identifier ?) i globals → decision → decision →
     291  ∀globals.bool → ∀i.i ∈ globals → decision → decision →
    292292  list (joint_seq LTL globals) ≝
    293293  λglobals,carry_lives_after,id,prf,addr1,addr2.
     
    300300  ∀globals.∀after : valuation register_lattice.
    301301  coloured_graph after →
    302   ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals)
     302  ℕ → label → joint_step ERTL globals → bind_step_block LTL globals
    303303  λglobals,after,grph,stack_sz,lbl,s.
     304  bret … (
    304305  let lookup ≝ λr.colouring … grph (inl … r) in
    305306  let lookup_arg ≝ λa.match a with
     
    311312  match s with
    312313  [ step_seq s' ⇒
    313     match s' return λ_.seq_block LTL globals (joint_step LTL globals) with
    314     [ COMMENT c ⇒ COMMENT … c
    315     | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
     314    match s' return λ_.step_block LTL globals with
     315    [ COMMENT c ⇒ [COMMENT … c]
     316    | COST_LABEL cost_lbl ⇒ [COST_LABEL … cost_lbl]
    316317    | POP r ⇒
    317318      POP … A ::
     
    330331        (lookup_arg addr1)
    331332        (lookup_arg addr2)
    332     | CLEAR_CARRY ⇒ CLEAR_CARRY …
    333     | SET_CARRY ⇒ CLEAR_CARRY …
     333    | CLEAR_CARRY ⇒ [CLEAR_CARRY ??]
     334    | SET_CARRY ⇒ [CLEAR_CARRY ??]
    334335    | OP2 op dst arg1 arg2 ⇒
    335336      translate_op2_smart ? carry_lives_after op
     
    367368        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    368369      ]
    369     | CALL f n_args _ ⇒
     370    ]
     371  | COND r ltrue ⇒
     372    〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉
     373  | CALL f n_args _ ⇒
    370374      match f with
    371       [ inl f ⇒ [ CALL LTL ? (inl … f) n_args it ]
     375      [ inl f ⇒
     376        〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉
    372377      | inr dp ⇒
    373378        let 〈dpl, dph〉 ≝ dp in
    374         move_to_dp … (lookup_arg dpl) (lookup_arg dph) @
    375         [ CALL LTL ? (inr … 〈it, it〉) n_args it ]
     379        〈add_dummy_variance … (move_to_dp … (lookup_arg dpl) (lookup_arg dph)),
     380         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
    376381      ]
    377     ]
    378   | COND r ltrue ⇒
    379     〈move RegisterA (lookup r),COND … it ltrue〉
    380   ].
     382  ]).
    381383
    382384definition translate_fin_step:
    383   ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL)
     385  ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals
    384386  λglobals,lbl,s.
    385   match s return λ_.seq_block LTL globals (joint_fin_step LTL) with
     387  bret … (〈[ ],
     388  match s with
    386389  [ RETURN ⇒ RETURN ?
    387390  | GOTO l ⇒ GOTO ? l
    388391  | TAILCALL abs _ _ ⇒ Ⓧabs
    389   ].
    390 
    391 definition translate_internal: ∀globals: list ident.
     392  ]〉).
     393
     394definition translate_data : ∀globals.
    392395  joint_closed_internal_function ERTL globals →
    393   joint_closed_internal_function LTL globals ≝
    394   λglobals,int_fun.
    395   (* initialize graph *)
    396   let entry ≝ pi1 … (joint_if_entry … int_fun) in
    397   let exit ≝ pi1 … (joint_if_exit … int_fun) in
    398   (* colour registers *)
    399   let after ≝ analyse_liveness globals int_fun in
    400   let coloured_graph ≝ build after in
    401   (* compute new stack size *)
    402   let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    403   (* initialize internal function *)
    404   let init ≝ init_graph_if LTL globals
    405     (joint_if_luniverse … int_fun)
    406     (joint_if_runiverse … int_fun)
    407     it it [ ] stack_sz entry exit in
    408   graph_translate …
    409     init
    410     (translate_step … coloured_graph stack_sz)
    411     (translate_fin_step …)
    412     int_fun.
    413 cases daemon (* TODO *) qed.
     396  bind_new register (b_graph_translate_data ERTL LTL globals) ≝
     397λglobals,int_fun.
     398(* colour registers *)
     399let after ≝ analyse_liveness globals int_fun in
     400let coloured_graph ≝ build after in
     401(* compute new stack size *)
     402let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
     403bret …
     404  (mk_b_graph_translate_data ERTL LTL globals
     405    (* init_ret ≝ *) it
     406    (* init_params ≝ *) it
     407    (* init_stack_size ≝ *) stack_sz
     408    (* added_prologue ≝ *) [ ]
     409    (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
     410    (* f_fin ≝ *) (translate_fin_step globals)
     411    ???).
     412@hide_prf
     413[ #l #c % ]
     414cases daemon (* TODO *)
     415qed.
    414416
    415417definition ertl_to_ltl: ertl_program → ltl_program ≝
    416   λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
     418  b_graph_transform_program … translate_data.
  • src/ERTL/liveness.ma

    r2490 r2681  
    8383        ]
    8484      (* Potentially destroys all caller-save hardware registers. *)
    85       | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    8685      ]
     86    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    8787    | COND r lbl_true ⇒ rl_bottom
    8888    ]
    8989  | final _ ⇒ rl_bottom
     90  | FCOND abs _ _ _ ⇒ Ⓧabs
    9091  ].
    9192
     
    138139        ]
    139140      (* Reads the hardware registers that are used to pass parameters. *)
    140       | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    141141      | _ ⇒ rl_bottom
    142142      ]
     143    | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    143144    | COND r lbl_true ⇒ rl_psingleton r
    144145    ]
     
    149150    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
    150151    ]
     152  | FCOND abs _ _ _ ⇒ Ⓧabs
    151153  ].
    152154
     
    218220      | _ ⇒ None ?
    219221      ]
    220     | COND _ _ ⇒ None ?
     222    | _ ⇒ None ?
    221223    ]
    222224  | _ ⇒ None ?
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2675 r2681  
    3939definition translate_step:
    4040 ∀globals.
    41  unit →
    4241 label
    4342  →joint_step ERTL globals
    4443   →bind_step_block ERTLptr globals ≝
    45  λglobals.λ_.λl.λs.
     44 λglobals.λl.λs.
    4645match s return λ_.bind_step_block ERTLptr globals with
    4746[ CALL called args dest ⇒
     
    6968definition translate_fin_step:
    7069 ∀globals.
    71  unit →
    7270 label
    7371  →joint_fin_step ERTL
    7472   →bind_fin_block ERTLptr globals ≝
    75  λglobals.λ_.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
     73 λglobals.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
     74
     75definition translate_data :
     76  ∀globals.joint_closed_internal_function ERTL globals →
     77  bind_new register (b_graph_translate_data ERTL ERTLptr globals) ≝
     78λglobals,def.bret …
     79  (mk_b_graph_translate_data …
     80    (* init_ret ≝ *) (joint_if_result … def)
     81    (* init_params ≝ *) (joint_if_params … def)
     82    (* init_stack_size ≝ *) (joint_if_stacksize … def)
     83    (* added_prologue ≝ *) [ ]
     84    (* f_step ≝ *) (translate_step globals)
     85    (* f_fin ≝ *) (translate_fin_step globals)
     86    ???).
     87@hide_prf
     88[ #l #c % ]
     89#l *
     90[ #l whd %{I} %{I} %1 %
     91| whd %{I I}
     92| #abs #called #args whd %{I I}
     93| * #called #args #dest whd in match translate_step; normalize nodelta whd
     94  [ %{I} %{I} #l %
     95  | #r whd %{I} %{(λ_.I)} % [| % [| % [| %{I} ]]] #l
     96    [1,3: %{I} %1 %
     97    |*: %
     98    ]
     99  ]
     100| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
     101| #s whd %{I} %{I} #l whd @(All_mp … (In ? (step_labels … s)))
     102  [ #l' #H %2{H} ] cases s -s //
     103]
     104qed.
    76105
    77106definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
    78   b_graph_transform_program ERTL ERTLptr (λ_.unit)
    79   (λglobals,int_fun.
    80     〈〈joint_if_result … int_fun,
    81       joint_if_params … int_fun,
    82       joint_if_stacksize … int_fun〉,
    83     it〉)
    84   translate_step
    85   translate_fin_step.
     107  b_graph_transform_program ERTL ERTLptr translate_data.
  • src/RTL/RTL.ma

    r2640 r2681  
    44  | rtl_stack_address: register → register → rtl_seq.
    55 
    6 definition RTL_uns ≝ λhas_tailcalls.mk_unserialized_params
     6definition RTL_uns ≝ mk_unserialized_params
    77    (* acc_a_reg ≝ *) register
    88    (* acc_b_reg ≝ *) register
     
    1919    (* ext_seq ≝ *) rtl_seq
    2020    (* ext_seq_labels ≝ *) (λ_.[])
    21     (* has_tailcalls ≝ *) has_tailcalls
     21    (* has_tailcalls ≝ *) false
    2222    (* paramsT ≝ *) (list register).
    2323
    24 definition RTL ≝ mk_graph_params (RTL_uns true).
     24definition RTL ≝ mk_graph_params RTL_uns.
    2525definition rtl_program ≝ joint_program RTL.
    2626
     
    7474coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
    7575  on _b : Byte to snd_arg RTL.
    76 
    77 
    78 (************ Same without tail calls ****************)
    79 
    80 definition RTL_ntc ≝ mk_graph_params (RTL_uns false).
    81 definition rtl_ntc_program ≝ joint_program RTL_ntc.
  • 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.
  • src/joint/Joint.ma

    r2655 r2681  
    416416}.
    417417
     418definition code_in_universe : ∀p,globals.
     419  codeT p globals → universe LabelTag → Prop ≝
     420  λp,globals,c,u.∀l.code_has_label … c l → fresh_for_univ … l u.
     421
     422lemma memb_to_present : ∀tag,A.∀i : identifier tag.∀m.
     423  i ∈ m → present tag A m i.
     424#tag #A #i #m whd in ⊢ (?%→%); cases (lookup tag A m i)
     425[ * | #x #_ % #ABS destruct ]
     426qed.
     427
     428lemma present_to_memb : ∀tag,A.∀i : identifier tag.∀m.
     429  present tag A m i → bool_to_Prop (i∈m).
     430#tag #A #i #m whd in ⊢ (%→?%); cases (lookup tag A m i)
     431[ * #ABS cases (ABS (refl …)) | #x #_ % ]
     432qed.
     433
     434lemma graph_code_in_universe_if : ∀p : graph_params.∀globals.
     435  ∀c : codeT p globals.∀u.fresh_map_for_univ … c u → code_in_universe … c u ≝
     436λp,g,c,u,H,l,G.H ? (memb_to_present … G).
     437
     438lemma graph_code_in_universe_only_if : ∀p : graph_params.∀globals.
     439  ∀c : codeT p globals.∀u.
     440  code_in_universe … c u → fresh_map_for_univ … c u ≝
     441λp,g,c,u,H,l,G.H ? (present_to_memb … G).
     442
     443include alias "basics/logic.ma".
     444
     445record good_if
     446(p : params) (globals : list ident) (def : joint_internal_function p globals)
     447: Prop ≝
     448{ unique_cost_labels :
     449  ∀l1,l2,c,nxt1,nxt2.
     450        stmt_at … (joint_if_code … def) l1 =
     451          Some … (sequential … (COST_LABEL … c) nxt1) →
     452        stmt_at … (joint_if_code … def) l2 =
     453          Some … (sequential … (COST_LABEL … c) nxt2) →
     454        l1 = l2
     455; entry_costed :
     456  ∃l,nxt.
     457        stmt_at … (joint_if_code … def) (joint_if_entry … def) =
     458          Some … (sequential … (COST_LABEL … l) nxt)
     459; code_is_closed : code_closed … (joint_if_code … def)
     460; code_is_in_universe :
     461  code_in_universe … (joint_if_code … def) (joint_if_luniverse … def)
     462}.
     463 
    418464definition joint_closed_internal_function ≝
    419465  λp,globals.
    420     Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def).
     466    Σdef : joint_internal_function p globals.good_if … def.
    421467
    422468unification hint 0 ≔ p,g ⊢
    423469  joint_closed_internal_function p g ≡
    424   Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)).
     470  Sig (joint_internal_function p g) (λdef.good_if … def).
    425471
    426472definition set_joint_code ≝
  • src/joint/Traces.ma

    r2645 r2681  
    9999
    100100definition joint_classify_step :
    101   ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
    102   λp,st,stmt.
     101  ∀p : evaluation_params.joint_step p (globals … p) → status_class ≝
     102  λp,stmt.
    103103  match stmt with
    104104  [ step_seq _ ⇒ cl_other
    105   | CALL f args dest ⇒
    106     match (! bl ← block_of_call … (ev_genv p) f st ;
    107             fetch_function … (ev_genv p) bl) with
    108     [ OK id_fn ⇒
    109       match \snd id_fn with
    110       [ Internal _ ⇒ cl_call
    111       | External _ ⇒ cl_other
    112       ]
    113     | Error _ ⇒ cl_other
    114     ]
     105  | CALL f args dest ⇒ cl_call
    115106  | COND _ _ ⇒ cl_jump
    116107  ].
    117108
    118109definition joint_classify_final :
    119   ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝
    120   λp,st,stmt.
     110  ∀p : evaluation_params.joint_fin_step p → status_class ≝
     111  λp,stmt.
    121112  match stmt with
    122113  [ GOTO _ ⇒ cl_other
    123114  | RETURN ⇒ cl_return
    124   | TAILCALL _ f args ⇒
    125     match (! bl ← block_of_call … (ev_genv p) f st ;
    126             fetch_function … (ev_genv p) bl) with
    127     [ OK id_fn ⇒
    128       match \snd id_fn with
    129       [ Internal _ ⇒ cl_tailcall
    130       | External _ ⇒ cl_return
    131       ]
    132     | Error _ ⇒ cl_other
    133     ]
     115  | TAILCALL _ f args ⇒ cl_tailcall
    134116  ].
    135117
     
    139121  ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
    140122  match s with
    141   [ sequential s _ ⇒ Some ? (joint_classify_step p st s)
    142   | final s ⇒ Some ? (joint_classify_final p st s)
     123  [ sequential s _ ⇒ Some ? (joint_classify_step p s)
     124  | final s ⇒ Some ? (joint_classify_final p s)
    143125  | FCOND _ _ _ _ ⇒ Some ? cl_jump
    144126  ].
     
    152134lemma joint_classify_call : ∀p : evaluation_params.∀st.
    153135  joint_classify p st = Some ? cl_call →
    154   ∃i_f,f',args,dest,next,bl,i',fd'.
     136  ∃i_f,f',args,dest,next.
    155137  fetch_statement … (ev_genv p) (pc … st) =
    156     OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
    157   block_of_call … (ev_genv p) f' st = OK ? bl ∧
    158   fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
     138    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉.
    159139#p #st
    160140whd in match joint_classify; normalize nodelta
    161141inversion (fetch_statement … (ev_genv p) (pc … st))
    162142[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
    163 * #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
    164 >m_return_bind normalize nodelta
    165   [3: whd in match joint_classify_final; normalize nodelta
    166     generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
    167     normalize nodelta ]
    168   #ABS destruct(ABS) ]
     143* #i_f *
     144[2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
     145  >m_return_bind normalize nodelta normalize in ⊢ (%→?); #ABS destruct
     146]
    169147* [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
    170 normalize nodelta
    171 [2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
    172 whd in match joint_classify_step;
    173 normalize nodelta
    174 inversion (block_of_call ?????)
    175 [ #bl #block_of_c  >m_return_bind
    176   inversion (fetch_function ???)
    177   [ * #i' *
    178     [ #fd' #fetch' #_
    179       %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
    180       % [ %{block_of_c} % ]
    181       whd in match fetch_internal_function; normalize nodelta
    182       >fetch' %
    183     ]
    184   ]
    185 ]
    186 #x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
     148normalize in ⊢ (%→?); #EQ destruct
     149%[|%[|%[|%[|%[| %]]]]]
    187150qed.
    188151
     
    340303   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
    341304   (* as_call_ident ≝ *) (joint_call_ident p)
    342    (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
     305   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). 
  • src/joint/TranslateUtils.ma

    r2675 r2681  
    9393(* ignoring register allocation for now *)
    9494
     95(*
    9596definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
    9697λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
    97 
     98*)
    9899(*
    99100lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
     
    111112]
    112113qed.
    113 *)
     114
    114115
    115116lemma fresh_was_fresh : ∀tag,id,id',u,u'.
     
    132133#tag * #id * #u * #u' normalize #EQ destruct //
    133134qed.
    134 
     135*)
    135136(*
    136137lemma adds_graph_list_fresh_preserve :
     
    242243qed.
    243244*)
    244 
     245(*
    245246axiom adds_graph_ok :
    246247  ∀g_pars,globals,B,src,dst,def.
     
    270271                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
    271272    src ~❨B,src::l❩~> it in joint_if_code … def'.
    272 
    273 (* preserves first statement if a cost label (should be an invariant) *)
    274 definition insert_prologue ≝
    275   λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
    276   λdef : joint_internal_function g_pars globals.
    277   let entry ≝ joint_if_entry … def in
    278   match stmt_at … entry
    279   return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
    280   with
    281   [ Some s ⇒ λ_.
    282     let default_add ≝ λ_ : unit.
    283       let 〈def', lbl〉 ≝ fresh_label … def in
    284       let def'' ≝ add_graph … lbl s def' in
    285       adds_graph … insts entry lbl def'' in
    286     match s with
    287     [ sequential s' next ⇒
    288       match s' with
    289       [ step_seq s'' ⇒
    290         match s'' with
    291         [ COST_LABEL _ ⇒
    292           adds_graph ?? (s'' :: insts) entry next def
    293         | _ ⇒
    294           default_add it
    295         ]
    296       | _ ⇒
    297         default_add it
    298       ]
    299     | _ ⇒
    300       default_add it
    301     ]
    302   | None ⇒ Ⓧ
    303   ] (pi2 … entry).
     273*)
     274
     275definition append_seq_list :
     276∀p,g.bind_step_block p g → bind_new register (list (joint_seq p g)) →
     277  bind_step_block p g ≝
     278λp,g,bbl,bl.
     279! 〈pref, op, post〉 ← bbl ; ! l ← bl ; return 〈pref, op, post @ l〉.
    304280
    305281(*
     
    332308  adds_graph … stmts src dst def.
    333309
     310(*
    334311axiom b_adds_graph_ok :
    335312  ∀g_pars,globals,B,src,dst,def.
     
    349326                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
    350327    src ~❨B,src::l,r❩~> dst in joint_if_code … def'.
    351  
     328*)
    352329definition b_fin_adds_graph :
    353330  ∀g_pars: graph_params.
     
    361338  fin_adds_graph … stmts src def.
    362339
     340(*
    363341axiom b_fin_adds_graph_ok :
    364342  ∀g_pars,globals,B,src,def.
     
    378356                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
    379357    src ~❨B,src::l,r❩~> it in joint_if_code … def'.
    380 
    381 (* translation with inline fresh register allocation *)
    382 definition b_graph_translate :
    383   ∀src_g_pars,dst_g_pars : graph_params.
    384   ∀globals: list ident.
    385   (* initialization info *)
    386   call_dest dst_g_pars → (* joint_if_result *)
    387   paramsT dst_g_pars → (* joint_if_params *)
    388   ℕ → (* joint_if_stacksize *)
    389   (* functions dictating the translation *)
    390   (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
    391   (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
    392   (* source function *)
    393   joint_closed_internal_function src_g_pars globals →
    394   (* destination function *)
    395   joint_closed_internal_function dst_g_pars globals ≝
    396   λsrc_g_pars,dst_g_pars,globals,
    397    init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def.
    398   let init ≝
    399     mk_joint_internal_function dst_g_pars globals
    400     (joint_if_luniverse … def)
    401     (joint_if_runiverse … def)
    402     init_ret init_params init_stack_size
    403     (add ?? (empty_map ? (joint_statement ??)) (joint_if_entry … def) (RETURN …))
    404     (pi1 … (joint_if_entry … def)) in
    405   let f : label → joint_statement (src_g_pars : params) globals →
    406     joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
    407     λlbl,stmt,def.
    408     match stmt with
    409     [ sequential inst next ⇒
    410       b_adds_graph … (trans_step lbl inst) lbl next def
    411     | final inst ⇒
    412       b_fin_adds_graph … (trans_fin_step lbl inst) lbl def
    413     | FCOND abs _ _ _ ⇒ Ⓧabs
    414     ] in
    415   foldi … f (joint_if_code … def) init.
    416 @hide_prf [ cases daemon (* TODO *) | >graph_code_has_point @mem_set_add_id ] qed.
     358*)
    417359
    418360definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
     
    447389*)
    448390
    449 
    450 axiom b_graph_translate_ok :
    451   ∀src_g_pars,dst_g_pars : graph_params.
    452   ∀globals: list ident.
    453   ∀init_ret,init_params,init_stack_size.
    454   ∀f_step,f_fin,def_in.
    455   let def_out ≝
    456     b_graph_translate src_g_pars dst_g_pars globals
    457       init_ret init_params init_stack_size f_step f_fin def_in in
    458   luniverse_ok ?? def_in →
    459   luniverse_ok … def_out ∧
    460   joint_if_result … def_out = init_ret ∧
    461   joint_if_params … def_out = init_params ∧
    462   joint_if_stacksize … def_out = init_stack_size ∧
    463   pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧
    464   ∃f_lbls : label → option (list label).
    465   ∃f_regs : label → option (list register).
    466   partial_partition … f_lbls ∧
    467   partial_partition … f_regs ∧
     391record b_graph_translate_data
     392  (src, dst : graph_params)
     393  (globals : list ident) : Type[0] ≝
     394{ init_ret : call_dest dst
     395; init_params : paramsT dst
     396; init_stack_size : ℕ
     397; added_prologue : list (joint_seq dst globals)
     398; f_step : label → joint_step src globals → bind_step_block dst globals
     399; f_fin : label → joint_fin_step src → bind_fin_block dst globals
     400; good_f_step_good :
     401  ∀l,s.bind_new_P ??
     402    (λblock.let 〈pref, op, post〉 ≝ block in
     403       All (label → joint_seq ??)
     404         (λs'.∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l))
     405         pref ∧
     406       (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧
     407       All (joint_seq ??) (step_forall_labels … (In ? (step_labels … s))) post)
     408    (f_step l s)
     409; good_f_fin :
     410  ∀l,s.bind_new_P ??
     411    (λblock.let 〈pref, op〉 ≝ block in
     412       All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧
     413       All … (In ? (fin_step_labels … s)) (fin_step_labels … op))
     414    (f_fin l s)
     415; f_step_on_cost :
     416  ∀l,c.f_step l (COST_LABEL … c) = bret … [ COST_LABEL … c ]
     417}.
     418
     419definition get_first_costlabel : ∀p,g.
     420  joint_closed_internal_function p g → costlabel × (succ p) ≝
     421  λp,g,def.
     422  match stmt_at … (joint_if_code … def) (joint_if_entry … def)
     423  return λx.stmt_at ???? = x → ? with
     424  [ Some s ⇒
     425    match s return λx.stmt_at ???? = Some ? x → ? with
     426    [ sequential s' nxt ⇒
     427      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
     428      [ step_seq s'' ⇒
     429        match s'' return λx.stmt_at ???? = Some ? (sequential … (step_seq … x) nxt) → ? with
     430        [ COST_LABEL c ⇒ λ_.〈c, nxt〉
     431        | _ ⇒ λabs.⊥
     432        ]
     433      | _ ⇒ λabs.⊥
     434      ]
     435    | _ ⇒ λabs.⊥
     436    ]
     437  | _ ⇒ λabs.⊥
     438  ] (refl …).
     439@hide_prf
     440cases def in abs; -def #def #good_def
     441cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct
     442qed.
     443
     444record b_graph_translate_props
     445  (src_g_pars, dst_g_pars : graph_params)
     446  (globals: list ident)
     447  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
     448  (data_regs : list register)
     449  (def_in : joint_closed_internal_function src_g_pars globals)
     450  (def_out : joint_closed_internal_function dst_g_pars globals)
     451  (f_lbls : label → option (list label))
     452  (f_regs : label → option (list register)) : Prop ≝
     453{ res_def_out_eq :
     454           joint_if_result … def_out = init_ret … data
     455; pars_def_out_eq :
     456           joint_if_params … def_out = init_params … data
     457; ss_def_out_eq :
     458           joint_if_stacksize … def_out = init_stack_size … data
     459; entry_eq :
     460          pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in)
     461; partition_lbls : partial_partition … f_lbls
     462; partition_regs : partial_partition … f_regs
     463; freshness_lbls :
    468464  (∀l.opt_All … (All …
    469465    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
    470            fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) ∧
     466           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l))
     467; freshness_regs :
    471468  (∀l.opt_All … (All …
    472469    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
    473            fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) ∧
     470           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l))
     471; freshness_data_regs :
     472  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
     473               fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs
     474; data_regs_disjoint : ∀l.opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l)
     475; multi_fetch_ok :
    474476  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
    475477  ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
    476478  match s with
    477479  [ sequential s' nxt ⇒
    478     l ~❨f_step l s', l::lbls, regs❩~> nxt in joint_if_code … def_out
     480    let block ≝
     481      if eq_identifier … (joint_if_entry … def_in) l then
     482        append_seq_list … (f_step … data l s') (added_prologue … data)
     483      else
     484        f_step … data l s' in
     485    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
    479486  | final s' ⇒
    480     l ~❨f_fin l s', l::lbls, regs❩~> it in joint_if_code … def_out
     487    l ~❨f_fin … data l s', l::lbls, regs❩~> it in joint_if_code … def_out
    481488  | FCOND abs _ _ _ ⇒ Ⓧabs
    482   ].
     489  ]
     490}.
     491
     492lemma if_merge_right : ∀A.∀b.∀x,y : A.x = y → if b then x else y = y.
     493#A * #x #y #EQ >EQ % qed.
     494
     495lemma append_seq_list_nil : ∀p,g,b.append_seq_list p g b [ ] = b.
     496#p #g #b elim b -b
     497[ ** #a #b #c normalize >append_nil %
     498| #f #IH @bnew_proper #r @IH
     499]
     500qed.
     501
     502definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉.
     503
     504(* translation with inline fresh register allocation *)
     505definition b_graph_translate :
     506  ∀src_g_pars,dst_g_pars : graph_params.
     507  ∀globals: list ident.
     508  (* initialization info *)
     509  ∀data : bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals).
     510  (* source function *)
     511  ∀def_in : joint_closed_internal_function src_g_pars globals.
     512  (* destination function *)
     513  Σdef_out : joint_closed_internal_function dst_g_pars globals.
     514  ∃data',regs,f_lbls,f_regs.
     515    bind_new_instantiates … data' data regs ∧
     516    b_graph_translate_props … data' regs def_in def_out f_lbls f_regs
     517   ≝
     518  λsrc_g_pars,dst_g_pars,globals,data,def.
     519  let runiv_data ≝ bcompile … (pair_swap ?? ∘ fresh RegisterTag) data (joint_if_runiverse … def) in
     520  let runiv ≝ \fst runiv_data in
     521  let data ≝ \snd runiv_data in
     522  let entry ≝ joint_if_entry … def in
     523  let init ≝
     524    mk_joint_internal_function dst_g_pars globals
     525    (joint_if_luniverse … def)
     526    runiv
     527    (init_ret … data) (init_params … data) (init_stack_size … data)
     528    (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))
     529    («pi1 … entry, mem_set_add_id …») in
     530  let f : label → joint_statement (src_g_pars : params) globals →
     531    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     532    λlbl,stmt,def.
     533    match stmt with
     534    [ sequential inst next ⇒
     535      b_adds_graph … (f_step … data lbl inst) lbl next def
     536    | final inst ⇒
     537      b_fin_adds_graph … (f_fin … data lbl inst) lbl def
     538    | FCOND abs _ _ _ ⇒ Ⓧabs
     539    ] in
     540  let def_out ≝ foldi ??? f (joint_if_code … def) init in
     541  let init_c_nxt ≝ get_first_costlabel … def in
     542  let def_out_nxt ≝ adds_graph_post … (added_prologue … data) (\snd (init_c_nxt)) def_out in
     543  ««add_graph … entry (sequential … (COST_LABEL … (\fst init_c_nxt)) (\snd def_out_nxt)) (\fst def_out_nxt), ?», ?».
     544@hide_prf
     545[ cases daemon
     546| cases daemon (* TODO *)
     547] qed.
    483548
    484549definition b_graph_transform_program :
    485550  ∀src_g_pars,dst_g_pars : graph_params.
    486   ∀X : list ident → Type[0].
    487551  (* initialization *)
    488552  (∀globals.joint_closed_internal_function src_g_pars globals →
    489     (call_dest dst_g_pars) × (paramsT dst_g_pars) × ℕ × (X globals)) →
    490   (* functions dictating the translation *)
    491   (∀globals.X globals → label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
    492   (∀globals.X globals → label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
    493   joint_program src_g_pars → joint_program dst_g_pars ≝
    494   λsrc,dst,X,init,f_step,f_fin,p.
     553    bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) →
     554  joint_program src_g_pars →
     555  joint_program dst_g_pars ≝
     556  λsrc,dst,init,p.
    495557  transform_program ??? p
    496558    (λvarnames.transf_fundef ?? (λdef_in.
    497       let 〈fields, init_data〉 ≝ init varnames def_in in
    498       let 〈init_ret, init_params, init_stack_size〉 ≝ fields in
    499       b_graph_translate … init_ret init_params init_stack_size
    500         (f_step ? init_data) (f_fin ? init_data) def_in)).
     559      b_graph_translate … (init varnames def_in) def_in)).
    501560
    502561definition added_registers :
     
    513572  opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
    514573
    515 (* translation without register allocation (more or less an alias) *)
     574(*(* translation without register allocation (more or less an alias) *)
    516575definition graph_translate :
    517576  ∀src_g_pars,dst_g_pars : graph_params.
     
    532591    (λl,s.return trans_step l s)
    533592    (λl,s.return trans_fin_step l s).
    534 
     593*)
    535594(*
    536595let rec add_translates
  • src/joint/semanticsUtils.ma

    r2675 r2681  
    33include "utilities/hide.ma".
    44include "ASM/BitVectorTrie.ma".
     5include "joint/TranslateUtils.ma".
    56
    67record hw_register_env : Type[0] ≝
     
    162163whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
    163164qed.
     165
     166axiom b_graph_transform_program_props :
     167 ∀src,dst:sem_graph_params.
     168 ∀data : ∀globals.joint_closed_internal_function src globals →
     169  bind_new register (b_graph_translate_data src dst globals).
     170 ∀prog_in : joint_program src.
     171 let prog_out ≝ b_graph_transform_program … data prog_in in
     172 let src_genv ≝ globalenv_noinit ? prog_in in
     173 let dst_genv ≝ globalenv_noinit ? prog_out in
     174 ∃init_regs : ident → list register.
     175 ∃f_lbls : ident → label → option (list label).
     176 ∃f_regs : ident → label → option (list register).
     177 ∀bl,id,def_in.
     178 fetch_internal_function ? src_genv bl = return 〈id, def_in〉 →
     179 ∃init_data,def_out.
     180 fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧
     181 bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧
     182 b_graph_translate_props src dst ? init_data (init_regs id)
     183    def_in def_out (f_lbls id) (f_regs id).
Note: See TracChangeset for help on using the changeset viewer.