Changeset 2681

Timestamp:

Feb 19, 2013, 6:48:32 PM (8 years ago)

Author:

tranquil

Message:

• improvements to the graph translation function
• fixed passes up to LTL

Location:

src

Files:

• ERTL/ERTLToLTL.ma (modified) (5 diffs)
• ERTL/liveness.ma (modified) (4 diffs)
• ERTLptr/ERTLtoERTLptr.ma (modified) (2 diffs)
• RTL/RTL.ma (modified) (3 diffs)
• RTL/RTLToERTL.ma (modified) (10 diffs)
• joint/Joint.ma (modified) (1 diff)
• joint/Traces.ma (modified) (4 diffs)
• joint/TranslateUtils.ma (modified) (12 diffs)
• joint/semanticsUtils.ma (modified) (2 diffs)

src/ERTL/ERTLToLTL.ma

@@ -289 +289 @@
 
 definition translate_address :
-  ∀globals.bool → ∀i.member ? (eq_identifier ?) i globals → decision → decision →
+  ∀globals.bool → ∀i.i ∈ globals → decision → decision →
   list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,id,prf,addr1,addr2.
@@ -300 +300 @@
   ∀globals.∀after : valuation register_lattice.
   coloured_graph after →
-  ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals) ≝
+  ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝
   λglobals,after,grph,stack_sz,lbl,s.
+  bret … (
   let lookup ≝ λr.colouring … grph (inl … r) in
   let lookup_arg ≝ λa.match a with
@@ -311 +312 @@
   match s with
   [ step_seq s' ⇒
-    match s' return λ_.seq_block LTL globals (joint_step LTL globals) with
-    [ COMMENT c ⇒ COMMENT … c
-    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
+    match s' return λ_.step_block LTL globals with
+    [ COMMENT c ⇒ [COMMENT … c]
+    | COST_LABEL cost_lbl ⇒ [COST_LABEL … cost_lbl]
     | POP r ⇒
       POP … A ::
@@ -330 +331 @@
         (lookup_arg addr1)
         (lookup_arg addr2)
-    | CLEAR_CARRY ⇒ CLEAR_CARRY …
-    | SET_CARRY ⇒ CLEAR_CARRY …
+    | CLEAR_CARRY ⇒ [CLEAR_CARRY ??]
+    | SET_CARRY ⇒ [CLEAR_CARRY ??]
     | OP2 op dst arg1 arg2 ⇒
       translate_op2_smart ? carry_lives_after op
@@ -367 +368 @@
         move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
       ]
-    | CALL f n_args _ ⇒
+    ]
+  | COND r ltrue ⇒
+    〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉
+  | CALL f n_args _ ⇒
       match f with
-      [ inl f ⇒ [ CALL LTL ? (inl … f) n_args it ]
+      [ inl f ⇒
+        〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉
       | inr dp ⇒
         let 〈dpl, dph〉 ≝ dp in
-        move_to_dp … (lookup_arg dpl) (lookup_arg dph) @
-        [ CALL LTL ? (inr … 〈it, it〉) n_args it ]
+        〈add_dummy_variance … (move_to_dp … (lookup_arg dpl) (lookup_arg dph)),
+         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
       ]
-    ]
-  | COND r ltrue ⇒
-    〈move RegisterA (lookup r),COND … it ltrue〉
-  ].
+  ]).
 
 definition translate_fin_step:
-  ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL) ≝
+  ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
   λglobals,lbl,s.
-  match s return λ_.seq_block LTL globals (joint_fin_step LTL) with
+  bret … (〈[ ],
+  match s with
   [ RETURN ⇒ RETURN ?
   | GOTO l ⇒ GOTO ? l
   | TAILCALL abs _ _ ⇒ Ⓧabs
-  ].
-
-definition translate_internal: ∀globals: list ident.
+  ]〉).
+
+definition translate_data : ∀globals.
   joint_closed_internal_function ERTL globals →
-  joint_closed_internal_function LTL globals ≝
-  λglobals,int_fun.
-  (* initialize graph *)
-  let entry ≝ pi1 … (joint_if_entry … int_fun) in
-  let exit ≝ pi1 … (joint_if_exit … int_fun) in
-  (* colour registers *)
-  let after ≝ analyse_liveness globals int_fun in
-  let coloured_graph ≝ build after in
-  (* compute new stack size *)
-  let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
-  (* initialize internal function *)
-  let init ≝ init_graph_if LTL globals
-    (joint_if_luniverse … int_fun)
-    (joint_if_runiverse … int_fun)
-    it it [ ] stack_sz entry exit in
-  graph_translate … 
-    init
-    (translate_step … coloured_graph stack_sz)
-    (translate_fin_step …)
-    int_fun.
-cases daemon (* TODO *) qed.
+  bind_new register (b_graph_translate_data ERTL LTL globals) ≝
+λglobals,int_fun.
+(* colour registers *)
+let after ≝ analyse_liveness globals int_fun in
+let coloured_graph ≝ build after in
+(* compute new stack size *)
+let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
+bret … 
+  (mk_b_graph_translate_data ERTL LTL globals
+    (* init_ret ≝ *) it
+    (* init_params ≝ *) it
+    (* init_stack_size ≝ *) stack_sz
+    (* added_prologue ≝ *) [ ]
+    (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
+    (* f_fin ≝ *) (translate_fin_step globals)
+    ???).
+@hide_prf
+[ #l #c % ]
+cases daemon (* TODO *)
+qed.
 
 definition ertl_to_ltl: ertl_program → ltl_program ≝
-  λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
+  b_graph_transform_program … translate_data.

src/ERTL/liveness.ma

@@ -83 +83 @@
         ]
       (* Potentially destroys all caller-save hardware registers. *)
-      | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
       ]
