Merge pull request #61 from goblint/atomic_support

Support for `_Atomic`
goblint · Jan 10, 2022 · ae80086 · ae80086
2 parents d393f04 + 395a517
commit ae80086
Show file tree

Hide file tree

Showing 8 changed files with 28 additions and 5 deletions.
diff --git a/src/cil.ml b/src/cil.ml
@@ -4278,7 +4278,8 @@ class defaultCilPrinterClass : cilPrinter = object (self)
   method pAttr (Attr(an, args): attribute) : doc * bool =
     (* Recognize and take care of some known cases *)
     match an, args with
-      "const", [] -> nil, false (* don't print const directly, because of split local declarations *)
+      "atomic", [] -> text "_Atomic", false
+    | "const", [] -> nil, false (* don't print const directly, because of split local declarations *)
     | "pconst", [] -> text "const", false (* pconst means print const *)
           (* Put the aconst inside the attribute list *)
     | "complex", [] when !c99Mode -> text "_Complex", false

diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml
@@ -96,7 +96,7 @@ and funspec =
     INLINE | VIRTUAL | EXPLICIT
 
 and cvspec =
-    CV_CONST | CV_VOLATILE | CV_RESTRICT | CV_COMPLEX
+    CV_CONST | CV_VOLATILE | CV_RESTRICT | CV_COMPLEX | CV_ATOMIC
 
 (* Type specifier elements. These appear at the start of a declaration *)
 (* Everywhere they appear in this file, they appear as a 'spec_elem list', *)

diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
@@ -2704,6 +2704,7 @@ and convertCVtoAttr (src: A.cvspec list) : A.attribute list =
   | CV_VOLATILE :: tl -> ("volatile",[]) :: (convertCVtoAttr tl)
   | CV_RESTRICT :: tl -> ("restrict",[]) :: (convertCVtoAttr tl)
   | CV_COMPLEX  :: tl -> ("complex",[]) ::  (convertCVtoAttr tl)
+  | CV_ATOMIC   :: tl -> ("atomic",[]) ::  (convertCVtoAttr tl)
 
 
 and makeVarInfoCabs

diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll
@@ -119,6 +119,7 @@ let init_lexicon _ =
       ("const", fun loc -> CONST loc);
       ("__const", fun loc -> CONST loc);
       ("__const__", fun loc -> CONST loc);
+      ("_Atomic", fun loc -> ATOMIC loc);
       ("_Complex", fun loc -> COMPLEX loc);
       ("__complex__", fun loc -> COMPLEX loc);
       ("static", fun loc -> STATIC loc);

diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly
@@ -257,7 +257,7 @@ let transformOffsetOf (speclist, dtype) member =
 %token<Cabs.cabsloc> GENERIC NORETURN /* C11 */
 %token<Cabs.cabsloc> ENUM STRUCT TYPEDEF UNION
 %token<Cabs.cabsloc> SIGNED UNSIGNED LONG SHORT
-%token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
+%token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST ATOMIC RESTRICT AUTO REGISTER
 %token<Cabs.cabsloc> THREAD
 
 %token<Cabs.cabsloc> SIZEOF ALIGNOF
@@ -323,7 +323,7 @@ let transformOffsetOf (speclist, dtype) member =
 %left	INF SUP INF_EQ SUP_EQ
 %left	INF_INF SUP_SUP
 %left	PLUS MINUS
-%left	STAR SLASH PERCENT CONST RESTRICT VOLATILE COMPLEX
+%left	STAR SLASH PERCENT CONST RESTRICT ATOMIC VOLATILE COMPLEX
 %right	EXCLAM TILDE PLUS_PLUS MINUS_MINUS CAST RPAREN ADDROF SIZEOF ALIGNOF IMAG REAL CLASSIFYTYPE
 %left 	LBRACKET
 %left	DOT ARROW LPAREN LBRACE
@@ -951,9 +951,11 @@ decl_spec_list:                         /* ISO 6.7 */
 |   REGISTER decl_spec_list_opt         { SpecStorage REGISTER :: $2, $1}
                                         /* ISO 6.7.2 */
 |   type_spec decl_spec_list_opt_no_named { SpecType (fst $1) :: $2, snd $1 }
+|   ATOMIC LPAREN decl_spec_list RPAREN decl_spec_list_opt_no_named { (fst $3) @ SpecCV(CV_ATOMIC) :: $5, $1 }
                                         /* ISO 6.7.4 */
 |   INLINE decl_spec_list_opt           { SpecInline :: $2, $1 }
 |   NORETURN decl_spec_list_opt         { SpecNoreturn  :: $2, $1 }
+
 |   cvspec decl_spec_list_opt           { (fst $1) :: $2, snd $1 }
 |   attribute_nocv decl_spec_list_opt   { SpecAttr (fst $1) :: $2, snd $1 }
 /* specifier pattern variable (must be last in spec list) */
@@ -1294,6 +1296,7 @@ cvspec:
 |   VOLATILE                            { SpecCV(CV_VOLATILE), $1 }
 |   RESTRICT                            { SpecCV(CV_RESTRICT), $1 }
 |   COMPLEX                             { SpecCV(CV_COMPLEX), $1 }
+|   ATOMIC                              { SpecCV(CV_ATOMIC), $1 }
 ;
 
 /*** GCC attributes ***/

diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml
@@ -148,7 +148,9 @@ let rec print_specifiers (specs: spec_elem list) =
         | CV_CONST -> "const"
         | CV_VOLATILE -> "volatile"
         | CV_RESTRICT -> "restrict"
-        | CV_COMPLEX -> "complex")
+        | CV_COMPLEX -> "complex"
+        | CV_ATOMIC -> "_Atomic"
+        )
     | SpecAttr al -> print_attribute al; space ()
     | SpecType bt -> print_type_spec bt
     | SpecPattern name -> printl ["@specifier";"(";name;")"]

diff --git a/test/small1/c11-atomic.c b/test/small1/c11-atomic.c
@@ -0,0 +1,14 @@
+#include "testharness.h"
+#include <stdnoreturn.h>
+
+_Atomic const int * p1;  // p is a pointer to an atomic const int
+const _Atomic(int) * p3; // same
+_Atomic(int) const * p3;
+// _Atomic(int*) const  p4; // unsupported as of now
+
+typedef _Atomic _Bool atomic_bool;
+
+
+int main() {
+    SUCCESS;
+}
diff --git a/test/testcil.pl b/test/testcil.pl
@@ -697,6 +697,7 @@ sub addToGroup {
 addTest("testrunc11/c11-caserange");
 addTest("testrunc11/c11-extendedFloat");
 addTest("testrunc11/c11-noreturn");
+addTest("testrunc11/c11-atomic");
 addTest("testrunc11/gcc-c11-generic-1");
 # TODO: these messages are not even checked?
 addTestFail("testc11/gcc-c11-generic-2-1", "Multiple defaults in generic");