Changeset 2993 for extracted


Ignore:
Timestamp:
Mar 28, 2013, 9:56:26 AM (7 years ago)
Author:
sacerdot
Message:
  1. performance improved: the type inference was inferring load_code_memory ... in computational positions, duplicating the work at every step of execution of the assembly code. We now force the use of the let-in-ed variable
  2. new extraction after 1)
  3. driver/printer.ml repaired
  4. the output of the intermediate passes is now printed on file
Location:
extracted
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCosts.ml

    r2951 r2993  
    228228  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
    229229  StructuredTraces.as_pc_of =
    230   (Obj.magic (Status.program_counter (Fetch.load_code_memory prog.ASM.oc)));
     230  (Obj.magic (Status.program_counter code_memory));
    231231  StructuredTraces.as_classify =
    232232  (Obj.magic (AbstractStatus.oC_classify code_memory));
     
    236236    Nat.O)))))))))))))))) (Obj.magic pc) prog.ASM.costlabels);
    237237  StructuredTraces.as_result = (fun st ->
    238   as_result_of_finaladdr (Fetch.load_code_memory prog.ASM.oc) (Obj.magic st)
    239     prog.ASM.final_pc); StructuredTraces.as_call_ident =
     238  as_result_of_finaladdr code_memory (Obj.magic st) prog.ASM.final_pc);
     239  StructuredTraces.as_call_ident =
    240240  (Obj.magic (oC_as_call_ident prog code_memory));
    241241  StructuredTraces.as_tailcall_ident = (fun clearme ->
     
    506506   | Nat.S program_size' ->
    507507     (fun _ ->
    508        (let { Types.fst = eta27505; Types.snd = ticks } =
     508       (let { Types.fst = eta16; Types.snd = ticks } =
    509509          Fetch.fetch (Fetch.load_code_memory prog.ASM.oc) program_counter'
    510510        in
    511        let { Types.fst = instruction; Types.snd = program_counter'' } =
    512          eta27505
     511       let { Types.fst = instruction; Types.snd = program_counter'' } = eta16
    513512       in
    514513       (fun _ ->
  • extracted/aSMCostsSplit.ml

    r2965 r2993  
    153153    ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
    154154let traverse_code prog =
    155 prerr_endline "<TRAVERSE_CODE"; let res =
    156155  Types.pi1
    157156    (traverse_code_internal prog
     
    160159        Nat.O)))))))))))))))))
    161160      (Glue.int_of_matitanat (List.length (ASM.oc prog))))
    162 in prerr_endline "TRAVERSE_CODE>"; res
    163161
    164162(** val compute_costs :
  • extracted/interpret2.ml

    r2951 r2993  
    165165    ASM.labelled_object_code -> Measurable.preclassified_system **)
    166166let oC_preclassified_system c =
     167  let lcm =(Fetch.load_code_memory c.ASM.oc) in
    167168  mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
    168169    (fun st ->
    169170    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
    170       (Interpret.execute_1 (Fetch.load_code_memory c.ASM.oc) (Obj.magic st)))
     171      (Interpret.execute_1 lcm (Obj.magic st))
     172    )
    171173    (Obj.magic (Status.initialise_status (Fetch.load_code_memory c.ASM.oc)))
    172174
Note: See TracChangeset for help on using the changeset viewer.