+    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
     | COND r lbl_true ⇒ rl_bottom
     ]
   | final _ ⇒ rl_bottom
+  | FCOND abs _ _ _ ⇒ Ⓧabs
   ].
 
@@ -138 +139 @@
         ]
       (* Reads the hardware registers that are used to pass parameters. *)
-      | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
       | _ ⇒ rl_bottom
       ]
+    | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
     | COND r lbl_true ⇒ rl_psingleton r
     ]
@@ -149 +150 @@
     | TAILCALL abs _ _ ⇒ match abs in False with [ ]
     ]
+  | FCOND abs _ _ _ ⇒ Ⓧabs
   ].
 
@@ -218 +220 @@
       | _ ⇒ None ?
       ]
-    | COND _ _ ⇒ None ?
+    | _ ⇒ None ?
     ]
   | _ ⇒ None ?

src/ERTLptr/ERTLtoERTLptr.ma

@@ -39 +39 @@
 definition translate_step:
  ∀globals.
- unit →
  label
   →joint_step ERTL globals
    →bind_step_block ERTLptr globals ≝
- λglobals.λ_.λl.λs.
+ λglobals.λl.λs.
 match s return λ_.bind_step_block ERTLptr globals with
 [ CALL called args dest ⇒
@@ -69 +68 @@
 definition translate_fin_step:
  ∀globals.
- unit →
  label
   →joint_fin_step ERTL
    →bind_fin_block ERTLptr globals ≝
- λglobals.λ_.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
+ λglobals.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
+
+definition translate_data :
+  ∀globals.joint_closed_internal_function ERTL globals →
+  bind_new register (b_graph_translate_data ERTL ERTLptr globals) ≝
+λglobals,def.bret …
+  (mk_b_graph_translate_data …
+    (* init_ret ≝ *) (joint_if_result … def)
+    (* init_params ≝ *) (joint_if_params … def)
+    (* init_stack_size ≝ *) (joint_if_stacksize … def)
+    (* added_prologue ≝ *) [ ]
+    (* f_step ≝ *) (translate_step globals)
+    (* f_fin ≝ *) (translate_fin_step globals)
+    ???).
+@hide_prf
+[ #l #c % ]
+#l *
+[ #l whd %{I} %{I} %1 %
+| whd %{I I}
+| #abs #called #args whd %{I I}
+| * #called #args #dest whd in match translate_step; normalize nodelta whd
+  [ %{I} %{I} #l %
+  | #r whd %{I} %{(λ_.I)} % [| % [| % [| %{I} ]]] #l
+    [1,3: %{I} %1 %
+    |*: %
+    ]
+  ]
+| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
+| #s whd %{I} %{I} #l whd @(All_mp … (In ? (step_labels … s)))
+  [ #l' #H %2{H} ] cases s -s //
+]
+qed.
 
 definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
-  b_graph_transform_program ERTL ERTLptr (λ_.unit)
-  (λglobals,int_fun.
-    〈〈joint_if_result … int_fun,
-      joint_if_params … int_fun,
-      joint_if_stacksize … int_fun〉,
-    it〉)
-  translate_step
-  translate_fin_step.
+  b_graph_transform_program ERTL ERTLptr translate_data.

src/RTL/RTL.ma

@@ -4 +4 @@
   | rtl_stack_address: register → register → rtl_seq.
  
-definition RTL_uns ≝ λhas_tailcalls.mk_unserialized_params
+definition RTL_uns ≝ mk_unserialized_params
     (* acc_a_reg ≝ *) register
     (* acc_b_reg ≝ *) register
@@ -19 +19 @@
     (* ext_seq ≝ *) rtl_seq
     (* ext_seq_labels ≝ *) (λ_.[])
-    (* has_tailcalls ≝ *) has_tailcalls
+    (* has_tailcalls ≝ *) false
     (* paramsT ≝ *) (list register).
 
-definition RTL ≝ mk_graph_params (RTL_uns true).
+definition RTL ≝ mk_graph_params RTL_uns.
 definition rtl_program ≝ joint_program RTL.
 
@@ -74 +74 @@
 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
   on _b : Byte to snd_arg RTL.
-
-
-(************ Same without tail calls ****************)
-
-definition RTL_ntc ≝ mk_graph_params (RTL_uns false).
-definition rtl_ntc_program ≝ joint_program RTL_ntc.

src/RTL/RTLToERTL.ma

@@ -1 +1 @@
 include "utilities/RegisterSet.ma".
 include "common/Identifiers.ma".
+include "RTL/RTL.ma".
 include "ERTL/ERTL.ma".
 include "joint/TranslateUtils.ma".
 
 include alias "basics/lists/list.ma".
-
-definition ertl_fresh_reg: 
- ∀globals.freshT ERTL globals register ≝
-  λglobals,def.
-    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
-    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
 
 definition save_hdws :
@@ -43 +38 @@
 definition get_params_stack :
   ∀globals.list register →
-  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
+  bind_new register (list (joint_seq ERTL globals)) ≝
   λglobals,params.
   νtmpr,addr1,addr2 in
@@ -61 +56 @@
   let 〈hdw_params, stack_params〉 ≝ list_split … n params in
   get_params_hdw globals hdw_params @@ get_params_stack … stack_params.
-
-definition prologue :
-  ∀globals.list register → register → register → list (register×Register) →
-  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
-  λglobals,params,sral,srah,sregs.
-  [ (ertl_new_frame : joint_seq ??) ;
-    POP … sral ;
-    POP … srah
-  ] @@ save_hdws … sregs @@ get_params … params.
 
 definition save_return :
@@ -93 +79 @@
   ].
 
+lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf.
+ All2 A B P l1 l2 →
+ (∀x,y.P x y → R (f x y)) →
+ All C R (map2 A B C f l1 l2 prf).
+#A #B #C #P #R #f #l1 elim l1 -l1
+[ * [ #prf * #H % ] #hd' #tl'
+| #hd #tl #IH * [2: #hd' #tl' ]
+] #prf normalize in prf; destruct
+* #H1 #H2 #H % [ @H @H1 | @IH assumption ] qed.
+
+lemma All2_True : ∀A,B,l1,l2.|l1| = |l2| → All2 A B (λ_.λ_.True) l1 l2.
+#A #B #l1 elim l1 -l1
+[ * [ #prf % ] #hd' #tl'
+| #hd #tl #IH * [2: #hd' #tl' ]
+] #prf normalize in prf; destruct %{I} @IH assumption
+qed.
+
+lemma All_True : ∀A,l.All A (λ_.True) l.
+#A #l elim l -l [ % | #hd #tl #IH %{I IH} ] qed.
+
 definition epilogue :
   ∀globals.list register → register → register → list (register × Register) →
-  list (joint_seq ERTL globals) ≝
+  Σl : list (joint_seq ERTL globals).
+  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
   λglobals,ret_regs,sral,srah,sregs.
   save_return … (map … (Reg ?) ret_regs) @
@@ -103 +110 @@
     ertl_del_frame ] @
   assign_result globals.
-
-definition allocate_regs :
-  ∀globals,rs.rs_set rs →
-  freshT ERTL globals (list (register×Register)) ≝
-  λglobals,rs,saved,def.
-   let allocate_regs_internal ≝
-    λr: Register.
-    λdef_sregs.
-    let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in
-    〈def, 〈r', r〉::\snd def_sregs〉 in
-  rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉.
-
-definition add_pro_and_epilogue :
-  ∀globals.list register → list register →
-  joint_internal_function ERTL globals →
-  joint_internal_function ERTL globals ≝
-  λglobals,params,ret_regs,def.
-  let start_lbl ≝ joint_if_entry … def in
-  let end_lbl ≝ joint_if_exit … def in
-  state_run … def (
-    ! sral ← ertl_fresh_reg … ;
-    ! srah ← ertl_fresh_reg … ;
-    ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ;
-    ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ;
-    let epilogue' ≝ epilogue … ret_regs sral srah sregs in
-    ! def' ← state_get … ;
-    let def'' ≝ insert_prologue … prologue' def' in
-    return insert_epilogue … epilogue' def''
-  ).
+@hide_prf
+@All_append
+[ whd in match save_return; normalize nodelta
+  cases (reduce_strong ????) ** #a #b * #c #d #prf normalize nodelta
+  @All_append
+  [ @(All_map2 … (All2_True … prf)) #x #y #_ %
+  | @(All_map … (All_True …)) #x #_ %
+  ]
+| @All_append
+  [ @(All_map … (All_True …)) #x #_ %
+  | %{(refl …)} %{(refl …)} %{(refl …)}
+    whd in match assign_result;
+    generalize in match reduce_strong; #f normalize nodelta
+    cases (f ????) #l #prf normalize nodelta
+    @(All_map2 … (All2_True … prf)) #x #y #_ %
+  ]
+]
+qed.
+
+definition prologue :
+  ∀globals.list register → register → register → list (register×Register) →
+  bind_new register (list (joint_seq ERTL globals)) ≝
+  λglobals,params,sral,srah,sregs.
+  [ (ertl_new_frame : joint_seq ??) ;
+    POP … sral ;
+    POP … srah
+  ] @@ save_hdws … sregs @@ get_params … params.
 
 definition set_params_hdw :
@@ -150 +155 @@
 
 definition set_params_stack :
-  ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
+  ∀globals.list psd_argument → bind_new register ? ≝
   λglobals,params.
   νaddr1,addr2 in
@@ -162 +167 @@
   flatten … (map … (set_param_stack globals addr1 addr2) params).
 
-definition set_params ≝
+definition set_params :
+  ∀globals.list psd_argument →
+  Σb : bind_new register (list (joint_seq ERTL globals)).
+  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
   λglobals,params.
   let n ≝ min (|params|) (|RegisterParams|) in
@@ -169 +177 @@
   let stack_params ≝ \snd hdw_stack_params in
   set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
+@hide_prf
+  @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:]
+  [ #r1 #r2
+    %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)}
+    @All_append [ % ]
+    elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta
+    whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH
+  | whd whd in match set_params_hdw; normalize nodelta
+    whd in match restore_hdws; normalize nodelta @(All_map … (All_True …))
+    #a #_ %
+  ]
+qed.
 
 definition fetch_result :
