Changeset 1973
 Timestamp:
 May 21, 2012, 4:57:23 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1965 r1973 434 434 let 〈label,instr〉 ≝ x in 435 435 let isize ≝ instruction_size_jmplen short_jump instr in 436 〈pc + isize, 437 match instr with 438 [ Instruction i ⇒ match i with 439 [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 440  JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 441  JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 442  JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 443  JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 444  JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 445  JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 446  CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 447  DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 448  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 449 ] 450  Call c ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 451  Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 452  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 453 ]〉 436 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma〉 454 437 ) 〈0, Stub ? ?〉 in 455 438 if geb (\fst final_policy) 2^16 then … … 464 447 #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 465 448 cases (le_to_or_lt_eq … Hi) Hi #Hi 466 cases p p #p cases p p #pc #p #Hp cases x x #l #pi cases pi 467 [1,7: #id cases id normalize nodelta 468 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 469 [1,2,3,6,7,24,25: #x #y 470 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_opt_insert_miss 471 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 472 @bitvector_of_nat_abs 473 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 474 @Hi2 475 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 476 @(transitive_lt … Hi2) @le_S_to_le @Hi 477 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 478 @sym_neq @lt_to_not_eq @le_S_to_le @Hi 479 ] 480 ] 481 @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 482 38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74: 483 [1,2,3,6,7,24,25: #x #y 484 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 485 >lookup_opt_insert_miss 486 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 487 @bitvector_of_nat_abs 488 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 489 @Hi2 490 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 491 @(transitive_lt … Hi2) <Hi @le_n 492 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 493 @sym_neq @lt_to_not_eq <Hi @le_n 494 ] 495 ] 496 <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 497 >Hi @Hi2 498 9,10,11,12,13,14,15,16,17: 499 [1,2,6,7: #x 3,4,5,8,9: #x #id] >lookup_opt_insert_miss 500 [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 501 [1,4,7,10,13,16,19,22,25: @Hi2 502 2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) @le_S_to_le @Hi 503 3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq @le_S_to_le @Hi 504 ] 505 1,3,5,7,9,11,13,15,17: 506 @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 507 ] 508 46,47,48,49,50,51,52,53,54: 509 [1,2,6,7: #x 3,4,5,8,9: #x #id] >lookup_opt_insert_miss 510 [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 511 [1,4,7,10,13,16,19,22,25: @Hi2 512 2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) <Hi @le_n 513 3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq <Hi @le_n 514 ] 515 1,3,5,7,9,11,13,15,17: 516 @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) <Hi @le_S @le_n 517 ] 518 ] 519 2,3,6,8,9,12: [3,6: #w] #z >lookup_opt_insert_miss 520 [2,4,6,8,10,12: @bitvector_of_nat_abs 521 [1,4,7,10,13,16: @Hi2 522 2,8,11: @(transitive_lt … Hi2) @le_S_to_le @Hi 523 5,14,17: @(transitive_lt … Hi2) <Hi @le_n 524 3,9,12: @sym_neq @lt_to_not_eq @le_S_to_le @Hi 525 6,15,18: <Hi @sym_neq @lt_to_not_eq @le_n 526 ] 527 ] 528 [1,3,4: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 529 2,5,6: 530 <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 531 >Hi @Hi2 532 ] 533 4,5,10,11: #dst normalize nodelta >lookup_opt_insert_miss 534 [2,4,6,8: @bitvector_of_nat_abs 535 [1,4,7,10: @Hi2 536 2,5: @(transitive_lt … Hi2) @le_S_to_le @Hi 537 8,11: @(transitive_lt … Hi2) <Hi @le_n 538 3,6: @sym_neq @lt_to_not_eq @le_S_to_le @Hi 539 9,12: @sym_neq @lt_to_not_eq <Hi @le_n 540 ] 541 1,3: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 542 5,7: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) <Hi @le_S @le_n 449 cases p p #p cases p p #pc #p #Hp cases x x #l #pi 450 [ >lookup_opt_insert_miss 451 [ @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 452  @bitvector_of_nat_abs 453 [ @Hi2 454  @(transitive_lt … Hi2) @le_S_to_le @Hi 455  @sym_neq @lt_to_not_eq @le_S_to_le @Hi 543 456 ] 544 457 ] 545  (* jump_not_in_policy *) #i >append_length <commutative_plus 546 #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 547 [ cases p p #p cases p p #pc #sigma #Hp cases x #l #ins cases ins 548 [ #pi cases pi normalize nodelta 549 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 550 [1,2,3,6,7,24,25: #x #y 551 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_insert_miss 552 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 553 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 554 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 555 @bitvector_of_nat_abs 556 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 557 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 558 @le_plus_a @Hi 559 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 560 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 561 @le_plus_n_r 562 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 563 @lt_to_not_eq @Hi 564 ] 565 ] 566 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] >lookup_insert_miss 567 [1,3,5,7,9,11,13,15,17: 568 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 569 2,4,6,8,10,12,14,16,18: 570 @bitvector_of_nat_abs 571 [1,4,7,10,13,16,19,22,25: 572 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 573 @le_plus_a @Hi 574 2,5,8,11,14,17,20,23,26: 575 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 576 @le_plus_n_r 577 3,6,9,12,15,18,21,24,27: 578 @lt_to_not_eq @Hi 579 ] 458  >lookup_opt_insert_miss 459 [ <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 460 >Hi @Hi2 461  @bitvector_of_nat_abs 462 [ @Hi2 463  @(transitive_lt … Hi2) <Hi @le_n 464  @sym_neq @lt_to_not_eq <Hi @le_n 580 465 ] 581 466 ] 582 2,3,4,5,6: #x [5: #y] >lookup_insert_miss583 [1,3,5,7,9:584 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)585 2,4,6,8,10:586 @bitvector_of_nat_abs587 [1,4,7,10,13:588 467 ] 468  (* jump_not_in_policy *) #i >append_length <commutative_plus 469 #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 470 [ cases p p #p cases p p #pc #sigma #Hp cases x #l #ins >lookup_insert_miss 471 [ >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 472  @bitvector_of_nat_abs 473 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 589 474 @le_plus_a @Hi 590 2,5,8,11,14: 591 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 475  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 592 476 @le_plus_n_r 593 3,6,9,12,15: 594 @lt_to_not_eq @Hi 477  @lt_to_not_eq @Hi 595 478 ] 596 479 ] 597 ] 598  >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); 599 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #ins cases ins 600 normalize nodelta 601 [2,3,6: #x [3: #y] >lookup_insert_hit #_ / by / 602 4,5: #x #H @⊥ cases H #H2 @H2 / by I/ 603 1: #pi cases pi 604 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 605 [1,2,3,6,7,24,25: #x #y 606 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 607 #_ >lookup_insert_hit / by / 608 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 609 #H @⊥ cases H #H2 @H2 / by I/ 610 ] 611 ] 612 ] 613 ] 614  (* policy_compact *) cases daemon (*XXX*) 615 ] 616  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; 617 cases p p #p cases p p #pc #sigma #Hp cases x 618 #lbl #instr cases instr normalize nodelta 619 [ #pi cases pi normalize nodelta 620 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 621 [1,2,3,6,7,24,25: #x #y 622 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 623 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 624 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 625 >lookup_insert_miss 626 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 627 @((proj2 ?? Hp) i Hi) 628 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 629 @bitvector_of_nat_abs 630 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 631 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 632 @le_plus_a @Hi 633 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 634 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 635 @le_plus_n_r 636 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 637 @lt_to_not_eq @Hi 638 ] 639 ] 640 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 641 >Hi >lookup_insert_hit @refl 642 ] 643 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 644 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 645 [1,3,5,7,9,11,13,15,17: >lookup_insert_miss 646 [1,3,5,7,9,11,13,15,17: @((proj2 ?? Hp) i Hi) 647 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 648 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 649 >append_length >commutative_plus @le_plus_a @Hi 650 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 651 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 652 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi 653 ] 654 ] 655 2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit @refl 656 ] 657 ] 658 2,3,4,5,6: #x [5: #y] cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 659 [1,3,5,7,9: >lookup_insert_miss 660 [1,3,5,7,9: @((proj2 ?? Hp) i Hi) 661 2,4,6,8,10: @bitvector_of_nat_abs 662 [1,4,7,10,13: @(transitive_lt … (pi2 ?? program)) >prf >append_length 663 >commutative_plus @le_plus_a @Hi 664 2,5,8,11,14: @(transitive_lt … (pi2 ?? program)) >prf >append_length 665 <plus_n_Sm @le_S_S @le_plus_n_r 666 3,6,9,12,15: @lt_to_not_eq @Hi 480  >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); 481 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #ins 482 >lookup_insert_hit #_ / by / 483 ] 484 ] 485  (* policy_compact *) cases daemon 486 ] 487  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; 488 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 489 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 490 [ >lookup_insert_miss 491 [ @((proj2 ?? Hp) i Hi) 492  @bitvector_of_nat_abs 493 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 494 @le_plus_a @Hi 495  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 496 @le_plus_n_r 497  @lt_to_not_eq @Hi 667 498 ] 668 499 ] 669 2,4,6,8,10: >Hi >lookup_insert_hit @refl 670 ] 671 ] 672 ] 500  >Hi >lookup_insert_hit @refl 501 ] 502 ] 673 503  @conj [ @conj [ @conj 674 504 [ #i #_ #Hi2 / by refl/ 675  #i #H @⊥ @(absurd … H) @not_le_Sn_O 676 ] 677  #i #H @⊥ @(absurd … H) @not_le_Sn_O 678 ] 679  #i #H @⊥ @(absurd … H) @not_le_Sn_O 680 ] 505 ]]] 506 #i #H @⊥ @(absurd … H) @not_le_Sn_O 681 507 ] 682 508 qed. … … 690 516 \snd pc1 = \snd pc2). 691 517 692 (*definition nec_plus_ultra ≝ 693 λprogram:list labelled_instruction.λp:ppc_pc_mapjump_expansion_policy. 694 ¬(∀i.i < program → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). *) 518 definition nec_plus_ultra ≝ 519 λprogram:list labelled_instruction.λp:ppc_pc_map. 520 ¬(∀i.i < program → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) → 521 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump). 695 522 696 523 (*include alias "common/Identifiers.ma".*) … … 809 636 ] 810 637 ] 811 qed. 638 qed. 812 639 813 640 lemma etblorp: ∀a,b,i.is_jump i → … … 885 712 let 〈no_ch,y〉 ≝ x in 886 713 match y with 887 [ None ⇒ (* nec_plus_ultra program old_policy *) True714 [ None ⇒ nec_plus_ultra program old_policy 888 715  Some p ⇒ And (And (And (And (And (out_of_program_none program p) 889 716 (jump_not_in_policy program p)) … … 940 767 else 941 768 〈eqb final_added 0, Some ? final_policy〉. 942 [ / by I/769 [ normalize nodelta cases daemon (* XXX nec_plus_ultra *) 943 770  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 944 771 >H2 in H; normalize nodelta H2 x #H @conj … … 1702 1529  #Hfull cases (jump_expansion_step program (create_label_map program) «Fp,?») in ⊢ (???% → %); 1703 1530 #x cases x x #Gch #Gpol cases Gpol normalize nodelta 1704 [ cases daemon (* XXX will need some form of nec_plus_ultra here 1705 #H #EQ2 @⊥ @(absurd ?? H) @Hfull *) 1531 [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull 1706 1532  #Gp #HGp #EQ2 cases Fch 1707 1533 [ normalize nodelta #i #Hi
Note: See TracChangeset
for help on using the changeset viewer.