Changeset 2999 for driver/cerco.ml

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:

• driver/cerco.ml (modified) (2 diffs)

driver/cerco.ml

@@ -34 +34 @@
 
 let argv1 = Sys.argv.(1) in
-let do_exec,filename,style =
+let do_exec,filename =
  if argv1 = "-exec" then
-  true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
+  true,Sys.argv.(2)
  else
-  false,argv1,(try Sys.argv.(2) with _ -> "instrumented") in
+  false,argv1 in
 let cl = ClightParser.process filename in
 let observe =
  let rec infinity = Extracted.Nat.S infinity in
  (fun pass prog ->
-   if do_exec || pass = Extracted.Compiler.Clight_label_pass ||
-      pass = Extracted.Compiler.Object_code_pass then
+   if do_exec || pass = Extracted.Compiler.Object_code_pass then
     Printer.print_program filename pass prog;
    if do_exec then
@@ -67 +66 @@
 let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
 let s_costmap = output.Extracted.Compiler.c_stack_cost in
-let style =
-  match style with
-  | "plain" -> Cost_plain
-  | "numbered" -> Cost_numbered (l_costmap,s_costmap)
-  | "instrumented" -> Cost_instrumented (l_costmap,s_costmap)
-  | x -> failwith ("I have no idea what " ^ x ^ " means")
-in
-print_endline (ClightPrinter.print_program style labelled);
-print_newline (); flush stdout;
-print_endline (ASMPrinter.print_program (Extracted.ASM.oc (Extracted.Compiler.c_labelled_object_code output)));
+let style = Cost_instrumented (l_costmap,s_costmap) in
+let instrumented = ClightPrinter.print_program style labelled in
+let filename = Filename.chop_extension filename ^ "-instrumented.c" in
+let och = open_out filename in
+output_string och instrumented;
+close_out och