Revised handling of block-scoped extern declarations

Currently, CompCert incorrectly handles 'extern' and function
declarations within a block.  For example:

int main(void)
{
   {
        extern int i;
        i = 0;
   }
   {
        extern float i;
        i = 10;
   }
}

CompCert fails to detect the inconsistent declarations of "i" in the
two blocks, simply because the first declaration is not in scope when
the second declaration is processed.

This commit changes the elaboration of file-scope declarations,
block-scope "extern" declarations and block-scope function
declarations so that they are checked against possible earlier
declarations found in the already-elaborated top-level declarations,
instead of in the current typing environment.

Owing to the lifting of block-scoped extern and static declarations to
the top-level already performed by the elaboration pass, the
already-elaborated top-level declarations give an accurate view of the
declarations of variables with internal or external linkage already
encountered and processed, even if they are not currently in scope.

1 files changed, 93 insertions, 46 deletions

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index a2a84970..8c90bbc8 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -56,13 +56,28 @@ let elab_loc l = (l.filename, l.lineno)
 
 let top_declarations = ref ([] : globdecl list)
 
-let emit_elab ?(enter:bool=true) env loc td =
+(* Environment that records the top declarations of functions and
+   variables with external or internal linkage.  Used for
+   analyzing "extern" declarations. *)
+
+let top_environment = ref Env.empty
+
+let emit_elab ?(debuginfo = true) ?(linkage = false) env loc td =
   let loc = elab_loc loc in
   let dec ={ gdesc = td; gloc = loc } in
-  if enter then  Debug.insert_global_declaration env dec;
-  top_declarations := dec :: !top_declarations
+  if debuginfo then Debug.insert_global_declaration env dec;
+  top_declarations := dec :: !top_declarations;
+  if linkage then begin
+    match td with
+    | Gdecl(sto, id, ty, init) ->
+        top_environment := Env.add_ident !top_environment id sto ty
+    | Gfundef f ->
+        top_environment :=
+          Env.add_ident !top_environment f.fd_name f.fd_storage (fundef_typ f)
+    | _ -> ()
+  end
 
-let reset() = top_declarations := []
+let reset() = top_declarations := []; top_environment := Env.empty
 
 let elaborated_program () =
   let p = !top_declarations in
@@ -1339,6 +1354,8 @@ let elab_expr loc env a =
             warning "implicit declaration of function '%s'" n;
             let ty = TFun(TInt(IInt, []), None, false, []) in
             (* Emit an extern declaration for it *)
+            (* FIXME: could conflict with an earlier extern declaration
+               that is not in scope.  *)
             let id = Env.fresh_ident n in
             emit_elab env loc (Gdecl(Storage_extern, id, ty, None));
             { edesc = EVar id; etyp = ty },env
@@ -1830,47 +1847,74 @@ let enter_typedefs loc env sto dl =
         emit_elab env loc (Gtypedef(id, ty));
         env') env dl
 
+let combine_toplevel_definitions loc env s old_sto old_ty sto ty =
+  let new_ty =
+    match combine_types AttrCompat env old_ty ty with
+    | Some new_ty ->
+        new_ty
+    | None ->
+        error loc
+           "redefinition of '%s' with incompatible type.@ \
+            Previous type: %a.@ \
+            New type: %a"
+          s Cprint.typ old_ty Cprint.typ ty;
+        ty in
+  let new_sto =
+    (* The only case not allowed is removing static *)
+    match old_sto,sto with
+    | Storage_static,Storage_static
+    | Storage_extern,Storage_extern
+    | Storage_register,Storage_register
+    | Storage_default,Storage_default -> sto
+    | _,Storage_static ->
+       error loc "static redefinition of '%s' after non-static definition" s;
+       sto
+    | Storage_static,_ -> Storage_static (* Static stays static *)
+    | Storage_extern,_ -> sto
+    | Storage_default,Storage_extern -> Storage_extern
+    | _,Storage_extern -> old_sto
+    | _,Storage_register
+    | Storage_register,_ -> Storage_register
+  in
+    (new_sto, new_ty)
+
 let enter_or_refine_ident local loc env s sto ty =
+  (* Check for illegal redefinitions:
+       - a name that was previously a typedef
+       - a variable that was already declared in the same local scope
+         (unless both old and new declarations are extern)
+       - an enum that was already declared in the same scope.
+     Redefinition of a variable at global scope (or extern) is treated below. *)
   if redef Env.lookup_typedef env s then
     error loc "redefinition of typedef '%s' as different kind of symbol" s;
-  match previous_def Env.lookup_ident env s with
+  begin match previous_def Env.lookup_ident env s with
   | Some(id, II_ident(old_sto, old_ty))