-  ∀globals.list register → list (joint_seq ERTL globals) ≝
+  ∀globals.list register →
+  Σl : list (joint_seq ERTL globals).
+  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
   λglobals,ret_regs.
   match reduce_strong ?? RegisterSTS RegisterRets with
@@ -185 +207 @@
     ]
   ].
+@hide_prf
+@All_append
+[ @(All_map2 … (All2_True … crl_proof)) #x #y #_ %
+| cases (reduce_strong ????) #l #prf normalize nodelta
+  @(All_map2 … (All2_True … prf)) #x #y #_ %
+]
+qed.
 
 definition translate_step :
-  ∀globals.label → joint_step RTL_ntc globals →
-    bind_seq_block ERTL globals (joint_step ERTL globals) ≝
+  ∀globals.label → joint_step RTL globals →
+    bind_step_block ERTL globals ≝
   λglobals.λ_.λs.
-  match s return λ_.bind_seq_block ?? (joint_step ??) with
+  match s return λ_.bind_step_block ?? with
   [ step_seq s ⇒
-    match s return λ_.bind_seq_block ?? (joint_step ??) with
-    [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *)
-    | POP _ ⇒ NOOP …  (*CSC: XXXX should not be in the syntax *)
-    | MOVE rs ⇒ PSD (\fst rs) ← \snd rs
+    match s return λ_.bind_step_block ?? with
+    [ PUSH _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
+    | POP _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
+    | MOVE rs ⇒ bret … [PSD (\fst rs) ← \snd rs]
     | COST_LABEL lbl ⇒
-      COST_LABEL … lbl
+      bret … [COST_LABEL … lbl]
     | ADDRESS x prf r1 r2 ⇒
-      ADDRESS ERTL ? x prf r1 r2
+      bret … [ADDRESS ERTL ? x prf r1 r2]
     | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
-      OPACCS ERTL ? op destr1 destr2 srcr1 srcr2  
+      bret … [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
     | OP1 op1 destr srcr ⇒
-      OP1 ERTL ? op1 destr srcr
+      bret … [OP1 ERTL ? op1 destr srcr]
     | OP2 op2 destr srcr1 srcr2 ⇒
-      OP2 ERTL ? op2 destr srcr1 srcr2
+      bret … [OP2 ERTL ? op2 destr srcr1 srcr2]
     | CLEAR_CARRY ⇒
-      CLEAR_CARRY …
+      bret … [CLEAR_CARRY ??]
     | SET_CARRY ⇒
-      SET_CARRY …
+      bret … [SET_CARRY ??]
     | LOAD destr addr1 addr2 ⇒
-      LOAD ERTL ? destr addr1 addr2
+      bret … [LOAD ERTL ? destr addr1 addr2]
     | STORE addr1 addr2 srcr ⇒
-      STORE ERTL ? addr1 addr2 srcr
+      bret … [STORE ERTL ? addr1 addr2 srcr]
     | COMMENT msg ⇒
-      COMMENT … msg
+      bret … [COMMENT … msg]
     | extension_seq ext ⇒
-      match ext with
+      match ext return λ_.bind_step_block ?? with
       [ rtl_stack_address addr1 addr2 ⇒
-        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
+        bret … [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
       ]
-    | CALL f args ret_regs ⇒
-      set_params ? args @@
-      CALL ERTL ? f (|args|) it :::
-      fetch_result ? ret_regs
     ]
+  | CALL f args ret_regs ⇒
+    ! pref ← pi1 … (set_params ? args) ;
+    bret ? (step_block ??) 〈add_dummy_variance … pref,
+             λ_.CALL ERTL ? f (|args|) it,
+             fetch_result ? ret_regs〉
   | COND r ltrue ⇒
-    COND ERTL ? r ltrue
+    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
   ].
 
 definition translate_fin_step :
-  ∀globals.label → joint_fin_step RTL_ntc →
-    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
-  λglobals.λ_.λs.
-  match s with
-  [ GOTO lbl' ⇒ GOTO … lbl'
-  | RETURN ⇒ RETURN ?
-  | TAILCALL abs _ _ ⇒ match abs in False with [ ]
-  ].
-
-(* hack with empty graphs used here *)
-definition translate_funct :
-  ∀globals.joint_closed_internal_function RTL_ntc globals →
-    joint_closed_internal_function ERTL globals ≝
-  λglobals,def.
-  let nb_params ≝ |joint_if_params ?? def| in
-  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
-  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
-  let entry' ≝ pi1 … (joint_if_entry … def) in
-  let exit' ≝ pi1 … (joint_if_exit … def) in
-  let def' ≝ init_graph_if ERTL globals
-      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
-      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
-      entry' exit' in
-  let def'' ≝ b_graph_translate …
-    (ertl_fresh_reg …)
-    def'
-    (translate_step globals)
-    (translate_fin_step globals)
-    def in
-  add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
- cases daemon (* TODO *) qed.
+  ∀globals.list register → register → register → list (register × Register) →
+    label → joint_fin_step RTL →
+    bind_fin_block ERTL globals ≝
+  λglobals.λret_regs,ral,rah,to_restore.λ_.λs.
+  match s return λ_.bind_fin_block ERTL ? with
+  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
+  | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉
+  | TAILCALL b _ _ ⇒ match b in False with [ ]
+  ].
+
+definition allocate_regs :
+  ∀X : Type[0].
+  (register → register → list (register×Register) → bind_new register X) →
+  bind_new register X ≝
+  λX,f.
+  νral,rah in
+  let allocate_regs_internal ≝
+    λacc : bind_new register (list (register × Register)).
+    λr: Register.
+    ! tl ← acc ;
+    νr' in return (〈r', r〉 :: tl) in
+  ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ;
+  f ral rah to_save.
+
+definition translate_data :
+ ∀globals.joint_closed_internal_function RTL globals →
+ bind_new register (b_graph_translate_data RTL ERTL globals) ≝
+λglobals,def.
+let params ≝ joint_if_params … def in
+let new_stacksize ≝
+  joint_if_stacksize … def + (|params| - |RegisterParams|) in
+allocate_regs …
+  (λral,rah,to_save.
+    ! prologue ← prologue globals params ral rah to_save ;
+    return mk_b_graph_translate_data RTL ERTL globals
+    (* init_ret ≝ *) it
+    (* init_params ≝ *) (|params|)
+    (* init_stack_size ≝ *) new_stacksize
+    (* added_prologue ≝ *) prologue
+    (* f_step ≝ *) (translate_step globals)
+    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
+    ???).
+@hide_prf
+[ #l #c % ]
+#l *
+[ #l whd %{I} %{I} %1 %
+| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
+| *
+| #called #args #dest @(mp_bind … (BindNewP …))
+  [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%]
+    [ @(All_map … H1) #a #EQ #l whd >EQ %
+    | #l %
+    | cases (fetch_result ??) @All_mp #s #EQ whd >EQ %
+    ]
+| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
+| * try #a try #b try #c try #d try #e whd
+  try (%{I} %{I} #l %)
+  cases a -a #a #b whd %{I} % [ %{I} ] #l %
+]
+qed.
 
 (* removing this because of how insert_prologue is now defined
@@ -312 +371 @@
 
 definition rtl_to_ertl : rtl_program → ertl_program ≝
- λp.
-  transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)).
+  b_graph_transform_program … translate_data.

src/joint/Joint.ma

@@ -416 +416 @@
 }.
 
