Making debug toggles more efficient

[mtzguido]

Currently, to check if a given debug_level is enabled for a given module, we need to traverse two lists (see Options.debug_at_level) comparing each element for equality. This is not normally bad, as both lists are empty, but as soon as we set any kind of debugging everything becomes slower. Compare for instance:

$ ramon -p 0 -q ./bin/fstar.exe ulib/FStar.Tactics.V2.fst --cache_off --admit_smt_queries true -f >/dev/null
[...]ramon: group.total          3.700s
ramon: group.mempeak        326MiB
ramon: group.pidpeak        4
ramon: status               exited
ramon: exitcode             0
ramon: walltime             3.721s
ramon: loadavg              0.99
$ ramon -p 0 -q ./bin/fstar.exe ulib/FStar.Tactics.V2.fst --cache_off --admit_smt_queries true -f --debug y >/dev/null
[...]
ramon: group.total          6.734s
ramon: group.mempeak        322MiB
ramon: group.pidpeak        4
ramon: status               exited
ramon: exitcode             0
ramon: walltime             6.760s
ramon: loadavg              1.00

adding more flags makes it worse.

This PR introduces a new FStar.Compiler.Debug in which we can register debug toggles, at initialization time, and then query them in constant time. The main function of interest is now

(* Obtain the toggle for a given debug key *)
val get_toggle (k : string) : ref bool

which can (and should only) be called from a top-level definition to obtain a reference. Calling get_toggle repeatedly with the same key will return the exact same reference, so many modules can use the same key without coordinating. (This function can be made more efficient --it's currently traversing a list-- but it anyway happens only once, during program startup time.) Then, the toggle can be queried just by looking at the reference. See this for how to use it:

diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst
index 268f03d481..16770cf6dc 100644
--- a/src/extraction/FStar.Extraction.ML.Modul.fst
+++ b/src/extraction/FStar.Extraction.ML.Modul.fst
@@ -50,6 +50,8 @@ module EMB    = FStar.Syntax.Embeddings
 module Cfg    = FStar.TypeChecker.Cfg
 module PO     = FStar.TypeChecker.Primops
 
+let dbg_ExtractionReify = Debug.get_toggle "ExtractionReify"
+
 type tydef_declaration = (mlsymbol * FStar.Extraction.ML.Syntax.metadata * int) //int is the arity
 
 type iface = {
@@ -554,7 +556,7 @@ let extract_reifiable_effect g ed
     in
 
     let rec extract_fv tm =
-        if Env.debug (tcenv_of_uenv g) <| Options.Other "ExtractionReify" then
+        if !dbg_ExtractionReify then
             BU.print1 "extract_fv term: %s\n" (Print.term_to_string tm);
         match (SS.compress tm).n with
         | Tm_uinst (tm, _) -> extract_fv tm
@@ -569,7 +571,7 @@ let extract_reifiable_effect g ed
 
     let extract_action g (a:S.action) =
         assert (match a.action_params with | [] -> true | _ -> false);
-        if Env.debug (tcenv_of_uenv g) <| Options.Other "ExtractionReify" then
+        if !dbg_ExtractionReify then
             BU.print2 "Action type %s and term %s\n"
             (Print.term_to_string a.action_typ)
             (Print.term_to_string a.action_defn);

With this change performance is much better:

$ ramon -p 0 -q ./bin/fstar.exe ulib/FStar.Tactics.V2.fst --cache_off --admit_smt_queries true -f --debug . >/dev/null
[...]
ramon: group.total          3.487s
ramon: group.mempeak        328MiB
ramon: group.pidpeak        4
ramon: status               exited
ramon: exitcode             0
ramon: walltime             3.523s
ramon: loadavg              0.99

--

I also changed the behavior of --debug. Now it takes toggle names (or Low/High/Medium/Extreme) instead of a module. F* assumes you're only interested in debugging the current module (i.e. whenever Options.should_check()) is on, but you can also provide --debug_all_modules to force debugging everywhere. The logic handling this is in FStar.TypeChecker.Tc, which resets the debug toggles when switching modules.

Another advantage is that we can now list all toggles easily, as they registered during program initialization. So I added --list_debug_keys:

$ ./bin/fstar.exe --list_debug_keys 
2635
380
Bind
CheckedFiles
Coercions
Core
CoreEq
CoreExit
CoreTop
Dec
[...]

Something to consider is whether we should add some hierarchy to the keys.