-    when sto = Storage_extern || Env.in_current_scope env id ->
-      if local && Env.in_current_scope env id then
-        error loc "redefinition of local variable '%s'" s;
-      let new_ty =
-        match combine_types AttrCompat env old_ty ty with
-        | Some new_ty ->
-            new_ty
-        | None ->
-            error loc
-               "redefinition of '%s' with incompatible type.@ \
-                Previous type: %a.@ \
-                New type: %a"
-              s Cprint.typ old_ty Cprint.typ ty;
-            ty in
-      let new_sto =
-	(* The only case not allowed is removing static *)
-	match old_sto,sto with
-	| Storage_static,Storage_static
-	| Storage_extern,Storage_extern
-	| Storage_register,Storage_register
-	| Storage_default,Storage_default -> sto
-	| _,Storage_static ->
-	   error loc "static redefinition of '%s' after non-static definition" s; sto
-	| Storage_static,_ -> Storage_static (* Static stays static *)
-	| Storage_extern,_ -> sto
-        | Storage_default,Storage_extern -> Storage_extern
-	| _,Storage_extern -> old_sto
-	| _,Storage_register
-	| Storage_register,_ -> Storage_register
-      in
-      (id, new_sto, Env.add_ident env id new_sto new_ty,new_ty)
-  | Some(id, II_enum v) when Env.in_current_scope env id ->
-      error loc "redefinition of enumerator '%s'" s;
-      (id, sto, Env.add_ident env id sto ty,ty)
+    when local && Env.in_current_scope env id
+               && not (sto = Storage_extern && old_sto = Storage_extern) ->
+      error loc "redefinition of local variable '%s'" s
+  | Some(id, II_enum _) when Env.in_current_scope env id ->
+     error loc "redefinition of enumerator '%s'" s
   | _ ->
-      let (id, env') = Env.enter_ident env s sto ty in (id, sto, env',ty)
+     ()
+  end;
+  (* For a block-scoped, non-"extern" variable, a new declaration
+     is entered, and it has no linkage. *)
+  if local && sto <> Storage_extern then begin
+    let (id, env') = Env.enter_ident env s sto ty in
+    (id, sto, env', ty, false)
+  end else begin
+  (* For a file-scoped or "extern" variable, we need to check against
+     prior declarations of this variable with internal or external linkage.
+     The variable has linkage. *)
+    match previous_def Env.lookup_ident !top_environment s with
+    | Some(id, II_ident(old_sto, old_ty)) ->
+        let (new_sto, new_ty) =
+          combine_toplevel_definitions loc env s old_sto old_ty sto ty in
+        (id, new_sto, Env.add_ident env id new_sto new_ty, new_ty, true)
+    | _ ->
+        let (id, env') = Env.enter_ident env s sto ty in
+        (id, sto, env', ty, true)
+  end
 
 let enter_decdefs local loc env sto dl =
   (* Sanity checks on storage class *)
@@ -1888,7 +1932,8 @@ 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 *)
-    let (id, sto', env1,ty) = enter_or_refine_ident local loc env s sto1 ty in
+    let (id, sto', env1, ty, linkage) =
+      enter_or_refine_ident local loc env s sto1 ty in
     (* process the initializer *)
     let (ty', init') = elab_initializer loc env1 s ty init in
     (* update environment with refined type *)
@@ -1903,7 +1948,7 @@ let enter_decdefs local loc env sto dl =
       ((sto', id, ty', init') :: decls, env2)
     else begin
       (* Global definition *)
-      emit_elab env2 loc (Gdecl(sto', id, ty', init'));
+      emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init'));
       (decls, env2)
     end in
   let (decls, env') = List.fold_left enter_decdef ([], env) dl in
@@ -2048,7 +2093,8 @@ let elab_fundef env spec name defs body loc =
     | _ ->
          fatal_error loc "wrong type for function definition" in
   (* Enter function in the environment, for recursive references *)
-  let (fun_id, sto1, env1, _) = enter_or_refine_ident false loc env1 s sto ty in
+  let (fun_id, sto1, env1, _, _) =
+    enter_or_refine_ident false loc env1 s sto ty in
   (* Enter parameters and extra declarations in the environment *)
   let env2 =
     List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty)
@@ -2058,9 +2104,10 @@ let elab_fundef env spec name defs body loc =
                    env2 extra_decls in
   (* Define "__func__" and enter it in the environment *)
   let (func_ty, func_init) = __func__type_and_init s in
-  let (func_id, _, env3, func_ty) =
+  let (func_id, _, env3, func_ty, _) =
     enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in
-  emit_elab ~enter:false env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
+  emit_elab ~debuginfo:false env3 loc
+                  (Gdecl(Storage_static, func_id, func_ty, Some func_init));
   (* Elaborate function body *)
   let body1 = !elab_funbody_f ty_ret env3 body in
   (* Special treatment of the "main" function *)
@@ -2095,7 +2142,7 @@ let elab_fundef env spec name defs body loc =
       fd_vararg = vararg;
       fd_locals = [];
       fd_body = body3 } in
-  emit_elab env1 loc (Gfundef fn);
+  emit_elab ~linkage:true env1 loc (Gfundef fn);
   env1
 
 (* Definitions *)