+definition code_in_universe : ∀p,globals.
+  codeT p globals → universe LabelTag → Prop ≝
+  λp,globals,c,u.∀l.code_has_label … c l → fresh_for_univ … l u.
+
+lemma memb_to_present : ∀tag,A.∀i : identifier tag.∀m.
+  i ∈ m → present tag A m i.
+#tag #A #i #m whd in ⊢ (?%→%); cases (lookup tag A m i)
+[ * | #x #_ % #ABS destruct ]
+qed.
+
+lemma present_to_memb : ∀tag,A.∀i : identifier tag.∀m.
+  present tag A m i → bool_to_Prop (i∈m).
+#tag #A #i #m whd in ⊢ (%→?%); cases (lookup tag A m i)
+[ * #ABS cases (ABS (refl …)) | #x #_ % ]
+qed.
+
+lemma graph_code_in_universe_if : ∀p : graph_params.∀globals.
+  ∀c : codeT p globals.∀u.fresh_map_for_univ … c u → code_in_universe … c u ≝
+λp,g,c,u,H,l,G.H ? (memb_to_present … G).
+
+lemma graph_code_in_universe_only_if : ∀p : graph_params.∀globals.
+  ∀c : codeT p globals.∀u.
+  code_in_universe … c u → fresh_map_for_univ … c u ≝
+λp,g,c,u,H,l,G.H ? (present_to_memb … G).
+
+include alias "basics/logic.ma".
+
+record good_if
+(p : params) (globals : list ident) (def : joint_internal_function p globals)
+: Prop ≝
+{ unique_cost_labels :
+  ∀l1,l2,c,nxt1,nxt2.
+        stmt_at … (joint_if_code … def) l1 =
+          Some … (sequential … (COST_LABEL … c) nxt1) →
+        stmt_at … (joint_if_code … def) l2 =
+          Some … (sequential … (COST_LABEL … c) nxt2) →
+        l1 = l2
+; entry_costed :
+  ∃l,nxt.
+        stmt_at … (joint_if_code … def) (joint_if_entry … def) =
+          Some … (sequential … (COST_LABEL … l) nxt)
+; code_is_closed : code_closed … (joint_if_code … def)
+; code_is_in_universe :
+  code_in_universe … (joint_if_code … def) (joint_if_luniverse … def)
+}.
+  
 definition joint_closed_internal_function ≝
   λp,globals.
-    Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def).
+    Σdef : joint_internal_function p globals.good_if … def.
 
 unification hint 0 ≔ p,g ⊢
   joint_closed_internal_function p g ≡
-  Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)).
+  Sig (joint_internal_function p g) (λdef.good_if … def).
 
 definition set_joint_code ≝

