From 7a522fc74d1704cc54044abc0e498bbfa5a8a75f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 25 Jul 2024 13:28:47 +0300 Subject: [PATCH 01/11] Add test for assign in attribute (issue #168) --- test/small1/attr-assign.c | 7 +++++++ test/testcil.pl | 1 + 2 files changed, 8 insertions(+) create mode 100755 test/small1/attr-assign.c diff --git a/test/small1/attr-assign.c b/test/small1/attr-assign.c new file mode 100755 index 000000000..8b83facc0 --- /dev/null +++ b/test/small1/attr-assign.c @@ -0,0 +1,7 @@ +// From some new MacOS headers: https://github.com/goblint/cil/issues/168 + +void foo(void) __attribute__((availability(macos,introduced=10.15))); + +void foo(void) { + return; +} diff --git a/test/testcil.pl b/test/testcil.pl index a33e9af7a..c8bcd082f 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -222,6 +222,7 @@ sub addToGroup { addTest("test/attr11 _GNUCC=1"); addTest("test/attr12 _GNUCC=1"); addTest("test/attr13 _GNUCC=1"); +addTest("test/attr-assign"); addTest("testrun/packed _GNUCC=1 WARNINGS_ARE_ERRORS=1"); addTest("test/packed2 _GNUCC=1"); addTest("test/bitfield"); From 659e310f5e3e8859ba79681ec13bcdc2b08aad32 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 25 Jul 2024 14:07:14 +0300 Subject: [PATCH 02/11] Add attribute assignment to parser --- src/frontc/cparser.mly | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index db8431cdc..51e813264 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1619,8 +1619,12 @@ conditional_attr: | logical_or_attr QUEST conditional_attr COLON conditional_attr { QUESTION($1, $3, $5) } +assignment_attr: + conditional_attr { $1 } +| unary_attr EQ assignment_attr { BINARY(ASSIGN, $1, $3) } -attr: conditional_attr { $1 } + +attr: assignment_attr { $1 } ; attr_list_ne: From bfb5f545da291a112c051a74b53c517adb64c10e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 25 Jul 2024 14:07:25 +0300 Subject: [PATCH 03/11] Add attribute float to parser --- src/frontc/cparser.mly | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 51e813264..9c010cd80 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1494,6 +1494,7 @@ primary_attr: | LPAREN attr RPAREN { $2 } | IDENT IDENT { CALL(VARIABLE (fst $1), [VARIABLE (fst $2)]) } | CST_INT { CONSTANT(CONST_INT (fst $1)) } +| CST_FLOAT { CONSTANT(CONST_FLOAT (fst $1)) } | const_string_or_wstring { CONSTANT(fst $1) } /*(* Const when it appears in attribute lists, is translated From 551e46066885f8f6dfb7eccbd4e712c2c09c371a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 25 Jul 2024 13:40:47 +0300 Subject: [PATCH 04/11] Add AAssign --- src/cil.ml | 10 ++++++++++ src/cil.mli | 1 + 2 files changed, 11 insertions(+) diff --git a/src/cil.ml b/src/cil.ml index 4bec87a9c..53bed82eb 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -344,6 +344,7 @@ and attrparam = | AAddrOf of attrparam (** & a **) | AIndex of attrparam * attrparam (** a1[a2] *) | AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **) + | AAssign of attrparam * attrparam (** a1 = a2 *) (** Information about a composite type (a struct or a union). Use @@ -1874,6 +1875,7 @@ let additiveLevel = 60 let comparativeLevel = 70 let bitwiseLevel = 75 let questionLevel = 100 +let assignLevel = 110 let getParenthLevel (e: exp) = match e with | Question _ -> questionLevel @@ -1924,6 +1926,7 @@ let getParenthLevelAttrParam (a: attrparam) = | AAddrOf _ -> 30 | ADot _ | AIndex _ | AStar _ -> 20 | AQuestion _ -> questionLevel + | AAssign _ -> assignLevel let isIntegralType t = @@ -4423,6 +4426,9 @@ class defaultCilPrinterClass : cilPrinter = object (self) self#pAttrParam () a1 ++ text " ? " ++ self#pAttrParam () a2 ++ text " : " ++ self#pAttrParam () a3 + | AAssign (a1, a2) -> + self#pAttrParam () a1 ++ text "=" ++ + self#pAttrParam () a2 (* A general way of printing lists of attributes *) @@ -5561,6 +5567,10 @@ and childrenAttrparam (vis: cilVisitor) (aa: attrparam) : attrparam = let e3' = fAttrP e3 in if e1' != e1 || e2' != e2 || e3' != e3 then AQuestion (e1', e2', e3') else aa + | AAssign (e1, e2) -> + let e1' = fAttrP e1 in + let e2' = fAttrP e2 in + if e1' != e1 || e2' != e2 then AAssign (e1', e2') else aa let rec visitCilFunction (vis : cilVisitor) (f : fundec) : fundec = diff --git a/src/cil.mli b/src/cil.mli index 099b6e8ea..4464d4c20 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -338,6 +338,7 @@ and attrparam = | AAddrOf of attrparam (** & a **) | AIndex of attrparam * attrparam (** a1[a2] *) | AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **) + | AAssign of attrparam * attrparam (** a1 = a2 *) (** {b Structures.} The {!compinfo} describes the definition of a structure or union type. Each such {!compinfo} must be defined at the From e684426a965a7b069de9bae4c8d7ddfc885194a3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 25 Jul 2024 14:06:47 +0300 Subject: [PATCH 05/11] Add AAssign to Cabs2cil --- src/frontc/cabs2cil.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 83d135ac8..b3f6c9173 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -2940,6 +2940,8 @@ and doAttr (a: A.attribute) : attribute list = ABinOp(LAnd, ae aa1, ae aa2) | A.BINARY(A.OR, aa1, aa2) -> ABinOp(LOr, ae aa1, ae aa2) + | A.BINARY(A.ASSIGN, aa1, aa2) -> + AAssign(ae aa1, ae aa2) | A.BINARY(abop, aa1, aa2) -> ABinOp (convBinOp abop, ae aa1, ae aa2) | A.UNARY(A.PLUS, aa) -> ae aa From ce1c7f7f6f1db90061ac6ff7caaf4e5fb2d71028 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 26 Jul 2024 10:50:43 +0300 Subject: [PATCH 06/11] Add float attributes to Cabs2cil --- src/frontc/cabs2cil.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index b3f6c9173..85dd9c092 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -2927,6 +2927,7 @@ and doAttr (a: A.attribute) : attribute list = | _ -> E.s (error "Invalid attribute constant: %s") end + | A.CONSTANT (A.CONST_FLOAT str) -> ACons (str, []) | A.CALL(A.VARIABLE n, args) -> begin let n' = if strip then stripUnderscore n else n in let ae' = Util.list_map ae args in From a1b28f2b696e1ad74b2bf9c81db8f979a0fd444f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 25 Jul 2024 14:21:16 +0300 Subject: [PATCH 07/11] Comment out attr-assign test --- test/testcil.pl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/testcil.pl b/test/testcil.pl index c8bcd082f..be107b9d7 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -222,7 +222,7 @@ sub addToGroup { addTest("test/attr11 _GNUCC=1"); addTest("test/attr12 _GNUCC=1"); addTest("test/attr13 _GNUCC=1"); -addTest("test/attr-assign"); +# addTest("test/attr-assign"); # TODO: only on OSX, Linux GCC errors on introduced addTest("testrun/packed _GNUCC=1 WARNINGS_ARE_ERRORS=1"); addTest("test/packed2 _GNUCC=1"); addTest("test/bitfield"); From 70a430312f6e93acf4f59af08ac65a225dc62852 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 25 Jul 2024 17:46:45 +0300 Subject: [PATCH 08/11] Disable some GCC 14 errors in tests --- test/Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/test/Makefile b/test/Makefile index 27f09f2b8..189d391b8 100644 --- a/test/Makefile +++ b/test/Makefile @@ -127,6 +127,9 @@ ifdef SEPARATE CILLY+= --nomerge endif +# Disable GCC 14 new warnings as errors because some tests contain them +CFLAGS += -Wno-error=implicit-int -Wno-error=implicit-function-declaration -Wno-error=int-conversion -Wno-error=incompatible-pointer-types + # sm: this will make gcc warnings into errors; it's almost never # what we want, but for a particular testcase (combine_copyptrs) # I need it to show the difference between something which works From 453a777040c7c1aee8a4b1d511d73491a249d03f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 26 Jul 2024 10:45:42 +0300 Subject: [PATCH 09/11] Add availability attribute with multiple dots to test --- test/small1/attr-assign.c | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/test/small1/attr-assign.c b/test/small1/attr-assign.c index 8b83facc0..ae7712d98 100755 --- a/test/small1/attr-assign.c +++ b/test/small1/attr-assign.c @@ -5,3 +5,10 @@ void foo(void) __attribute__((availability(macos,introduced=10.15))); void foo(void) { return; } + +// Version numbers may have multiple dots: https://github.com/goblint/cil/pull/171#issuecomment-2250670652 +void bar(void) __attribute__((availability(macos,introduced=10.13.4))); + +void bar(void) { + return; +} From f441f5496b41d249bbe848c9d90a459c9dcf9255 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 26 Jul 2024 10:52:13 +0300 Subject: [PATCH 10/11] Add hack for parsing version numbers with multiple dots --- src/frontc/cparser.mly | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 9c010cd80..4983a3c37 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1495,6 +1495,7 @@ primary_attr: | IDENT IDENT { CALL(VARIABLE (fst $1), [VARIABLE (fst $2)]) } | CST_INT { CONSTANT(CONST_INT (fst $1)) } | CST_FLOAT { CONSTANT(CONST_FLOAT (fst $1)) } +| CST_FLOAT CST_FLOAT { CONSTANT(CONST_FLOAT (fst $1 ^ fst $2)) } /* Clang-like hack to parse version numbers like "10.13.4" (https://github.com/goblint/cil/pull/171#issuecomment-2250670652). We lex them as "10.13" and ".4". */ | const_string_or_wstring { CONSTANT(fst $1) } /*(* Const when it appears in attribute lists, is translated From ac3a40a5dbafd3e12d080526f0ed44061cf52548 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 26 Jul 2024 11:25:02 +0300 Subject: [PATCH 11/11] Exclude nonsense kernel1 test --- test/small2/kernel1.c | 2 +- test/testcil.pl | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/test/small2/kernel1.c b/test/small2/kernel1.c index 46c2673f7..05f8814d2 100644 --- a/test/small2/kernel1.c +++ b/test/small2/kernel1.c @@ -1,4 +1,4 @@ - +// This test is nonsense: DECLARE_WAIT_QUEUE_HEAD is a macro in Linux kernel DECLARE_WAIT_QUEUE_HEAD(log_wait); diff --git a/test/testcil.pl b/test/testcil.pl index be107b9d7..64c8c1a97 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -658,7 +658,7 @@ sub addToGroup { addBadComment("scott/globalprob", "Notbug. Not a bug if fails on a non-Linux machine ;-)"); addTest("scott/bisonerror $gcc"); addTest("scott/cmpzero"); -addTest("scott/kernel1 $gcc"); +# addTest("scott/kernel1 $gcc"); addTest("scott/kernel2 $gcc"); addTest("scott/xcheckers $gcc"); addTest("scott/memberofptr $gcc");