Changeset 2993 for driver/cerco.ml

Timestamp:

Mar 28, 2013, 9:56:26 AM (8 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

File:

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

driver/cerco.ml

@@ -34 +34 @@
 
 let argv1 = Sys.argv.(1) in
-let do_print,filename,style =
+let do_exec,filename,style =
  if argv1 = "-exec" then
   true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
@@ -41 +41 @@
 let cl = ClightParser.process filename in
 let observe =
- if do_print then
-  let rec infinity = Extracted.Nat.S infinity in
-  (fun pass prog ->
-    print_string (Printer.print_program pass prog);
+ 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
+    Printer.print_program filename pass prog;
+   if do_exec then
     Extracted.Semantics.run_and_print pass prog infinity
-     (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); Extracted.Types.It)
-     (fun evn -> print_string (string_of_intensional_event evn); Extracted.Types.It)
-     (fun msg -> print_endline (Error.errormsg msg); Extracted.Types.It)
-     (fun n-> print_endline (string_of_int (Extracted.Glue.int_of_bitvector n)); Extracted.Types.It))
- else (fun _ _ -> Extracted.Types.It) 
+     (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); flush stdout;
+       Extracted.Types.It)
+     (fun evn -> print_string (string_of_intensional_event evn); flush stdout;
+       Extracted.Types.It)
+     (fun msg -> print_endline (Error.errormsg msg); flush stdout;
+       Extracted.Types.It)
+     (fun n-> print_endline (string_of_int(Extracted.Glue.int_of_bitvector n));
+       flush stdout; Extracted.Types.It)
+   else
+    Extracted.Types.It)
 in
 let output =