src/joint/Traces.ma

@@ -99 +99 @@
 
 definition joint_classify_step :
-  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
-  λp,st,stmt.
+  ∀p : evaluation_params.joint_step p (globals … p) → status_class ≝
+  λp,stmt.
   match stmt with
   [ step_seq _ ⇒ cl_other
-  | CALL f args dest ⇒
-    match (! bl ← block_of_call … (ev_genv p) f st ;
-            fetch_function … (ev_genv p) bl) with
-    [ OK id_fn ⇒
-      match \snd id_fn with
-      [ Internal _ ⇒ cl_call
-      | External _ ⇒ cl_other
-      ]
-    | Error _ ⇒ cl_other
-    ]
+  | CALL f args dest ⇒ cl_call
   | COND _ _ ⇒ cl_jump
   ].
 
 definition joint_classify_final :
-  ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝
-  λp,st,stmt.
+  ∀p : evaluation_params.joint_fin_step p → status_class ≝
+  λp,stmt.
   match stmt with
   [ GOTO _ ⇒ cl_other
   | RETURN ⇒ cl_return
-  | TAILCALL _ f args ⇒
-    match (! bl ← block_of_call … (ev_genv p) f st ;
-            fetch_function … (ev_genv p) bl) with
-    [ OK id_fn ⇒
-      match \snd id_fn with
-      [ Internal _ ⇒ cl_tailcall
-      | External _ ⇒ cl_return
-      ]
-    | Error _ ⇒ cl_other
-    ]
+  | TAILCALL _ f args ⇒ cl_tailcall
   ].
 
@@ -139 +121 @@
   ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
   match s with
