Remove global symbol generator

Rather than having a global symbol generating function gensym used
throughout the C backend, instead 'generate' them as needed like:

let (gensym, reset_gensym_counter) = symbol_generator "gs"

This just makes things a bit neater and means we can reset the counter
between definitions in jib_compile without worrying about other modules
relying on global uniqueness

7 files changed, 20 insertions, 16 deletions

diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 216c402e..52c4584c 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -482,15 +482,7 @@ let ae_lit lit typ = AE_val (AV_lit (lit, typ))
 
 let is_dead_aexp (AE_aux (_, env, _)) = prove __POS__ env nc_false
 
-(** GLOBAL: gensym_counter is used to generate fresh identifiers where
-   needed. It should be safe to reset between top level
-   definitions. **)
-let gensym_counter = ref 0
-
-let gensym () =
-  let id = mk_id ("gs#" ^ string_of_int !gensym_counter) in
-  incr gensym_counter;
-  id
+let (gensym, _) = symbol_generator "anf"
 
 let rec split_block l = function
   | [exp] -> [], exp
diff --git a/src/jib/anf.mli b/src/jib/anf.mli
index 3ce0b286..f28cf420 100644
--- a/src/jib/anf.mli
+++ b/src/jib/anf.mli
@@ -129,10 +129,6 @@ and 'a aval =
   | AV_record of ('a aval) Bindings.t * 'a
   | AV_cval of cval * 'a
 
-(** Function for generating unique identifiers during ANF
-   translation. *)
-val gensym : unit -> id
-
 (** {2 Functions for transforming ANF expressions} *)
 
 val aval_typ : typ aval -> typ
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index aceb32de..bf22c5d2 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -90,6 +90,9 @@ let optimize_alias = ref false
 let optimize_fixed_int = ref false
 let optimize_fixed_bits = ref false
 
+let (gensym, _) = symbol_generator "cb"
+let ngensym () = name (gensym ())
+
 let c_debug str =
   if !c_verbosity > 0 then prerr_endline (Lazy.force str) else ()
 
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 23208e4a..1a0411aa 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -62,6 +62,7 @@ let opt_memo_cache = ref false
 
 let optimize_aarch64_fast_struct = ref false
 
+let (gensym, reset_gensym_counter) = symbol_generator "gs"
 let ngensym () = name (gensym ())
 
 (**************************************************************************)
@@ -1259,6 +1260,7 @@ let compile_funcl ctx id pat guard exp =
 
 (** Compile a Sail toplevel definition into an IR definition **)
 let rec compile_def n total ctx def =
+  reset_gensym_counter ();
   match def with
   | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), _))
        when !opt_memo_cache ->
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 1a39e9b6..d4e67daa 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -65,8 +65,6 @@ val opt_debug_flow_graphs : bool ref
    ARM v8.5 spec. *)
 val optimize_aarch64_fast_struct : bool ref
 
-val ngensym : unit -> name
-
 (** {2 Jib context} *)
 
 (** Context for compiling Sail to Jib. We need to pass a (global)
diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
index 37ae753f..28ec40b9 100644
--- a/src/jib/jib_smt_fuzz.ml
+++ b/src/jib/jib_smt_fuzz.ml
@@ -55,6 +55,9 @@ open Jib_smt
 open Jib_util
 open Smtlib
 
+let (gensym, _) = symbol_generator "fuzz"
+let ngensym () = name (gensym ())
+
 let gen_value (Typ_aux (aux, _) as typ) =
   match aux with
   | Typ_id id when string_of_id id = "bit" ->
@@ -183,7 +186,7 @@ let fuzz_cdef ctx all_cdefs = function
                  in
 
                  let jib =
-                   let gs = Jib_compile.ngensym () in
+                   let gs = ngensym () in
                    [ifuncall (CL_id (gs, ret_ctyp)) id (List.map snd values)]
                    @ gen_assertion ret_ctyp result gs
                    @ [iend ()]
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 4227a436..a1dac297 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -54,6 +54,16 @@ open Jib
 open Value2
 open PPrint
 
+let symbol_generator str =
+  let counter = ref 0 in
+  let gensym () =
+    let id = mk_id (str ^ "#" ^ string_of_int !counter) in
+    incr counter;
+    id
+  in
+  let reset () = counter := 0 in
+  (gensym, reset)
+
 (* Define wrappers for creating bytecode instructions. Each function
    uses a counter to assign each instruction a unique identifier. *)