Changeset 3065


Ignore:
Timestamp:
Apr 2, 2013, 1:37:45 PM (4 years ago)
Author:
sacerdot
Message:

Efficiency of semantics of assembled improved: ticks_of was re-computing the
address_of_word_labels map again and again.

Files:
6 edited

Legend:

Unmodified
Added
Removed
  • extracted/assembly.ml

    r3061 r3065  
    32523252
    32533253(** val ticks_of :
    3254     ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
    3255     (BitVector.word -> Bool.bool) -> BitVector.word -> (Nat.nat, Nat.nat)
    3256     Types.prod **)
    3257 let ticks_of program sigma policy ppc =
    3258   let { Types.fst = labels; Types.snd = costs } =
    3259     Fetch.create_label_cost_map program.ASM.code
    3260   in
    3261   let addr_of = fun id ->
    3262     Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3263       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3264       Nat.O))))))))))))))))
    3265       (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
    3266   in
     3254    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
     3255    (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
     3256    BitVector.word -> (Nat.nat, Nat.nat) Types.prod **)
     3257let ticks_of program addr_of sigma policy ppc =
    32673258  let { Types.fst = fetched; Types.snd = new_ppc } =
    32683259    ASM.fetch_pseudo_instruction program.ASM.code ppc
  • extracted/assembly.mli

    r2905 r3065  
    172172
    173173val ticks_of :
    174   ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
    175   (BitVector.word -> Bool.bool) -> BitVector.word -> (Nat.nat, Nat.nat)
    176   Types.prod
     174  ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
     175  (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
     176  BitVector.word -> (Nat.nat, Nat.nat) Types.prod
    177177
  • extracted/fetch.ml

    r3064 r3065  
    144144    ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
    145145let address_of_word_labels code_mem id =
     146prerr_endline "ADDRESS_OF_WORD_LABELS";
    146147  let labels = (create_label_cost_map code_mem).Types.fst in
    147148  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  • extracted/interpret2.ml

    r3064 r3065  
    180180let execute_1_pseudo_instruction' cm addr_of_label addr_of_symbol sigma policy status =
    181181  Interpret.execute_1_pseudo_instruction cm (fun x _ ->
    182     Assembly.ticks_of cm sigma policy x) addr_of_label addr_of_symbol status
     182    Assembly.ticks_of cm addr_of_label sigma policy x) addr_of_label
     183    addr_of_symbol status
    183184
    184185(** val classify_pseudo_instruction :
  • src/ASM/Assembly.ma

    r3057 r3065  
    12791279
    12801280definition ticks_of:
    1281     ∀p:pseudo_assembly_program.
     1281    ∀p:pseudo_assembly_program.∀addr_of: Identifier → Word.
    12821282    ∀sigma:Word → Word. ∀policy:Word → bool.
    12831283     ∀ppc:Word.
    12841284      nat_of_bitvector … ppc < |code p| → nat × nat ≝
    12851285  λprogram: pseudo_assembly_program.
    1286   λsigma.
    1287   λpolicy.
    1288   λppc: Word. λppc_ok.
    1289     let 〈labels, costs〉 ≝ create_label_cost_map (code program) in
    1290     let addr_of ≝ λid.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
     1286  λaddr_of,sigma,policy,ppc,ppc_ok.
    12911287    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in
    12921288     ticks_of0 program addr_of sigma policy ppc fetched.
  • src/ASM/Interpret2.ma

    r3064 r3065  
    5555 λcm,addr_of_label,addr_of_symbol,sigma,policy,status.
    5656  execute_1_pseudo_instruction cm
    57    (ticks_of cm sigma policy) addr_of_label addr_of_symbol status ….
     57   (ticks_of cm addr_of_label sigma policy) addr_of_label addr_of_symbol status ….
    5858cases daemon (*CSC: we need to prove that we remain inside the program
    5959 (code closed), which is impossible in case of function pointers.
Note: See TracChangeset for help on using the changeset viewer.