(WIP) Add monitor for the compiler

Signed-off-by: Jerome Simeon <[email protected]>

Makefile.coq_modules

@@ -14,6 +14,7 @@
 
 MODULES = \
   Version \
+  Utils/Misc \
   Backend/ForeignErgo \
   Backend/Model/DateTimeModelPart \
   Backend/Model/MathModelPart \
@@ -26,17 +27,16 @@ MODULES = \
   Backend/Lib/EOperators \
   Backend/Lib/ECodeGen \
   Backend/ErgoBackend \
-  Common/Utils/Misc \
-  Common/Utils/Provenance \
-  Common/Utils/Names \
-  Common/Utils/NamespaceContext \
-  Common/Utils/Ast \
-  Common/Utils/Result \
-  Common/Utils/PrintTypedData \
-  Common/CTO/CTO \
-  Common/Types/ErgoCTypeUtil \
-  Common/Types/ErgoType \
-  Common/Types/ErgoTypetoErgoCType \
+  Common/Provenance \
+  Common/Names \
+  Common/NamespaceContext \
+  Common/Ast \
+  Common/Result \
+  Common/PrintTypedData \
+  Types/CTO \
+  Types/ErgoCTypeUtil \
+  Types/ErgoType \
+  Types/ErgoTypetoErgoCType \
   Ergo/Lang/Ergo \
   Ergo/Lang/ErgoMap \
   Ergo/Lang/ErgoSem \

extraction/.gitignore

@@ -25,3 +25,7 @@ src/Cto_j.ml
 src/Cto_j.mli
 src/Cto_t.ml
 src/Cto_t.mli
+src/Monitor_j.ml
+src/Monitor_j.mli
+src/Monitor_t.ml
+src/Monitor_t.mli

extraction/ErgoExtraction.v

@@ -31,8 +31,9 @@ Extract Constant Digits.nat_to_string10 => "(fun x -> Util.char_list_of_string (
 
 Extract Constant String.append => "(fun s1 s2 -> Util.char_list_append s1 s2)".
 
-Require Import ErgoSpec.Common.Utils.Misc.
+Require Import ErgoSpec.Utils.Misc.
 Extract Constant Misc.coq_toposort => "(fun label file l -> Util.coq_toposort label file l)".
+Extract Constant Misc.coq_time => "(fun msg f x -> Util.coq_time msg f x)".
 Extract Constant Misc.get_local_part => "(fun name -> Util.get_local_part name)".
 
 (* Ergo modules *)

extraction/Makefile

@@ -98,7 +98,13 @@ src/Cto_t.ml src/Cto_t.mli: src/Cto.atd
 src/Cto_j.ml src/Cto_j.mli: src/Cto.atd
 	atdgen -j -j-std $<
 
-ATDS=src/Cto_t.ml src/Cto_t.mli src/Cto_j.ml src/Cto_j.mli
+src/Monitor_t.ml src/Monitor_t.mli: src/Monitor.atd
+	atdgen -t $<
+
+src/Monitor_j.ml src/Monitor_j.mli: src/Monitor.atd
+	atdgen -j -j-std $<
+
+ATDS=src/Cto_t.ml src/Cto_t.mli src/Cto_j.ml src/Cto_j.mli src/Monitor_t.ml src/Monitor_t.mli src/Monitor_j.ml src/Monitor_j.mli
 
 ## Stdlib
 

extraction/ergoc.ml

@@ -30,7 +30,9 @@ let args_list gconf =
       ("--target", Arg.String (ErgoConfig.set_target_lang gconf),
        "<lang> Target platform (default: es6) " ^ available_targets);
       ("--link", Arg.Unit (ErgoConfig.set_link gconf),
-       " Adds the Ergo runtime to the target code (es5,es6,cicero only)")
+       " Adds the Ergo runtime to the target code (es5,es6,cicero only)");
+      ("--monitor", Arg.Set Util.monitoring,
+       " Produce compilation time information");
     ]
 
 let usage =

extraction/src/ErgoCompile.ml

@@ -58,14 +58,25 @@ let ergo_link gconf result =
   else
     result
 
