Check for redefinition of globals and preserve static initialized variables (#81)

* Added check for redefinition of globals.

Since Cleanup may remove duplicated static functions or global
definitions we need to check for duplication during elaboration,
not just in C2C.
Bug 23410

* Do not eliminate unreferenced static variables with initializers

This way all initialized variables make it to the C2C pass,
where the initializers are checked for constant-ness.
Bug 23410

2 files changed, 33 insertions, 6 deletions

diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index fe674d9b..75ee0e5a 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -118,11 +118,23 @@ let add_enum e =
     e
 
 (* Saturate the set of referenced identifiers, starting with externally
-   visible global declarations *)
+   visible global declarations.
+
+   Externally-visible globals include a minima:
+   - Definitions of functions, unless "static" or "inline".
+   - Declaration of variables with default storage.
+
+   We choose to also treat as visible and therefore to keep:
+   - "static" initialized variables, so that the checks on initializers
+     performed in C2C are performed on all initializers.
+     If the variable turns out to be unused, it will be removed
+     later by the Unusedglob pass.
+*)
 
 let visible_decl (sto, id, ty, init) =
-  sto = Storage_default &&
-  match ty with TFun _ -> false | _ -> true
+    init <> None ||
+    (sto = Storage_default &&
+     match ty with TFun _ -> false | _ -> true)
 
 let visible_fundef f =
   match f.fd_storage with
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 1712b55e..88262421 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -69,6 +69,17 @@ let top_declarations = ref ([] : globdecl list)
 
 let top_environment = ref Env.empty
 
+(* Set of all globals with a definitions *)
+
+module StringSet = Set.Make(String)
+
+let global_defines = ref StringSet.empty
+
+let add_global_define loc name =
+  if StringSet.mem name !global_defines then
+    error loc "redefinition of '%s'" name;
+  global_defines := StringSet.add name !global_defines
+
 let emit_elab ?(debuginfo = true) ?(linkage = false) env loc td =
   let loc = elab_loc loc in
   let dec ={ gdesc = td; gloc = loc } in
@@ -84,7 +95,7 @@ let emit_elab ?(debuginfo = true) ?(linkage = false) env loc td =
     | _ -> ()
   end
 
-let reset() = top_declarations := []; top_environment := Env.empty
+let reset() = top_declarations := []; top_environment := Env.empty; global_defines := StringSet.empty
 
 let elaborated_program () =
   let p = !top_declarations in
@@ -2181,12 +2192,17 @@ let enter_decdefs local loc env sto dl =
     let sto1 = if local && isfun then Storage_extern else sto in
     (* enter ident in environment with declared type, because
        initializer can refer to the ident *)
+    if init <> NO_INIT && not local then
+      add_global_define loc s;
     let (id, sto', env1, ty, linkage) =
       enter_or_refine_ident local loc env s sto1 ty in
     if not isfun && is_void_type env ty then
       fatal_error loc "'%s' has incomplete type" s;
     (* process the initializer *)
     let (ty', init') = elab_initializer loc env1 s ty init in
+    (* if (sto = Storage_static || not local) then
+     *   (\* Check for constant initializer for static and global variables *\)
+     *   is_constant_init env loc init'; *)
     (* update environment with refined type *)
     let env2 = Env.add_ident env1 id sto' ty' in
     (* check for incomplete type *)
@@ -2350,6 +2366,7 @@ let elab_fundef env spec name defs body loc =
         (ty_ret, params, vararg, attr)
     | _ -> fatal_error loc "wrong type for function definition" in
   (* Enter function in the environment, for recursive references *)
+  add_global_define loc s;
   let (fun_id, sto1, env1, _, _) =
     enter_or_refine_ident false loc env1 s sto ty in
   let incomplete_param env ty =
@@ -2469,8 +2486,6 @@ let elab_asm_operand vararg loc env (ASMOPERAND(label, wide, chars, e)) =
 
 (* Contexts for elaborating statements *)
 
-module StringSet = Set.Make(String)
-
 type stmt_context = {
   ctx_return_typ: typ;          (**r return type for the function *)
   ctx_labels: StringSet.t;      (**r all labels defined in the function *)