Changeset 3095 for src/ASM


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.