Changeset 3095 for driver/extracted


Ignore:
Timestamp:
Apr 4, 2013, 9:53:30 PM (7 years ago)
Author:
sacerdot
Message:

Some performance improvement: an heavy computation was done again and again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/policyStep.ml

    r3043 r3095  
    9595     Types.pi1
    9696       (FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ acc ->
     97         let prefixlen = List.length prefix in
     98         let bvprefixlen =
     99           Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     100             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     101             (Nat.S (Nat.S Nat.O)))))))))))))))) prefixlen
     102         in
     103         let bvSprefixlen =
     104           Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     105             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     106             (Nat.S Nat.O)))))))))))))))) bvprefixlen
     107         in
    97108         (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } =
    98109            Types.pi1 acc
     
    105116           | ASM.Instruction i ->
    106117             PolicyFront.jump_expansion_step_instruction (Types.pi1 labels)
    107                (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) i
     118               (Types.pi1 old_sigma) inc_pc_sigma prefixlen i
    108119           | ASM.Comment x0 -> Types.None
    109120           | ASM.Cost x0 -> Types.None
     
    111122             Types.Some
    112123               (PolicyFront.select_jump_length (Types.pi1 labels)
    113                  (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) j)
     124                 (Types.pi1 old_sigma) inc_pc_sigma prefixlen j)
    114125           | ASM.Jnz (x0, x1, x2) -> Types.None
    115126           | ASM.Call c ->
    116127             Types.Some
    117128               (PolicyFront.select_call_length (Types.pi1 labels)
    118                  (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) c)
     129                 (Types.pi1 old_sigma) inc_pc_sigma prefixlen c)
    119130           | ASM.Mov (x0, x1, x2) -> Types.None
    120131         in
     
    123134           (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    124135             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    125              (Nat.S Nat.O))))))))))))))))
    126              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    127                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    128                (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length prefix))
     136             (Nat.S Nat.O)))))))))))))))) bvprefixlen
    129137             (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
    130138             Assembly.Short_jump }).Types.snd
     
    152160           (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    153161             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    154              (Nat.S Nat.O))))))))))))))))
    155              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    156                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    157                (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
    158                (List.length prefix))) (Types.pi1 old_sigma).Types.snd
    159              { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd
     162             (Nat.S Nat.O)))))))))))))))) bvSprefixlen
     163             (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
     164             Assembly.Short_jump }).Types.snd
    160165         in
    161166         let updated_sigma =
    162167           BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    163168             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    164              (Nat.S Nat.O))))))))))))))))
    165              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    166                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    167                (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
    168                (List.length prefix))) { Types.fst = (Nat.plus inc_pc isize);
    169              Types.snd = old_Slength }
     169             (Nat.S Nat.O)))))))))))))))) bvSprefixlen { Types.fst =
     170             (Nat.plus inc_pc isize); Types.snd = old_Slength }
    170171             (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    171172               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    172                (Nat.S Nat.O))))))))))))))))
    173                (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
    174                  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    175                  (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
    176                  (List.length prefix)) { Types.fst = inc_pc; Types.snd =
    177                new_length } inc_sigma)
     173               (Nat.S Nat.O)))))))))))))))) bvprefixlen { Types.fst = inc_pc;
     174               Types.snd = new_length } inc_sigma)
    178175         in
    179176         { Types.fst = new_added; Types.snd = { Types.fst =
Note: See TracChangeset for help on using the changeset viewer.