Changeset 2999 for driver


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.

Location:
driver
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • driver/ASMPrinter.ml

    r2778 r2999  
    33
    44let print_program p =
    5   let code_memory = Extracted.Fetch.load_code_memory p in
    6   let intel_hex = IntelHex.pack_exported_code_memory 16 65535 code_memory in
     5  let intel_hex =
     6   IntelHex.pack_exported_code_memory 16 65535 p.Extracted.ASM.cm in
    77  IntelHex.string_of_intel_hex_format intel_hex
  • driver/ASMPrinter.mli

    r2778 r2999  
    22(** This module provides a function to print [ASM] programs. *)
    33
    4 val print_program : Extracted.ASM.object_code -> string
     4val print_program : Extracted.ASM.labelled_object_code -> string
  • driver/cerco.ml

    r2993 r2999  
    3434
    3535let argv1 = Sys.argv.(1) in
    36 let do_exec,filename,style =
     36let do_exec,filename =
    3737 if argv1 = "-exec" then
    38   true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
     38  true,Sys.argv.(2)
    3939 else
    40   false,argv1,(try Sys.argv.(2) with _ -> "instrumented") in
     40  false,argv1 in
    4141let cl = ClightParser.process filename in
    4242let observe =
    4343 let rec infinity = Extracted.Nat.S infinity in
    4444 (fun pass prog ->
    45    if do_exec || pass = Extracted.Compiler.Clight_label_pass ||
    46       pass = Extracted.Compiler.Object_code_pass then
     45   if do_exec || pass = Extracted.Compiler.Object_code_pass then
    4746    Printer.print_program filename pass prog;
    4847   if do_exec then
     
    6766let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
    6867let s_costmap = output.Extracted.Compiler.c_stack_cost in
    69 let style =
    70   match style with
    71   | "plain" -> Cost_plain
    72   | "numbered" -> Cost_numbered (l_costmap,s_costmap)
    73   | "instrumented" -> Cost_instrumented (l_costmap,s_costmap)
    74   | x -> failwith ("I have no idea what " ^ x ^ " means")
    75 in
    76 print_endline (ClightPrinter.print_program style labelled);
    77 print_newline (); flush stdout;
    78 print_endline (ASMPrinter.print_program (Extracted.ASM.oc (Extracted.Compiler.c_labelled_object_code output)));
     68let style = Cost_instrumented (l_costmap,s_costmap) in
     69let instrumented = ClightPrinter.print_program style labelled in
     70let filename = Filename.chop_extension filename ^ "-instrumented.c" in
     71let och = open_out filename in
     72output_string och instrumented;
     73close_out och
  • driver/printer.ml

    r2993 r2999  
    266266       (Extracted.LIN_printer.print_LIN_program joint_LTL_LIN_printing_params)
    267267   | Extracted.Compiler.Object_code_pass ->
    268       ASMPrinter.print_program (Extracted.ASM.oc (Obj.magic program))
     268      ASMPrinter.print_program (Obj.magic program)
    269269   | _ -> ""
    270270 in
Note: See TracChangeset for help on using the changeset viewer.