Changeset 3095 for driver/extracted

Timestamp:

Apr 4, 2013, 9:53:30 PM (8 years ago)

Author:

sacerdot

Message:

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

File:

• driver/extracted/policyStep.ml (modified) (5 diffs)

driver/extracted/policyStep.ml

@@ -95 +95 @@
      Types.pi1
        (FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ acc ->
+         let prefixlen = List.length prefix in
+         let bvprefixlen =
+           Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+             (Nat.S (Nat.S Nat.O)))))))))))))))) prefixlen
+         in
+         let bvSprefixlen =
+           Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+             (Nat.S Nat.O)))))))))))))))) bvprefixlen
+         in
          (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } =
             Types.pi1 acc
@@ -105 +116 @@
            | ASM.Instruction i ->
              PolicyFront.jump_expansion_step_instruction (Types.pi1 labels)
-               (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) i
+               (Types.pi1 old_sigma) inc_pc_sigma prefixlen i
            | ASM.Comment x0 -> Types.None
            | ASM.Cost x0 -> Types.None
@@ -111 +122 @@
              Types.Some
                (PolicyFront.select_jump_length (Types.pi1 labels)
-                 (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) j)
+                 (Types.pi1 old_sigma) inc_pc_sigma prefixlen j)
            | ASM.Jnz (x0, x1, x2) -> Types.None
            | ASM.Call c ->
              Types.Some
                (PolicyFront.select_call_length (Types.pi1 labels)
-                 (Types.pi1 old_sigma) inc_pc_sigma (List.length prefix) c)
+                 (Types.pi1 old_sigma) inc_pc_sigma prefixlen c)
            | ASM.Mov (x0, x1, x2) -> Types.None
          in
@@ -123 +134 @@
            (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-             (Nat.S Nat.O))))))))))))))))
-             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-               (Nat.S (Nat.S Nat.O)))))))))))))))) (List.length prefix))
+             (Nat.S Nat.O)))))))))))))))) bvprefixlen
              (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
              Assembly.Short_jump }).Types.snd
@@ -152 +160 @@
            (BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-             (Nat.S Nat.O))))))))))))))))
-             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-               (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
-               (List.length prefix))) (Types.pi1 old_sigma).Types.snd
-             { Types.fst = Nat.O; Types.snd = Assembly.Short_jump }).Types.snd
+             (Nat.S Nat.O)))))))))))))))) bvSprefixlen
+             (Types.pi1 old_sigma).Types.snd { Types.fst = Nat.O; Types.snd =
+             Assembly.Short_jump }).Types.snd
          in
          let updated_sigma =
            BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-             (Nat.S Nat.O))))))))))))))))
-             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-               (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S
-               (List.length prefix))) { Types.fst = (Nat.plus inc_pc isize);
-             Types.snd = old_Slength }
+             (Nat.S Nat.O)))))))))))))))) bvSprefixlen { Types.fst =
+             (Nat.plus inc_pc isize); Types.snd = old_Slength }
              (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-               (Nat.S Nat.O))))))))))))))))
-               (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S
-                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
-                 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
-                 (List.length prefix)) { Types.fst = inc_pc; Types.snd =
-               new_length } inc_sigma)
+               (Nat.S Nat.O)))))))))))))))) bvprefixlen { Types.fst = inc_pc;
+               Types.snd = new_length } inc_sigma)
          in
          { Types.fst = new_added; Types.snd = { Types.fst =