+let print_generate source_file ext result =
+  let fpref = Filename.chop_extension source_file in
+  let fout = outname (target_f None fpref) ext in
+  Printf.printf " '%s'\n" fout;
+  make_file fout result
+
+let print_monitor source_file =
+  if !Util.monitoring
+  then
+    let result = Util.get_monitor_output () in
+    Printf.printf "Monitoring for '%s' -->" source_file;
+    print_generate source_file ".monitor.json" result
+  else ()
+
 let ergo_proc gconf inputs =
   let target_lang = ErgoConfig.get_target_lang gconf in
   let ext = extension_of_lang target_lang in
   let (source_file,result) = ergo_compile target_lang inputs in
   Printf.printf "Compiling Ergo '%s' -- " source_file;
-  let fpref = Filename.chop_extension source_file in
-  let fout = outname (target_f None fpref) ext in
   let result = ergo_link gconf result in
-  Printf.printf "creating '%s'\n" fout;
-  make_file fout result
-
+  print_generate source_file ext result;
+  print_monitor source_file

extraction/src/Monitor.atd

@@ -0,0 +1,32 @@
+(*
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *)
+
+<doc text="Ergo monitor data structure.
+
+   Based on the documentation available at:
+   XXXX
+
+">
+
+type phase = {
+    name : string;
+    cputime : float;
+    cummulative : float;
+    subphases : phase list;
+  } <ocaml field_prefix="ergo_monitor_">
+
+type monitor = {
+    phases : phase list;
+} <ocaml field_prefix="ergo_monitor_">
+

extraction/src/Util.ml

@@ -13,6 +13,7 @@
  *)
 
 (* This module contains a few basic utilities *)
