Changeset 1283 for src/RTL/RTLtoERTL.ma
 Timestamp:
 Sep 30, 2011, 3:12:40 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1282 r1283 10 10 λdestr_srcr.λstart_lbl. 11 11 let 〈destr, srcr〉 ≝ destr_srcr in 12 adds_graph ertl_params1 globals [ sequential … (MOVE … 〈pseudo destr,hardware srcr〉) start_lbl] start_lbl12 adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl 13 13 in 14 14 map ? ? save_hdws_internal l. … … 20 20 λstart_lbl: label. 21 21 let 〈srcr, destr〉 ≝ srcr_destr in 22 adds_graph ertl_params1 globals [ sequential … (MOVE … 〈hardware destr, pseudo srcr〉) start_lbl] start_lbl22 adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl 23 23 in 24 24 map ? ? restore_hdws_internal l. … … 28 28 λparams: list register. 29 29 match params with 30 [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … start_lbl] start_lbl]30 [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl] 31 31  _ ⇒ 32 32 let l ≝ zip_pottier ? ? params RegisterParams in … … 44 44 let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in 45 45 adds_graph ertl_params1 globals [ 46 sequential … (extension … (ertl_st_ext_frame_size addr1)) start_lbl;47 sequential … (INT … tmpr int_offset) start_lbl;48 sequential … (OP2 … Sub addr1 addr1 tmpr) start_lbl;49 sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;50 sequential … (OP2 … Add addr1 addr1 tmpr) start_lbl;51 sequential … (INT … addr2 (bitvector_of_nat 8 0)) start_lbl;52 sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;53 sequential … (OP2 … Addc addr2 addr2 tmpr) start_lbl;54 sequential … (LOAD … destr addr1 addr2) start_lbl46 sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1)); 47 sequential ertl_params_ … (INT … tmpr int_offset); 48 sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr); 49 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉); 50 sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr); 51 sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0)); 52 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); 53 sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr); 54 sequential ertl_params_… (LOAD … destr addr1 addr2) 55 55 ] start_lbl dest_lbl def. 56 56 … … 58 58 λglobals,params. 59 59 match params with 60 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl ]60 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ] 61 61  _ ⇒ mapi ? ? (get_param_stack globals) params ]. 62 62 … … 84 84 add_translates … 85 85 ((adds_graph ertl_params1 … [ 86 sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl86 sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) 87 87 ]) :: 88 (adds_graph … [89 sequential … (POP … sral) start_lbl;90 sequential … (POP … srah) start_lbl88 (adds_graph ertl_params1 … [ 89 sequential ertl_params_ … (POP … sral); 90 sequential ertl_params_ … (POP … srah) 91 91 ]) :: 92 92 (save_hdws … sregs) @ … … 113 113 let restl ≝ \snd (\fst crl) in 114 114 let restr ≝ \snd (\snd crl) in 115 let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) start_lblin116 let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) start_lblin115 let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in 116 let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in 117 117 let saves ≝ map2 … f_save commonl commonr crl_proof in 118 let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) start_lblin118 let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in 119 119 let defaults ≝ map … f_default restl in 120 120 adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def … … 127 127 let commonl ≝ \fst (\fst crl) in 128 128 let commonr ≝ \fst (\snd crl) in 129 let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) start_lblin129 let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in 130 130 let insts ≝ map2 ? ? ? f commonl commonr crl_proof in 131 131 adds_graph ertl_params1 … insts start_lbl … … 149 149 [save_return globals ret_regs] @ 150 150 restore_hdws … sregs @ 151 [adds_graph … [152 sequential … (PUSH … srah) start_lbl;153 sequential … (PUSH … sral) start_lbl151 [adds_graph ertl_params1 … [ 152 sequential ertl_params_ … (PUSH … srah); 153 sequential ertl_params_ … (PUSH … sral) 154 154 ]] @ 155 155 [adds_graph ertl_params1 … [ 156 sequential … (extension … ertl_st_ext_del_frame) start_lbl156 sequential ertl_params_ … (extension … ertl_st_ext_del_frame) 157 157 ]] @ 158 158 [assign_result globals] … … 205 205 λglobals,params. 206 206 match params with 207 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl]207 [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl] 208 208  _ ⇒ 209 209 let l ≝ zip_pottier ? ? params RegisterParams in … … 223 223 let 〈ignore, int_off〉 ≝ half_add ? off int_size in 224 224 adds_graph ertl_params1 … [ 225 sequential … (INT … addr1 int_off) start_lbl;226 sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;227 sequential … (CLEAR_CARRY …) start_lbl;228 sequential … (OP2 … Sub addr1 tmpr addr1) start_lbl;229 sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;230 sequential … (INT … addr2 (zero ?)) start_lbl;231 sequential … (OP2 … Sub addr2 tmpr addr2) start_lbl;232 sequential … (STORE … addr1 addr2 srcr) start_lbl225 sequential ertl_params_ … (INT … addr1 int_off); 226 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉); 227 sequential ertl_params_ … (CLEAR_CARRY …); 228 sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1); 229 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); 230 sequential ertl_params_ … (INT … addr2 (zero ?)); 231 sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2); 232 sequential ertl_params_ … (STORE … addr1 addr2 srcr) 233 233 ] start_lbl dest_lbl def. 234 234 … … 236 236 λglobals,params. 237 237 match params with 238 [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO … start_lbl] start_lbl]238 [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl] 239 239  _ ⇒ 240 240 let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in … … 259 259 let commonl ≝ \fst (\fst crl) in 260 260 let commonr ≝ \fst (\snd crl) in 261 let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) start_lblin261 let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in 262 262 let saves ≝ map2 ? ? ? f_save commonl commonr ? in 263 263 match reduce_strong ? ? ret_regs RegisterSTS with … … 265 265 let commonl ≝ \fst (\fst crl) in 266 266 let commonr ≝ \fst (\snd crl) in 267 let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) start_lblin267 let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in 268 268 let restores ≝ map2 ? ? ? f_restore commonl commonr ? in 269 269 adds_graph ertl_params1 … (saves @ restores) start_lbl]]. … … 281 281 add_translates ertl_params1 globals ( 282 282 set_params … args @ [ 283 adds_graph ertl_params1 … [ sequential … (CALL_ID … f nb_args it) start_lbl];283 adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ]; 284 284 fetch_result … ret_regs 285 285 ] … … 311 311  rtlntc_st_ext_address r1 r2 ⇒ 312 312 adds_graph ertl_params1 … [ 313 sequential … (MOVE … 〈pseudo r1, hardware RegisterSPL〉) lbl;314 sequential … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) lbl313 sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉); 314 sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) 315 315 ] lbl lbl' def] 316 316 (*CSC: everything is just copied to retype it from now on;
Note: See TracChangeset
for help on using the changeset viewer.