Merge pull request #209 from goblint/static-assert-check

Check `_Static_assert`

Author: sim642

src/frontc/cabs.ml

@@ -83,8 +83,8 @@ type typeSpecifier = (* Merge all specifiers into one type *)
      a forward declaration or simple reference to the type); they
      also have a list of __attribute__s that appeared between the
      keyword and the type name (definitions only) *)
-  | Tstruct of string * field_group list option * attribute list
-  | Tunion of string * field_group list option * attribute list
+  | Tstruct of string * struct_decl list option * attribute list
+  | Tunion of string * struct_decl list option * attribute list
   | Tenum of string * enum_item list option * attribute list
   | TtypeofE of expression                      (* GCC __typeof__ *)
   | TtypeofT of specifier * decl_type       (* GCC __typeof__ *)
@@ -150,6 +150,10 @@ and name_group = specifier * name list
 (* The optional expression is the bitfield *)
 and field_group = specifier * (name * expression option) list
 
+and struct_decl =
+  | FIELD_GROUP of field_group
+  | FIELD_STATIC_ASSERT of expression * string option * cabsloc
+
 (* like name_group, except the declared variables are allowed to have initializers *)
 (* e.g.: int x=1, y=2; *)
 and init_name_group = specifier * init_name list
@@ -187,7 +191,7 @@ and definition =
  | TRANSFORMER of definition * definition list * cabsloc
  (* expression transformer: source and destination *)
  | EXPRTRANSFORMER of expression * expression * cabsloc
- | STATIC_ASSERT of expression * string * cabsloc
+ | STATIC_ASSERT of expression * string option * cabsloc
 
 
 (* the string is a file name, and then the list of toplevel forms *)

src/frontc/cabs2cil.ml

@@ -2667,6 +2667,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
         if n = "" then E.s (error "Missing struct tag on incomplete struct");
         findCompType "struct" n []
     | [A.Tstruct (n, Some nglist, extraAttrs)] -> (* A definition of a struct *)
+      let nglist = doStructDecls nglist in
       let (specs, names) = List.split nglist in
       let n' =
         if n <> "" then n else anonStructName "struct" suggestedAnonName specs in
@@ -2678,6 +2679,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
         if n = "" then E.s (error "Missing union tag on incomplete union");
         findCompType "union" n []
     | [A.Tunion (n, Some nglist, extraAttrs)] -> (* A definition of a union *)
+        let nglist = doStructDecls nglist in
         let (specs, names) = List.split nglist in
         let n' =
           if n <> "" then n else anonStructName "union" suggestedAnonName specs in
@@ -2827,6 +2829,23 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
   in
   bt,!storage,!isinline,List.rev (!attrs @ (convertCVtoAttr !cvattrs))
 
+
+and doStructDecls (struct_decls: struct_decl list): field_group list =
+  List.filter_map (function
+      | FIELD_GROUP fg -> Some fg
+      | FIELD_STATIC_ASSERT (e, str, loc) ->
+        let loc = convLoc loc in
+        let d_message () = function
+          | None -> nil
+          | Some str -> dprintf ": %s" str
+        in
+        begin match isIntegerConstant e with
+          | Some 0 -> E.s (error "Static assert failed at %a%a" d_loc loc d_message str)
+          | Some _ -> None
+          | None -> E.s (error "Static assert with a non-constant at %a%a" d_loc loc d_message str)
+        end
+    ) struct_decls
+
 (* given some cv attributes, convert them into named attributes for
    uniform processing *)
 and convertCVtoAttr (src: A.cvspec list) : A.attribute list =
@@ -6624,7 +6643,19 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function
             E.s (bug "doDecl returns non-empty statement for global"))
         dl;
       empty
-  | STATIC_ASSERT _ -> empty
+  | STATIC_ASSERT (e, str, loc) ->
+    if isglobal || isstmt then
+      currentLoc := convLoc loc;
+    currentExpLoc := convLoc loc;
+    let d_message () = function
+      | None -> nil
+      | Some str -> dprintf ": %s" str
+    in
+    begin match isIntegerConstant e with
+      | Some 0 -> E.s (error "Static assert failed at %a%a" d_loc !currentLoc d_message str)
+      | Some _ -> empty
+      | None -> E.s (error "Static assert with a non-constant at %a%a" d_loc !currentLoc d_message str)
+    end
   | _ -> E.s (error "unexpected form of declaration")
 
 and doTypedef ((specs, nl): A.name_group) =

