use nanosecond timing from monotonic clock mtime for profiling; disti…

…nguish it from time_of_day

.devcontainer/minimal.Dockerfile

@@ -46,7 +46,7 @@ ARG OCAML_VERSION=4.14.0
 RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
 RUN opam option depext-run-installs=true
 ENV OPAMYES=1
-RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace
+RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib mtime pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace
 
 # Get compiled Z3
 RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \

.docker/base/Dockerfile

@@ -18,7 +18,7 @@ WORKDIR /home/build
 # Prepare and build OPAM and OCaml
 RUN opam init -y --disable-sandboxing
 RUN opam update
-RUN opam install -y ocamlbuild ocamlfind batteries stdint zarith yojson fileutils pprint menhir sedlex ppx_deriving ppx_deriving_yojson process pprint visitors fix wasm ppxlib=0.22.0
+RUN opam install -y ocamlbuild ocamlfind batteries stdint zarith yojson fileutils pprint menhir mtime sedlex ppx_deriving ppx_deriving_yojson process pprint visitors fix wasm ppxlib=0.22.0
 
 # Prepare and build Z3
 ENV z3=z3-4.8.5-x64-debian-8.11

fstar.opam

@@ -14,6 +14,7 @@ depends: [
   "memtrace"
   "menhirLib"
   "menhir" {build & >= "2.1"}
+  "mtime"
   "pprint"
   "sedlex"
   "ppxlib" {>= "0.27.0"}

ocaml/default.nix

@@ -1,5 +1,5 @@
 { batteries, buildDunePackage, includeBinaryAnnotations ? false
-, installShellFiles, lib, makeWrapper, menhir, menhirLib, memtrace, ocaml
+, installShellFiles, lib, makeWrapper, menhir, menhirLib, memtrace, mtime, ocaml
 , pprint, ppxlib, ppx_deriving, ppx_deriving_yojson, process, removeReferencesTo
 , sedlex, stdint, version, yojson, zarith }:
 
@@ -32,6 +32,7 @@ buildDunePackage {
     yojson
     zarith
     memtrace
+    mtime
   ];
 
   enableParallelBuilding = true;

ocaml/fstar-lib/FStarC_Compiler_Util.ml

@@ -14,21 +14,26 @@ let is_punctuation c = List.mem c [33; 34; 35; 37; 38; 39; 40; 41; 42; 44; 45; 4
 
 let return_all x = x
 
-type time = float
-let now () = BatUnix.gettimeofday ()
-let now_ms () = Z.of_int (int_of_float (now () *. 1000.0))
-let time_diff (t1:time) (t2:time) : float * Prims.int =
-  let n = t2 -. t1 in
-  n,
-  Z.of_float (n *. 1000.0)
-let record_time f =
-    let start = now () in
+type time_ns = int64
+let now_ns () = Mtime_clock.now_ns()
+let time_diff_ns t1 t2 = 
+  Z.of_int (Int64.to_int (Int64.sub t2 t1))
+let time_diff_ms t1 t2 = Z.div (time_diff_ns t1 t2) (Z.of_int 1000000)
+let record_time_ns f =
+    let start = now_ns () in
     let res = f () in
-    let _, elapsed = time_diff start (now()) in
+    let elapsed = time_diff_ns start (now_ns()) in
     res, elapsed
+let record_time_ms f =
+    let res, ns = record_time_ns f in
+    res, Z.div ns (Z.of_int 1000000)
+
+type time_of_day = float
+let get_time_of_day () = BatUnix.gettimeofday()
+let get_time_of_day_ms () = Z.of_int (int_of_float (get_time_of_day () *. 1000.0))
 let get_file_last_modification_time f = (BatUnix.stat f).BatUnix.st_mtime
 let is_before t1 t2 = compare t1 t2 < 0
-let string_of_time = string_of_float
+let string_of_time_of_day = string_of_float
 
 exception Impos
 
@@ -99,7 +104,7 @@ type proc =
      stop_marker: (string -> bool) option;
      id : string;
      prog : string;
-     start_time : time}
+     start_time : time_of_day}
 
 let all_procs : (proc list) ref = ref []
 
@@ -156,7 +161,7 @@ let start_process'
                outc = Unix.out_channel_of_descr stdin_w;
                stop_marker = stop_marker;
                killed = false;
-               start_time = now()} in
+               start_time = get_time_of_day()} in
   (* print_string ("Started process " ^ proc.id ^ "\n" ^ (stack_dump())); *)
   all_procs := proc :: !all_procs;
   proc

ocaml/fstar-lib/FStarC_Parser_ParseIt.ml

@@ -39,13 +39,13 @@ let find_file filename =
     | None ->
       raise_error_text FStarC_Compiler_Range.dummyRange Fatal_ModuleOrFileNotFound (U.format1 "Unable to find file: %s\n" filename)
 
-let vfs_entries : (U.time * string) U.smap = U.smap_create (Z.of_int 1)
+let vfs_entries : (U.time_of_day * string) U.smap = U.smap_create (Z.of_int 1)
 
 let read_vfs_entry fname =
   U.smap_try_find vfs_entries (U.normalize_file_path fname)
 
 let add_vfs_entry fname contents =
-  U.smap_add vfs_entries (U.normalize_file_path fname) (U.now (), contents)
+  U.smap_add vfs_entries (U.normalize_file_path fname) (U.get_time_of_day (), contents)
 
 let get_file_last_modification_time filename =
   match read_vfs_entry filename with

ocaml/fstar-lib/FStarC_Parser_ParseIt.mli

@@ -15,9 +15,9 @@ type input_frag = {
     frag_col:Prims.int
 }
 
-val read_vfs_entry : string -> (U.time * string) option
+val read_vfs_entry : string -> (U.time_of_day * string) option
 val add_vfs_entry: string -> string -> unit
-val get_file_last_modification_time: string -> U.time
+val get_file_last_modification_time: string -> U.time_of_day
 
 type parse_frag =
     | Filename of filename

ocaml/fstar-lib/dune

@@ -13,6 +13,7 @@
     pprint
     process
     sedlex
+    mtime.clock.os
  )
  (modes native byte)
  ; ^ Note: we need to compile fstar-lib in bytecode since some