Changeset 1283
 Timestamp:
 Sep 30, 2011, 3:12:40 AM (8 years ago)
 Location:
 src
 Files:

 3 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; 
src/RTLabs/RTLAbstoRTL.ma
r1282 r1283 158 158 definition translate_move_internal ≝ 159 159 λglobals. 160 λstart_lbl: label.161 160 λdestr: register. 162 161 λsrcr: register. 163 sequential rtl_params_ globals (MOVE … 〈destr,srcr〉) start_lbl.162 sequential rtl_params_ globals (MOVE … 〈destr,srcr〉). 164 163 165 164 definition translate_move ≝ … … 174 173 let restl ≝ \snd (\fst crl_crr) in 175 174 let restr ≝ \snd (\snd crl_crr) in 176 let f_common ≝ translate_move_internal globals start_lblin175 let f_common ≝ translate_move_internal globals in 177 176 let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in 178 177 let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) … … 212 211 add_translates … [ 213 212 adds_graph rtl_params1 … [ 214 sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl213 sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) 215 214 ]; 216 215 translate_move globals destrs zeros 
src/joint/TranslateUtils.ma
r1282 r1283 39 39 fresh LabelTag (joint_if_luniverse … def). 40 40 41 definition change_label ≝42 λpars1,globals.λe: joint_statement (graph_params pars1 globals) globals.λl.43 match e with44 [ GOTO _ ⇒ GOTO … l45  RETURN ⇒ RETURN ??46  sequential instr _ ⇒ sequential … globals instr l].47 48 (*CSC: bad programming habit: the code below puts everywhere a fake49 label and then adds_graph fixes them *)50 (*CSC: this is just an instance of add_translates below! *)51 41 let rec adds_graph 52 42 (pars1: params1) (globals: list ident) 53 (stmt_list: list ( joint_statement (graph_params_ pars1) globals))43 (stmt_list: list (label → joint_statement (graph_params_ pars1) globals)) 54 44 (start_lbl: label) (dest_lbl: label) 55 45 (def: joint_internal_function … (graph_params pars1 globals)) … … 59 49  cons stmt stmt_list ⇒ 60 50 match stmt_list with 61 [ nil ⇒ add_graph … start_lbl ( change_label …stmt dest_lbl) def51 [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def 62 52  _ ⇒ 63 53 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 64 let stmt ≝ change_label … stmt tmp_lbl in 65 let def ≝ add_graph … start_lbl stmt def in 54 let def ≝ add_graph … start_lbl (stmt tmp_lbl) def in 66 55 adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]]. 67 56 68 (*CSC: bad programming habit: the code below puts everywhere a fake69 label and then adds_graph fixes them *)70 57 let rec add_translates 71 58 (pars1: params1) (globals: list ident)
Note: See TracChangeset
for help on using the changeset viewer.