Changeset 3095


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

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

Files:
2 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 =
  • src/ASM/PolicyStep.ma

    r3039 r3095  
    11541154    program
    11551155    (λprefix.λx.λtl.λprf.λacc.
     1156      let prefixlen ≝ |prefix| in
     1157      let bvprefixlen ≝ bitvector_of_nat ? prefixlen in
     1158      let bvSprefixlen ≝ increment … bvprefixlen in
    11561159      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
    11571160      let 〈label,instr〉 ≝ x in
     
    11661169       *)
    11671170      let add_instr ≝ match instr with
    1168       [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma (|prefix|) j)
    1169       | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    1170       | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma (|prefix|) i
     1171      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma prefixlen j)
     1172      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma prefixlen c)
     1173      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma prefixlen i
    11711174      | _             ⇒ None ?
    11721175      ] in
    11731176      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
    11741177      let old_length ≝
    1175         \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
     1178        \snd (bvt_lookup … bvprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
    11761179      let old_size ≝ instruction_size_jmplen old_length instr in
    11771180      let 〈new_length, isize〉 ≝ match add_instr with
     
    11841187      ] in
    11851188      let old_Slength ≝
    1186         \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
     1189        \snd (bvt_lookup … bvSprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
    11871190      let updated_sigma ≝
    11881191        (* we add the new PC to the next position and the new jump length to this one *)
    1189         bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
    1190         (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
     1192        bvt_insert … bvSprefixlen 〈inc_pc + isize, old_Slength〉
     1193        (bvt_insert … bvprefixlen 〈inc_pc, new_length〉 inc_sigma) in
    11911194      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
    11921195    ) 〈0, 〈0,
     
    12471250  | @not_lt_to_le @ltb_false_to_not_lt @p1
    12481251  ]
    1249 |4: lapply (pi2 ?? acc) >p -acc inversion inc_pc_sigma
     1252|4:
     1253  >(?:bvSprefixlen = bitvector_of_nat … (S prefixlen))
     1254  [2: normalize nodelta >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat %]
     1255  lapply (pi2 ?? acc) >p -acc inversion inc_pc_sigma
    12501256  #inc_pc #inc_sigma #Hips normalize nodelta
    1251   inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
     1257  inversion (bvt_lookup … bvprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    12521258  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
    12531259  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.