Changeset 1060 for src/RTLabs
- Timestamp:
- Jul 8, 2011, 12:17:14 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLAbstoRTL.ma
r1059 r1060 3 3 include "common/AssocList.ma". 4 4 include "common/Graphs.ma". 5 include "common/Maps.ma".6 5 (* include "common/IntValue.ma". *) 7 6 include "common/FrontEndOps.ma". … … 227 226 | rtl_st_int r i _ ⇒ rtl_st_int r i lbl 228 227 | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl 229 | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2lbl228 | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl 230 229 | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl 231 230 | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl … … 238 237 | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a 239 238 | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2 239 | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl 240 | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl 240 241 | rtl_st_return r ⇒ rtl_st_return r 241 242 ]. … … 299 300 λsrcrs: list register. 300 301 λstart_lbl: label. 302 match reduce_strong register destrs srcrs with 303 [ dp crl_crr len_proof ⇒ 304 let commonl ≝ \fst (\fst crl_crr) in 305 let commonr ≝ \fst (\snd crl_crr) in 306 let restl ≝ \snd (\fst crl_crr) in 307 let restr ≝ \snd (\snd crl_crr) in 308 let f_common ≝ translate_move_internal start_lbl in 309 let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in 310 let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 311 add_translates [ translate1 ; translate2 ] start_lbl 312 ]. 313 @len_proof 314 qed. 315 316 let rec make 317 (A: Type[0]) (elt: A) (n: nat) on n ≝ 318 match n with 319 [ O ⇒ [ ] 320 | S n' ⇒ elt :: make A elt n' 321 ]. 322 323 lemma make_length: 324 ∀A: Type[0]. 325 ∀elt: A. 326 ∀n: nat. 327 n = length ? (make A elt n). 328 #A #ELT #N 329 elim N 330 [ normalize % 331 | #N #IH 332 normalize <IH % 333 ] 334 qed. 335 336 definition translate_cast_unsigned ≝ 337 λdestrs. 338 λstart_lbl. 339 λdest_lbl. 340 λdef. 341 let 〈def, tmp_zero〉 ≝ fresh_reg def in 342 let zeros ≝ make ? tmp_zero (length ? destrs) in 343 add_translates [ 344 adds_graph [ 345 rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl 346 ]; 347 translate_move destrs zeros 348 ] start_lbl dest_lbl def. 349 350 definition translate_cast_signed ≝ 351 λdestrs. 352 λsrcr. 353 λstart_lbl. 354 λdest_lbl. 355 λdef. 356 let 〈def, tmp_128〉 ≝ fresh_reg def in 357 let 〈def, tmp_255〉 ≝ fresh_reg def in 358 let 〈def, tmpr〉 ≝ fresh_reg def in 359 let 〈def, dummy〉 ≝ fresh_reg def in 360 let insts ≝ [ 361 rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl; 362 rtl_st_op2 And tmpr tmp_128 srcr start_lbl; 363 rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl; 364 rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl; 365 rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl 366 ] in 367 let srcrs ≝ make ? tmpr (length ? destrs) in 368 add_translates [ 369 adds_graph insts; 370 translate_move destrs srcrs 371 ] start_lbl dest_lbl def. 372 373 definition translate_cast ≝ 374 λsrc_size. 375 λsrc_sign. 376 λdest_size. 377 λdestrs. 378 λsrcrs. 379 match | srcrs | return λx. | srcrs | = x → ? with 380 [ O ⇒ λzero_prf. adds_graph [ ] 381 | S n' ⇒ λsucc_prf. 382 if ltb dest_size src_size then 383 translate_move destrs srcrs 384 else 385 match reduce_strong ? destrs srcrs with 386 [ dp crl len_proof ⇒ 387 let commonl ≝ \fst (\fst crl) in 388 let commonr ≝ \fst (\snd crl) in 389 let restl ≝ \snd (\fst crl) in 390 let restr ≝ \snd (\snd crl) in 391 let insts_common ≝ translate_move commonl commonr in 392 let sign_reg ≝ last_safe ? srcrs ? in 393 let insts_sign ≝ 394 match src_sign with 395 [ Unsigned ⇒ translate_cast_unsigned restl 396 | Signed ⇒ translate_cast_signed restl sign_reg 397 ] 398 in 399 add_translates [ insts_common; insts_sign ] 400 ] 401 ] (refl ? (|srcrs|)). 402 >succ_prf // 403 qed. 404 405 definition translate_negint ≝ 406 λdestrs. 407 λsrcrs. 408 λstart_lbl. 409 λdest_lbl. 410 λdef. 411 λprf: | destrs | = | srcrs |. (* assert in caml code *) 412 let 〈def, tmpr〉 ≝ fresh_reg def in 413 let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in 414 let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in 415 let insts_init ≝ [ 416 rtl_st_set_carry start_lbl; 417 rtl_st_int tmpr (zero ?) start_lbl 418 ] in 419 let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in 420 let insts_add ≝ map … f_add destrs in 421 adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. 422 423 definition translate_notbool ≝ 424 λdestrs. 425 λsrcrs. 426 λstart_lbl. 427 λdest_lbl. 428 λdef. 429 match destrs with 430 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 431 | cons destr destrs ⇒ 432 let 〈def, tmpr〉 ≝ fresh_reg def in 433 let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in 434 let save_srcrs ≝ translate_move tmp_srcrs srcrs in 435 let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in 436 let f ≝ λtmp_srcr. [ 437 rtl_st_clear_carry start_lbl; 438 rtl_st_int tmpr (zero ?) start_lbl; 439 rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl; 440 rtl_st_int tmpr (zero ?) start_lbl; 441 rtl_st_op2 Addc tmpr tmpr tmpr start_lbl; 442 rtl_st_op2 Xor destr destr tmpr start_lbl 443 ] in 444 let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in 445 let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in 446 add_translates [ 447 save_srcrs; adds_graph insts; epilogue 448 ] start_lbl dest_lbl def 449 ]. 450 451 definition translate_intermediate_op1 ≝ 452 λop1. 453 λdestrs. 454 λsrcrs. 455 λstart_lbl. 456 λdest_lbl. 457 λdef. 301 458 λprf: | destrs | = | srcrs |. 302 let 〈crl, crr〉 ≝ reduce register destrs srcrs in 303 let 〈commonl, restl〉 ≝ crl in 304 let 〈commonr, restr〉 ≝ crr in 305 let f_common ≝ translate_move_internal start_lbl in 306 let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in 307 let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 308 add_translates [ translate1 ; translate2 ] start_lbl. 309 310 let rec translate_move destrs srcrs start_lbl = 311 let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in 312 let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in 313 let translates1 = adds_graph (List.map2 f_common common1 common2) in 314 let translates2 = translate_cst (AST.Cst_int 0) rest1 in 315 add_translates [translates1 ; translates2] start_lbl 459 match op1 with 460 [ intermediate_op1_cast src_size src_sign dest_size ⇒ 461 translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def 462 | intermediate_op1_negint ⇒ 463 translate_negint destrs srcrs start_lbl dest_lbl def prf 464 | intermediate_op1_notbool ⇒ 465 translate_notbool destrs srcrs start_lbl dest_lbl def 466 | intermediate_op1_notint ⇒ 467 let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in 468 let l ≝ map2 … f destrs srcrs prf in 469 adds_graph l start_lbl dest_lbl def 470 | intermediate_op1_ptrofint ⇒ 471 translate_move destrs srcrs start_lbl dest_lbl def 472 | intermediate_op1_intofptr ⇒ 473 translate_move destrs srcrs start_lbl dest_lbl def 474 | intermediate_op1_id ⇒ 475 translate_move destrs srcrs start_lbl dest_lbl def 476 ]. 316 477 317 478 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.