Changeset 3065 for src/ASM


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

Location:
src/ASM
Files:
2 edited

Legend:

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