Changeset 3064


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

Efficiency of the semantics of assembly improved by avoiding the recomputation
of address_of_word_labels maps at every step.

Files:
6 edited

Legend:

Unmodified
Added
Removed
  • extracted/fetch.ml

    r3059 r3064  
    138138    BitVectorTrie.bitVectorTrie) Types.prod **)
    139139let create_label_cost_map program =
     140prerr_endline "CREATE_LABEL_COST_MAP";
    140141  Types.pi1 (create_label_cost_map0 program)
    141142
  • extracted/interpret.ml

    r3062 r3064  
    42554255    match instr with
    42564256    | ASM.Instruction instr0 ->
    4257       execute_1_preinstruction ticks cm (fun x y ->
    4258         Fetch.address_of_word_labels cm.ASM.code x) instr0 s0
     4257      execute_1_preinstruction ticks cm (fun x y -> addr_of_label x) instr0
     4258        s0
    42594259    | ASM.Comment cmt ->
    42604260      Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
  • extracted/interpret2.ml

    r3043 r3064  
    214214
    215215(** val aSM_as_result :
    216     ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
    217     Types.option **)
    218 let aSM_as_result prog st =
    219   let finaladdr =
    220     Fetch.address_of_word_labels prog.ASM.code prog.ASM.final_label
    221   in
     216    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
     217    Status.pseudoStatus -> Integers.int Types.option **)
     218let aSM_as_result prog addr_of_labels st =
     219  let finaladdr = addr_of_labels prog.ASM.final_label in
    222220  ASMCosts.as_result_of_finaladdr prog st finaladdr
    223221
     
    258256    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
    259257    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
    260     StructuredTraces.as_result = (Obj.magic (aSM_as_result prog));
     258    StructuredTraces.as_result =
     259    (Obj.magic (aSM_as_result prog addr_of_label));
    261260    StructuredTraces.as_call_ident =
    262261    (Obj.magic
  • extracted/interpret2.mli

    r3043 r3064  
    159159
    160160val aSM_as_result :
    161   ASM.pseudo_assembly_program -> Status.pseudoStatus -> Integers.int
    162   Types.option
     161  ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
     162  Status.pseudoStatus -> Integers.int Types.option
    163163
    164164open AssocList
  • src/ASM/Interpret.ma

    r3062 r3064  
    11981198  let s ≝
    11991199    match instr with
    1200     [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (code cm) x) instr s
     1200    [ Instruction instr ⇒
     1201       execute_1_preinstruction ticks …
     1202        (λx, y. addr_of_label x) instr s
    12011203    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    12021204    | Cost cst ⇒ s
  • src/ASM/Interpret2.ma

    r3039 r3064  
    100100qed.
    101101
    102 definition ASM_as_result: ∀prog. PseudoStatus prog → option int ≝
    103  λprog,st.
    104   let finaladdr ≝ address_of_word_labels (code prog) (final_label … prog) in
     102definition ASM_as_result: ∀prog. (Identifier → Word) → PseudoStatus prog → option int ≝
     103 λprog,addr_of_labels,st.
     104  let finaladdr ≝ addr_of_labels (final_label … prog) in
    105105   as_result_of_finaladdr … st finaladdr.
    106106
     
    138138      (ASM_as_label_of_pc prog …)
    139139      (ASM_next_instruction_properly_relates_program_counters prog)
    140       (ASM_as_result …)
     140      (ASM_as_result … addr_of_label)
    141141      (ASM_as_call_ident prog addr_of_label addr_of_symbol sigma policy …)
    142142      ?.
Note: See TracChangeset for help on using the changeset viewer.