Ignore:
Timestamp:
Mar 28, 2013, 12:47:55 PM (7 years ago)
Author:
sacerdot
Message:

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interpret2.ml

    r2997 r2999  
    129129    (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
    130130let mk_trans_system_of_abstract_status s as_eval =
    131   { SmallstepExec.is_final = (fun x -> s.StructuredTraces.as_result);
     131  { SmallstepExec.is_final = (fun x -> StructuredTraces.as_result s);
    132132    SmallstepExec.step = (fun x status ->
    133133    let tr =
     
    158158    Measurable.pcs_labelled = (fun x st ->
    159159    Bool.notb (PositiveMap.is_none (StructuredTraces.as_label s st)));
    160     Measurable.pcs_classify = (fun x -> s.StructuredTraces.as_classify);
     160    Measurable.pcs_classify = (fun x -> StructuredTraces.as_classify s);
    161161    Measurable.pcs_callee = (fun x st _ ->
    162     s.StructuredTraces.as_call_ident st) }
     162    StructuredTraces.as_call_ident s st) }
    163163
    164164(** val oC_preclassified_system :
    165165    ASM.labelled_object_code -> Measurable.preclassified_system **)
    166166let oC_preclassified_system c =
    167   let lcm = Fetch.load_code_memory c.ASM.oc in
    168167  mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
    169168    (fun st ->
    170169    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
    171       (Interpret.execute_1 lcm (Obj.magic st)))
    172     (Obj.magic (Status.initialise_status (Fetch.load_code_memory c.ASM.oc)))
     170      (Interpret.execute_1 c.ASM.cm (Obj.magic st)))
     171    (Obj.magic (Status.initialise_status c.ASM.cm))
    173172
    174173open Assembly
Note: See TracChangeset for help on using the changeset viewer.