Changeset 3255 for src/RTL/RTLToERTL.ma
 Timestamp:
 May 8, 2013, 4:53:31 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLToERTL.ma
r3145 r3255 9 9 10 10 definition save_hdws : 11 ∀globals.list (register× Register) → list (joint_seq ERTL globals) ≝11 ∀globals.list (register×(Σr.ertl_hdw_readable r∧ertl_hdw_writable r)) → list (joint_seq ERTL globals) ≝ 12 12 λglobals. 13 let save_hdws_internal ≝14 λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in13 let save_hdws_internal : (register×(Σr.?)) → ? ≝ 14 λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in 15 15 map ?? save_hdws_internal. 16 [ @(π1 (pi2 ?? (\snd destr_srcr)))  @I ] qed. 16 17 17 18 definition restore_hdws : 18 ∀globals.list (psd_argument× Register) → list (joint_seq ERTL globals) ≝19 ∀globals.list (psd_argument×(Σr.ertl_hdw_readable r∧ertl_hdw_writable r)) → list (joint_seq ERTL globals) ≝ 19 20 λglobals. 20 21 let restore_hdws_internal ≝ 21 λdestr_srcr:psd_argument× ?.HDW (\snd destr_srcr) ← \fst destr_srcr in22 λdestr_srcr:psd_argument×(Σr.?).HDW (\snd destr_srcr) ← \fst destr_srcr in 22 23 map ? ? restore_hdws_internal. 24 @(π2 (pi2 ?? (\snd destr_srcr))) qed. 25 26 definition RegisterParamsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝ 27 [Register30; Register31; Register32; Register33; Register34; Register35; 28 Register36; Register37]. %% qed. 29 30 definition RegisterCalleeSavedSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝ 31 [Register20; Register21; Register22; Register23; Register24; Register25; 32 Register26; Register27]. %% qed. 33 34 definition RegisterRetsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝ 35 [Register00; Register01; Register02; Register03]. %% qed. 23 36 24 37 definition get_params_hdw : 25 38 ∀globals.list register → list (joint_seq ERTL globals) ≝ 26 39 λglobals,params. 27 save_hdws … (zip_pottier … params RegisterParams ).40 save_hdws … (zip_pottier … params RegisterParamsSig). 28 41 29 42 definition get_param_stack : … … 50 63 addr1 ← addr1 .Add. tmpr ; 51 64 addr2 ← addr2 .Addc. zero_byte ] @ 52 flatten … (map ?? (get_param_stack globals addr1 addr2) params). 65 flatten … (map ?? (get_param_stack globals addr1 addr2) params). % qed. 53 66 54 67 definition get_params ≝ … … 58 71 get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params. 59 72 73 (* 60 74 definition save_return : 61 ∀globals.list psd_argument→ list (joint_seq ERTL globals) ≝75 ∀globals.list register → list (joint_seq ERTL globals) ≝ 62 76 λglobals,ret_regs. 63 77 match reduce_strong ? ? RegisterSTS ret_regs with … … 67 81 let restl ≝ \snd (\fst crl) in 68 82 (* let restr ≝ \snd (\snd crl) in *) 69 map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @ 70 map … (λst.HDW st ← zero_byte) restl 71 ]. 72 73 definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝ 74 λglobals. 75 match reduce_strong ?? RegisterRets RegisterSTS with 83 map2 … (λst : Σr.?.λr : register.HDW st ← r) commonl commonr crl_proof @ 84 map … (λst : Σr.?.HDW st ← zero_byte) restl 85 ]. @(pi2 ?? st) qed. 86 *) 87 88 89 definition assign_result : ∀globals. 90 list register → list (joint_seq ERTL globals) ≝ 91 λglobals,ret_regs. 92 match reduce_strong ?? RegisterRetsSig ret_regs with 76 93 [ mk_Sig crl crl_proof ⇒ 77 94 let commonl ≝ \fst (\fst crl) in 78 95 let commonr ≝ \fst (\snd crl) in 79 map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof 80 ]. 96 let restl ≝ \snd (\fst crl) in 97 map2 … (λR : Σr.?.λr : register.HDW R ← PSD r) commonl commonr crl_proof @ 98 map … (λR : Σr.?.HDW R ← zero_byte) restl 99 ]. [ @I *: @(π2 (pi2 ?? R)) ] qed. 81 100 82 101 lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf. … … 101 120 102 121 definition epilogue : 103 ∀globals.list register → register → register → list (register × Register) →122 ∀globals.list register → register → register → list (register × (Σr.?)) → 104 123 Σl : list (joint_seq ERTL globals). 105 124 All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝ 106 125 λglobals,ret_regs,sral,srah,sregs. 107 save_return … (map … (Reg ?) ret_regs) @108 restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs)@126 restore_hdws … (map ?? (λx.〈Reg ? (\fst x), \snd x〉) sregs) @ 127 assign_result globals ret_regs @ 109 128 [ PUSH ERTL ? sral ; 110 PUSH … srah ; 111 ertl_del_frame ] @ 112 assign_result globals. 129 PUSH … srah ]. 113 130 @hide_prf 114 131 @All_append 115 [ whd in match save_return; normalize nodelta 116 cases (reduce_strong ????) ** #a #b * #c #d #prf normalize nodelta 117 @All_append 118 [ @(All_map2 … (All2_True … prf)) #x #y #_ % 119  @(All_map … (All_True …)) #x #_ % 120 ] 132 [ @(All_map … (All_True …)) #x #_ % 121 133  @All_append 122 [ @(All_map … (All_True …)) #x #_ % 123  %{(refl …)} %{(refl …)} %{(refl …)} 124 whd in match assign_result; 134 [ whd in match assign_result; 125 135 generalize in match reduce_strong; #f normalize nodelta 126 136 cases (f ????) #l #prf normalize nodelta 127 @(All_map2 … (All2_True … prf)) #x #y #_ % 137 @All_append 138 [ @(All_map2 … (All2_True … prf)) #x #y #_ % 139  @(All_map … (All_True …)) #x #_ % 140 ] 141  %%% 128 142 ] 129 143 ] … … 132 146 definition prologue : 133 147 ∀globals.list register → register → register → register → register → register → 134 list (register× Register) →148 list (register×(Σr.?)) → 135 149 bind_new register (list (joint_seq ERTL globals)) ≝ 136 150 λglobals,params,sral,srah,tmpr,addr1,addr2,sregs. 137 [ (ertl_new_frame : joint_seq ??) ; 138 POP … srah ; 151 [ POP … srah ; 139 152 POP … sral 140 153 ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params. … … 143 156 ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ 144 157 λglobals,params. 145 restore_hdws globals (zip_pottier ? ? params RegisterParams). 146 147 (* Paolo: The following can probably be done way more efficiently with INC DPTR *) 158 restore_hdws globals (zip_pottier ? ? params RegisterParamsSig). 148 159 149 160 definition set_param_stack : … … 167 178 addr2 ← addr2 .Sub. zero_byte 168 179 ] @ 169 flatten … (map … (set_param_stack globals addr1 addr2) params). 180 flatten … (map … (set_param_stack globals addr1 addr2) params). % qed. 170 181 171 182 definition set_params : … … 174 185 BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝ 175 186 λglobals,params. 176 let n ≝ min (params) (RegisterParams ) in187 let n ≝ min (params) (RegisterParamsSig) in 177 188 let hdw_stack_params ≝ split ? params n in 178 189 let hdw_params ≝ \fst hdw_stack_params in … … 197 208 All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝ 198 209 λglobals,ret_regs. 199 match reduce_strong ?? RegisterSTS RegisterRetswith210 match reduce_strong ?? ret_regs RegisterRetsSig with 200 211 [ mk_Sig crl crl_proof ⇒ 201 212 let commonl ≝ \fst (\fst crl) in 202 213 let commonr ≝ \fst (\snd crl) in 203 map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @ 204 match reduce_strong ?? ret_regs RegisterSTS with 205 [ mk_Sig crl crl_proof ⇒ 206 let commonl ≝ \fst (\fst crl) in 207 let commonr ≝ \fst (\snd crl) in 208 map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof 209 ] 214 map2 … (λr.λR : Σr.?.PSD r ← HDW R) commonl commonr crl_proof 210 215 ]. 211 @hide_prf 212 @All_append 213 [ @(All_map2 … (All2_True … crl_proof)) #x #y #_ % 214  cases (reduce_strong ????) #l #prf normalize nodelta 215 @(All_map2 … (All2_True … prf)) #x #y #_ % 216 ] 216 @hide_prf [2: % 3: @(π1 (pi2 … R)) ] 217 @(All_map2 … (All2_True … crl_proof)) #x #y #_ % 217 218 qed. 218 219 … … 260 261  COND r ltrue ⇒ 261 262 bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉 262 ]. 263 ]. % qed. 263 264 264 265 definition translate_fin_step : 265 ∀globals.list register → register → register → list (register × Register) →266 ∀globals.list register → register → register → list (register × (Σr.?)) → 266 267 label → joint_fin_step RTL → 267 268 bind_fin_block ERTL globals ≝ … … 275 276 definition allocate_regs : 276 277 ∀X : Type[0]. 277 (list (register× Register) → bind_new register X) →278 (list (register×(Σr.?)) → bind_new register X) → 278 279 bind_new register X ≝ 279 280 λX,f. 280 281 let allocate_regs_internal ≝ 281 λacc : bind_new register (list (register × Register)).282 λr: Register.282 λacc : bind_new register (list (register × (Σr.?))). 283 λr: Σr.?. 283 284 ! tl ← acc ; 284 285 νr' in return (〈r', r〉 :: tl) in 285 ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ;286 ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSavedSig ; 286 287 f to_save. 287 288 … … 314 315 try #a try #b try #c try #d try #e try #f destruct 315 316 cases a in b; #a1 #a2 normalize nodelta #EQ destruct 316  #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 317 % (* XXX: FAILS, unintentional list reversal??? *) 317  #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 % 318 318 ] 319 319 (* #l *
Note: See TracChangeset
for help on using the changeset viewer.