Changeset 2681 for src/joint


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
Location:
src/joint
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • 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.