Changeset 3104 for src/ASM


Ignore:
Timestamp:
Apr 6, 2013, 6:37:17 PM (7 years ago)
Author:
sacerdot
Message:

Performance improvement.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r3082 r3104  
    11771177  (foldl_strong ?
    11781178   (λprefix.
    1179      Σres: nat × (BitVectorTrie Byte 16).
    1180       let 〈i,mem〉 ≝ res in
    1181       i = |prefix| ∧
     1179     Σres: nat × Word × (BitVectorTrie Byte 16).
     1180      let 〈i,bvi,mem〉 ≝ res in
     1181      i = |prefix| ∧ bvi = bitvector_of_nat … i ∧
    11821182      (i ≤ 2^16 →
    11831183        ∀pc. ∀pc_ok: pc < |prefix|.
     
    11851185   program
    11861186   (λprefix,v,tl,prf,i_mem.
    1187      let 〈i,mem〉 ≝ i_mem in
    1188       〈S i,insert … (bitvector_of_nat … i) v mem〉)
    1189   〈0,Stub Byte 16〉).
    1190 [3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
    1191 | % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
    1192 | cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
    1193   [ >length_append >H1 normalize //
     1187     let 〈i,bvi,mem〉 ≝ i_mem in
     1188      〈S i,increment … bvi,insert … bvi v mem〉)
     1189  〈0,zero ?,Stub Byte 16〉).
     1190[3: cases (foldl_strong ? (λprefix.Σres.?) ???) ** #i #bvi #mem ** #H1 #H3 >H1 #H2 @H2
     1191| % // % // (*#_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))*)
     1192| cases i_mem in p; ** #i' #bvi' #mem' normalize nodelta #H #EQ destruct(EQ)
     1193  cases H -H * #H1 #H3 #H2 destruct (p1) %
     1194  [ % [ >length_append >H1 normalize //
     1195      | >increment_zero_bitvector_of_nat_1 >H3 <add_bitvector_of_nat % ]
    11941196  | #LE #pc #pc_ok
    11951197    cases (le_to_or_lt_eq … pc_ok)
     
    11981200      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
    11991201      <H1 <plus_n_O whd in ⊢ (???%); //
    1200     | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
     1202    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix
     1203      [2: /2 by lt_plus_to_lt_l/]
    12011204      >H2 [2: @(transitive_le … LE) //]
    12021205      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
    1203       whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
     1206      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false % >H3
    12041207      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
    12051208      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
  • src/ASM/Assembly.ma

    r3076 r3104  
    855855       let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    856856       let lookup_datalabels ≝ λx.
    857          match lookup ASMTag … (construct_datalabels preamble) x with
     857         match lookup ASMTag … datalabels x with
    858858         [ Some addr ⇒ 〈XData, addr〉
    859859         | None ⇒ 〈Code, lookup_labels x〉
Note: See TracChangeset for help on using the changeset viewer.