src/frontc/cabsvisit.ml

@@ -189,13 +189,22 @@ and childrenTypeSpecifier vis ts =
     let nel' = mapNoCopy doOneField nel in
     if s' != s || nel' != nel then (s', nel') else input
   in
+  let childrenStructDecl input =
+    match input with
+    | FIELD_GROUP fg -> 
+      let fg' = childrenFieldGroup fg in
+      if fg' != fg then FIELD_GROUP fg' else input
+    | FIELD_STATIC_ASSERT (e, str, l) ->
+      let e' = visitCabsExpression vis e in
+      if e' != e then FIELD_STATIC_ASSERT (e', str, l) else input
+  in
   match ts with
     Tstruct (n, Some fg, extraAttrs) ->
       (*(trace "sm" (dprintf "visiting struct %s\n" n));*)
-      let fg' = mapNoCopy childrenFieldGroup fg in
+      let fg' = mapNoCopy childrenStructDecl fg in
       if fg' != fg then Tstruct( n, Some fg', extraAttrs) else ts
   | Tunion (n, Some fg, extraAttrs) ->
-      let fg' = mapNoCopy childrenFieldGroup fg in
+      let fg' = mapNoCopy childrenStructDecl fg in
       if fg' != fg then Tunion( n, Some fg', extraAttrs) else ts
   | Tenum (n, Some ei, extraAttrs) ->
       let doOneEnumItem ((s, attrs, e, loc) as ei) =
@@ -321,7 +330,9 @@ and childrenDefinition vis d =
       let dl' = mapNoCopyList (visitCabsDefinition vis) dl in
       if dl' != dl then LINKAGE (n, l, dl') else d
 
-  | STATIC_ASSERT _ -> d
+  | STATIC_ASSERT (e, str, l) ->
+    let e' = visitCabsExpression vis e in
+    if e' != e then STATIC_ASSERT (e', str, l) else d
   | TRANSFORMER _ -> d
   | EXPRTRANSFORMER _ -> d
 

src/frontc/cparser.mly

@@ -370,7 +370,7 @@ let transformOffsetOf (speclist, dtype) member =
 
 %type <spec_elem list * cabsloc> decl_spec_list
 %type <typeSpecifier * cabsloc> type_spec
-%type <Cabs.field_group list> struct_decl_list
+%type <Cabs.struct_decl list> struct_decl_list
 
 
 %type <Cabs.name> old_proto_decl
@@ -999,18 +999,18 @@ declaration:                                /* ISO 6.7.*/
                                        { doDeclaration (joinLoc (snd $1) $3) (fst $1) $2 }
 |   decl_spec_list_no_attr_only SEMICOLON
                                        { doDeclaration (joinLoc (snd $1) $2) (fst $1) [] }
-|   static_assert_declaration          { let (e, m, loc) = $1 in STATIC_ASSERT (e, m, loc) }
+|   static_assert_declaration SEMICOLON { let (e, m, loc) = $1 in STATIC_ASSERT (e, m, loc) }
 ;
 
 static_assert_declaration:
 
 |   STATIC_ASSERT LPAREN expression RPAREN /* C23 */
       {
-        (fst $3, "", $1)
+        (fst $3, None, $1)
       }
 |   STATIC_ASSERT LPAREN expression COMMA const_raw_string RPAREN
       {
-        (fst $3, fst $5, $1)
+        (fst $3, Some (fst $5), $1)
       }
 ;
 
@@ -1149,26 +1149,23 @@ struct_decl_list: /* (* ISO 6.7.2. Except that we allow empty structs. We
                    */
    /* empty */                           { [] }
 |  decl_spec_list                 SEMICOLON struct_decl_list
