Changeset 2993


Ignore:
Timestamp:
Mar 28, 2013, 9:56:26 AM (4 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
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • driver/cerco.ml

    r2964 r2993  
    3434
    3535let argv1 = Sys.argv.(1) in
    36 let do_print,filename,style =
     36let do_exec,filename,style =
    3737 if argv1 = "-exec" then
    3838  true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
     
    4141let cl = ClightParser.process filename in
    4242let observe =
    43  if do_print then
    44   let rec infinity = Extracted.Nat.S infinity in
    45   (fun pass prog ->
    46     print_string (Printer.print_program pass prog);
     43 let rec infinity = Extracted.Nat.S infinity in
     44 (fun pass prog ->
     45   if do_exec || pass = Extracted.Compiler.Clight_label_pass ||
     46      pass = Extracted.Compiler.Object_code_pass then
     47    Printer.print_program filename pass prog;
     48   if do_exec then
    4749    Extracted.Semantics.run_and_print pass prog infinity
    48      (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); Extracted.Types.It)
    49      (fun evn -> print_string (string_of_intensional_event evn); Extracted.Types.It)
    50      (fun msg -> print_endline (Error.errormsg msg); Extracted.Types.It)
    51      (fun n-> print_endline (string_of_int (Extracted.Glue.int_of_bitvector n)); Extracted.Types.It))
    52  else (fun _ _ -> Extracted.Types.It)
     50     (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); flush stdout;
     51       Extracted.Types.It)
     52     (fun evn -> print_string (string_of_intensional_event evn); flush stdout;
     53       Extracted.Types.It)
     54     (fun msg -> print_endline (Error.errormsg msg); flush stdout;
     55       Extracted.Types.It)
     56     (fun n-> print_endline (string_of_int(Extracted.Glue.int_of_bitvector n));
     57       flush stdout; Extracted.Types.It)
     58   else
     59    Extracted.Types.It)
    5360in
    5461let output =
  • driver/printer.ml

    r2982 r2993  
    221221    l)
    222222
    223 let print_program pass (program : Extracted.Preamble.__) =
     223let extension_of_pass =
     224 function
     225 | Extracted.Compiler.Clight_pass                -> "clight"
     226 | Extracted.Compiler.Clight_switch_removed_pass -> "clight_sr"
     227 | Extracted.Compiler.Clight_label_pass          -> "clight_l"
     228 | Extracted.Compiler.Clight_simplified_pass     -> "clight_s"
     229 | Extracted.Compiler.Cminor_pass                -> "cminor"
     230 | Extracted.Compiler.Rtlabs_pass                -> "rtlabs"
     231 | Extracted.Compiler.Rtl_separate_pass          -> "rtl"
     232 | Extracted.Compiler.Rtl_uniq_pass              -> "rtl_u"
     233 | Extracted.Compiler.Ertl_pass                  -> "ertl"
     234 | Extracted.Compiler.Ertlptr_pass               -> "ertlptr"
     235 | Extracted.Compiler.Ltl_pass                   -> "ltl"
     236 | Extracted.Compiler.Lin_pass                   -> "lin"
     237 | Extracted.Compiler.Assembly_pass              -> "assembly"
     238 | Extracted.Compiler.Object_code_pass           -> "hex"
     239;;
     240
     241
     242let print_program sourcename pass (program : Extracted.Preamble.__) =
    224243 let beprint pcs =
    225244  print_graph (pcs (Extracted.Types.fst (Obj.magic program))) in
     
    250269   | _ -> ""
    251270 in
    252   "\n" ^ lines ^ "\n"
     271  let filename =
     272   Filename.chop_extension sourcename ^ "." ^ extension_of_pass pass in
     273  let och = open_out filename in
     274  output_string och lines;
     275  close_out och
  • driver/printer.mli

    r2901 r2993  
    1 val print_program: Extracted.Compiler.pass -> Extracted.Preamble.__ -> string
     1val print_program:
     2 string -> Extracted.Compiler.pass -> Extracted.Preamble.__ -> unit
  • 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
  • src/ASM/ASMCosts.ma

    r2910 r2993  
    4242      (λs1,s2. execute_1 … s1 = s2)
    4343      word_deqset
    44       (program_counter …)
    45       (OC_classify )
     44      (program_counter … code_memory)
     45      (OC_classify code_memory)
    4646      (λpc.lookup_opt … pc (costlabels prog))
    4747      (next_instruction_properly_relates_program_counters code_memory)
    48       (λst. as_result_of_finaladdr … st (final_pc prog))
    49       (OC_as_call_ident prog )
     48      (λst. as_result_of_finaladdr … code_memory … st (final_pc prog))
     49      (OC_as_call_ident prog code_memory)
    5050      ?.
    5151 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
  • src/ASM/Interpret2.ma

    r2910 r2993  
    3939definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
    4040 λc:labelled_object_code.
     41  let lcm ≝ load_code_memory … (oc c) in
    4142  mk_preclassified_system_of_abstract_status
    4243   labelled_object_code
    4344   (OC_abstract_status c)
    44    (λst. return (execute_1 … st))
     45   (λst. return (execute_1 lcm … st))
    4546   (initialise_status … (load_code_memory (oc c))).
    4647
Note: See TracChangeset for help on using the changeset viewer.