 Timestamp:
 Jul 18, 2012, 1:26:43 PM (8 years ago)
 Location:
 src/RTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLToERTL_paolo.ma
r2174 r2208 15 15 16 16 definition restore_hdws : 17 ∀globals.list ( rtl_argument×Register) → list (joint_seq ertl_params globals) ≝17 ∀globals.list (psd_argument×Register) → list (joint_seq ertl_params globals) ≝ 18 18 λglobals. 19 19 let restore_hdws_internal ≝ 20 λdestr_srcr: rtl_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in20 λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in 21 21 map ? ? restore_hdws_internal. 22 22 … … 26 26 save_hdws … (zip_pottier … params RegisterParams). 27 27 28 (* Paolo: The following can probably be done way more efficiently with INC DPTR *)29 30 28 definition get_param_stack : 31 ∀globals.register → register → nat →register →29 ∀globals.register → register → register → 32 30 list (joint_seq ertl_params globals) ≝ 33 λglobals,addr1,addr2,off,destr. 34 let int_offset : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in 35 [ (ertl_frame_size addr1 : joint_seq ??) ; 36 CLEAR_CARRY … ; 37 addr1 ← addr1 .Sub. int_offset ; (* are we sure carry bit is unimportant? *) 38 PSD destr ← HDW RegisterSPL ; 39 addr1 ← addr1 .Add. destr ; 40 PSD addr2 ← HDW RegisterSPH ; 41 addr2 ← addr2 .Addc. 0 ; 42 LOAD … destr addr1 addr2 31 λglobals,addr1,addr2,destr. 32 (* liveness analysis will erase the last useless ops *) 33 [ LOAD ?? destr addr1 addr2 ; 34 addr1 ← addr1 .Add. (int_size : Byte) ; 35 addr2 ← addr2 .Addc. zero_byte 43 36 ]. 44 37 … … 47 40 bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝ 48 41 λglobals,params. 49 νaddr1,addr2 in 50 flatten … (mapi ?? (get_param_stack globals addr1 addr2) params). 42 νtmpr,addr1,addr2 in 43 let params_length_byte : Byte ≝ bitvector_of_nat ? (params) in 44 [ (ertl_frame_size tmpr : joint_seq ??) ; 45 CLEAR_CARRY ?? ; 46 tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *) 47 PSD addr1 ← HDW RegisterSPL ; 48 PSD addr2 ← HDW RegisterSPH ; 49 addr1 ← addr1 .Add. tmpr ; 50 addr2 ← addr2 .Addc. zero_byte ] @ 51 flatten … (map ?? (get_param_stack globals addr1 addr2) params). 51 52 52 53 definition get_params ≝ … … 66 67 67 68 definition save_return : 68 ∀globals.list rtl_argument → list (joint_seq ertl_params globals) ≝69 ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝ 69 70 λglobals,ret_regs. 70 71 match reduce_strong ? ? RegisterSTS ret_regs with … … 74 75 let restl ≝ \snd (\fst crl) in 75 76 (* let restr ≝ \snd (\snd crl) in *) 76 map2 … (λst.λr : rtl_argument.HDW st ← r) commonl commonr crl_proof @77 map … (λst.HDW st ← 0) restl77 map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @ 78 map … (λst.HDW st ← zero_byte) restl 78 79 ]. 79 80 … … 91 92 list (joint_seq ertl_params globals) ≝ 92 93 λglobals,ret_regs,sral,srah,sregs. 93 save_return … (map … Regret_regs) @94 restore_hdws … (map … (λpr.〈Reg (\fst pr),\snd pr〉) sregs) @94 save_return … (map … (Reg ?) ret_regs) @ 95 restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @ 95 96 [ PUSH ertl_params ? srah ; 96 97 PUSH … sral ; … … 128 129 129 130 definition set_params_hdw : 130 ∀globals.list rtl_argument → list (joint_seq ertl_params globals) ≝131 ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝ 131 132 λglobals,params. 132 133 restore_hdws globals (zip_pottier ? ? params RegisterParams). … … 135 136 136 137 definition set_param_stack : 137 ∀globals.register → register → nat → rtl_argument →138 ∀globals.register → register → psd_argument → 138 139 list (joint_seq ertl_params globals) ≝ 139 λglobals,addr1,addr2,off,arg. 140 let int_off : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in 140 λglobals,addr1,addr2,arg. 141 [ STORE … addr1 addr2 arg ; 142 addr1 ← addr1 .Add. (int_size : Byte) ; 143 addr2 ← addr2 .Addc. zero_byte 144 ]. 145 146 definition set_params_stack : 147 ∀globals.list psd_argument → bind_new (localsT ertl_params) ? ≝ 148 λglobals,params. 149 νaddr1,addr2 in 150 let params_length_byte : Byte ≝ bitvector_of_nat ? (params) in 141 151 [ PSD addr1 ← HDW RegisterSPL ; 142 CLEAR_CARRY … ;143 addr1 ← addr1 .Sub. int_off ;144 152 PSD addr2 ← HDW RegisterSPH ; 145 addr2 ← addr2 .Sub. 0 ; 146 STORE … addr1 addr2 arg 147 ]. 148 149 definition set_params_stack : 150 ∀globals.list rtl_argument → bind_new (localsT ertl_params) ? ≝ 151 λglobals,params. 152 νaddr1,addr2 in 153 flatten … (mapi … (set_param_stack globals addr1 addr2) params). 153 CLEAR_CARRY ?? ; 154 addr1 ← addr1 .Sub. params_length_byte ; 155 addr2 ← addr2 .Sub. zero_byte 156 ] @ 157 flatten … (map … (set_param_stack globals addr1 addr2) params). 154 158 155 159 definition set_params ≝ … … 186 190 [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *) 187 191  POP _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *) 188  MOVE rs ⇒ PSD (\fst rs) ← 189 match \snd rs with 190 [ Reg src ⇒ PSD src 191  Imm b ⇒ INT b 192 ] 192  MOVE rs ⇒ PSD (\fst rs) ← \snd rs 193 193  COST_LABEL lbl ⇒ 194 194 COST_LABEL … lbl … … 254 254 let def' ≝ 255 255 mk_joint_internal_function globals ertl_params 256 (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)256 (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *) 257 257 nb_params new_locals ((joint_if_stacksize … def) + added_stacksize) 258 258 graph' entry' exit' in 
src/RTL/RTL_paolo.ma
r2186 r2208 1 1 include "joint/Joint_paolo.ma". 2 3 inductive rtl_argument : Type[0] ≝4  Reg : register → rtl_argument5  Imm : Byte → rtl_argument.6 7 coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg8 on _r : register to rtl_argument.9 10 coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm11 on _b : Byte to rtl_argument.12 13 definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).14 15 coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat16 on _n : nat to rtl_argument.17 2 18 3 inductive rtl_seq : Type[0] ≝ … … 20 5 21 6 inductive rtl_call : Type[0] ≝ 22  rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.7  rtl_call_ptr: register → register → list psd_argument → list register → rtl_call. 23 8 24 9 inductive rtl_tailcall : Type[0] ≝ 25  rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall26  rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall.10  rtl_tailcall_id: ident → list psd_argument → rtl_tailcall 11  rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall. 27 12 28 13 definition rtl_uns_params ≝ mk_unserialized_params … … 30 15 (* acc_a_reg ≝ *) register 31 16 (* acc_b_reg ≝ *) register 32 (* acc_a_arg ≝ *) rtl_argument33 (* acc_b_arg ≝ *) rtl_argument17 (* acc_a_arg ≝ *) psd_argument 18 (* acc_b_arg ≝ *) psd_argument 34 19 (* dpl_reg ≝ *) register 35 20 (* dph_reg ≝ *) register 36 (* dpl_arg ≝ *) rtl_argument37 (* dph_arg ≝ *) rtl_argument38 (* snd_arg ≝ *) rtl_argument39 (* pair_move ≝ *) (register × rtl_argument)40 (* call_args ≝ *) (list rtl_argument)21 (* dpl_arg ≝ *) psd_argument 22 (* dph_arg ≝ *) psd_argument 23 (* snd_arg ≝ *) psd_argument 24 (* pair_move ≝ *) (register × psd_argument) 25 (* call_args ≝ *) (list psd_argument) 41 26 (* call_dest ≝ *) (list register) 42 27 (* ext_seq ≝ *) rtl_seq … … 59 44 definition rtl_statement ≝ joint_statement rtl_params. 60 45 61 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? rtl_argument r a)).46 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)). 62 47 63 48 (* aid unification *) … … 71 56 unification hint 0 ≔ 72 57 (**) ⊢ 73 acc_a_arg rtl_params ≡ rtl_argument.58 acc_a_arg rtl_params ≡ psd_argument. 74 59 unification hint 0 ≔ 75 60 (**) ⊢ 76 acc_b_arg rtl_params ≡ rtl_argument.61 acc_b_arg rtl_params ≡ psd_argument. 77 62 unification hint 0 ≔ 78 63 (**) ⊢ … … 83 68 unification hint 0 ≔ 84 69 (**) ⊢ 85 dpl_arg rtl_params ≡ rtl_argument.70 dpl_arg rtl_params ≡ psd_argument. 86 71 unification hint 0 ≔ 87 72 (**) ⊢ 88 dph_arg rtl_params ≡ rtl_argument.73 dph_arg rtl_params ≡ psd_argument. 89 74 unification hint 0 ≔ 90 75 (**) ⊢ 91 snd_arg rtl_params ≡ rtl_argument.76 snd_arg rtl_params ≡ psd_argument. 92 77 unification hint 0 ≔ 93 78 (**) ⊢ 94 pair_move rtl_params ≡ register × rtl_argument.79 pair_move rtl_params ≡ register × psd_argument. 95 80 unification hint 0 ≔ 96 81 (**) ⊢ 97 call_args rtl_params ≡ list rtl_argument.82 call_args rtl_params ≡ list psd_argument. 98 83 unification hint 0 ≔ 99 84 (**) ⊢ … … 120 105 joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals. 121 106 122 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg107 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg 123 108 on _r : register to snd_arg rtl_params. 124 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm109 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte 125 110 on _b : Byte to snd_arg rtl_params. 126 111 … … 132 117 (* acc_a_reg ≝ *) register 133 118 (* acc_b_reg ≝ *) register 134 (* acc_a_arg ≝ *) rtl_argument135 (* acc_b_arg ≝ *) rtl_argument119 (* acc_a_arg ≝ *) psd_argument 120 (* acc_b_arg ≝ *) psd_argument 136 121 (* dpl_reg ≝ *) register 137 122 (* dph_reg ≝ *) register 138 (* dpl_arg ≝ *) rtl_argument139 (* dph_arg ≝ *) rtl_argument140 (* snd_arg ≝ *) rtl_argument141 (* pair_move ≝ *) (register × rtl_argument)142 (* call_args ≝ *) (list rtl_argument)123 (* dpl_arg ≝ *) psd_argument 124 (* dph_arg ≝ *) psd_argument 125 (* snd_arg ≝ *) psd_argument 126 (* pair_move ≝ *) (register × psd_argument) 127 (* call_args ≝ *) (list psd_argument) 143 128 (* call_dest ≝ *) (list register) 144 129 (* ext_seq ≝ *) rtl_seq
Note: See TracChangeset
for help on using the changeset viewer.