Changeset 1057 for src/RTLabs
 Timestamp:
 Jul 5, 2011, 5:53:11 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1053 r1057 4 4 include "common/Graphs.ma". 5 5 include "common/Maps.ma". 6 include " utilities/HMap.ma".6 include "common/IntValue.ma". 7 7 8 8 definition add_graph ≝ … … 25 25 rtl_if_exit'. 26 26 27 definition fresh_label ≝27 definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝ 28 28 λdef. 29 match fresh LabelTag (rtl_if_luniverse def) with 30 [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ) 31  Error _ ⇒ None ? 32 ]. 29 let 〈lbl, new_univ〉 ≝ fresh LabelTag (rtl_if_luniverse def) in 30 let locals ≝ rtl_if_locals def in 31 let rtl_if_luniverse' ≝ new_univ in 32 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 33 let rtl_if_sig' ≝ rtl_if_sig def in 34 let rtl_if_result' ≝ rtl_if_result def in 35 let rtl_if_params' ≝ rtl_if_params def in 36 let rtl_if_locals' ≝ rtl_if_locals def in 37 let rtl_if_stacksize' ≝ rtl_if_stacksize def in 38 let rtl_if_graph' ≝ rtl_if_graph def in 39 let rtl_if_entry' ≝ rtl_if_entry def in 40 let rtl_if_exit' ≝ rtl_if_exit def in 41 〈mk_rtl_internal_function 42 rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result' 43 rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph' 44 rtl_if_entry' rtl_if_exit', lbl〉. 33 45 34 46 axiom register_fresh: universe RegisterTag → register. … … 232 244 labels as unbounded nats then this function will never fail. 233 245 *) 246 (* Fixed with changes to label generation. 247 *) 234 248 let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝ 235 249 match stmt_list with 236 [ nil ⇒ Some ?def250 [ nil ⇒ def 237 251  cons hd tl ⇒ 238 252 match tl with 239 [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)253 [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def 240 254  cons hd' tl' ⇒ 241 let tmp_lbl ≝ fresh_label def in 242 match tmp_lbl with 243 [ None ⇒ None ? 244  Some tmp_lbl ⇒ 245 let stmt ≝ change_label tmp_lbl hd in 246 let def ≝ add_graph start_lbl stmt def in 247 adds_graph tl tmp_lbl dest_lbl def 248 ] 249 ] 250 ]. 251 252 (* dpm: had to lift this into option *) 255 let 〈new_def, tmp_lbl〉 ≝ fresh_label def in 256 let stmt ≝ change_label tmp_lbl hd in 257 let def ≝ add_graph start_lbl stmt new_def in 258 adds_graph tl tmp_lbl dest_lbl new_def 259 ] 260 ]. 261 253 262 let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label) 254 263 (def: ?) on translate_list ≝ 255 264 match translate_list with 256 [ nil ⇒ Some ?def265 [ nil ⇒ def 257 266  cons hd tl ⇒ 258 267 match tl with 259 268 [ nil ⇒ hd start_lbl dest_lbl def 260 269  cons hd' tl' ⇒ 261 let tmp_lbl≝ fresh_label def in262 match tmp_lbl with263 [ None ⇒ None ?264  Some tmp_lbl ⇒265 match hd start_lbl tmp_lbl def with266 [ None ⇒ None ? 267  Some def ⇒ add_translates tl tmp_lbl dest_lbl def 268 ]269 ]270 ]271 ].270 let 〈new_def, tmp_lbl〉 ≝ fresh_label def in 271 let applied ≝ hd start_lbl tmp_lbl new_def in 272 add_translates tl tmp_lbl dest_lbl applied 273 ] 274 ]. 275 276 definition translate_cst_int_internal ≝ 277 λdest_lbl. 278 λr. 279 λi. 280 rtl_st_int r i dest_lbl. 272 281 273 282 definition translate_cst ≝ … … 281 290 match destrs with 282 291 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 283  cons hd tl ⇒ 284 match tl with 285 [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_int hd i dest_lbl) def) 286  cons hd' tl' ⇒ None ? 287 ] 288 ] 292  _ ⇒ 293 (* this case needs changing when Z is added to stdlib as we are using 294 nats instead of ints here! *) 295 let size ≝ length ? destrs in 296 let is ≝ map … (to_int size) (break size (of_int size (nat_of_bitvector ? i)) size) in 297 let is' ≝ map … (bitvector_of_nat ?) is in 298 let l ≝ map2 … (translate_cst_int_internal dest_lbl) destrs is' ? in 299 adds_graph l start_lbl dest_lbl def 300 ] 301  cast_addrsymbol id ⇒ 302 let 〈r1, r2〉 ≝ make_addr ? destrs ? in 303 add_graph start_lbl (rtl_st_addr r1 r2 id dest_lbl) def 304  _ ⇒ ? 305 ]. 289 306  cast_addrsymbol id ⇒ 290 307 match destrs with … … 318 335 (*  cast_float f ⇒ None ? *) (* what are we doing with floats? *) 319 336 ]. 337 338 let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with 339 340  AST.Cst_stack > 341 let (r1, r2) = make_addr destrs in 342 add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def 343 344  AST.Cst_offset off > 345 let i = concrete_offset off in 346 translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def 347 348  AST.Cst_sizeof size > 349 let i = concrete_size size in 350 translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def 320 351 321 352 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.