From 68df90c91ab67a32fc666bf18798bba9ae6c5f9d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jul 2016 15:02:32 +0200 Subject: 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. --- cparser/Elab.ml | 139 +++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 93 insertions(+), 46 deletions(-) (limited to 'cparser/Elab.ml') 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 *) -- cgit From 7aa563e8d3730e37f42979989f2fa87c940a4d4b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jul 2016 16:42:12 +0200 Subject: Improved handling of C90 calls to undeclared functions In a call such as "f(expr, ..., expr)", if the identifier "f" is not declared, declare it as specified in the ISO C90 standard, namely like "extern int f()" would do it. Previously, the declaration was done "on the side" and not properly recorded in the environments. The diff is relatively large because the "enter_or_refine_ident" had to be moved up in the file. --- cparser/Elab.ml | 148 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 75 insertions(+), 73 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 8c90bbc8..1888f053 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -107,6 +107,77 @@ let redef fn env arg = | None -> false | Some(id, info) -> Env.in_current_scope env id +(* Auxiliaries for handling declarations and redeclarations *) + +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; + begin match previous_def Env.lookup_ident env s with + | Some(id, II_ident(old_sto, old_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 + | _ -> + () + 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 + (* Forward declarations *) let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp * Env.t) ref @@ -1353,11 +1424,11 @@ let elab_expr loc env a = | VARIABLE n when not (Env.ident_is_bound env n) -> warning "implicit declaration of function '%s'" n; let ty = TFun(TInt(IInt, []), None, false, []) in + (* Check against other definitions and enter in env *) + let (id, sto, env, ty, linkage) = + enter_or_refine_ident true loc env n Storage_extern ty 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)); + emit_elab ~linkage env loc (Gdecl(sto, id, ty, None)); { edesc = EVar id; etyp = ty },env | _ -> elab env a1 in let bl = mmap elab env al in @@ -1847,75 +1918,6 @@ 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; - begin match previous_def Env.lookup_ident env s with - | Some(id, II_ident(old_sto, old_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 - | _ -> - () - 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 *) if sto = Storage_register && not local then -- cgit From 5b13c78e65a282bde23517f2da4059beb551dd9e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 22 Jul 2016 10:09:39 +0200 Subject: Nicer error message for redefinitions with incompatible type --- cparser/Elab.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 1888f053..76f8efdb 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -115,11 +115,12 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = | Some new_ty -> new_ty | None -> + let id = Env.fresh_ident s in error loc "redefinition of '%s' with incompatible type.@ \ - Previous type: %a.@ \ - New type: %a" - s Cprint.typ old_ty Cprint.typ ty; + Previous declaration: %a.@ \ + New declaration: %a" + s Cprint.simple_decl (id, old_ty) Cprint.simple_decl (id, ty); ty in let new_sto = (* The only case not allowed is removing static *) -- cgit