Merge pull request #95 from AbsInt/noreturn

Added the _Noreturn keyword.

11 files changed, 150 insertions, 26 deletions

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<cabsloc> 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<string * option expression * cabsloc> enumerator
 %type<string * cabsloc> enumeration_constant
 %type<cvspec * cabsloc> type_qualifier type_qualifier_noattr
-%type<cabsloc> function_specifier
+%type<funspec * cabsloc> function_specifier
 %type<name> declarator declarator_noattrend direct_declarator
 %type<(decl_type -> decl_type) * cabsloc> pointer
 %type<list cvspec (* Reverse order *)> 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 27502a3b..613ec17f 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 <organization> 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 <COPYRIGHT
+ * HOLDER> 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 <stdalign.h>.  */
+
+#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 <organization> 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 <COPYRIGHT
+ * HOLDER> 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 <stdnoreturn.h>.  */
+
+#ifndef _STDNORETURN_H
+#define _STDNORETURN_H
+
+#define noreturn _Noreturn
+
+#endif	/* stdnoreturn.h */