Changeset 1067
 Timestamp:
 Jul 13, 2011, 5:37:42 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1066 r1067 1157 1157 definition translate_stmt ≝ 1158 1158 λlenv. 1159 λret: register. (* change from o'caml code, this is taken from func. record *) 1159 1160 λlbl: label. 1160 1161 λstmt. … … 1196 1197 translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def 1197 1198  St_jumptable r l ⇒ ? (* assert false: not implemented yet *) 1198  St_return r ⇒ 1199 match r with 1200 [ None ⇒ add_graph lbl (rtl_st_return [ ]) def 1201  Some r ⇒ add_graph lbl (rtl_st_return (find_local_env r lenv)) def 1202 ] 1203  _ ⇒ ? 1204 ]. 1205 1206 let translate_stmt lenv lbl stmt def = match stmt with 1207 1208  RTLabs.St_skip lbl' > 1209 add_graph lbl (RTL.St_skip lbl') def 1210 1211  RTLabs.St_cost (cost_lbl, lbl') > 1212 add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def 1213 1214  RTLabs.St_cst (destr, cst, lbl') > 1215 translate_cst cst (find_local_env destr lenv) lbl lbl' def 1216 1217  RTLabs.St_op1 (op1, destr, srcr, lbl') > 1218 translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) 1219 lbl lbl' def 1220 1221  RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') > 1222 translate_op2 op2 (find_local_env destr lenv) 1223 (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def 1224 1225  RTLabs.St_load (_, addr, destr, lbl') > 1226 translate_load (find_local_env addr lenv) (find_local_env destr lenv) 1227 lbl lbl' def 1228 1229  RTLabs.St_store (_, addr, srcr, lbl') > 1230 translate_store (find_local_env addr lenv) (find_local_env srcr lenv) 1231 lbl lbl' def 1232 1233  RTLabs.St_call_id (f, args, None, _, lbl') > 1234 add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def 1235 1236  RTLabs.St_call_id (f, args, Some retr, _, lbl') > 1237 add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, 1238 find_local_env retr lenv, lbl')) def 1239 1240  RTLabs.St_call_ptr (f, args, None, _, lbl') > 1241 let (f1, f2) = find_and_addr f lenv in 1242 add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def 1243 1244  RTLabs.St_call_ptr (f, args, Some retr, _, lbl') > 1245 let (f1, f2) = find_and_addr f lenv in 1246 add_graph lbl 1247 (RTL.St_call_ptr 1248 (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def 1249 1250  RTLabs.St_tailcall_id (f, args, _) > 1251 add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def 1252 1253  RTLabs.St_tailcall_ptr (f, args, _) > 1254 let (f1, f2) = find_and_addr f lenv in 1255 add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def 1256 1257  RTLabs.St_cond (r, lbl_true, lbl_false) > 1258 translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def 1259 1260  RTLabs.St_jumptable _ > 1261 error "Jump tables not supported yet." 1262 1263  RTLabs.St_return None > 1264 add_graph lbl (RTL.St_return []) def 1265 1266  RTLabs.St_return (Some r) > 1267 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 1199  St_return ⇒ add_graph lbl (rtl_st_return (find_local_env ret lenv)) def 1200 ]. 1201 [10: cases not_implemented (* jtable case *) 1202 *: cases daemon (* TODO: proofs regarding lengths of lists, examine! *) 1203 ] 1204 qed. 1205 1206 definition translate_internal ≝ 1207 λdef. 1208 let runiverse ≝ f_reggen def in 1209 let lenv ≝ initialize_local_env runiverse 1210 (f_params def @ f_locals def) (f_result def) in ?. 1211 1212 let translate_internal def = 1213 let runiverse = def.RTLabs.f_runiverse in 1214 let lenv = 1215 initialize_local_env runiverse 1216 (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in 1217 let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in 1218 let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in 1219 let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in 1220 let locals = set_of_list locals in 1221 let result = match def.RTLabs.f_result with 1222  None > [] 1223  Some (r, _) > find_local_env r lenv in 1224 let res = 1225 { RTL.f_luniverse = def.RTLabs.f_luniverse ; 1226 RTL.f_runiverse = runiverse ; 1227 RTL.f_result = result ; 1228 RTL.f_params = params ; 1229 RTL.f_locals = locals ; 1230 RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ; 1231 RTL.f_graph = Label.Map.empty ; 1232 RTL.f_entry = def.RTLabs.f_entry ; 1233 RTL.f_exit = def.RTLabs.f_exit } in 1234 Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res 1268 1235 1269 1236 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.