Changeset 3064 for src


Ignore:
Timestamp:
Apr 2, 2013, 1:02:59 PM (7 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.

Location:
src/ASM
Files:
2 edited

Legend:

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