Changeset 3097 for driver


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

Performance improvement in policy computation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/policyStep.ml

    r3095 r3097  
    9292    PolicyFront.ppc_pc_map Types.option) Types.prod Types.sig0 **)
    9393let jump_expansion_step program labels old_sigma =
    94   (let { Types.fst = final_added; Types.snd = final_policy } =
     94  (let { Types.fst = ignore; Types.snd = res } =
    9595     Types.pi1
    96        (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
     96       (FoldStuff.foldl_strong (Types.pi1 program)
     97         (fun prefix x tl _ prefixlens_acc ->
     98         (let { Types.fst = prefixlens; Types.snd = acc } =
     99            Types.pi1 prefixlens_acc
     100          in
     101         (fun _ ->
     102         (let { Types.fst = prefixlen; Types.snd = bvprefixlen } = prefixlens
     103          in
     104         (fun _ ->
    103105         let bvSprefixlen =
    104106           Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    106108             (Nat.S Nat.O)))))))))))))))) bvprefixlen
    107109         in
    108          (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } =
    109             Types.pi1 acc
    110           in
     110         (let { Types.fst = inc_added; Types.snd = inc_pc_sigma } = acc in
    111111         (fun _ ->
    112112         (let { Types.fst = label; Types.snd = instr } = x in
     
    174174               Types.snd = new_length } inc_sigma)
    175175         in
     176         { Types.fst = { Types.fst = (Nat.S prefixlen); Types.snd =
     177         (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     178           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     179           (Nat.S Nat.O)))))))))))))))) bvprefixlen) }; Types.snd =
    176180         { Types.fst = new_added; Types.snd = { Types.fst =
    177          (Nat.plus inc_pc isize); Types.snd = updated_sigma } })) __)) __)
    178          { Types.fst = Nat.O; Types.snd = { Types.fst = Nat.O; Types.snd =
     181         (Nat.plus inc_pc isize); Types.snd = updated_sigma } } })) __)) __))
     182           __)) __) { Types.fst = { Types.fst = Nat.O; Types.snd =
     183         (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     184           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     185           Nat.O))))))))))))))))) }; Types.snd = { Types.fst = Nat.O;
     186         Types.snd = { Types.fst = Nat.O; Types.snd =
    179187         (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    180188           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    193201             Assembly.Short_jump }).Types.snd } (BitVectorTrie.Stub (Nat.S
    194202           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    195            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } })
     203           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))) } } })
    196204   in
     205  (fun _ ->
     206  (let { Types.fst = final_added; Types.snd = final_policy } = res in
    197207  (fun _ ->
    198208  (match Util.gtb final_policy.Types.fst
     
    205215   | Bool.False ->
    206216     (fun _ -> { Types.fst = (Nat.eqb final_added Nat.O); Types.snd =
    207        (Types.Some final_policy) })) __)) __
    208 
     217       (Types.Some final_policy) })) __)) __)) __
     218
Note: See TracChangeset for help on using the changeset viewer.