include "RTL/RTLTailcall.ma". include "utilities/RegisterSet.ma". include "common/Identifiers.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 : ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝ λglobals. let save_hdws_internal ≝ λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in map ?? save_hdws_internal. definition restore_hdws : ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝ λglobals. let restore_hdws_internal ≝ λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in map ? ? restore_hdws_internal. definition get_params_hdw : ∀globals.list register → list (joint_seq ERTL globals) ≝ λglobals,params. save_hdws … (zip_pottier … params RegisterParams). definition get_param_stack : ∀globals.register → register → register → list (joint_seq ERTL globals) ≝ λglobals,addr1,addr2,destr. (* liveness analysis will erase the last useless ops *) [ LOAD ?? destr addr1 addr2 ; addr1 ← addr1 .Add. (int_size : Byte) ; addr2 ← addr2 .Addc. zero_byte ]. definition get_params_stack : ∀globals.list register → bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝ λglobals,params. νtmpr,addr1,addr2 in let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in [ (ertl_frame_size tmpr : joint_seq ??) ; CLEAR_CARRY ?? ; tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *) PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ; addr1 ← addr1 .Add. tmpr ; addr2 ← addr2 .Addc. zero_byte ] @ flatten … (map ?? (get_param_stack globals addr1 addr2) params). definition get_params ≝ λglobals,params. let n ≝ min (length … params) (length … RegisterParams) in 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 : ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ λglobals,ret_regs. match reduce_strong ? ? RegisterSTS ret_regs with [ mk_Sig crl crl_proof ⇒ let commonl ≝ \fst (\fst crl) in let commonr ≝ \fst (\snd crl) in let restl ≝ \snd (\fst crl) in (* let restr ≝ \snd (\snd crl) in *) map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @ map … (λst.HDW st ← zero_byte) restl ]. definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝ λglobals. match reduce_strong ?? RegisterRets RegisterSTS with [ mk_Sig crl crl_proof ⇒ let commonl ≝ \fst (\fst crl) in let commonr ≝ \fst (\snd crl) in map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof ]. definition epilogue : ∀globals.list register → register → register → list (register × Register) → list (joint_seq ERTL globals) ≝ λglobals,ret_regs,sral,srah,sregs. save_return … (map … (Reg ?) ret_regs) @ restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @ [ PUSH ERTL ? srah ; PUSH … sral ; 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'' ). definition set_params_hdw : ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ λglobals,params. restore_hdws globals (zip_pottier ? ? params RegisterParams). (* Paolo: The following can probably be done way more efficiently with INC DPTR *) definition set_param_stack : ∀globals.register → register → psd_argument → list (joint_seq ERTL globals) ≝ λglobals,addr1,addr2,arg. [ STORE … addr1 addr2 arg ; addr1 ← addr1 .Add. (int_size : Byte) ; addr2 ← addr2 .Addc. zero_byte ]. definition set_params_stack : ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝ λglobals,params. νaddr1,addr2 in let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ; CLEAR_CARRY ?? ; addr1 ← addr1 .Sub. params_length_byte ; addr2 ← addr2 .Sub. zero_byte ] @ flatten … (map … (set_param_stack globals addr1 addr2) params). definition set_params ≝ λglobals,params. let n ≝ min (|params|) (|RegisterParams|) in let hdw_stack_params ≝ split ? params n in let hdw_params ≝ \fst hdw_stack_params in let stack_params ≝ \snd hdw_stack_params in set_params_hdw globals hdw_params @@ set_params_stack globals stack_params. definition fetch_result : ∀globals.list register → list (joint_seq ERTL globals) ≝ λglobals,ret_regs. match reduce_strong ?? RegisterSTS RegisterRets with [ mk_Sig crl crl_proof ⇒ let commonl ≝ \fst (\fst crl) in let commonr ≝ \fst (\snd crl) in map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @ match reduce_strong ?? ret_regs RegisterSTS with [ mk_Sig crl crl_proof ⇒ let commonl ≝ \fst (\fst crl) in let commonr ≝ \fst (\snd crl) in map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof ] ]. definition translate_step : ∀globals.label → joint_step RTL_ntc globals → bind_seq_block ERTL globals (joint_step ERTL globals) ≝ λglobals.λ_.λs. match s return λ_.bind_seq_block ?? (joint_step ??) 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 | COST_LABEL lbl ⇒ COST_LABEL … lbl | ADDRESS x prf r1 r2 ⇒ ADDRESS ERTL ? x prf r1 r2 | OPACCS op destr1 destr2 srcr1 srcr2 ⇒ OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 | OP1 op1 destr srcr ⇒ OP1 ERTL ? op1 destr srcr | OP2 op2 destr srcr1 srcr2 ⇒ OP2 ERTL ? op2 destr srcr1 srcr2 | CLEAR_CARRY ⇒ CLEAR_CARRY … | SET_CARRY ⇒ SET_CARRY … | LOAD destr addr1 addr2 ⇒ LOAD ERTL ? destr addr1 addr2 | STORE addr1 addr2 srcr ⇒ STORE ERTL ? addr1 addr2 srcr | COMMENT msg ⇒ COMMENT … msg | extension_seq ext ⇒ match ext with [ rtl_stack_address addr1 addr2 ⇒ [ 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 ] | COND r ltrue ⇒ 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. (* removing this because of how insert_prologue is now defined definition generate ≝ λglobals. λstmt. λdef: joint_internal_function globals ERTL. let 〈entry, def〉 ≝ fresh_label … def in let graph ≝ add … (joint_if_code … def) entry stmt in set_joint_if_graph … (ERTL globals) graph def ??. [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *) | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF *) cases daemon (*CSC: XXX *) ] qed. let rec find_and_remove_first_cost_label_internal (globals: list ident) (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat) on num_nodes ≝ match num_nodes with [ O ⇒ 〈None ?, def〉 | S num_nodes' ⇒ match lookup … (joint_if_code … def) lbl with [ None ⇒ 〈None ?, def〉 | Some stmt ⇒ match stmt with [ sequential inst lbl ⇒ match inst with [ COST_LABEL cost_lbl ⇒ 〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉 | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] | RETURN ⇒ 〈None …, def〉 | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]]]. definition find_and_remove_first_cost_label ≝ λglobals,def. find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)). definition move_first_cost_label_up_internal ≝ λglobals,def. let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in match cost_label with [ None ⇒ def | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def ]. definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). *) definition rtl_to_ertl : rtl_program → ertl_program ≝ λp. let p ≝ tailcall_simplify p in (* tailcall simplification here *) transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)).