+open Monitor_j (* For the monitor JSON output *)
 
 (* this can't go in Logger, since that creates a circular dependency *)
 type nrc_logger_token_type = string
@@ -239,3 +240,64 @@ let class_prefix_of_filename filename =
   | Invalid_argument _ -> "logic"
   end
 
+(** Monitoring *)
+
+(* monitor contains a mapping from compilation phase to (f1,f2) where f1 is the new time entering the phase and f2 is the total time in that phase *)
+let monitor : (string, float * float) Hashtbl.t = Hashtbl.create 37
+let monitoring = ref false
+let monitor_output : (Monitor_j.phase list) Stack.t =
+  let s = Stack.create () in
+  Stack.push [] s;
+  s
+
+let enter_monitor monitor output phase =
+  Stack.push [] output;
+  begin try
+    let (f1,f2) = Hashtbl.find monitor phase in (* f1 should always be 0.0 *)
+    Hashtbl.replace monitor phase (Sys.time(), f2)
+  with _ ->
+    Hashtbl.add monitor phase (Sys.time(), 0.0)
+  end
+let exit_monitor monitor output phase =
+  let prev = Stack.pop output in
+  let prevprev = Stack.pop output in
+  begin try
+    let (f1,f2) = Hashtbl.find monitor phase in
+    let picktime : float = Sys.time () in
+    let cputime : float = picktime -. f1 in
+    let cummtime : float = picktime -. f1 +. f2 in
+    Hashtbl.replace monitor phase (0.0, cummtime);
+    Stack.push (prevprev @ [{
+      ergo_monitor_name = phase;
+      ergo_monitor_cputime = cputime;
+      ergo_monitor_cummulative = cummtime;
+      ergo_monitor_subphases =prev
+    }]) output
+  with _ ->
+    begin
+      Hashtbl.add monitor phase (0.0, 0.0); (* Should never happen *)
+      Stack.push (prevprev @ [{
+        ergo_monitor_name = phase;
+        ergo_monitor_cputime = 0.0;
+        ergo_monitor_cummulative = 0.0;
+        ergo_monitor_subphases = prev
+      }]) output
+    end
+  end
+
+let coq_time phase f x =
+  if !monitoring
+  then
+    let phase = string_of_char_list phase in
+    begin
+      enter_monitor monitor monitor_output phase;
+      let y = f x in
+      exit_monitor monitor monitor_output phase;
+      y
+    end
+  else
+    f x
+
+let get_monitor_output () =
+  string_of_monitor { ergo_monitor_phases = Stack.top monitor_output }
+

extraction/src/Util.mli

@@ -88,3 +88,9 @@ val get_local_part : char list -> (char list) option
 val class_prefix_of_filename : string -> string
 
 type nrc_logger_token_type = string
+
+(** Monitoring *)
+val coq_time : char list -> ('a -> 'b) -> 'a -> 'b
+val monitoring : bool ref
+val get_monitor_output : unit -> string
+

mechanization/Backend/Lib/ENNRCtoJavaScript.v

@@ -26,6 +26,8 @@ Require Import Qcert.NNRC.NNRCRuntime.
 Require Import Qcert.JavaScript.JavaScriptRuntime.
 Require Import Qcert.Translation.ForeignToJavaScript.
 
+Require Import ErgoSpec.Utils.Misc.
+
 Local Open Scope string_scope.
 
 Section ENNRCtoJavaScript.
@@ -93,7 +95,7 @@ Section ENNRCtoJavaScript.
       end.
 
     Definition rename_top (e:nnrc) : nnrc :=
-      fst (rename nil e).
+      fst (coq_time "nnrc(rename)" (rename nil) e).
   End global_rename.
 
 Section sanitizer.

mechanization/Common/Utils/Ast.v → mechanization/Common/Ast.v

@@ -14,8 +14,8 @@
 
 Require Import String.
 Require Import ErgoSpec.Backend.ErgoBackend.
-Require Import ErgoSpec.Common.Utils.Names.
-Require Import ErgoSpec.Common.Utils.Provenance.
+Require Import ErgoSpec.Common.Names.
+Require Import ErgoSpec.Common.Provenance.
 
 Section Ast.
   Section Imports.

mechanization/Common/Utils/NamespaceContext.v → mechanization/Common/NamespaceContext.v

@@ -19,9 +19,9 @@
 Require Import String.
 Require Import List.
 Require Import ErgoSpec.Backend.ErgoBackend.
-Require Import ErgoSpec.Common.Utils.Provenance.
-Require Import ErgoSpec.Common.Utils.Names.
-Require Import ErgoSpec.Common.Utils.Result.
+Require Import ErgoSpec.Common.Provenance.
+Require Import ErgoSpec.Common.Names.
+Require Import ErgoSpec.Common.Result.
 
 Section NamespaceContext.
 

mechanization/Common/Utils/PrintTypedData.v → mechanization/Common/PrintTypedData.v

@@ -16,11 +16,11 @@ Require Import Ascii.
 Require Import String.
 Require Import List.
 
+Require Import ErgoSpec.Utils.Misc.
 Require Import ErgoSpec.Backend.ErgoBackend.
-Require Import ErgoSpec.Common.Utils.Misc.
-Require Import ErgoSpec.Common.Utils.Result.
-Require Import ErgoSpec.Common.Utils.Provenance.
-Require Import ErgoSpec.Common.Utils.NamespaceContext.
+Require Import ErgoSpec.Common.Result.
+Require Import ErgoSpec.Common.Provenance.
+Require Import ErgoSpec.Common.NamespaceContext.
 
 Require Import JsAst.JsNumber. (* XXX To be fixed on Q*cert side - JS *)
 

mechanization/Common/Utils/Result.v → mechanization/Common/Result.v

@@ -19,9 +19,9 @@ Require Import String.
 Require Import List.
 Require Import ZArith.
 Require Import ErgoSpec.Backend.ErgoBackend.
-Require Import ErgoSpec.Common.Utils.Provenance.
-Require Import ErgoSpec.Common.Utils.Names.
-Require Import ErgoSpec.Common.Utils.Ast.
+Require Import ErgoSpec.Common.Provenance.
+Require Import ErgoSpec.Common.Names.
+Require Import ErgoSpec.Common.Ast.
 
 Section Result.
   Inductive eerror : Set :=

mechanization/Compiler/ErgoCompiler.v

@@ -16,14 +16,14 @@ Require String.
 Require Qcert.Common.Brands.BrandRelation.
 
 Require ErgoSpec.Version.
+Require ErgoSpec.Utils.Misc.
 Require ErgoSpec.Backend.ErgoBackend.
-Require ErgoSpec.Common.Utils.Misc.
-Require ErgoSpec.Common.Utils.Provenance.
-Require ErgoSpec.Common.Utils.Names.
-Require ErgoSpec.Common.Utils.Result.
-Require ErgoSpec.Common.Utils.Ast.
-Require ErgoSpec.Common.CTO.CTO.
-Require ErgoSpec.Common.Types.ErgoType.
+Require ErgoSpec.Common.Provenance.
+Require ErgoSpec.Common.Names.
+Require ErgoSpec.Common.Result.
+Require ErgoSpec.Common.Ast.
+Require ErgoSpec.Types.CTO.
+Require ErgoSpec.Types.ErgoType.
 Require ErgoSpec.Ergo.Lang.Ergo.
 Require ErgoSpec.Ergo.Lang.ErgoSugar.
 Require ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.