Changeset 3097


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

Performance improvement in policy computation.

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

    r3095 r3097  
    11371137    ≝
    11381138  λprogram.λlabels.λold_sigma.
    1139   let 〈final_added, final_policy〉 ≝
     1139  let 〈ignore,res〉 ≝
    11401140    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    1141     (λprefix.Σx:ℕ × ppc_pc_map.
     1141    (λprefix.Σxx:(ℕ × Word) × (ℕ × ppc_pc_map).
     1142      let 〈prefixlens,x〉 ≝ xx in
     1143      let 〈prefixlen,bvprefixlen〉 ≝ prefixlens in
    11421144      let 〈added,policy〉 ≝ x in
    1143       And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
     1145      And (And (prefixlen = |prefix|) (bvprefixlen = bitvector_of_nat … prefixlen))
     1146      (And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
    11441147      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    11451148      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
     
    11511154      (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
    11521155       \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
    1153       (sigma_safe prefix labels old_sigma policy))
     1156      (sigma_safe prefix labels old_sigma policy)))
    11541157    program
    1155     (λprefix.λx.λtl.λprf.λacc.
    1156       let prefixlen ≝ |prefix| in
    1157       let bvprefixlen ≝ bitvector_of_nat ? prefixlen in
    1158       let bvSprefixlen ≝ increment … bvprefixlen in 
    1159       let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
     1158    (λprefix.λx.λtl.λprf.λprefixlens_acc.
     1159      let 〈prefixlens,acc〉 ≝ (pi1 ?? prefixlens_acc) in
     1160      let 〈prefixlen,bvprefixlen〉 ≝ prefixlens in
     1161      let bvSprefixlen ≝ increment … bvprefixlen in
     1162      let 〈inc_added, inc_pc_sigma〉 ≝ acc in
    11601163      let 〈label,instr〉 ≝ x in
    11611164      (* Now, we must add the current ppc and its pc translation.
     
    11921195        bvt_insert … bvSprefixlen 〈inc_pc + isize, old_Slength〉
    11931196        (bvt_insert … bvprefixlen 〈inc_pc, new_length〉 inc_sigma) in
    1194       〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
    1195     ) 〈0, 〈0,
     1197      〈〈S prefixlen,increment … bvprefixlen〉,〈new_added, 〈plus inc_pc isize, updated_sigma〉〉〉
     1198    ) 〈〈0,zero 16〉,〈0, 〈0,
    11961199      bvt_insert …
    11971200        (bitvector_of_nat ? 0)
    11981201        〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
    1199         (Stub ??)〉〉
     1202        (Stub ??)〉〉
    12001203    ) in
     1204  let 〈final_added, final_policy〉 ≝ res in
    12011205    if gtb (\fst final_policy) 2^16 then
    12021206      〈eqb final_added 0, None ?〉
     
    12041208      〈eqb final_added 0, Some ? final_policy〉.
    12051209[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
    1206   #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
     1210  #x #H #Heq >Heq in H; normalize nodelta -Heq -x cases ignore #prefixlen #bvprefixlen
     1211  >p1 -res normalize nodelta * #EQprefixlens #Hind
    12071212  (* USE: inc_pc = fst of policy (from fold) *)
    1208   >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
     1213  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p2;
    12091214  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
    12101215  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
     
    12361241    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
    12371242  ]
    1238 | normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
    1239   >H2 in H; normalize nodelta -H2 -x #H @conj
    1240   [ @conj [ @conj
     1243| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?);
     1244  #x normalize nodelta #H #H2
     1245  >H2 in H; normalize nodelta -H2 -x cases ignore -ignore #prefixlen #bvprefixlen
     1246  normalize nodelta >p1 -p1 normalize nodelta * #EQprefixlens #H @conj
     1247  [ @conj [ @conj
    12411248  [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
    12421249     * jump_increase, sigma_compact_unsafe (from fold) *)
     
    12481255     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
    12491256  ]
    1250   | @not_lt_to_le @ltb_false_to_not_lt @p1
     1257  | @not_lt_to_le @ltb_false_to_not_lt @p2
    12511258  ]
    12521259|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
     1260  lapply (pi2 ?? prefixlens_acc) >p in ⊢ (% → ?); -prefixlens_acc normalize nodelta
     1261  >p1 -prefixlens >p2 -acc >p3 in prf; -x #prf normalize nodelta inversion inc_pc_sigma
    12561262  #inc_pc #inc_sigma #Hips normalize nodelta
    12571263  inversion (bvt_lookup … bvprefixlen (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    1258   #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
    1259   #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
    1260   #Heq1 #Heq2
     1264  #old_pc #old_length #Holdeq ** #Hpolicy1 >Hpolicy1 -prefixlen
     1265  #Hpolicy2 >Hpolicy2 in Holdeq; -bvprefixlen #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim *
     1266  #prefixlen' #bvprefixlen' * #added #policy normalize nodelta @pair_elim #new_length #isize
     1267  normalize nodelta #Heq1 #Heq2 cases (pair_destruct ?????? Heq2) -Heq2
     1268  #Heq2c cases (pair_destruct ?????? Heq2c) -Heq2c #Heq2c <Heq2c -prefixlen'
     1269  #Heq2d <Heq2d -bvprefixlen' #Heq2
    12611270 cut (S (|prefix|) < 2^16)
    12621271 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
    12631272   <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
    12641273 cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
    1265  cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
    1266   % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    1267   [ (* not_jump_default *)
     1274 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a
     1275 >(?:increment … (bitvector_of_nat … (|prefix|)) = bitvector_of_nat … (S (|prefix|)))
     1276 [2: >increment_zero_bitvector_of_nat_1 <add_bitvector_of_nat %]
     1277 #Heq2b <Heq2a normalize nodelta
     1278  % [ % | % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]]
     1279  [ >length_append <plus_n_Sm <plus_n_O %
     1280  | %
     1281  | (* not_jump_default *)
    12681282    @(jump_expansion_step1 … Heq1 Heq2b) try assumption
    12691283    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
     
    12751289    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    12761290  | (* jump_increase *)
    1277     @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
     1291    @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … ???? old_length Holdeq
    12781292      … Heq1 prefix_ok1 prefix_ok Heq2b)
    12791293    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1280     cases (pi2 … old_sigma) * * * #Hnjd #_ #_ #_ #_ @Hnjd
     1294    try % cases (pi2 … old_sigma) * * * #Hnjd #_ #_ #_ #_ @Hnjd
    12811295  | (* sigma_compact_unsafe *)
    12821296    @(jump_expansion_step4 … Heq1 … Heq2b) try assumption
     
    12861300  | (* policy_jump_equal → added = 0 *)
    12871301    @(jump_expansion_step5 … inc_added … Holdeq … Heq1 … Heq2b) try assumption
    1288     try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
     1302    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) try %
    12891303    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    12901304  | (* added = 0 → policy_pc_equal *)
     1305    >Heq2a
    12911306    @(jump_expansion_step6 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 … Heq2a Heq2b) try assumption
    12921307    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    12931308    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    1294     cases (pi2 … old_sigma) * #_ #X #_ @X
     1309    try (cases (pi2 … old_sigma) * #_ #X #_ @X) %
    12951310  | (* out_of_program_none *)
    12961311    @(jump_expansion_step7 … Heq2b)
    12971312    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
    12981313  | (* lookup p = lookup old_sigma + added *)
     1314    >Heq2a
    12991315    @(jump_expansion_step8 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 Heq2a Heq2b) try assumption
    13001316    [ cases (pi2 … old_sigma) * #_ #H1 #H2 % assumption
     1317    | %
    13011318    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    1302     | @(proj2 ?? (proj1 ?? Hpolicy)) ]
     1319    | >(proj2 ?? (proj1 ?? Hpolicy)) @eq_f2 try %
     1320      cases (lookup (? × ?)????) in Holdeq; #x #y #H destruct (H) %
     1321    ]
    13031322  | (* sigma_safe *)
    1304     @(jump_expansion_step9 … prf … p1 … Holdeq … Heq1 prefix_ok1 prefix_ok)
     1323    >Heq2a
     1324    @(jump_expansion_step9 … prf … Holdeq … Heq1 prefix_ok1 prefix_ok)
    13051325    [ @inc_pc_sigma
     1326    | %
    13061327    | >Hips %
    13071328    | @inc_added
    13081329    | >Hips @Heq2b
    13091330    | @(proj2 ?? (proj1 ?? (pi2 ?? old_sigma)))
    1310     | >Hips @(proj2 ?? (proj1 ?? Hpolicy))
     1331    | >Hips >(proj2 ?? (proj1 ?? Hpolicy)) @eq_f2 try %
     1332      cases (lookup (? × ?)????) in Holdeq; #x #y #H destruct (H) %
    13111333    | >Hips @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    13121334    | >Hips @(proj2 ?? Hpolicy)
    13131335    ]
    13141336  ]
    1315 | normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    1316   [ #i cases i
     1337| normalize nodelta % [% | % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]]
     1338  [ %
     1339  | %
     1340  | #i cases i
    13171341    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    13181342    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    13191343    ]
    1320   | >lookup_insert_hit @refl 
     1344  | >lookup_insert_hit @refl
    13211345  | >lookup_insert_hit @refl
    13221346  | #i #Hi <(le_n_O_to_eq … Hi)
Note: See TracChangeset for help on using the changeset viewer.