From 12f766e61377ff694cb9cc1433b844e631ce4071 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 18 Oct 2024 13:57:55 -0700 Subject: [PATCH] use nanosecond timing from monotonic clock mtime for profiling; distinguish it from time_of_day --- .devcontainer/minimal.Dockerfile | 2 +- .docker/base/Dockerfile | 2 +- fstar.opam | 1 + ocaml/default.nix | 3 +- ocaml/fstar-lib/FStarC_Compiler_Util.ml | 31 ++++--- ocaml/fstar-lib/FStarC_Parser_ParseIt.ml | 4 +- ocaml/fstar-lib/FStarC_Parser_ParseIt.mli | 4 +- ocaml/fstar-lib/dune | 1 + .../generated/FStarC_Interactive_Ide_Types.ml | 9 +- .../generated/FStarC_Interactive_Legacy.ml | 4 +- .../FStarC_Interactive_PushHelper.ml | 4 +- ocaml/fstar-lib/generated/FStarC_Main.ml | 2 +- ocaml/fstar-lib/generated/FStarC_Profiling.ml | 6 +- .../generated/FStarC_SMTEncoding_Encode.ml | 2 +- .../generated/FStarC_SMTEncoding_Z3.ml | 2 +- .../generated/FStarC_Tactics_V1_Basic.ml | 2 +- .../generated/FStarC_Tactics_V2_Basic.ml | 4 +- .../generated/FStarC_TypeChecker_Cfg.ml | 16 ++-- .../generated/FStarC_TypeChecker_Normalize.ml | 84 +++++++++---------- .../generated/FStarC_TypeChecker_Rel.ml | 7 +- .../generated/FStarC_TypeChecker_TcTerm.ml | 2 +- ocaml/fstar-lib/generated/FStarC_Universal.ml | 13 ++- .../generated/FStarC_Tests_Data.ml | 12 +-- src/basic/FStarC.Compiler.Util.fsti | 21 +++-- src/basic/FStarC.Profiling.fst | 4 +- src/fstar/FStarC.Interactive.Ide.Types.fst | 6 +- src/fstar/FStarC.Interactive.Legacy.fst | 4 +- src/fstar/FStarC.Interactive.PushHelper.fst | 4 +- src/fstar/FStarC.Main.fst | 2 +- src/fstar/FStarC.Universal.fst | 12 ++- src/parser/FStarC.Parser.ParseIt.fsti | 4 +- src/smtencoding/FStarC.SMTEncoding.Encode.fst | 2 +- src/smtencoding/FStarC.SMTEncoding.Z3.fst | 2 +- src/tactics/FStarC.Tactics.V1.Basic.fst | 2 +- src/tactics/FStarC.Tactics.V2.Basic.fst | 4 +- src/tests/FStarC.Tests.Data.fst | 12 +-- src/typechecker/FStarC.TypeChecker.Cfg.fst | 10 +-- .../FStarC.TypeChecker.Normalize.fst | 24 +++--- src/typechecker/FStarC.TypeChecker.Rel.fst | 6 +- src/typechecker/FStarC.TypeChecker.TcTerm.fst | 2 +- 40 files changed, 178 insertions(+), 160 deletions(-) diff --git a/.devcontainer/minimal.Dockerfile b/.devcontainer/minimal.Dockerfile index bab557a854b..ebc1e4f60c3 100644 --- a/.devcontainer/minimal.Dockerfile +++ b/.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 \ diff --git a/.docker/base/Dockerfile b/.docker/base/Dockerfile index 560afeb70b7..e7f8827c168 100644 --- a/.docker/base/Dockerfile +++ b/.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 diff --git a/fstar.opam b/fstar.opam index fecdbf99242..5edfa9b8352 100644 --- a/fstar.opam +++ b/fstar.opam @@ -14,6 +14,7 @@ depends: [ "memtrace" "menhirLib" "menhir" {build & >= "2.1"} + "mtime" "pprint" "sedlex" "ppxlib" {>= "0.27.0"} diff --git a/ocaml/default.nix b/ocaml/default.nix index 8381704b749..ab09c88b203 100644 --- a/ocaml/default.nix +++ b/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; diff --git a/ocaml/fstar-lib/FStarC_Compiler_Util.ml b/ocaml/fstar-lib/FStarC_Compiler_Util.ml index 9f3cee6eca1..b8903986786 100644 --- a/ocaml/fstar-lib/FStarC_Compiler_Util.ml +++ b/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 diff --git a/ocaml/fstar-lib/FStarC_Parser_ParseIt.ml b/ocaml/fstar-lib/FStarC_Parser_ParseIt.ml index 44af2a46cfc..792cd095f58 100644 --- a/ocaml/fstar-lib/FStarC_Parser_ParseIt.ml +++ b/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 diff --git a/ocaml/fstar-lib/FStarC_Parser_ParseIt.mli b/ocaml/fstar-lib/FStarC_Parser_ParseIt.mli index 01cb2edb5e4..21c90174eae 100644 --- a/ocaml/fstar-lib/FStarC_Parser_ParseIt.mli +++ b/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 diff --git a/ocaml/fstar-lib/dune b/ocaml/fstar-lib/dune index 0cdcbcb2982..e819359e059 100644 --- a/ocaml/fstar-lib/dune +++ b/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 diff --git a/ocaml/fstar-lib/generated/FStarC_Interactive_Ide_Types.ml b/ocaml/fstar-lib/generated/FStarC_Interactive_Ide_Types.ml index c665d45ff21..ad142a94e4c 100644 --- a/ocaml/fstar-lib/generated/FStarC_Interactive_Ide_Types.ml +++ b/ocaml/fstar-lib/generated/FStarC_Interactive_Ide_Types.ml @@ -104,12 +104,12 @@ type optmod_t = FStarC_Syntax_Syntax.modul FStar_Pervasives_Native.option type timed_fname = { tf_fname: Prims.string ; - tf_modtime: FStarC_Compiler_Util.time } + tf_modtime: FStarC_Compiler_Util.time_of_day } let (__proj__Mktimed_fname__item__tf_fname : timed_fname -> Prims.string) = fun projectee -> match projectee with | { tf_fname; tf_modtime;_} -> tf_fname let (__proj__Mktimed_fname__item__tf_modtime : - timed_fname -> FStarC_Compiler_Util.time) = + timed_fname -> FStarC_Compiler_Util.time_of_day) = fun projectee -> match projectee with | { tf_fname; tf_modtime;_} -> tf_modtime type repl_task = @@ -394,7 +394,8 @@ let (__proj__Mkgrepl_state__item__grepl_stdin : grepl_state -> FStarC_Compiler_Util.stream_reader) = fun projectee -> match projectee with | { grepl_repls; grepl_stdin;_} -> grepl_stdin -let (t0 : FStarC_Compiler_Util.time) = FStarC_Compiler_Util.now () +let (t0 : FStarC_Compiler_Util.time_of_day) = + FStarC_Compiler_Util.get_time_of_day () let (dummy_tf_of_fname : Prims.string -> timed_fname) = fun fname -> { tf_fname = fname; tf_modtime = t0 } let (string_of_timed_fname : timed_fname -> Prims.string) = @@ -404,7 +405,7 @@ let (string_of_timed_fname : timed_fname -> Prims.string) = if modtime = t0 then FStarC_Compiler_Util.format1 "{ %s }" fname else - (let uu___2 = FStarC_Compiler_Util.string_of_time modtime in + (let uu___2 = FStarC_Compiler_Util.string_of_time_of_day modtime in FStarC_Compiler_Util.format2 "{ %s; %s }" fname uu___2) let (string_of_repl_task : repl_task -> Prims.string) = fun uu___ -> diff --git a/ocaml/fstar-lib/generated/FStarC_Interactive_Legacy.ml b/ocaml/fstar-lib/generated/FStarC_Interactive_Legacy.ml index 5b41b45f47c..09ecc7bf5ba 100644 --- a/ocaml/fstar-lib/generated/FStarC_Interactive_Legacy.ml +++ b/ocaml/fstar-lib/generated/FStarC_Interactive_Legacy.ml @@ -464,8 +464,8 @@ let (deps_of_our_file : (deps1, maybe_intf, dep_graph)) type m_timestamps = (Prims.string FStar_Pervasives_Native.option * Prims.string * - FStarC_Compiler_Util.time FStar_Pervasives_Native.option * - FStarC_Compiler_Util.time) Prims.list + FStarC_Compiler_Util.time_of_day FStar_Pervasives_Native.option * + FStarC_Compiler_Util.time_of_day) Prims.list let rec (tc_deps : modul_t -> stack_t -> diff --git a/ocaml/fstar-lib/generated/FStarC_Interactive_PushHelper.ml b/ocaml/fstar-lib/generated/FStarC_Interactive_PushHelper.ml index 088f376c974..b45eaa2717c 100644 --- a/ocaml/fstar-lib/generated/FStarC_Interactive_PushHelper.ml +++ b/ocaml/fstar-lib/generated/FStarC_Interactive_PushHelper.ml @@ -153,7 +153,7 @@ let (repl_ld_tasks_of_deps : fun deps -> fun final_tasks -> let wrap fname = - let uu___ = FStarC_Compiler_Util.now () in + let uu___ = FStarC_Compiler_Util.get_time_of_day () in { FStarC_Interactive_Ide_Types.tf_fname = fname; FStarC_Interactive_Ide_Types.tf_modtime = uu___ @@ -224,7 +224,7 @@ let (deps_and_repl_ld_tasks_of_our_file : else ()); (let uu___4 = let uu___5 = - let uu___6 = FStarC_Compiler_Util.now () in + let uu___6 = FStarC_Compiler_Util.get_time_of_day () in { FStarC_Interactive_Ide_Types.tf_fname = intf; FStarC_Interactive_Ide_Types.tf_modtime = uu___6 diff --git a/ocaml/fstar-lib/generated/FStarC_Main.ml b/ocaml/fstar-lib/generated/FStarC_Main.ml index 24bdc28d43e..b12c3252e99 100644 --- a/ocaml/fstar-lib/generated/FStarC_Main.ml +++ b/ocaml/fstar-lib/generated/FStarC_Main.ml @@ -519,7 +519,7 @@ let main : 'uuuuu . unit -> 'uuuuu = match () with | () -> (setup_hooks (); - (let uu___3 = FStarC_Compiler_Util.record_time go in + (let uu___3 = FStarC_Compiler_Util.record_time_ms go in match uu___3 with | (uu___4, time) -> ((let uu___6 = FStarC_Options.query_stats () in diff --git a/ocaml/fstar-lib/generated/FStarC_Profiling.ml b/ocaml/fstar-lib/generated/FStarC_Profiling.ml index c176a6e0187..b5b601569f6 100644 --- a/ocaml/fstar-lib/generated/FStarC_Profiling.ml +++ b/ocaml/fstar-lib/generated/FStarC_Profiling.ml @@ -86,7 +86,7 @@ let profile : match () with | () -> (FStarC_Compiler_Effect.op_Colon_Equals c.running true; - (let uu___5 = FStarC_Compiler_Util.record_time f in + (let uu___5 = FStarC_Compiler_Util.record_time_ns f in match uu___5 with | (res, elapsed) -> ((let uu___7 = @@ -128,7 +128,9 @@ let (report_human : Prims.string -> counter -> unit) = " (Warning, some operations raised exceptions and we not accounted for)" else "") in let uu___ = - let uu___1 = FStarC_Compiler_Effect.op_Bang c.total_time in + let uu___1 = + let uu___2 = FStarC_Compiler_Effect.op_Bang c.total_time in + uu___2 / (Prims.parse_int "1000000") in FStarC_Compiler_Util.string_of_int uu___1 in FStarC_Compiler_Util.print4 "%s, profiled %s:\t %s ms%s\n" tag c.cid uu___ warn diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml index 03b60e497b9..5a4f2ae8d2b 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml @@ -7863,7 +7863,7 @@ let (encode_query : "Encoding query formula {: %s\n" uu___6 else ()); (let uu___5 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___6 -> FStarC_SMTEncoding_EncodeTerm.encode_formula q1 env1) in diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml index 97dae3f0503..82970f5a79c 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Z3.ml @@ -1292,7 +1292,7 @@ let (z3_job : (fun uu___3 -> match () with | () -> - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___4 -> doZ3Exe log_file r fresh input label_messages queryid)) () diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml index 8d2bc756249..d9b592bdc66 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml @@ -1478,7 +1478,7 @@ let (fresh : unit -> FStarC_BigInt.t FStarC_Tactics_Monad.tac) = let (curms : unit -> FStarC_BigInt.t FStarC_Tactics_Monad.tac) = fun uu___ -> let uu___1 = - let uu___2 = FStarC_Compiler_Util.now_ms () in + let uu___2 = FStarC_Compiler_Util.get_time_of_day_ms () in FStarC_BigInt.of_int_fs uu___2 in ret uu___1 let (__tc : diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml index 433d15a4e45..31568b60bce 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml @@ -1859,7 +1859,7 @@ let meas : FStarC_Tactics_Monad.mk_tac (fun ps -> let uu___ = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___1 -> FStarC_Tactics_Monad.run f ps) in match uu___ with | (r, ms) -> @@ -1968,7 +1968,7 @@ let (curms : unit -> FStarC_BigInt.t FStarC_Tactics_Monad.tac) = fun uu___ -> (fun uu___ -> let uu___1 = - let uu___2 = FStarC_Compiler_Util.now_ms () in + let uu___2 = FStarC_Compiler_Util.get_time_of_day_ms () in FStarC_BigInt.of_int_fs uu___2 in Obj.magic (FStarC_Class_Monad.return FStarC_Tactics_Monad.monad_tac () diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Cfg.ml index 7e078eb6359..675106e440b 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Cfg.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Cfg.ml @@ -2340,13 +2340,13 @@ let (primop_time_reset : unit -> unit) = fun uu___ -> FStarC_Compiler_Util.smap_clear primop_time_map let (primop_time_count : Prims.string -> Prims.int -> unit) = fun nm -> - fun ms -> + fun ns -> let uu___ = FStarC_Compiler_Util.smap_try_find primop_time_map nm in match uu___ with | FStar_Pervasives_Native.None -> - FStarC_Compiler_Util.smap_add primop_time_map nm ms - | FStar_Pervasives_Native.Some ms0 -> - FStarC_Compiler_Util.smap_add primop_time_map nm (ms0 + ms) + FStarC_Compiler_Util.smap_add primop_time_map nm ns + | FStar_Pervasives_Native.Some ns0 -> + FStarC_Compiler_Util.smap_add primop_time_map nm (ns0 + ns) let (fixto : Prims.int -> Prims.string -> Prims.string) = fun n -> fun s -> @@ -2361,7 +2361,7 @@ let (primop_time_report : unit -> Prims.string) = fun uu___ -> let pairs = FStarC_Compiler_Util.smap_fold primop_time_map - (fun nm -> fun ms -> fun rest -> (nm, ms) :: rest) [] in + (fun nm -> fun ns -> fun rest -> (nm, ns) :: rest) [] in let pairs1 = FStarC_Compiler_Util.sort_with (fun uu___1 -> @@ -2372,10 +2372,12 @@ let (primop_time_report : unit -> Prims.string) = (fun uu___1 -> fun rest -> match uu___1 with - | (nm, ms) -> + | (nm, ns) -> let uu___2 = let uu___3 = - let uu___4 = FStarC_Compiler_Util.string_of_int ms in + let uu___4 = + FStarC_Compiler_Util.string_of_int + (ns / (Prims.parse_int "1000000")) in fixto (Prims.of_int (10)) uu___4 in FStarC_Compiler_Util.format2 "%sms --- %s\n" uu___3 nm in FStarC_Compiler_String.op_Hat uu___2 rest) pairs1 "" diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize.ml index 2b21b2161c3..f9782fa8b18 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize.ml @@ -6,7 +6,7 @@ let (dbg_NormRebuild : Prims.bool FStarC_Compiler_Effect.ref) = let (maybe_debug : FStarC_TypeChecker_Cfg.cfg -> FStarC_Syntax_Syntax.term -> - (FStarC_Syntax_Syntax.term * FStarC_Compiler_Util.time) + (FStarC_Syntax_Syntax.term * FStarC_Compiler_Util.time_ns) FStar_Pervasives_Native.option -> unit) = fun cfg -> @@ -17,12 +17,10 @@ let (maybe_debug : then match dbg with | FStar_Pervasives_Native.Some (tm, time_then) -> - let time_now = FStarC_Compiler_Util.now () in + let time_now = FStarC_Compiler_Util.now_ns () in let uu___ = let uu___1 = - let uu___2 = - FStarC_Compiler_Util.time_diff time_then time_now in - FStar_Pervasives_Native.snd uu___2 in + FStarC_Compiler_Util.time_diff_ms time_then time_now in FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___1 in let uu___1 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term tm in @@ -2410,36 +2408,34 @@ let rec (norm : | FStar_Pervasives_Native.Some (s, tm) when is_nbe_request s -> let tm' = closure_as_term cfg env1 tm in - let start = FStarC_Compiler_Util.now () in - let tm_norm = nbe_eval cfg s tm' in - let fin = FStarC_Compiler_Util.now () in - (if - (cfg.FStarC_TypeChecker_Cfg.debug).FStarC_TypeChecker_Cfg.print_normalized - then - (let cfg'1 = - FStarC_TypeChecker_Cfg.config s - cfg.FStarC_TypeChecker_Cfg.tcenv in - let uu___5 = - let uu___6 = - let uu___7 = - FStarC_Compiler_Util.time_diff start fin in - FStar_Pervasives_Native.snd uu___7 in - FStarC_Class_Show.show - FStarC_Class_Show.showable_int uu___6 in - let uu___6 = - FStarC_Class_Show.show - FStarC_Syntax_Print.showable_term tm' in - let uu___7 = - FStarC_Class_Show.show - FStarC_TypeChecker_Cfg.showable_cfg cfg'1 in - let uu___8 = - FStarC_Class_Show.show - FStarC_Syntax_Print.showable_term tm_norm in - FStarC_Compiler_Util.print4 - "NBE result timing (%s ms){\nOn term {\n%s\n}\nwith steps {%s}\nresult is{\n\n%s\n}\n}\n" - uu___5 uu___6 uu___7 uu___8) - else (); - rebuild cfg env1 stack2 tm_norm) + let uu___4 = + FStarC_Compiler_Util.record_time_ms + (fun uu___5 -> nbe_eval cfg s tm') in + (match uu___4 with + | (tm_norm, elapsed) -> + (if + (cfg.FStarC_TypeChecker_Cfg.debug).FStarC_TypeChecker_Cfg.print_normalized + then + (let cfg'1 = + FStarC_TypeChecker_Cfg.config s + cfg.FStarC_TypeChecker_Cfg.tcenv in + let uu___6 = + FStarC_Class_Show.show + FStarC_Class_Show.showable_int elapsed in + let uu___7 = + FStarC_Class_Show.show + FStarC_Syntax_Print.showable_term tm' in + let uu___8 = + FStarC_Class_Show.show + FStarC_TypeChecker_Cfg.showable_cfg cfg'1 in + let uu___9 = + FStarC_Class_Show.show + FStarC_Syntax_Print.showable_term tm_norm in + FStarC_Compiler_Util.print4 + "NBE result timing (%s ms){\nOn term {\n%s\n}\nwith steps {%s}\nresult is{\n\n%s\n}\n}\n" + uu___6 uu___7 uu___8 uu___9) + else (); + rebuild cfg env1 stack2 tm_norm)) | FStar_Pervasives_Native.Some (s, tm) -> (if (cfg.FStarC_TypeChecker_Cfg.debug).FStarC_TypeChecker_Cfg.print_normalized @@ -2585,15 +2581,11 @@ let rec (norm : FStarC_TypeChecker_Cfg.compat_memo_ignore_cfg = (cfg.FStarC_TypeChecker_Cfg.compat_memo_ignore_cfg) } in - let t0 = FStarC_Compiler_Util.now () in - let uu___5 = - FStarC_Compiler_Util.record_time - (fun uu___6 -> norm cfg'1 env1 [] tm) in - match uu___5 with - | (tm_normed, ms) -> - (maybe_debug cfg tm_normed - (FStar_Pervasives_Native.Some (tm, t0)); - rebuild cfg env1 stack2 tm_normed))))) + let t0 = FStarC_Compiler_Util.now_ns () in + let tm_normed = norm cfg'1 env1 [] tm in + maybe_debug cfg tm_normed + (FStar_Pervasives_Native.Some (tm, t0)); + rebuild cfg env1 stack2 tm_normed)))) | FStarC_Syntax_Syntax.Tm_type u -> let u1 = norm_universe cfg env1 u in let uu___2 = @@ -7673,7 +7665,7 @@ let (normalize_with_primitive_steps : t.FStarC_Syntax_Syntax.pos "normalize_with_primitive_steps call" e t; (let uu___8 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___9 -> if is_nbe then nbe_eval c s t else norm c [] [] t) in match uu___8 with @@ -7749,7 +7741,7 @@ let (normalize_comp : (let uu___7 = FStarC_Errors.with_ctx "While normalizing a computation type" (fun uu___8 -> - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___9 -> norm_comp cfg [] c)) in match uu___7 with | (c1, ms) -> diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Rel.ml index 7d56c825e76..105a7af81ee 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Rel.ml @@ -14428,7 +14428,8 @@ let (solve_and_commit : wl.attempting in FStarC_Compiler_Util.print1 "solving problems %s {\n" uu___2 else ()); - (let uu___1 = FStarC_Compiler_Util.record_time (fun uu___2 -> solve wl) in + (let uu___1 = + FStarC_Compiler_Util.record_time_ms (fun uu___2 -> solve wl) in match uu___1 with | (sol, ms) -> ((let uu___3 = FStarC_Compiler_Effect.op_Bang dbg_RelBench in @@ -14440,7 +14441,7 @@ let (solve_and_commit : (match sol with | Success (deferred, defer_to_tac, implicits) -> let uu___3 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___4 -> FStarC_Syntax_Unionfind.commit tx) in (match uu___3 with | ((), ms1) -> @@ -14727,7 +14728,7 @@ let (sub_or_eq_comp : let prob1 = FStarC_TypeChecker_Common.CProb prob in (def_check_prob "sub_comp" prob1; (let uu___5 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___6 -> let uu___7 = solve_and_commit (singleton wl1 prob1 true) diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml index 20b2f2f0b45..76a97476ce6 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml @@ -1894,7 +1894,7 @@ let rec (tc_term : uu___4 uu___5 uu___6 uu___7 else ()); (let uu___2 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___3 -> tc_maybe_toplevel_term { diff --git a/ocaml/fstar-lib/generated/FStarC_Universal.ml b/ocaml/fstar-lib/generated/FStarC_Universal.ml index 5008c09fb9c..da3a6f81e28 100644 --- a/ocaml/fstar-lib/generated/FStarC_Universal.ml +++ b/ocaml/fstar-lib/generated/FStarC_Universal.ml @@ -1150,7 +1150,7 @@ let (tc_one_file : if uu___2 then (FStar_Pervasives_Native.None, Prims.int_zero) else - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___4 -> with_env env1 (fun env2 -> @@ -1164,7 +1164,7 @@ let (tc_one_file : if uu___1 then (env1, Prims.int_zero) else - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___3 -> let uu___4 = with_env env1 @@ -1173,7 +1173,12 @@ let (tc_one_file : tcmod) in match uu___4 with | (env2, uu___5) -> env2) in let tc_source_file uu___1 = - let uu___2 = parse env pre_fn fn in + let uu___2 = + let uu___3 = + let uu___4 = FStarC_Parser_Dep.module_name_of_file fn in + FStar_Pervasives_Native.Some uu___4 in + FStarC_Profiling.profile (fun uu___4 -> parse env pre_fn fn) + uu___3 "FStarC.Universal.tc_source_file.parse" in match uu___2 with | (fmod, env1) -> let mii = @@ -1223,7 +1228,7 @@ let (tc_one_file : fmod.FStarC_Syntax_Syntax.name in FStar_Pervasives_Native.Some uu___6 in FStarC_Profiling.profile (fun uu___6 -> check env1) - uu___5 "FStarC.Universal.tc_source_file" in + uu___5 "FStarC.Universal.tc_source_file.check" in match uu___4 with | ((tcmod, smt_decls), env2) -> let tc_time = Prims.int_zero in diff --git a/ocaml/fstar-tests/generated/FStarC_Tests_Data.ml b/ocaml/fstar-tests/generated/FStarC_Tests_Data.ml index b3fe2acc290..e8d6506bdb1 100644 --- a/ocaml/fstar-tests/generated/FStarC_Tests_Data.ml +++ b/ocaml/fstar-tests/generated/FStarC_Tests_Data.ml @@ -48,7 +48,7 @@ let (run_all : unit -> unit) = fun uu___ -> FStarC_Compiler_Util.print_string "data tests\n"; (let uu___2 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___3 -> let uu___4 = Obj.magic @@ -65,7 +65,7 @@ let (run_all : unit -> unit) = FStarC_Class_Show.show FStarC_Class_Show.showable_int ms in FStarC_Compiler_Util.print1 "FlatSet insert: %s\n" uu___4); (let uu___4 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___5 -> all_mem nn (FStarC_Compiler_FlatSet.setlike_flat_set @@ -76,7 +76,7 @@ let (run_all : unit -> unit) = FStarC_Class_Show.show FStarC_Class_Show.showable_int ms1 in FStarC_Compiler_Util.print1 "FlatSet all_mem: %s\n" uu___6); (let uu___6 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___7 -> all_remove nn (FStarC_Compiler_FlatSet.setlike_flat_set @@ -102,7 +102,7 @@ let (run_all : unit -> unit) = then failwith "FlatSet all_remove failed" else ()); (let uu___10 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___11 -> let uu___12 = Obj.magic @@ -121,7 +121,7 @@ let (run_all : unit -> unit) = FStarC_Compiler_Util.print1 "RBSet insert: %s\n" uu___12); (let uu___12 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___13 -> all_mem nn (FStarC_Compiler_RBSet.setlike_rbset @@ -134,7 +134,7 @@ let (run_all : unit -> unit) = FStarC_Compiler_Util.print1 "RBSet all_mem: %s\n" uu___14); (let uu___14 = - FStarC_Compiler_Util.record_time + FStarC_Compiler_Util.record_time_ms (fun uu___15 -> all_remove nn (FStarC_Compiler_RBSet.setlike_rbset diff --git a/src/basic/FStarC.Compiler.Util.fsti b/src/basic/FStarC.Compiler.Util.fsti index 880adc8a5b0..b60fe411c12 100644 --- a/src/basic/FStarC.Compiler.Util.fsti +++ b/src/basic/FStarC.Compiler.Util.fsti @@ -25,14 +25,19 @@ exception Impos val max_int: int val return_all: 'a -> ML 'a -type time -val now : unit -> time -val now_ms : unit -> int -val time_diff: time -> time -> float&int -val record_time: (unit -> 'a) -> ('a & int) -val is_before: time -> time -> bool -val get_file_last_modification_time: string -> time -val string_of_time: time -> string +type time_ns +val now_ns : unit -> time_ns +val time_diff_ms: time_ns -> time_ns -> int +val time_diff_ns: time_ns -> time_ns -> int +val record_time_ns: (unit -> 'a) -> ('a & int) +val record_time_ms: (unit -> 'a) -> ('a & int) + +type time_of_day +val get_time_of_day : unit -> time_of_day +val get_time_of_day_ms : unit -> int +val is_before: time_of_day -> time_of_day -> bool +val get_file_last_modification_time: string -> time_of_day +val string_of_time_of_day: time_of_day -> string (* generic utils *) (* smap: map from string keys *) diff --git a/src/basic/FStarC.Profiling.fst b/src/basic/FStarC.Profiling.fst index a2e8e2e2390..e079244e1b8 100644 --- a/src/basic/FStarC.Profiling.fst +++ b/src/basic/FStarC.Profiling.fst @@ -74,7 +74,7 @@ let profile (f: unit -> 'a) (module_name:option string) (cid:string) : 'a = else begin try c.running := true; //mark the counter as running - let res, elapsed = BU.record_time f in + let res, elapsed = BU.record_time_ns f in c.total_time := !c.total_time + elapsed; //accumulate the time c.running := false; //finally mark the counter as not running res @@ -105,7 +105,7 @@ let report_human tag c = BU.print4 "%s, profiled %s:\t %s ms%s\n" tag c.cid - (BU.string_of_int (!c.total_time)) + (BU.string_of_int (!c.total_time / 1000000)) warn let report tag c = diff --git a/src/fstar/FStarC.Interactive.Ide.Types.fst b/src/fstar/FStarC.Interactive.Ide.Types.fst index b032e8ebdce..8da8938fb4b 100644 --- a/src/fstar/FStarC.Interactive.Ide.Types.fst +++ b/src/fstar/FStarC.Interactive.Ide.Types.fst @@ -89,7 +89,7 @@ type optmod_t = option Syntax.Syntax.modul type timed_fname = { tf_fname: string; - tf_modtime: time } + tf_modtime: time_of_day } (** Every snapshot pushed in the repl stack is annotated with one of these. The ``LD``-prefixed (“Load Dependency”) onces are useful when loading or updating @@ -166,7 +166,7 @@ type grepl_state = { grepl_repls: U.psmap repl_state; grepl_stdin: stream_reader (* REPL tasks and states *) (*************************) -let t0 = Util.now () +let t0 = Util.get_time_of_day () (** Create a timed_fname with a dummy modtime **) let dummy_tf_of_fname fname = @@ -175,7 +175,7 @@ let dummy_tf_of_fname fname = let string_of_timed_fname { tf_fname = fname; tf_modtime = modtime } = if modtime = t0 then Util.format1 "{ %s }" fname - else Util.format2 "{ %s; %s }" fname (string_of_time modtime) + else Util.format2 "{ %s; %s }" fname (string_of_time_of_day modtime) let string_of_repl_task = function | LDInterleaved (intf, impl) -> diff --git a/src/fstar/FStarC.Interactive.Legacy.fst b/src/fstar/FStarC.Interactive.Legacy.fst index b5355d831da..8bc35d721b5 100644 --- a/src/fstar/FStarC.Interactive.Legacy.fst +++ b/src/fstar/FStarC.Interactive.Legacy.fst @@ -240,7 +240,7 @@ let deps_of_our_file filename = deps, maybe_intf, dep_graph (* .fsti name (optional) * .fst name * .fsti recorded timestamp (optional) * .fst recorded timestamp *) -type m_timestamps = list (option string & string & option time & time) +type m_timestamps = list (option string & string & option time_of_day & time_of_day) (* * type check remaining dependencies and record the timestamps. @@ -286,7 +286,7 @@ let rec tc_deps (m:modul_t) (stack:stack_t) *) let update_deps (filename:string) (m:modul_t) (stk:stack_t) (env:env_t) (ts:m_timestamps) : (stack_t & env_t & m_timestamps) = - let is_stale (intf:option string) (impl:string) (intf_t:option time) (impl_t:time) :bool = + let is_stale (intf:option string) (impl:string) (intf_t:option time_of_day) (impl_t:time_of_day) :bool = let impl_mt = get_file_last_modification_time impl in (is_before impl_t impl_mt || (match intf, intf_t with diff --git a/src/fstar/FStarC.Interactive.PushHelper.fst b/src/fstar/FStarC.Interactive.PushHelper.fst index d37566e62f6..8f3f34bc9d9 100644 --- a/src/fstar/FStarC.Interactive.PushHelper.fst +++ b/src/fstar/FStarC.Interactive.PushHelper.fst @@ -47,7 +47,7 @@ let set_check_kind env check_kind = (** Build a list of dependency loading tasks from a list of dependencies **) let repl_ld_tasks_of_deps (deps: list string) (final_tasks: list repl_task) = - let wrap fname = { tf_fname = fname; tf_modtime = U.now () } in + let wrap fname = { tf_fname = fname; tf_modtime = U.get_time_of_day () } in let rec aux (deps:list string) (final_tasks:list repl_task) : list repl_task = match deps with @@ -86,7 +86,7 @@ let deps_and_repl_ld_tasks_of_our_file filename if not (Parser.Dep.is_implementation impl) then raise_error0 Errors.Fatal_MissingImplementation (U.format1 "Expecting an implementation, got %s" impl); - [LDInterfaceOfCurrentFile ({ tf_fname = intf; tf_modtime = U.now () }) ] + [LDInterfaceOfCurrentFile ({ tf_fname = intf; tf_modtime = U.get_time_of_day () }) ] | [impl] -> [] | _ -> diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index f3f0d8f3c15..061d34c4abc 100644 --- a/src/fstar/FStarC.Main.fst +++ b/src/fstar/FStarC.Main.fst @@ -362,7 +362,7 @@ let handle_error e = let main () = try setup_hooks (); - let _, time = Util.record_time go in + let _, time = Util.record_time_ms go in if FStarC.Options.query_stats() then Util.print2_error "TOTAL TIME %s ms: %s\n" (FStarC.Compiler.Util.string_of_int time) diff --git a/src/fstar/FStarC.Universal.fst b/src/fstar/FStarC.Universal.fst index 944c4026882..c6436407bf3 100644 --- a/src/fstar/FStarC.Universal.fst +++ b/src/fstar/FStarC.Universal.fst @@ -381,7 +381,7 @@ let tc_one_file | Some tgt -> if not (Options.should_extract (string_of_lid tcmod.name) tgt) then None, 0 - else FStarC.Compiler.Util.record_time (fun () -> + else FStarC.Compiler.Util.record_time_ms (fun () -> with_env env (fun env -> let _, defs = FStarC.Extraction.ML.Modul.extract env tcmod in defs) @@ -391,14 +391,18 @@ let tc_one_file if Options.codegen() = None then env, 0 else - FStarC.Compiler.Util.record_time (fun () -> + FStarC.Compiler.Util.record_time_ms (fun () -> let env, _ = with_env env (fun env -> FStarC.Extraction.ML.Modul.extract_iface env tcmod) in env ) in let tc_source_file () = - let fmod, env = parse env pre_fn fn in + let fmod, env = + Profiling.profile (fun () -> parse env pre_fn fn) + (Some (Parser.Dep.module_name_of_file fn)) + "FStarC.Universal.tc_source_file.parse" + in let mii = FStarC.Syntax.DsEnv.inclusion_info (tcenv_of_uenv env).dsenv fmod.name in let check_mod () = let check env = @@ -422,7 +426,7 @@ let tc_one_file let ((tcmod, smt_decls), env) = Profiling.profile (fun () -> check env) (Some (string_of_lid fmod.name)) - "FStarC.Universal.tc_source_file" + "FStarC.Universal.tc_source_file.check" in let tc_time = 0 in diff --git a/src/parser/FStarC.Parser.ParseIt.fsti b/src/parser/FStarC.Parser.ParseIt.fsti index e0c5a35758a..0b8e2250a66 100644 --- a/src/parser/FStarC.Parser.ParseIt.fsti +++ b/src/parser/FStarC.Parser.ParseIt.fsti @@ -30,11 +30,11 @@ type input_frag = { frag_col:int } -val read_vfs_entry : string -> option (time & string) +val read_vfs_entry : string -> option (time_of_day & string) // This lets the ide tell us about edits not (yet) reflected on disk. val add_vfs_entry: fname:string -> contents:string -> unit // This reads mtimes from the VFS as well -val get_file_last_modification_time: fname:string -> time +val get_file_last_modification_time: fname:string -> time_of_day type parse_frag = | Filename of filename diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fst b/src/smtencoding/FStarC.SMTEncoding.Encode.fst index a3ebb108bcc..f3f86800565 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Encode.fst @@ -2016,7 +2016,7 @@ let encode_query use_env_msg (tcenv:Env.env) (q:S.term) let env_decls, env = encode_env_bindings env bindings in if Debug.medium () || !dbg_SMTEncoding || !dbg_SMTQuery then BU.print1 "Encoding query formula {: %s\n" (show q); - let (phi, qdecls), ms = BU.record_time (fun () -> encode_formula q env) in + let (phi, qdecls), ms = BU.record_time_ms (fun () -> encode_formula q env) in let labels, phi = ErrorReporting.label_goals use_env_msg (Env.get_range tcenv) phi in let label_prefix, label_suffix = encode_labels labels in let caption = diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst index de6399816e5..7ed10b12e91 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Z3.fst @@ -752,7 +752,7 @@ let z3_job Profiling.profile (fun () -> try - BU.record_time (fun () -> doZ3Exe log_file r fresh input label_messages queryid) + BU.record_time_ms (fun () -> doZ3Exe log_file r fresh input label_messages queryid) with e -> refresh None; //refresh the solver but don't handle the exception; it'll be caught upstream raise e diff --git a/src/tactics/FStarC.Tactics.V1.Basic.fst b/src/tactics/FStarC.Tactics.V1.Basic.fst index f01556caa79..8ee648da06a 100644 --- a/src/tactics/FStarC.Tactics.V1.Basic.fst +++ b/src/tactics/FStarC.Tactics.V1.Basic.fst @@ -596,7 +596,7 @@ let fresh () : tac Z.t = ret (Z.of_int_fs n))) let curms () : tac Z.t = - ret (BU.now_ms () |> Z.of_int_fs) + ret (BU.get_time_of_day_ms () |> Z.of_int_fs) (* Annoying duplication here *) let __tc (e : env) (t : term) : tac (term & typ & guard_t) = diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fst b/src/tactics/FStarC.Tactics.V2.Basic.fst index b80fdf161d5..1b5e04a735d 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fst +++ b/src/tactics/FStarC.Tactics.V2.Basic.fst @@ -578,7 +578,7 @@ let is_false t = let meas (s:string) (f : tac 'a) : tac 'a = mk_tac (fun ps -> - let (r, ms) = BU.record_time (fun () -> Tactics.Monad.run f ps) in + let (r, ms) = BU.record_time_ms (fun () -> Tactics.Monad.run f ps) in BU.print2 "++ Tactic %s ran in \t\t%sms\n" s (show ms); r) @@ -606,7 +606,7 @@ let fresh () : tac Z.t = return (Z.of_int_fs n) let curms () : tac Z.t = - return (BU.now_ms () |> Z.of_int_fs) + return (BU.get_time_of_day_ms () |> Z.of_int_fs) (* Annoying duplication here *) let __tc (e : env) (t : term) : tac (term & typ & guard_t) = diff --git a/src/tests/FStarC.Tests.Data.fst b/src/tests/FStarC.Tests.Data.fst index 6e2a6853b9f..07f22ca9947 100644 --- a/src/tests/FStarC.Tests.Data.fst +++ b/src/tests/FStarC.Tests.Data.fst @@ -44,21 +44,21 @@ let nn = 10000 let run_all () = BU.print_string "data tests\n"; - let (f, ms) = BU.record_time (fun () -> insert nn (empty () <: FlatSet.t int)) in + let (f, ms) = BU.record_time_ms (fun () -> insert nn (empty () <: FlatSet.t int)) in BU.print1 "FlatSet insert: %s\n" (show ms); - let (f_ok, ms) = BU.record_time (fun () -> all_mem nn f) in + let (f_ok, ms) = BU.record_time_ms (fun () -> all_mem nn f) in BU.print1 "FlatSet all_mem: %s\n" (show ms); - let (f, ms) = BU.record_time (fun () -> all_remove nn f) in + let (f, ms) = BU.record_time_ms (fun () -> all_remove nn f) in BU.print1 "FlatSet all_remove: %s\n" (show ms); if not f_ok then failwith "FlatSet all_mem failed"; if not (is_empty f) then failwith "FlatSet all_remove failed"; - let (rb, ms) = BU.record_time (fun () -> insert nn (empty () <: RBSet.t int)) in + let (rb, ms) = BU.record_time_ms (fun () -> insert nn (empty () <: RBSet.t int)) in BU.print1 "RBSet insert: %s\n" (show ms); - let (rb_ok, ms) = BU.record_time (fun () -> all_mem nn rb) in + let (rb_ok, ms) = BU.record_time_ms (fun () -> all_mem nn rb) in BU.print1 "RBSet all_mem: %s\n" (show ms); - let (rb, ms) = BU.record_time (fun () -> all_remove nn rb) in + let (rb, ms) = BU.record_time_ms (fun () -> all_remove nn rb) in BU.print1 "RBSet all_remove: %s\n" (show ms); if not rb_ok then failwith "RBSet all_mem failed"; diff --git a/src/typechecker/FStarC.TypeChecker.Cfg.fst b/src/typechecker/FStarC.TypeChecker.Cfg.fst index 39d23fc07f7..7b3d35965e2 100644 --- a/src/typechecker/FStarC.TypeChecker.Cfg.fst +++ b/src/typechecker/FStarC.TypeChecker.Cfg.fst @@ -302,10 +302,10 @@ let primop_time_map : BU.smap int = BU.smap_create 50 let primop_time_reset () = BU.smap_clear primop_time_map -let primop_time_count (nm : string) (ms : int) : unit = +let primop_time_count (nm : string) (ns : int) : unit = match BU.smap_try_find primop_time_map nm with - | None -> BU.smap_add primop_time_map nm ms - | Some ms0 -> BU.smap_add primop_time_map nm (ms0 + ms) + | None -> BU.smap_add primop_time_map nm ns + | Some ns0 -> BU.smap_add primop_time_map nm (ns0 + ns) let fixto n s = if String.length s < n @@ -313,9 +313,9 @@ let fixto n s = else s let primop_time_report () : string = - let pairs = BU.smap_fold primop_time_map (fun nm ms rest -> (nm, ms)::rest) [] in + let pairs = BU.smap_fold primop_time_map (fun nm ns rest -> (nm, ns)::rest) [] in let pairs = BU.sort_with (fun (_, t1) (_, t2) -> t1 - t2) pairs in - List.fold_right (fun (nm, ms) rest -> (BU.format2 "%sms --- %s\n" (fixto 10 (BU.string_of_int ms)) nm) ^ rest) pairs "" + List.fold_right (fun (nm, ns) rest -> (BU.format2 "%sms --- %s\n" (fixto 10 (BU.string_of_int (ns / 1000000))) nm) ^ rest) pairs "" let extendable_primops_dirty : ref bool = BU.mk_ref true diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst index 0432f64f2ef..ccf13ab27f6 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fst @@ -65,15 +65,15 @@ let dbg_NormRebuild = Debug.get_toggle "NormRebuild" * Higher-Order Symb Comput (2007) 20: 209–230 **********************************************************************************************) -let maybe_debug (cfg:Cfg.cfg) (t:term) (dbg:option (term & BU.time)) = +let maybe_debug (cfg:Cfg.cfg) (t:term) (dbg:option (term & BU.time_ns)) = if cfg.debug.print_normalized then match dbg with | Some (tm, time_then) -> - let time_now = BU.now () in + let time_now = BU.now_ns () in // BU.print1 "Normalizer result timing (%s ms)\n" // (show (snd (BU.time_diff time_then time_now))) BU.print4 "Normalizer result timing (%s ms){\nOn term {\n%s\n}\nwith steps {%s}\nresult is{\n\n%s\n}\n}\n" - (show (snd (BU.time_diff time_then time_now))) + (show (BU.time_diff_ms time_then time_now)) (show tm) (show cfg) (show t) @@ -415,8 +415,8 @@ let reduce_primops norm_cb cfg (env:env) tm : term & bool = } in let r = if false - then begin let (r, ms) = BU.record_time (fun () -> prim_step.interpretation psc norm_cb universes args_1) in - primop_time_count (show fv.fv_name.v) ms; + then begin let (r, ns) = BU.record_time_ns (fun () -> prim_step.interpretation psc norm_cb universes args_1) in + primop_time_count (show fv.fv_name.v) ns; r end else prim_step.interpretation psc norm_cb universes args_1 @@ -981,16 +981,14 @@ let rec norm : cfg -> env -> stack -> term -> term = | Some (s, tm) when is_nbe_request s -> let tm' = closure_as_term cfg env tm in - let start = BU.now() in - let tm_norm = nbe_eval cfg s tm' in - let fin = BU.now () in + let tm_norm, elapsed = BU.record_time_ms (fun _ -> nbe_eval cfg s tm') in if cfg.debug.print_normalized then begin let cfg' = Cfg.config s cfg.tcenv in // BU.print1 "NBE result timing (%s ms)\n" // (show (snd (BU.time_diff start fin))) BU.print4 "NBE result timing (%s ms){\nOn term {\n%s\n}\nwith steps {%s}\nresult is{\n\n%s\n}\n}\n" - (show (snd (BU.time_diff start fin))) + (show elapsed) (show tm') (show cfg') (show tm_norm) @@ -1020,8 +1018,8 @@ let rec norm : cfg -> env -> stack -> term -> term = (* We reduce the term in an empty stack to prevent unwanted interactions. Later, we rebuild the normalized term with the current stack. This is not a tail-call, but this happens rarely enough that it should not be a problem. *) - let t0 = BU.now () in - let (tm_normed, ms) = BU.record_time (fun () -> norm cfg' env [] tm) in + let t0 = BU.now_ns () in + let tm_normed = norm cfg' env [] tm in maybe_debug cfg tm_normed (Some (tm, t0)); rebuild cfg env stack tm_normed end @@ -2765,7 +2763,7 @@ let normalize_with_primitive_steps ps s e (t:term) = log_top c (fun () -> BU.print1 ">>> cfg = %s\n" (show c)); def_check_scoped t.pos "normalize_with_primitive_steps call" e t; let (r, ms) = - BU.record_time (fun () -> + BU.record_time_ms (fun () -> if is_nbe then nbe_eval c s t else norm c [] [] t @@ -2792,7 +2790,7 @@ let normalize_comp s e c = log_top cfg (fun () -> BU.print1 ">>> cfg = %s\n" (show cfg)); def_check_scoped c.pos "normalize_comp call" e c; let (c, ms) = Errors.with_ctx "While normalizing a computation type" (fun () -> - BU.record_time (fun () -> + BU.record_time_ms (fun () -> norm_comp cfg [] c)) in log_top cfg (fun () -> BU.print2 "}\nNormalization result = (%s) in %s ms\n" (show c) (show ms)); diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index 3487afbafd2..d6c2ae1ab47 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -4836,13 +4836,13 @@ let solve_and_commit wl err if !dbg_RelBench then BU.print1 "solving problems %s {\n" (FStarC.Common.string_of_list (fun p -> string_of_int (p_pid p)) wl.attempting); - let (sol, ms) = BU.record_time (fun () -> solve wl) in + let (sol, ms) = BU.record_time_ms (fun () -> solve wl) in if !dbg_RelBench then BU.print1 "} solved in %s ms\n" (string_of_int ms); match sol with | Success (deferred, defer_to_tac, implicits) -> - let ((), ms) = BU.record_time (fun () -> UF.commit tx) in + let ((), ms) = BU.record_time_ms (fun () -> UF.commit tx) in if !dbg_RelBench then BU.print1 "committed in %s ms\n" (string_of_int ms); Some (deferred, defer_to_tac, implicits) @@ -4925,7 +4925,7 @@ let sub_or_eq_comp env (use_eq:bool) c1 c2 = let wl = { wl with repr_subcomp_allowed = true } in let prob = CProb prob in def_check_prob "sub_comp" prob; - let (r, ms) = BU.record_time + let (r, ms) = BU.record_time_ms (fun () -> with_guard env prob <| solve_and_commit (singleton wl prob true) (fun _ -> None)) in if !dbg_Rel || !dbg_RelTop || !dbg_RelBench then diff --git a/src/typechecker/FStarC.TypeChecker.TcTerm.fst b/src/typechecker/FStarC.TypeChecker.TcTerm.fst index 19a73ddfd62..a2bbd9f07c8 100644 --- a/src/typechecker/FStarC.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStarC.TypeChecker.TcTerm.fst @@ -738,7 +738,7 @@ let rec tc_term env e = (tag_of (SS.compress e)) (print_expected_ty_str env); - let r, ms = BU.record_time (fun () -> + let r, ms = BU.record_time_ms (fun () -> tc_maybe_toplevel_term ({env with top_level=false}) e) in if Debug.medium () then begin BU.print4 "(%s) } tc_term of %s (%s) took %sms\n" (Range.string_of_range <| Env.get_range env)