 Timestamp:
 Oct 3, 2011, 4:07:22 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1285 r1286 323 323 ]. 324 324 325 (*326 327 325 (* TODO: examine this properly. This is a change from the O'caml code due 328 326 to us dropping the explicit use of a cast destination size field. We … … 331 329 *) 332 330 definition translate_op1 ≝ 331 λglobals: list ident. 333 332 λop1: unary_operation. 334 333 λdestrs: list register. … … 337 336 λstart_lbl: label. 338 337 λdest_lbl: label. 339 λdef: rtl_internal_function .338 λdef: rtl_internal_function globals. 340 339 match op1 with 341 340 [ Ocastint src_sign src_size ⇒ 342 341 let dest_size ≝ destrs * 8 in 343 342 let src_size ≝ bitsize_of_intsize src_size in 344 translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def343 translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def 345 344  Onegint ⇒ 346 translate_negint destrs srcrs start_lbl dest_lbl def prf345 translate_negint globals destrs srcrs start_lbl dest_lbl def prf 347 346  Onotbool ⇒ 348 translate_notbool destrs srcrs start_lbl dest_lbl def347 translate_notbool globals destrs srcrs start_lbl dest_lbl def 349 348  Onotint ⇒ 350 let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lblin349 let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in 351 350 let l ≝ map2 … f destrs srcrs prf in 352 adds_graph l start_lbl dest_lbl def351 adds_graph rtl_params1 globals l start_lbl dest_lbl def 353 352  Optrofint r ⇒ 354 translate_move destrs srcrs start_lbl dest_lbl def353 translate_move globals destrs srcrs start_lbl dest_lbl def 355 354  Ointofptr r ⇒ 356 translate_move destrs srcrs start_lbl dest_lbl def355 translate_move globals destrs srcrs start_lbl dest_lbl def 357 356  Oid ⇒ 358 translate_move destrs srcrs start_lbl dest_lbl def357 translate_move globals destrs srcrs start_lbl dest_lbl def 359 358  _ ⇒ ? (* float operations implemented in runtime *) 360 359 ]. … … 362 361 qed. 363 362 364 definition translate_op ≝ 363 definition translate_op: ∀globals. ? → list register → list register → list register → 364 label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 365 λglobals: list ident. 365 366 λop. 366 λdestrs .367 λsrcrs1 .368 λsrcrs2 .369 λstart_lbl .370 λdest_lbl .371 λdef .367 λdestrs: list register. 368 λsrcrs1: list register. 369 λsrcrs2: list register. 370 λstart_lbl: label. 371 λdest_lbl: label. 372 λdef: rtl_internal_function globals. 372 373 match reduce_strong register register srcrs1 srcrs2 with 373 374 [ dp reduced first_reduced_proof ⇒ … … 386 387 let destrs_rest ≝ \snd (\fst reduced) in 387 388 let srcrs_cted ≝ \fst (\snd reduced) in 388 let 〈def, tmpr〉 ≝ fresh_reg def in389 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 389 390 let insts_init ≝ [ 390 rtl_st_clear_carry start_lbl;391 rtl_st_int tmpr (zero ?) start_lbl391 sequential … (CLEAR_CARRY …); 392 sequential … (INT rtl_params_ globals tmpr (zero …)) 392 393 ] in 393 let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lblin394 let insts_add ≝ map3 …f_add destrs_common srcrsl_common srcrsr_common ? ? in395 let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lblin396 let insts_add_cted ≝ map2 ? ? ?f_add_cted destrs_cted srcrs_cted ? in397 let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lblin394 let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in 395 let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in 396 let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in 397 let insts_add_cted ≝ map2 … f_add_cted destrs_cted srcrs_cted ? in 398 let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in 398 399 let insts_rest ≝ map … f_rest destrs_rest in 399 adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def400 adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def 400 401 ] 401 402 ] … … 403 404 [1: @third_reduced_proof 404 405 3: @first_reduced_proof 405 *: cases daemon (* TODO*)406 *: cases daemon (* XXX: some of these look like they may be false *) 406 407 ] 407 408 qed. 408 409 409 410 let rec translate_mul1 410 (dummy: register) (tmpr: register) (destrs: list register) 411 (srcrs1: list register) (srcr2: register) (start_lbl: label) 412 on srcrs1 ≝ 411 (globals: list ident) (dummy: register) (tmpr: register) 412 (destrs: list register) (srcrs1: list register) (srcr2: register) 413 (start_lbl: label) 414 on srcrs1 ≝ 413 415 match destrs with 414 [ nil ⇒ adds_graph [ rtl_st_skip start_lbl] start_lbl416 [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl 415 417  cons destr tl ⇒ 416 418 match tl with … … 418 420 match srcrs1 with 419 421 [ nil ⇒ 420 adds_graph [421 rtl_st_int tmpr (zero ?) start_lbl;422 rtl_st_op2 Addc destr destr tmpr start_lbl422 adds_graph rtl_params1 globals [ 423 sequential … (INT rtl_params_ globals tmpr (zero …)); 424 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) 423 425 ] start_lbl 424 426  cons srcr1 tl' ⇒ 425 adds_graph [426 rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;427 rtl_st_op2 Addc destr destr tmpr start_lbl427 adds_graph rtl_params1 globals [ 428 sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1); 429 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) 428 430 ] start_lbl 429 431 ] … … 431 433 match srcrs1 with 432 434 [ nil ⇒ 433 add_translates [434 adds_graph [435 rtl_st_int tmpr (zero ?) start_lbl;436 rtl_st_op2 Addc destr destr tmpr start_lbl;437 rtl_st_op2 Addc destr2 tmpr tmpr start_lbl435 add_translates rtl_params1 globals [ 436 adds_graph rtl_params1 globals [ 437 sequential … (INT rtl_params_ globals tmpr (zero …)); 438 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr); 439 sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr) 438 440 ]; 439 translate_cst (Ointconst I8 (zero ?)) destrs441 translate_cst globals (Ointconst I8 (zero …)) destrs 440 442 ] start_lbl 441 443  cons srcr1 srcrs1 ⇒ 442 444 match destrs with 443 445 [ nil ⇒ 444 add_translates [445 adds_graph [446 rtl_st_int tmpr (zero ?) start_lbl;447 rtl_st_op2 Addc destr destr tmpr start_lbl;448 rtl_st_op2 Addc destr2 tmpr tmpr start_lbl446 add_translates rtl_params1 globals [ 447 adds_graph rtl_params1 globals [ 448 sequential … (INT rtl_params_ globals tmpr (zero …)); 449 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr); 450 sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr) 449 451 ]; 450 translate_cst (Ointconst I8 (zero ?)) destrs452 translate_cst globals (Ointconst I8 (zero ?)) destrs 451 453 ] start_lbl 452 454  cons destr2 destrs ⇒ 453 add_translates [454 adds_graph [455 rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;456 rtl_st_op2 Addc destr destr tmpr start_lbl455 add_translates rtl_params1 globals [ 456 adds_graph rtl_params1 globals [ 457 sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1); 458 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) 457 459 ]; 458 translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2460 translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2 459 461 ] start_lbl 460 462 ] … … 464 466 465 467 definition translate_muli ≝ 468 λglobals: list ident. 466 469 λdummy: register. 467 470 λtmpr: register. … … 474 477 λtranslates: list ?. 475 478 λsrcr2i: register. 476 let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ?tmp_destrs i i_prf in479 let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in 477 480 let tmp_destrs2' ≝ 478 481 match tmp_destrs2 with 479 482 [ nil ⇒ [ ] 480 483  cons tmp_destr2 tmp_destrs2 ⇒ [ 481 adds_graph [482 rtl_st_clear_carry dummy_lbl;483 rtl_st_int tmp_destr2 (zero ?) dummy_lbl484 adds_graph rtl_params1 globals [ 485 sequential rtl_params_ globals (CLEAR_CARRY …); 486 sequential … (INT rtl_params_ globals tmp_destr2 (zero …)) 484 487 ]; 485 translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;486 translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;487 adds_graph [488 rtl_st_clear_carry dummy_lbl488 translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i; 489 translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1; 490 adds_graph rtl_params1 globals [ 491 sequential rtl_params_ globals (CLEAR_CARRY …) 489 492 ]; 490 translate_op Addc destrs destrs tmp_destrs493 translate_op globals Addc destrs destrs tmp_destrs 491 494 ] 492 495 ] … … 495 498 496 499 axiom translate_mul: 500 ∀globals: list ident. 497 501 ∀destrs: list register. 498 502 ∀srcrs1: list register. … … 500 504 ∀start_lbl: label. 501 505 ∀dest_lbl: label. 502 ∀def: rtl_internal_function .503 rtl_internal_function .506 ∀def: rtl_internal_function globals. 507 rtl_internal_function globals. 504 508 505 509 (*
Note: See TracChangeset
for help on using the changeset viewer.