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