Changeset 3098 for src


Ignore:
Timestamp:
Apr 6, 2013, 11:44:00 AM (7 years ago)
Author:
sacerdot
Message:

Performance improvement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r3078 r3098  
    409409    ] ≝
    410410  λ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
    413416    (not_jump_default prefix policy)
    414417    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
     
    416419    (sigma_compact_unsafe prefix labels policy))
    417420    (∀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〉)))
    419422  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
    422426   let 〈label,instr〉 ≝ x in
    423427   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
    427432    None ?
    428433  else
    429     Some ? (pi1 ?? final_policy).
     434    Some ? final_policy.
    430435[ / 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
    436444    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    437445    [ >lookup_insert_miss
     
    442450        | @Hi
    443451        ]
    444       | @bitvector_of_nat_abs
     452      | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat
     453        @bitvector_of_nat_abs
    445454        [ @(transitive_lt ??? Hi) @le_S_to_le]
    446455        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
     
    453462        elim ((proj2 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl
    454463        >(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
    456466        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r
    457467        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S
     
    462472    ]
    463473  | (* 0 ↦ 0 *)
    464     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    465474    >lookup_insert_miss
    466475    [ (* USE[pass]: 0 ↦ 0 *)
    467476      @(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
    469479      [ @ltb_true_to_lt / by refl/
    470480      | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm
     
    475485  ]
    476486  | (* 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   
    479491  ]
    480492  | (* 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 nodelta
    482493    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    483494    [ >lookup_opt_insert_miss
     
    501512      ]
    502513      [2: lapply (le_S_to_le … Hi) -Hi #Hi]
     514      >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat     
    503515      @bitvector_of_nat_abs
    504516      [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus
     
    509521      ]
    510522    | >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
    512526        (* USE: everything is short, fst p = pc *)
    513527        elim ((proj2 ?? Hp) (|prefix|) (le_n ?)) #pc #Hl
     
    517531        | @le_n
    518532        ]
    519       | @bitvector_of_nat_abs
     533      | >increment_zero_bitvector_of_nat_1 >EQacc <add_bitvector_of_nat
     534        @bitvector_of_nat_abs
    520535        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus
    521536          @le_plus_a @le_n
     
    528543  ]
    529544  | (* 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 nodelta
    531545    cases (le_to_or_lt_eq … Hi) -Hi #Hi
    532546    [ >lookup_opt_insert_miss
    533547      [ (* USE[pass]: everything is short *)
    534548        @((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
    536552        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    537553          >commutative_plus @le_plus_a @le_S_S_to_le @Hi
     
    541557        ]
    542558      ]
    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))
    544562      @refl
    545563    ]
    546   ]
    547 | @conj [ @conj [ @conj [ @conj
     564  ]]
     565| normalize nodelta % % [ @conj [ @conj [ @conj
    548566  [ #i cases i
    549567    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
Note: See TracChangeset for help on using the changeset viewer.