Changeset 3098
 Timestamp:
 Apr 6, 2013, 11:44:00 AM (7 years ago)
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

driver/extracted/policyFront.ml
r3043 r3098 657 657 ppc_pc_map Types.option Types.sig0 **) 658 658 let jump_expansion_start program labels = 659 let final_policy = 660 FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ p > 661 let { Types.fst = pc; Types.snd = sigma } = Types.pi1 p in 662 let { Types.fst = label; Types.snd = instr } = x in 663 let isize = instruction_size_jmplen Assembly.Short_jump instr in 664 { Types.fst = (Nat.plus pc isize); Types.snd = 665 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 666 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 667 Nat.O)))))))))))))))) 668 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 669 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 670 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix))) 671 { Types.fst = (Nat.plus pc isize); Types.snd = Assembly.Short_jump } 672 sigma) }) { Types.fst = Nat.O; Types.snd = 673 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 674 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 675 Nat.O)))))))))))))))) 676 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 677 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 678 (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O; 679 Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S (Nat.S 680 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 681 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } 682 in 683 (match Util.gtb (Types.pi1 final_policy).Types.fst 659 (let { Types.fst = ignore; Types.snd = final_policy } = 660 Types.pi1 661 (FoldStuff.foldl_strong (Types.pi1 program) 662 (fun prefix x tl _ acc_pol > 663 (let { Types.fst = acc; Types.snd = p } = Types.pi1 acc_pol in 664 (fun _ > 665 let { Types.fst = pc; Types.snd = sigma } = p in 666 let { Types.fst = label; Types.snd = instr } = x in 667 let isize = instruction_size_jmplen Assembly.Short_jump instr in 668 let sacc = 669 Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 670 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 671 (Nat.S Nat.O)))))))))))))))) acc 672 in 673 { Types.fst = sacc; Types.snd = { Types.fst = (Nat.plus pc isize); 674 Types.snd = 675 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 676 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 677 (Nat.S Nat.O)))))))))))))))) sacc { Types.fst = 678 (Nat.plus pc isize); Types.snd = Assembly.Short_jump } sigma) } })) 679 __) { Types.fst = 680 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 681 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 682 Nat.O))))))))))))))))); Types.snd = { Types.fst = Nat.O; 683 Types.snd = 684 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 685 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 686 (Nat.S Nat.O)))))))))))))))) 687 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 688 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 689 (Nat.S (Nat.S Nat.O)))))))))))))))) Nat.O) { Types.fst = Nat.O; 690 Types.snd = Assembly.Short_jump } (BitVectorTrie.Stub (Nat.S 691 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 692 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } }) 693 in 694 (fun _ > 695 (match Util.gtb final_policy.Types.fst 684 696 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 685 697 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 686 698 (Nat.S (Nat.S Nat.O))))))))))))))))) with 687 699  Bool.True > (fun _ > Types.None) 688  Bool.False > (fun _ > Types.Some (Types.pi1 final_policy))) __689 700  Bool.False > (fun _ > Types.Some final_policy)) __)) __ 701 
src/ASM/PolicyFront.ma
r3078 r3098 409 409 ] ≝ 410 410 λprogram.λlabels. 411 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 412 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And 411 let 〈ignore,final_policy〉 ≝ foldl_strong (option Identifier × pseudo_instruction) 412 (λprefix.Σacc_policy:Word × ppc_pc_map. 413 let 〈acc,policy〉 ≝ acc_policy in 414 And (acc = bitvector_of_nat … (prefix)) 415 (And (And (And (And 413 416 (not_jump_default prefix policy) 414 417 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) … … 416 419 (sigma_compact_unsafe prefix labels policy)) 417 420 (∀i.i ≤ prefix → ∃pc. 418 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) 421 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))) 419 422 program 420 (λprefix.λx.λtl.λprf.λp. 421 let 〈pc,sigma〉 ≝ pi1 ?? p in 423 (λprefix.λx.λtl.λprf.λacc_pol. 424 let 〈acc,p〉 ≝ pi1 ?? acc_pol in 425 let 〈pc,sigma〉 ≝ p in 422 426 let 〈label,instr〉 ≝ x in 423 427 let isize ≝ instruction_size_jmplen short_jump instr in 424 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (prefix))) 〈pc+isize,short_jump〉 sigma〉 425 ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in 426 if gtb (\fst (pi1 ?? final_policy)) 2^16 then 428 let Sacc ≝ increment … acc in 429 〈Sacc,〈pc + isize, bvt_insert … Sacc 〈pc+isize,short_jump〉 sigma〉〉 430 ) 〈zero ?,〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉〉 in 431 if gtb (\fst final_policy) 2^16 then 427 432 None ? 428 433 else 429 Some ? (pi1 ?? final_policy).434 Some ? final_policy. 430 435 [ / by I/ 431  lapply p p cases final_policy final_policy #p #Hp #hg 432 @conj [ @Hp  @not_lt_to_le @ltb_false_to_not_lt @hg ] 433  @conj [ @conj [ @conj [ @conj 434 [ (* not_jump_default *) cases p p #p cases p p #pc #sigma #Hp 435 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi 436  cases (foldl_strong ?(λprefix.Σx.?)???) in p; #pi1 #IS #EQp1 >EQp1 in IS; * 437 #_ #X % try assumption @not_lt_to_le @ltb_false_to_not_lt @p1 438  cases p in p1; p #pc #sigma #p1 lapply (pi2 ?? acc_pol) >p1 acc_pol 439 normalize nodelta * #EQacc #Hp cases x in prf; #lbl #ins #prf normalize nodelta 440 % [ >EQacc >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat 441 >length_append >commutative_plus % 442  @conj [ @conj [ @conj [ @conj 443 [ (* not_jump_default *) #i >append_length <commutative_plus #Hi 436 444 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 437 445 [ >lookup_insert_miss … … 442 450  @Hi 443 451 ] 444  @bitvector_of_nat_abs 452  >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 453 @bitvector_of_nat_abs 445 454 [ @(transitive_lt ??? Hi) @le_S_to_le] 446 455 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length … … 453 462 elim ((proj2 ?? Hp) (prefix) (le_n (prefix))) #pc #Hl 454 463 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl 455  @bitvector_of_nat_abs 464  >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 465 @bitvector_of_nat_abs 456 466 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r 457 467  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S … … 462 472 ] 463 473  (* 0 ↦ 0 *) 464 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta465 474 >lookup_insert_miss 466 475 [ (* USE[pass]: 0 ↦ 0 *) 467 476 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 468  @bitvector_of_nat_abs 477  >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 478 @bitvector_of_nat_abs 469 479 [ @ltb_true_to_lt / by refl/ 470 480  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm … … 475 485 ] 476 486  (* fst p = pc *) 477 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 478 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 487 >append_length >(commutative_plus (prefix)) 488 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 489 >lookup_insert_hit @refl 490 479 491 ] 480 492  (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; 481 cases p p #p cases p p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta482 493 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 483 494 [ >lookup_opt_insert_miss … … 501 512 ] 502 513 [2: lapply (le_S_to_le … Hi) Hi #Hi] 514 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 503 515 @bitvector_of_nat_abs 504 516 [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus … … 509 521 ] 510 522  >lookup_opt_insert_miss 511 [ >Hi >lookup_opt_insert_hit normalize nodelta 523 [ >Hi 524 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 525 >lookup_opt_insert_hit normalize nodelta 512 526 (* USE: everything is short, fst p = pc *) 513 527 elim ((proj2 ?? Hp) (prefix) (le_n ?)) #pc #Hl … … 517 531  @le_n 518 532 ] 519  @bitvector_of_nat_abs 533  >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 534 @bitvector_of_nat_abs 520 535 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus 521 536 @le_plus_a @le_n … … 528 543 ] 529 544  (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi; 530 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta531 545 cases (le_to_or_lt_eq … Hi) Hi #Hi 532 546 [ >lookup_opt_insert_miss 533 547 [ (* USE[pass]: everything is short *) 534 548 @((proj2 ?? Hp) i (le_S_S_to_le … Hi)) 535  @bitvector_of_nat_abs 549  550 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 551 @bitvector_of_nat_abs 536 552 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 537 553 >commutative_plus @le_plus_a @le_S_S_to_le @Hi … … 541 557 ] 542 558 ] 543  >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr)) 559  >Hi 560 >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat 561 >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump ins)) 544 562 @refl 545 563 ] 546 ] 547  @conj[ @conj [ @conj [ @conj564 ]] 565  normalize nodelta % % [ @conj [ @conj [ @conj 548 566 [ #i cases i 549 567 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
Note: See TracChangeset
for help on using the changeset viewer.