Changeset 3098


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

Performance improvement.

Files:
2 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/policyFront.ml

    r3043 r3098  
    657657    ppc_pc_map Types.option Types.sig0 **)
    658658let 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
    684696           (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    685697             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    686698             (Nat.S (Nat.S Nat.O))))))))))))))))) with
    687699   | 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  
    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.