Remove the cparser/Builtins module

Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).

Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.

19 files changed, 82 insertions, 104 deletions

diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index ec4f4aaa..d6a1ea35 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -18,10 +18,10 @@
 open C
 
 let builtins = {
-  Builtins.typedefs = [
+  builtin_typedefs = [
     "__builtin_va_list", TPtr(TVoid [], [])
   ];
-  Builtins.functions = [
+  builtin_functions = [
     (* Integer arithmetic *)
     "__builtin_clz",
       (TInt(IInt, []), [TInt(IUInt, [])], false);
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index b81bd022..4d0e52e1 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -155,8 +155,8 @@ let ais_annot_functions =
     []
 
 let builtins_generic = {
-  Builtins.typedefs = [];
-  Builtins.functions =
+  builtin_typedefs = [];
+  builtin_functions =
     ais_annot_functions
       @
     [
@@ -300,9 +300,12 @@ let builtins_generic = {
 
 (* Add processor-dependent builtins *)
 
-let builtins =
-  Builtins.({ typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs;
-    functions = builtins_generic.Builtins.functions @ CBuiltins.builtins.functions })
+let builtins = {
+  builtin_typedefs =
+    builtins_generic.builtin_typedefs @ CBuiltins.builtins.builtin_typedefs;
+  builtin_functions =
+    builtins_generic.builtin_functions @ CBuiltins.builtins.builtin_functions
+}
 
 (** ** The known attributes *)
 
@@ -1233,7 +1236,7 @@ let convertFundecl env (sto, id, ty, optinit) =
     if id.name = "free" then AST.EF_free else
     if Str.string_match re_runtime id.name 0 then  AST.EF_runtime(id'', sg) else
     if Str.string_match re_builtin id.name 0
-    && List.mem_assoc id.name builtins.Builtins.functions
+    && List.mem_assoc id.name builtins.builtin_functions
     then AST.EF_builtin(id'', sg)
     else AST.EF_external(id'', sg) in
   (id',  AST.Gfun(Ctypes.External(ef, args, res, cconv)))
@@ -1432,7 +1435,7 @@ let convertProgram p =
   Hashtbl.clear decl_atom;
   Hashtbl.clear stringTable;
   Hashtbl.clear wstringTable;
-  let p = cleanupGlobals (Builtins.declarations() @ p) in
+  let p = cleanupGlobals (Env.initial_declarations() @ p) in
   try
     let env = translEnv Env.empty p in
     let typs = convertCompositedefs env [] p in
diff --git a/cparser/Builtins.ml b/cparser/Builtins.ml
deleted file mode 100644
index 8eb1abfd..00000000
--- a/cparser/Builtins.ml
+++ /dev/null
@@ -1,54 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Compiler built-ins *)
-
-open C
-open Cutil
-
-let env = ref Env.empty
-let idents = ref []
-let decls = ref []
-
-let environment () = !env
-let identifiers () = !idents
-let declarations () = List.rev !decls
-
-let add_typedef (s, ty) =
-  let (id, env') = Env.enter_typedef !env s ty in
-  env := env';
-  idents := id :: !idents;
-  decls := {gdesc = Gtypedef(id, ty); gloc = no_loc} :: !decls
-
-let add_function (s, (res, args, va)) =
-  let ty =
-    TFun(res,
-         Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
-         va, []) in
-  let (id, env') = Env.enter_ident !env s Storage_extern ty in
-  env := env';
-  idents := id :: !idents;
-  decls := {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
-
-type t = {
-  typedefs: (string * C.typ) list;
-  functions: (string * (C.typ * C.typ list * bool)) list
-}
-
-let set blt =
-  env := Env.empty;
-  idents := [];
-  List.iter add_typedef blt.typedefs;
-  List.iter add_function blt.functions
diff --git a/cparser/Builtins.mli b/cparser/Builtins.mli
deleted file mode 100644
index 7f9d78a9..00000000
--- a/cparser/Builtins.mli
+++ /dev/null
@@ -1,25 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-val environment: unit -> Env.t
-val identifiers: unit -> C.ident list
-val declarations: unit -> C.globdecl list
-
-type t = {
-  typedefs: (string * C.typ) list;
-  functions: (string * (C.typ * C.typ list * bool)) list
-}
-
-val set: t -> unit
diff --git a/cparser/C.mli b/cparser/C.mli
index cc8d4065..15717565 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -264,3 +264,10 @@ and globdecl_desc =
   | Gpragma of string                   (* #pragma directive *)
 
 type program = globdecl list
+
+(** Builtin types and functions *)
+
+type builtins = {
+  builtin_typedefs: (string * typ) list;
+  builtin_functions: (string * (typ * typ list * bool)) list
+}
diff --git a/cparser/Checks.ml b/cparser/Checks.ml
index ef62edd6..17caf19a 100644
--- a/cparser/Checks.ml
+++ b/cparser/Checks.ml
@@ -117,7 +117,7 @@ let traverse_program
           pragma env g.gloc s;
           env in
       traverse env gl in
-  traverse (Builtins.environment ()) p
+  traverse (Env.initial ()) p
 
 (* Unknown attributes warning *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index b2934c67..eea60127 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -3089,7 +3089,7 @@ let _ = elab_funbody_f := elab_funbody
 
 let elab_file prog =
   reset();
-  let env = Builtins.environment () in
+  let env = Env.initial () in
   let elab_def env d = snd (elab_definition false false false env d) in
   ignore (List.fold_left elab_def env prog);
   let p = elaborated_program () in
diff --git a/cparser/Env.ml b/cparser/Env.ml
index 5fa4571a..4723a725 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -276,6 +276,46 @@ let add_enum env id info =
 let add_types env_old env_new =
   { env_new with env_ident = env_old.env_ident;env_scope = env_old.env_scope;}
 
+(* Initial environment describing the built-in types and functions *)
+
+module Init = struct
+
+let env = ref empty
+let idents = ref []
+let decls = ref []
+
+let no_loc = ("", -1)
+
+let add_typedef (s, ty) =
+  let (id, env') = enter_typedef !env s ty in
+  env := env';
+  idents := id :: !idents;
+  decls := {gdesc = Gtypedef(id, ty); gloc = no_loc} :: !decls
+
+let add_function (s, (res, args, va)) =
+  let ty =
+    TFun(res,
+         Some (List.map (fun ty -> (fresh_ident "", ty)) args),
+         va, []) in
+  let (id, env') = enter_ident !env s Storage_extern ty in
+  env := env';
+  idents := id :: !idents;
+  decls :=
+    {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
+
+end
+
+let initial () = !Init.env
+let initial_identifiers () = !Init.idents
+let initial_declarations () = List.rev !Init.decls
+
+let set_builtins blt =
+  Init.env := empty;
+  Init.idents := [];
+  Init.decls := [];
+  List.iter Init.add_typedef blt.builtin_typedefs;
+  List.iter Init.add_function blt.builtin_functions
+
 (* Error reporting *)
 
 open Printf
diff --git a/cparser/Env.mli b/cparser/Env.mli
index 7ea2c514..1baab68f 100644
--- a/cparser/Env.mli
+++ b/cparser/Env.mli
@@ -77,3 +77,10 @@ val add_typedef : t -> C.ident -> typedef_info -> t
 val add_enum : t -> C.ident -> enum_info -> t
 
 val add_types : t -> t -> t
+
+(* Initial environment describing the builtin types and functions *)
+
+val initial: unit -> t
+val initial_identifiers: unit -> C.ident list
+val initial_declarations: unit -> C.globdecl list
+val set_builtins: C.builtins -> unit
diff --git a/cparser/GCC.ml b/cparser/GCC.ml
index 010d12f3..458e51d3 100644
--- a/cparser/GCC.ml
+++ b/cparser/GCC.ml
@@ -38,10 +38,10 @@ let intPtrType = TPtr(TInt(IInt, []), [])
 let sizeType() = TInt(size_t_ikind(), [])
 
 let builtins = {
-  Builtins.typedefs = [
+  builtin_typedefs = [
   "__builtin_va_list", voidPtrType
 ];
-  Builtins.functions = [
+  builtin_functions = [
   "__builtin___fprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType ], true) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
   "__builtin___memcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false);
   "__builtin___memmove_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false);
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 3c27f3a9..4c70c7ae 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -418,4 +418,4 @@ let program p =
     | _ -> false
     end;
   Hashtbl.clear byteswapped_fields;
-  transf_globdecls (Builtins.environment()) [] p
+  transf_globdecls (Env.initial()) [] p
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index eb31eaf0..64412194 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -246,7 +246,7 @@ let rec globdecls env accu = function
 (* Reserve names of builtins *)
 
 let reserve_builtins () =
-  List.fold_left enter_public empty_env (Builtins.identifiers())
+  List.fold_left enter_public empty_env (Env.initial_identifiers())
 
 (* Reserve global declarations with public visibility *)
 
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 0a2ce3bb..349a3155 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -227,4 +227,4 @@ let program
       in
         transf_globdecls env' ({g with gdesc = desc'} :: accu) gl
 
-  in transf_globdecls (Builtins.environment()) [] p
+  in transf_globdecls (Env.initial()) [] p
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 66b497cc..d25f70c6 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -399,4 +399,4 @@ let rec unblock_glob env accu = function
 let program p =
   next_scope_id := 0;
   {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
-  unblock_glob (Builtins.environment()) [] p
+  unblock_glob (Env.initial()) [] p
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 3498a779..f9684355 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -123,7 +123,7 @@ let insert_type ty =
           | TNamed (id,_) ->
               let typ = try
                 let _,t =
-                  List.find (fun a -> fst a = id.name) CBuiltins.builtins.Builtins.typedefs in
+                  List.find (fun a -> fst a = id.name) CBuiltins.builtins.builtin_typedefs in
                 Some (attr_aux t)
               with Not_found -> None in
               let t = {
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 36b5c354..bfb3542b 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -118,7 +118,7 @@ let init () =
                    else Machine.rv32
     | _         -> assert false
   end;
-  Builtins.set C2C.builtins;
+  Env.set_builtins C2C.builtins;
   Cutil.declare_attributes C2C.attributes;
   CPragmas.initialize()
 
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 11b7aef9..e29a41f1 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -18,11 +18,11 @@
 open C
 
 let builtins = {
-  Builtins.typedefs = [
+  builtin_typedefs = [
     "__builtin_va_list",
     TArray(TInt(IUInt, []), Some 3L, [])
   ];
-  Builtins.functions = [
+  builtin_functions = [
     (* Integer arithmetic *)
     "__builtin_mulhw",
       (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false);
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index 0c981d11..edaf586d 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -18,10 +18,10 @@
 open C
 
 let builtins = {
-  Builtins.typedefs = [
+  builtin_typedefs = [
     "__builtin_va_list", TPtr(TVoid [], [])
   ];
-  Builtins.functions = [
+  builtin_functions = [
     (* Synchronization *)
     "__builtin_fence",
       (TVoid [], [], false);
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index 69a2eb64..6fb8b697 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -26,10 +26,10 @@ let (va_list_type, va_list_scalar, size_va_list) =
     (TPtr(TVoid [], []), true, 4)
 
 let builtins = {
-  Builtins.typedefs = [
+  builtin_typedefs = [
     "__builtin_va_list", va_list_type;
   ];
-  Builtins.functions = [
+  builtin_functions = [
     (* Integer arithmetic *)
     "__builtin_bswap64",
       (TInt(IULongLong, []), [TInt(IULongLong, [])], false);