-                                         { (fst $1,
+                                         { FIELD_GROUP (fst $1,
                                             [(missingFieldDecl, None)]) :: $3 }
 /*(* GCC allows extra semicolons *)*/
 |                                 SEMICOLON struct_decl_list
                                          { $2 }
 |  decl_spec_list field_decl_list SEMICOLON struct_decl_list
-                                          { (fst $1, $2)
+                                          { FIELD_GROUP (fst $1, $2)
                                             :: $4 }
 /*(* MSVC allows pragmas in strange places *)*/
 |  pragma struct_decl_list                { $2 }
 
 |  error                          SEMICOLON struct_decl_list
                                           { $3 }
 /*(* C11 allows static_assert-declaration *)*/
-|  static_assert_declaration             {
-       []
-   }
-
 |  static_assert_declaration      SEMICOLON struct_decl_list  {
-       $3
+       let (e, m, loc) = $1 in
+       FIELD_STATIC_ASSERT (e, m, loc) :: $3
    }
 
 ;

src/frontc/cprint.ml

@@ -244,13 +244,26 @@ and print_decl (n: string) = function
       comprint ")"
 
 
-and print_fields (flds : field_group list) =
+and print_fields (flds : struct_decl list) =
   if flds = [] then print " { } "
   else begin
     print " {";
     indent ();
     List.iter
-      (fun fld -> print_field_group fld; print ";"; new_line ())
+      (function
+        | FIELD_GROUP fld -> print_field_group fld; print ";"; new_line ()
+        | FIELD_STATIC_ASSERT (e, str, loc) ->
+          print "_Static_assert(";
+          print_expression e;
+          begin match str with
+            | Some str ->
+              print ",";
+              print_string str;
+            | None -> ()
+          end;
+          print ");";
+          new_line ()
+      )
       flds;
     unindent ();
     print "} "
@@ -909,8 +922,12 @@ and print_def def =
       setLoc(loc);
       print "_Static_assert(";
       print_expression e;
-      print ",";
-      print_string str;
+      begin match str with
+        | Some str ->
+          print ",";
+          print_string str;
+        | None -> ()
+      end;
       print ");";
 
 (* sm: print a comment if the printComments flag is set *)

src/frontc/patch.ml

@@ -558,12 +558,18 @@ begin
     )
 end
 
-and unifyField (pat : field_group) (tgt : field_group) : binding list =
+and unifyField (pat : struct_decl) (tgt : struct_decl) : binding list =
 begin
-  match pat,tgt with (spec1, list1), (spec2, list2) -> (
+  match pat, tgt with
+  | FIELD_GROUP (spec1, list1), FIELD_GROUP (spec2, list2) ->
     (unifySpecifiers spec1 spec2) @
     (unifyList list1 list2 unifyNameExprOpt)
-  )
+  | FIELD_STATIC_ASSERT (exp1, str1, l1), FIELD_STATIC_ASSERT (exp2, str2, l2) ->
+    (unifyExpr exp1 exp2) @
+    (unifyStringOpt str1 str2)
+  | _, _ ->
+    if verbose then (trace "patchDebug" (dprintf "mismatching struct_decl-s\n"));
+      raise NoMatch
 end
 
 and unifyNameExprOpt (pat : name * expression option)
@@ -700,6 +706,15 @@ begin
   )
 end
 
+and unifyStringOpt (pat : string option)
+                   (tgt : string option) : binding list =
+begin
+  match pat,tgt with
+  | None, None -> []
+  | Some str1, Some str2 -> unifyString str1 str2
+  | _,_ -> raise NoMatch
+end
+
 and unifyExpr (pat : expression) (tgt : expression) : binding list =
 begin
   (* if they're equal, that's good enough *)

test/small1/c11-static-assert-fail1.c

@@ -0,0 +1,7 @@
+#include "testharness.h"
+
+_Static_assert (2 > 18, "blubb");
+
+int main() {
+    SUCCESS;
+}

test/small1/c11-static-assert-fail2.c

@@ -0,0 +1,6 @@
+#include "testharness.h"
+
+int main() {
+    _Static_assert (2 > 18, "blubb");
+    SUCCESS;
+}

test/small1/c11-static-assert-fail3.c

@@ -0,0 +1,10 @@
+#include "testharness.h"
+
+struct S {
+    int x;
+    _Static_assert (2 > 18, "blubb");
+};
+
+int main() {
+    SUCCESS;
+}

test/small1/c11-static-assert.c

@@ -1,10 +1,17 @@
 #include "testharness.h"
 #include <stdnoreturn.h>
 
-_Static_assert (2  <= 18, "blubb");
+_Static_assert (2 <= 18);
+_Static_assert (2 <= 18, "blubb");
 
+struct S {
+    int x;
+    _Static_assert (2 <= 18);
+    _Static_assert (2 <= 18, "blubb");
+};
 
 int main() {
-    _Static_assert (2  <= 18, "blubb");
+    _Static_assert (2 <= 18);
+    _Static_assert (2 <= 18, "blubb");
     SUCCESS;
 }