From 4e62a2c4b2c809ea020423e7e328ba96e379d64d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 23 Mar 2016 14:22:33 +0100 Subject: Added the _Noreturn keyword. CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541 --- cparser/Cabs.v | 5 ++++- cparser/Cabshelper.ml | 2 +- cparser/Cutil.ml | 21 +++++++++++++++++++++ cparser/Cutil.mli | 5 +++++ cparser/Elab.ml | 36 +++++++++++++++++++++++------------- cparser/Lexer.mll | 2 ++ cparser/Parser.vy | 19 ++++++++++--------- cparser/pre_parser.mly | 3 ++- runtime/Makefile | 3 ++- runtime/include/stdalign.h | 42 ++++++++++++++++++++++++++++++++++++++++++ runtime/include/stdnoreturn.h | 38 ++++++++++++++++++++++++++++++++++++++ 11 files changed, 150 insertions(+), 26 deletions(-) create mode 100644 runtime/include/stdalign.h create mode 100644 runtime/include/stdnoreturn.h diff --git a/cparser/Cabs.v b/cparser/Cabs.v index f5cab15a..d087e8c7 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -60,6 +60,9 @@ with cvspec := | CV_CONST | CV_VOLATILE | CV_RESTRICT | CV_ATTR : attribute -> cvspec +with funspec := + INLINE | NORETURN + (* Type specifier elements. These appear at the start of a declaration *) (* Everywhere they appear in this file, they appear as a 'list spec_elem', *) (* which is not interpreted by cabs -- rather, this "word soup" is passed *) @@ -68,7 +71,7 @@ with cvspec := with spec_elem := | SpecCV : cvspec -> spec_elem (* const/volatile *) | SpecStorage : storage -> spec_elem - | SpecInline + | SpecFunction: funspec -> spec_elem | SpecType : typeSpecifier -> spec_elem (* Declarator type. They modify the base type given in the specifier. Keep diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml index b4e6a082..958f242c 100644 --- a/cparser/Cabshelper.ml +++ b/cparser/Cabshelper.ml @@ -35,7 +35,7 @@ let rec isExtern = function let rec isInline = function [] -> false - | SpecInline :: _ -> true + | (SpecFunction INLINE) :: _ -> true | _ :: rest -> isInline rest let rec isTypedef = function diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 1bbb8e98..4b4e1b81 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -1118,3 +1118,24 @@ let rec subst_stmt phi s = List.map subst_asm_operand inputs, clob) } + +let contains_return s = + let rec aux s = + match s.sdesc with + | Sskip + | Sbreak + | Scontinue + | Sdo _ + | Sdecl _ + | Sasm _ + | Sgoto _ -> false + | Sif(_, s1, s2) + | Sseq(s1, s2) -> aux s1 || aux s2 + | Sswitch (_, s) + | Slabeled (_, s) + | Swhile (_, s) + | Sdowhile(s, _ ) -> aux s + | Sfor(s1, _ , s2, s3) -> aux s1 || aux s2 || aux s3 + | Sreturn _ -> true + | Sblock sl -> List.fold_left (fun acc s -> acc || aux s) false sl in + aux s diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 3dcfe4aa..91b073ab 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -255,3 +255,8 @@ val subst_expr: exp IdentMap.t -> exp -> exp val subst_init: exp IdentMap.t -> init -> init val subst_decl: exp IdentMap.t -> decl -> decl val subst_stmt: exp IdentMap.t -> stmt -> stmt + +(* Statement properties *) + +val contains_return: stmt -> bool + (* Does the stmt contain a return. *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 130f37cd..e73b2f97 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -389,6 +389,7 @@ let rec elab_specifier ?(only = false) loc env specifier = - a list of type specifiers *) let sto = ref Storage_default and inline = ref false + and noreturn = ref false and attr = ref [] and tyspecs = ref [] and typedef = ref false in @@ -409,12 +410,13 @@ let rec elab_specifier ?(only = false) loc env specifier = error loc "multiple uses of 'typedef'"; typedef := true end - | SpecInline -> inline := true + | SpecFunction INLINE -> inline := true + | SpecFunction NORETURN -> noreturn := true | SpecType tys -> tyspecs := tys :: !tyspecs in List.iter do_specifier specifier; - let simple ty = (!sto, !inline, !typedef, add_attributes_type !attr ty, env) in + let simple ty = (!sto, !inline, !noreturn ,!typedef, add_attributes_type !attr ty, env) in (* As done in CIL, partition !attr into type-related attributes, which are returned, and other attributes, which are left in !attr. @@ -485,21 +487,21 @@ let rec elab_specifier ?(only = false) loc env specifier = add_attributes (get_type_attrs()) (elab_attributes env a) in let (id', env') = elab_struct_or_union only Struct loc id optmembers a' env in - (!sto, !inline, !typedef, TStruct(id', !attr), env') + (!sto, !inline, !noreturn, !typedef, TStruct(id', !attr), env') | [Cabs.Tstruct_union(UNION, id, optmembers, a)] -> let a' = add_attributes (get_type_attrs()) (elab_attributes env a) in let (id', env') = elab_struct_or_union only Union loc id optmembers a' env in - (!sto, !inline, !typedef, TUnion(id', !attr), env') + (!sto, !inline, !noreturn, !typedef, TUnion(id', !attr), env') | [Cabs.Tenum(id, optmembers, a)] -> let a' = add_attributes (get_type_attrs()) (elab_attributes env a) in let (id', env') = elab_enum only loc id optmembers a' env in - (!sto, !inline, !typedef, TEnum(id', !attr), env') + (!sto, !inline, !noreturn, !typedef, TEnum(id', !attr), env') (* Specifier doesn't make sense *) | _ -> @@ -575,7 +577,7 @@ and elab_parameters env params = (* Elaboration of a function parameter *) and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = - let (sto, inl, tydef, bty, env1) = elab_specifier loc env spec in + let (sto, inl, noret, tydef, bty, env1) = elab_specifier loc env spec in if tydef then error loc "'typedef' used in function parameter"; let ((ty, _), _) = elab_type_declarator loc env1 bty false decl in @@ -585,6 +587,8 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = "'extern' or 'static' storage not supported for function parameter"; if inl then error loc "'inline' can only appear on functions"; + if noret then + error loc "'_Noreturn' can only appear on functions"; let id = match id with None -> "" | Some id -> id in if id <> "" && redef Env.lookup_ident env id then error loc "redefinition of parameter '%s'" id; @@ -596,22 +600,24 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = (* Elaboration of a (specifier, Cabs "name") pair *) and elab_fundef_name env spec (Name (id, decl, attr, loc)) = - let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in + let (sto, inl, noret, tydef, bty, env') = elab_specifier loc env spec in if tydef then error loc "'typedef' is forbidden here"; let ((ty, kr_params), env'') = elab_type_declarator loc env' bty true decl in let a = elab_attributes env attr in - (id, sto, inl, add_attributes_type a ty, kr_params, env'') + (id, sto, inl, noret, add_attributes_type a ty, kr_params, env'') (* Elaboration of a name group. C99 section 6.7.6 *) and elab_name_group loc env (spec, namelist) = - let (sto, inl, tydef, bty, env') = + let (sto, inl, noret, tydef, bty, env') = elab_specifier loc env spec in if tydef then error loc "'typedef' is forbidden here"; if inl then error loc "'inline' is forbidden here"; + if noret then + error loc "'_Noreturn' is forbidden here"; let elab_one_name env (Name (id, decl, attr, loc)) = let ((ty, _), env1) = elab_type_declarator loc env bty false decl in @@ -622,7 +628,7 @@ and elab_name_group loc env (spec, namelist) = (* Elaboration of an init-name group *) and elab_init_name_group loc env (spec, namelist) = - let (sto, inl, tydef, bty, env') = + let (sto, inl, noret, tydef, bty, env') = elab_specifier ~only:(namelist=[]) loc env spec in let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) = let ((ty, _), env1) = @@ -630,6 +636,8 @@ and elab_init_name_group loc env (spec, namelist) = let a = elab_attributes env attr in if inl && not (is_function_type env ty) then error loc "'inline' can only appear on functions"; + if noret && not (is_function_type env ty) then + error loc "'_Noreturn' can only appear on functions"; ((id, add_attributes_type a ty, init), env1) in (mmap elab_one_name env' namelist, sto, tydef) @@ -827,9 +835,9 @@ and elab_enum only loc tag optmembers attrs env = (* Elaboration of a naked type, e.g. in a cast *) let elab_type loc env spec decl = - let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in + let (sto, inl, noret, tydef, bty, env') = elab_specifier loc env spec in let ((ty, _), env'') = elab_type_declarator loc env' bty false decl in - if sto <> Storage_default || inl || tydef then + if sto <> Storage_default || inl || noret || tydef then error loc "'typedef', 'extern', 'static', 'register' and 'inline' are meaningless in cast"; (ty, env'') @@ -1890,7 +1898,7 @@ let enter_decdefs local loc env sto dl = (List.rev decls, env') let elab_fundef env spec name defs body loc = - let (s, sto, inline, ty, kr_params, env1) = elab_fundef_name env spec name in + let (s, sto, inline, noret, ty, kr_params, env1) = elab_fundef_name env spec name in if sto = Storage_register then fatal_error loc "A function definition cannot have 'register' storage class"; begin match kr_params, defs with @@ -1982,6 +1990,8 @@ let elab_fundef env spec name defs body loc = warning loc "return type of 'main' should be 'int'"; body' end else body' in + if noret && contains_return body' then + warning loc "function '%s' declared 'noreturn' should not return" s; (* Build and emit function definition *) let fn = { fd_storage = sto1; diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 871f2bf9..d3747e22 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -65,6 +65,7 @@ let () = ("goto", fun loc -> GOTO loc); ("if", fun loc -> IF loc); ("inline", fun loc -> INLINE loc); + ("_Noreturn", fun loc -> NORETURN loc); ("int", fun loc -> INT loc); ("long", fun loc -> LONG loc); ("register", fun loc -> REGISTER loc); @@ -551,6 +552,7 @@ and singleline_comment = parse | MOD_ASSIGN loc -> loop MOD_ASSIGN't loc | MUL_ASSIGN loc -> loop MUL_ASSIGN't loc | NEQ loc -> loop NEQ't loc + | NORETURN loc -> loop NORETURN't loc | OR_ASSIGN loc -> loop OR_ASSIGN't loc | PACKED loc -> loop PACKED't loc | PERCENT loc -> loop PERCENT't loc diff --git a/cparser/Parser.vy b/cparser/Parser.vy index 16f6a0ef..ab07cb94 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -32,7 +32,7 @@ Require Import List. LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN %token LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA - SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE + SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID STRUCT UNION ENUM UNDERSCORE_BOOL PACKED ALIGNAS ATTRIBUTE ASM @@ -67,7 +67,7 @@ Require Import List. %type enumerator %type enumeration_constant %type type_qualifier type_qualifier_noattr -%type function_specifier +%type function_specifier %type declarator declarator_noattrend direct_declarator %type<(decl_type -> decl_type) * cabsloc> pointer %type type_qualifier_list @@ -344,8 +344,8 @@ declaration_specifiers_typespec_opt: { SpecType (fst typ)::rest } | qual = type_qualifier rest = declaration_specifiers_typespec_opt { SpecCV (fst qual)::rest } -| loc = function_specifier rest = declaration_specifiers_typespec_opt - { SpecInline::rest } +| func = function_specifier rest = declaration_specifiers_typespec_opt + { SpecFunction (fst func)::rest } | /* empty */ { [] } @@ -363,8 +363,8 @@ declaration_specifiers: { (SpecCV (fst qual)::fst rest, snd qual) } | attr = attribute_specifier rest = declaration_specifiers { (SpecCV (CV_ATTR (fst attr))::fst rest, snd attr) } -| loc = function_specifier rest = declaration_specifiers - { (SpecInline::fst rest, loc) } +| func = function_specifier rest = declaration_specifiers + { (SpecFunction (fst func)::fst rest, snd func) } init_declarator_list: | init = init_declarator @@ -571,7 +571,9 @@ gcc_attribute_word: (* 6.7.4 *) function_specifier: | loc = INLINE - { loc } + { (INLINE, loc) } +| loc = NORETURN + { (NORETURN, loc)} (* 6.7.5 *) declarator: @@ -870,7 +872,7 @@ asm_attributes: { [] } | CONST attr = asm_attributes { CV_CONST :: attr } -| VOLATILE attr = asm_attributes +| VOLATILE attr = asm_attributes { CV_VOLATILE :: attr } asm_arguments: @@ -950,4 +952,3 @@ declaration_list: { [d] } | dl = declaration_list d = declaration { d :: dl } - diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly index 21008f1c..05dd1016 100644 --- a/cparser/pre_parser.mly +++ b/cparser/pre_parser.mly @@ -54,7 +54,7 @@ COLON AND MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT - AUTO REGISTER INLINE CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE + AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE UNDERSCORE_BOOL CONST VOLATILE VOID STRUCT UNION ENUM CASE DEFAULT IF ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK RETURN BUILTIN_VA_ARG ALIGNOF ATTRIBUTE ALIGNAS PACKED ASM @@ -608,6 +608,7 @@ gcc_attribute_word: function_specifier: | INLINE +| NORETURN {} (* We add this non-terminal here to force the resolution of the diff --git a/runtime/Makefile b/runtime/Makefile index 99eeaa54..e49bf3c7 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -7,7 +7,8 @@ OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \ vararg.o LIB=libcompcert.a INCLUDES=include/float.h include/stdarg.h include/stdbool.h \ - include/stddef.h include/varargs.h + include/stddef.h include/varargs.h include/stdalign.h \ + include/stdnoreturn.h VPATH=$(ARCH) diff --git a/runtime/include/stdalign.h b/runtime/include/stdalign.h new file mode 100644 index 00000000..1560d8fc --- /dev/null +++ b/runtime/include/stdalign.h @@ -0,0 +1,42 @@ +/* This file is part of the Compcert verified compiler. + * + * Copyright (c) 2015 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + + +/* ISO C11: 7.15 Alignment . */ + +#ifndef _STDALIGN_H +#define _STDALIGN_H + +#define alignas _Alignas +#define alignof _Alignof + +#define __alignas_is_defined 1 +#define __alignof_is_defined 1 + +#endif /* stdalign.h */ diff --git a/runtime/include/stdnoreturn.h b/runtime/include/stdnoreturn.h new file mode 100644 index 00000000..0604c37b --- /dev/null +++ b/runtime/include/stdnoreturn.h @@ -0,0 +1,38 @@ +/* This file is part of the Compcert verified compiler. + * + * Copyright (c) 2015 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + + +/* ISO C11: 7.23 _Noreturn . */ + +#ifndef _STDNORETURN_H +#define _STDNORETURN_H + +#define noreturn _Noreturn + +#endif /* stdnoreturn.h */ -- cgit