-  [ sequential s _ ⇒ Some ? (joint_classify_step p st s)
-  | final s ⇒ Some ? (joint_classify_final p st s)
+  [ sequential s _ ⇒ Some ? (joint_classify_step p s)
+  | final s ⇒ Some ? (joint_classify_final p s)
   | FCOND _ _ _ _ ⇒ Some ? cl_jump
   ].
@@ -152 +134 @@
 lemma joint_classify_call : ∀p : evaluation_params.∀st.
   joint_classify p st = Some ? cl_call →
-  ∃i_f,f',args,dest,next,bl,i',fd'.
+  ∃i_f,f',args,dest,next.
   fetch_statement … (ev_genv p) (pc … st) =
-    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
-  block_of_call … (ev_genv p) f' st = OK ? bl ∧
-  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
+    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉.
 #p #st
 whd in match joint_classify; normalize nodelta
 inversion (fetch_statement … (ev_genv p) (pc … st))
 [2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
-* #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
->m_return_bind normalize nodelta
-  [3: whd in match joint_classify_final; normalize nodelta
-    generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
-    normalize nodelta ]
-  #ABS destruct(ABS) ]
+* #i_f *
+[2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
+  >m_return_bind normalize nodelta normalize in ⊢ (%→?); #ABS destruct
+]
 * [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
-normalize nodelta
-[2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
-whd in match joint_classify_step;
-normalize nodelta
-inversion (block_of_call ?????)
-[ #bl #block_of_c  >m_return_bind
-  inversion (fetch_function ???)
-  [ * #i' *
-    [ #fd' #fetch' #_
-      %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
-      % [ %{block_of_c} % ]
-      whd in match fetch_internal_function; normalize nodelta
-      >fetch' %
-    ]
-  ]
-]
-#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
+normalize in ⊢ (%→?); #EQ destruct
+%[|%[|%[|%[|%[| %]]]]]
 qed.
 
@@ -340 +303 @@
    (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
    (* as_call_ident ≝ *) (joint_call_ident p)
-   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
+   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). 

src/joint/TranslateUtils.ma

@@ -93 +93 @@
 (* ignoring register allocation for now *)
 
+(*
 definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
 λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
-
+*)
 (*
 lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
@@ -111 +112 @@
 ]
 qed.
-*)
+
 
 lemma fresh_was_fresh : ∀tag,id,id',u,u'.
@@ -132 +133 @@
 #tag * #id * #u * #u' normalize #EQ destruct //
 qed.
-
+*)
 (*
 lemma adds_graph_list_fresh_preserve :
@@ -242 +243 @@
 qed.
 *)
-
+(*
 axiom adds_graph_ok :
   ∀g_pars,globals,B,src,dst,def.
@@ -270 +271 @@
                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     src ~❨B,src::l❩~> it in joint_if_code … def'.
-
-(* preserves first statement if a cost label (should be an invariant) *)
-definition insert_prologue ≝
-  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
-  λdef : joint_internal_function g_pars globals.
-  let entry ≝ joint_if_entry … def in
-  match stmt_at … entry
-  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
-  with
-  [ Some s ⇒ λ_.
-    let default_add ≝ λ_ : unit.
-      let 〈def', lbl〉 ≝ fresh_label … def in
-      let def'' ≝ add_graph … lbl s def' in
-      adds_graph … insts entry lbl def'' in
-    match s with
-    [ sequential s' next ⇒
-      match s' with
-      [ step_seq s'' ⇒
-        match s'' with
-        [ COST_LABEL _ ⇒
-          adds_graph ?? (s'' :: insts) entry next def
-        | _ ⇒
-          default_add it
-        ]
-      | _ ⇒
-        default_add it
-      ]
-    | _ ⇒
-      default_add it
-    ]
-  | None ⇒ Ⓧ
-  ] (pi2 … entry).
+*)
+
+definition append_seq_list :
+∀p,g.bind_step_block p g → bind_new register (list (joint_seq p g)) →
+  bind_step_block p g ≝
+λp,g,bbl,bl.
+! 〈pref, op, post〉 ← bbl ; ! l ← bl ; return 〈pref, op, post @ l〉.
 
 (*
@@ -332 +308 @@
   adds_graph … stmts src dst def.
 
+(*
 axiom b_adds_graph_ok :
   ∀g_pars,globals,B,src,dst,def.
@@ -349 +326 @@
                  fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
     src ~❨B,src::l,r❩~> dst in joint_if_code … def'.
- 
+*)
 definition b_fin_adds_graph :
   ∀g_pars: graph_params.
@@ -361 +338 @@
   fin_adds_graph … stmts src def.
 
+(*
 axiom b_fin_adds_graph_ok :
   ∀g_pars,globals,B,src,def.
@@ -378 +356 @@
                  fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
     src ~❨B,src::l,r❩~> it in joint_if_code … def'.
-
-(* translation with inline fresh register allocation *)
-definition b_graph_translate :
-  ∀src_g_pars,dst_g_pars : graph_params.
-  ∀globals: list ident.
-  (* initialization info *)
-  call_dest dst_g_pars → (* joint_if_result *)
-  paramsT dst_g_pars → (* joint_if_params *)
-  ℕ → (* joint_if_stacksize *)
-  (* functions dictating the translation *)
-  (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
-  (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
-  (* source function *)
-  joint_closed_internal_function src_g_pars globals →
-  (* destination function *)
-  joint_closed_internal_function dst_g_pars globals ≝
-  λsrc_g_pars,dst_g_pars,globals,
-   init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def.
-  let init ≝
-    mk_joint_internal_function dst_g_pars globals
-    (joint_if_luniverse … def)
-    (joint_if_runiverse … def)
-    init_ret init_params init_stack_size
-    (add ?? (empty_map ? (joint_statement ??)) (joint_if_entry … def) (RETURN …))
-    (pi1 … (joint_if_entry … def)) in
-  let f : label → joint_statement (src_g_pars : params) globals →
-    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 
-    λlbl,stmt,def.
-    match stmt with
-    [ sequential inst next ⇒
-      b_adds_graph … (trans_step lbl inst) lbl next def
-    | final inst ⇒
-      b_fin_adds_graph … (trans_fin_step lbl inst) lbl def
-    | FCOND abs _ _ _ ⇒ Ⓧabs
-    ] in
-  foldi … f (joint_if_code … def) init.
-@hide_prf [ cases daemon (* TODO *) | >graph_code_has_point @mem_set_add_id ] qed.
+*)
 
 definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
@@ -447 +389 @@
 *)
 
-
-axiom b_graph_translate_ok :
-  ∀src_g_pars,dst_g_pars : graph_params.
-  ∀globals: list ident.
-  ∀init_ret,init_params,init_stack_size.
-  ∀f_step,f_fin,def_in.
-  let def_out ≝
-    b_graph_translate src_g_pars dst_g_pars globals
-      init_ret init_params init_stack_size f_step f_fin def_in in
-  luniverse_ok ?? def_in →
-  luniverse_ok … def_out ∧
-  joint_if_result … def_out = init_ret ∧
-  joint_if_params … def_out = init_params ∧
-  joint_if_stacksize … def_out = init_stack_size ∧
-  pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧
-  ∃f_lbls : label → option (list label).
-  ∃f_regs : label → option (list register).
-  partial_partition … f_lbls ∧
-  partial_partition … f_regs ∧
+record b_graph_translate_data
+  (src, dst : graph_params)
+  (globals : list ident) : Type[0] ≝
+{ init_ret : call_dest dst
+; init_params : paramsT dst
+; init_stack_size : ℕ
+; added_prologue : list (joint_seq dst globals)
+; f_step : label → joint_step src globals → bind_step_block dst globals
+; f_fin : label → joint_fin_step src → bind_fin_block dst globals
+; good_f_step_good :
+  ∀l,s.bind_new_P ??
+    (λblock.let 〈pref, op, post〉 ≝ block in
+       All (label → joint_seq ??)
+         (λs'.∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l))
+         pref ∧
+       (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧
+       All (joint_seq ??) (step_forall_labels … (In ? (step_labels … s))) post)
+    (f_step l s)
+; good_f_fin :
+  ∀l,s.bind_new_P ??
+    (λblock.let 〈pref, op〉 ≝ block in
+       All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧
+       All … (In ? (fin_step_labels … s)) (fin_step_labels … op))
+    (f_fin l s)
+; f_step_on_cost :
+  ∀l,c.f_step l (COST_LABEL … c) = bret … [ COST_LABEL … c ]
+}.
+
+definition get_first_costlabel : ∀p,g.
+  joint_closed_internal_function p g → costlabel × (succ p) ≝
+  λp,g,def.
+  match stmt_at … (joint_if_code … def) (joint_if_entry … def)
+  return λx.stmt_at ???? = x → ? with
+  [ Some s ⇒
+    match s return λx.stmt_at ???? = Some ? x → ? with
+    [ sequential s' nxt ⇒
+      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
+      [ step_seq s'' ⇒
+        match s'' return λx.stmt_at ???? = Some ? (sequential … (step_seq … x) nxt) → ? with
+        [ COST_LABEL c ⇒ λ_.〈c, nxt〉
+        | _ ⇒ λabs.⊥
+        ]
+      | _ ⇒ λabs.⊥
+      ]
+    | _ ⇒ λabs.⊥
+    ]
+  | _ ⇒ λabs.⊥
+  ] (refl …).
+@hide_prf
+cases def in abs; -def #def #good_def
+cases (entry_costed … good_def) #c * #nxt' #EQ >EQ #ABS destruct
+qed.
+
+record b_graph_translate_props 
+  (src_g_pars, dst_g_pars : graph_params)
+  (globals: list ident)
+  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
+  (data_regs : list register)
+  (def_in : joint_closed_internal_function src_g_pars globals)
+  (def_out : joint_closed_internal_function dst_g_pars globals)
+  (f_lbls : label → option (list label))
+  (f_regs : label → option (list register)) : Prop ≝
+{ res_def_out_eq :
+           joint_if_result … def_out = init_ret … data
+; pars_def_out_eq :
+           joint_if_params … def_out = init_params … data
+; ss_def_out_eq :
+           joint_if_stacksize … def_out = init_stack_size … data
+; entry_eq :
+          pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in)
+; partition_lbls : partial_partition … f_lbls
+; partition_regs : partial_partition … f_regs
+; freshness_lbls :
   (∀l.opt_All … (All …
     (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
-           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) ∧
+           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l))
+; freshness_regs :
   (∀l.opt_All … (All …
     (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
-           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) ∧
+           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l))
+; freshness_data_regs :
+  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
+               fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs
+; data_regs_disjoint : ∀l.opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l)
+; multi_fetch_ok :
   ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
   ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
   match s with
   [ sequential s' nxt ⇒
-    l ~❨f_step l s', l::lbls, regs❩~> nxt in joint_if_code … def_out
+    let block ≝
+      if eq_identifier … (joint_if_entry … def_in) l then
+        append_seq_list … (f_step … data l s') (added_prologue … data)
+      else
+        f_step … data l s' in
+    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
   | final s' ⇒
-    l ~❨f_fin l s', l::lbls, regs❩~> it in joint_if_code … def_out
+    l ~❨f_fin … data l s', l::lbls, regs❩~> it in joint_if_code … def_out
   | FCOND abs _ _ _ ⇒ Ⓧabs
-  ].
+  ]
+}.
+
+lemma if_merge_right : ∀A.∀b.∀x,y : A.x = y → if b then x else y = y.
+#A * #x #y #EQ >EQ % qed.
+
+lemma append_seq_list_nil : ∀p,g,b.append_seq_list p g b [ ] = b.
+#p #g #b elim b -b
+[ ** #a #b #c normalize >append_nil %
+| #f #IH @bnew_proper #r @IH
+]
+qed.
+
+definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉.
+
+(* translation with inline fresh register allocation *)
+definition b_graph_translate :
+  ∀src_g_pars,dst_g_pars : graph_params.
+  ∀globals: list ident.
+  (* initialization info *)
+  ∀data : bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals).
+  (* source function *)
+  ∀def_in : joint_closed_internal_function src_g_pars globals.
+  (* destination function *)
+  Σdef_out : joint_closed_internal_function dst_g_pars globals.
+  ∃data',regs,f_lbls,f_regs.
+    bind_new_instantiates … data' data regs ∧
+    b_graph_translate_props … data' regs def_in def_out f_lbls f_regs
+   ≝
+  λsrc_g_pars,dst_g_pars,globals,data,def.
+  let runiv_data ≝ bcompile … (pair_swap ?? ∘ fresh RegisterTag) data (joint_if_runiverse … def) in
+  let runiv ≝ \fst runiv_data in
+  let data ≝ \snd runiv_data in
+  let entry ≝ joint_if_entry … def in
+  let init ≝
+    mk_joint_internal_function dst_g_pars globals
+    (joint_if_luniverse … def)
+    runiv
+    (init_ret … data) (init_params … data) (init_stack_size … data)
+    (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))
+    («pi1 … entry, mem_set_add_id …») in
+  let f : label → joint_statement (src_g_pars : params) globals →
+    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 
+    λlbl,stmt,def.
+    match stmt with
+    [ sequential inst next ⇒
+      b_adds_graph … (f_step … data lbl inst) lbl next def
+    | final inst ⇒
+      b_fin_adds_graph … (f_fin … data lbl inst) lbl def
+    | FCOND abs _ _ _ ⇒ Ⓧabs
+    ] in
+  let def_out ≝ foldi ??? f (joint_if_code … def) init in
+  let init_c_nxt ≝ get_first_costlabel … def in
+  let def_out_nxt ≝ adds_graph_post … (added_prologue … data) (\snd (init_c_nxt)) def_out in
+  ««add_graph … entry (sequential … (COST_LABEL … (\fst init_c_nxt)) (\snd def_out_nxt)) (\fst def_out_nxt), ?», ?».
+@hide_prf
+[ cases daemon
+| cases daemon (* TODO *)
+] qed.
 
 definition b_graph_transform_program :
   ∀src_g_pars,dst_g_pars : graph_params.
-  ∀X : list ident → Type[0].
   (* initialization *)
   (∀globals.joint_closed_internal_function src_g_pars globals →
-    (call_dest dst_g_pars) × (paramsT dst_g_pars) × ℕ × (X globals)) →
-  (* functions dictating the translation *)
-  (∀globals.X globals → label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
-  (∀globals.X globals → label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
-  joint_program src_g_pars → joint_program dst_g_pars ≝
-  λsrc,dst,X,init,f_step,f_fin,p.
+    bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) →
+  joint_program src_g_pars →
+  joint_program dst_g_pars ≝
+  λsrc,dst,init,p.
   transform_program ??? p
     (λvarnames.transf_fundef ?? (λdef_in.
-      let 〈fields, init_data〉 ≝ init varnames def_in in
-      let 〈init_ret, init_params, init_stack_size〉 ≝ fields in
-      b_graph_translate … init_ret init_params init_stack_size
-        (f_step ? init_data) (f_fin ? init_data) def_in)).
+      b_graph_translate … (init varnames def_in) def_in)).
 
 definition added_registers :
@@ -513 +572 @@
   opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
 
-(* translation without register allocation (more or less an alias) *)
+(*(* translation without register allocation (more or less an alias) *)
 definition graph_translate :
   ∀src_g_pars,dst_g_pars : graph_params.
@@ -532 +591 @@
     (λl,s.return trans_step l s)
     (λl,s.return trans_fin_step l s).
-
+*)
 (* 
 let rec add_translates

src/joint/semanticsUtils.ma

@@ -3 +3 @@
 include "utilities/hide.ma".
 include "ASM/BitVectorTrie.ma".
+include "joint/TranslateUtils.ma".
 
 record hw_register_env : Type[0] ≝
@@ -162 +163 @@
 whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
 qed.
+
+axiom b_graph_transform_program_props :
+ ∀src,dst:sem_graph_params.
+ ∀data : ∀globals.joint_closed_internal_function src globals →
+  bind_new register (b_graph_translate_data src dst globals).
+ ∀prog_in : joint_program src.
+ let prog_out ≝ b_graph_transform_program … data prog_in in
+ let src_genv ≝ globalenv_noinit ? prog_in in
+ let dst_genv ≝ globalenv_noinit ? prog_out in
+ ∃init_regs : ident → list register.
+ ∃f_lbls : ident → label → option (list label).
+ ∃f_regs : ident → label → option (list register).
+ ∀bl,id,def_in.
+ fetch_internal_function ? src_genv bl = return 〈id, def_in〉 →
+ ∃init_data,def_out.
+ fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧
+ bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧
+ b_graph_translate_props src dst ? init_data (init_regs id)
+    def_in def_out (f_lbls id) (f_regs id).