diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index e8284c4df..6c9b42d3b 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -4,6 +4,7 @@ name: build and run tests on: - push - pull_request + - workflow_dispatch jobs: tests: diff --git a/CHANGES.md b/CHANGES.md index 1122f4fd0..e0b9d1d51 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,9 @@ +## 2.0.4 +* Add `Return` statement expression location (#167). +* Add `availability` attribute support (#168, #171). +* Remove unused `Libmaincil` module (#165). +* Fix some synthetic locations (#166, #167). + ## 2.0.3 * Add `asm inline` parsing (#151). * Ignore top level qualifiers in `__builtin_types_compatible_p` (#157). diff --git a/META.goblint-cil.template b/META.goblint-cil.template index e5aba4bb2..cf051e8fe 100644 --- a/META.goblint-cil.template +++ b/META.goblint-cil.template @@ -2,10 +2,10 @@ package "default-features" ( requires="goblint-cil.dataslicing goblint-cil.liveness goblint-cil.pta goblint-cil.makecfg goblint-cil.syntacticsearch" -version = "2.0.3" +version = "2.0.4" ) package "all-features" ( requires="goblint-cil.dataslicing goblint-cil.liveness goblint-cil.pta goblint-cil.makecfg goblint-cil.zrapp goblint-cil.syntacticsearch" -version = "2.0.3" +version = "2.0.4" ) diff --git a/README.md b/README.md index 2fc45c67f..049e27287 100644 --- a/README.md +++ b/README.md @@ -84,7 +84,7 @@ instance in the OCaml toplevel using [Findlib][findlib]: # #require "goblint-cil";; [...] # GoblintCil.cilVersion;; - - : string = "2.0.3" + - : string = "2.0.4" [findlib]: http://projects.camlcity.org/projects/findlib.html diff --git a/dune-project b/dune-project index b6e92840b..e0929b4e5 100644 --- a/dune-project +++ b/dune-project @@ -2,7 +2,7 @@ (name goblint-cil) (implicit_transitive_deps false) (generate_opam_files true) -(version 2.0.3) +(version 2.0.4) (source (github goblint/cil)) ; (documentation "https://goblint.github.io/cil") (authors "George Necula" "Scott McPeak" "Westley Weimer" "Gabriel Kerneis" "Ralf Vogler" "Michael Schwarz" "Simmo Saan") diff --git a/goblint-cil.opam b/goblint-cil.opam index cf5377505..17e39f5a1 100644 --- a/goblint-cil.opam +++ b/goblint-cil.opam @@ -1,6 +1,6 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" -version: "2.0.3" +version: "2.0.4" synopsis: "A front-end for the C programming language that facilitates program analysis and transformation" description: """ @@ -64,4 +64,4 @@ depexts: [ ["perl-FindBin"] {os-distribution = "fedora"} ["build-base"] {os-distribution = "alpine"} ] -available: arch = "x86_64" +available: arch = "x86_64" | arch = "arm64" diff --git a/goblint-cil.opam.template b/goblint-cil.opam.template index e98127179..f48259706 100644 --- a/goblint-cil.opam.template +++ b/goblint-cil.opam.template @@ -3,4 +3,4 @@ depexts: [ ["perl-FindBin"] {os-distribution = "fedora"} ["build-base"] {os-distribution = "alpine"} ] -available: arch = "x86_64" +available: arch = "x86_64" | arch = "arm64" diff --git a/src/check.ml b/src/check.ml index 06a030223..1fc37396f 100644 --- a/src/check.ml +++ b/src/check.ml @@ -390,7 +390,7 @@ and checkEnumInfo (isadef: defuse) enum = (* Add it to the map before we go on *) H.add enumUsed enum.ename (enum, ref isadef); checkAttributes enum.eattr; - List.iter (fun (tn, _, _) -> defineName tn) enum.eitems; + List.iter (fun (tn, attrs, _, _) -> defineName tn; checkAttributes attrs) enum.eitems; end and checkTypeInfo (isadef: defuse) ti = diff --git a/src/cil.ml b/src/cil.ml index 4bec87a9c..b40466fe8 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 @@ -398,7 +399,7 @@ and fieldinfo = { enumeration. Make sure you have a [GEnumTag] for each of of these. *) and enuminfo = { mutable ename: string; (** The name. Always non-empty *) - mutable eitems: (string * exp * location) list; (** Items with names + mutable eitems: (string * attributes * exp * location) list; (** Items with names and values. This list should be non-empty. The item @@ -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 = @@ -4011,8 +4014,10 @@ class defaultCilPrinterClass : cilPrinter = object (self) text "enum" ++ align ++ text (" " ^ enum.ename) ++ text " {" ++ line ++ (docList ~sep:(chr ',' ++ line) - (fun (n,i, loc) -> - text (n ^ " = ") + (fun (n, attrs, i, loc) -> + text n + ++ self#pAttrs () attrs + ++ text (n ^ " = ") ++ self#pExp () i) () enum.eitems) ++ unalign ++ line ++ text "} " @@ -4423,6 +4428,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 +5569,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 = @@ -5612,7 +5624,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global = | GEnumTag (enum, _) -> (* (trace "visit" (dprintf "visiting global enum %s\n" enum.ename)); *) (* Do the values and attributes of the enumerated items *) - let itemVisit (name, exp, loc) = (name, visitCilExpr vis exp, loc) in + let itemVisit (name, attrs, exp, loc) = (name, visitCilAttributes vis attrs, visitCilExpr vis exp, loc) in enum.eitems <- mapNoCopy itemVisit enum.eitems; enum.eattr <- visitCilAttributes vis enum.eattr; g diff --git a/src/cil.mli b/src/cil.mli index 099b6e8ea..d63e5535f 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 @@ -422,7 +423,7 @@ and fieldinfo = { and enuminfo = { mutable ename: string; (** The name. Always non-empty. *) - mutable eitems: (string * exp * location) list; + mutable eitems: (string * attributes * exp * location) list; (** Items with names and values. This list should be non-empty. The item values must be compile-time constants. *) mutable eattr: attributes; diff --git a/src/dune b/src/dune index 92375f31c..ef8e36031 100644 --- a/src/dune +++ b/src/dune @@ -4,7 +4,7 @@ (public_name goblint-cil) (name goblintCil) (libraries zarith unix str stdlib-shims) - (modules (:standard \ main mainFeature ciloptions machdepConfigure modelConfigure)) + (modules (:standard \ main mainFeature ciloptions machdepConfigure machdepArchConfigure modelConfigure)) ) (executable @@ -21,6 +21,21 @@ (target machdep-ml.exe) (action (run %{read-lines:../bin/real-gcc} -D_GNUCC machdep-ml.c -o %{target}))) +(executable + (name machdepArchConfigure) + (modules machdepArchConfigure) + (libraries dune-configurator)) + +(rule + (deps machdep-config.h machdep-ml.c) + (target machdep32) + (action (with-stdout-to %{target} (run ./machdepArchConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 32)))) + +(rule + (deps machdep-config.h machdep-ml.c) + (target machdep64) + (action (with-stdout-to %{target} (run ./machdepArchConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 64)))) + ; for Cilly.pm (executable (name modelConfigure) @@ -40,6 +55,7 @@ (action (with-stdout-to %{target} (run ./modelConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 64)))) (rule + (deps machdep32 machdep64) (target machdep.ml) (action (run %{bin:cppo} -V OCAML:%{ocaml_version} %{dep:machdep.cppo.ml} -x machdep:./%{dep:machdep-ml.exe} diff --git a/src/ext/zrapp/zrapp.ml b/src/ext/zrapp/zrapp.ml index a1fd7e498..bd3fef444 100644 --- a/src/ext/zrapp/zrapp.ml +++ b/src/ext/zrapp/zrapp.ml @@ -412,8 +412,10 @@ class zraCilPrinterClass : cilPrinter = object (self) text "enum" ++ align ++ text (" " ^ enum.ename) ++ self#pAttrs () enum.eattr ++ text " {" ++ line ++ (docList ~sep:(chr ',' ++ line) - (fun (n,i, loc) -> - text (n ^ " = ") + (fun (n, attrs, i, loc) -> + text n + ++ self#pAttrs () attrs + ++ text (n ^ " = ") ++ self#pExp () i) () enum.eitems) ++ unalign ++ line ++ text "};\n" diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index 7a9db7b14..4ac432e04 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -168,7 +168,7 @@ and init_name = name * init_expression and single_name = specifier * name -and enum_item = string * expression * cabsloc +and enum_item = string * attribute list * expression * cabsloc (* ** Declaration definition (at toplevel) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 83d135ac8..707612f6b 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -2675,7 +2675,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of | [A.Tenum (n, Some eil, extraAttrs)] -> (* A definition of an enum *) let rec justNames eil = match eil with [] -> [] - | (str, expr, loc) :: eis -> str :: justNames eis + | (str, attrs, expr, loc) :: eis -> str :: justNames eis in let names = justNames eil in let n' = @@ -2721,7 +2721,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of else IULongLong (* assume there can be not enum constants that don't fit in long long since there can only be 128bit constants if long long is also 128bit *) in (* as each name,value pair is determined, this is called *) - let rec processName kname (i: exp) loc rest = begin + let rec processName kname attrs (i: exp) loc rest = begin (* add the name to the environment, but with a faked 'typ' field; we don't know the full type yet (since that includes all of the tag values), but we won't need them in here *) @@ -2731,16 +2731,16 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of environment when we're finished *) let newname, _ = newAlphaName true "" kname in - (kname, (newname, i, loc)) :: loop (increm i 1) rest + (kname, (newname, doAttributes attrs, i, loc)) :: loop (increm i 1) rest end and loop i = function [] -> [] - | (kname, A.NOTHING, cloc) :: rest -> + | (kname, attrs, A.NOTHING, cloc) :: rest -> (* use the passed-in 'i' as the value, since none specified *) - processName kname i (convLoc cloc) rest + processName kname attrs i (convLoc cloc) rest - | (kname, e, cloc) :: rest -> + | (kname, attrs, e, cloc) :: rest -> (* constant-eval 'e' to determine tag value *) let e' = getIntConstExp e in let e'' = @@ -2750,7 +2750,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of if !lowerConstants then kintegerCilint ik n else e' | _ -> E.s (error "Constant initializer %a not an integer" d_exp e') in - processName kname e'' (convLoc cloc) rest + processName kname attrs e'' (convLoc cloc) rest in let fields = loop zero eil in @@ -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 @@ -2940,6 +2941,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 diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index 85d44f933..444392e58 100644 --- a/src/frontc/cabsvisit.ml +++ b/src/frontc/cabsvisit.ml @@ -198,9 +198,10 @@ and childrenTypeSpecifier vis ts = let fg' = mapNoCopy childrenFieldGroup fg in if fg' != fg then Tunion( n, Some fg', extraAttrs) else ts | Tenum (n, Some ei, extraAttrs) -> - let doOneEnumItem ((s, e, loc) as ei) = + let doOneEnumItem ((s, attrs, e, loc) as ei) = + let attrs' = visitCabsAttributes vis attrs in let e' = visitCabsExpression vis e in - if e' != e then (s, e', loc) else ei + if attrs' != attrs || e' != e then (s, attrs', e', loc) else ei in vis#vEnterScope (); let ei' = mapNoCopy doOneEnumItem ei in diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index db8431cdc..039162895 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1188,8 +1188,8 @@ enum_list: /* (* ISO 6.7.2.2 *) */ | enum_list COMMA error { $1 } ; enumerator: - IDENT {(fst $1, NOTHING, snd $1)} -| IDENT EQ expression {(fst $1, fst $3, snd $1)} + IDENT attributes {(fst $1, $2, NOTHING, snd $1)} +| IDENT attributes EQ expression {(fst $1, $2, fst $4, snd $1)} ; @@ -1494,6 +1494,8 @@ 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)) } +| 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 @@ -1619,8 +1621,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: diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 2ea32fce6..4194cb051 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -262,10 +262,11 @@ and print_enum_items items = indent (); print_commas true - (fun (id, exp, loc) -> print id; + (fun (id, attrs, exp, loc) -> print id; if exp = NOTHING then () else begin space (); + print_attributes attrs; print "= "; print_expression exp end) diff --git a/src/machdep.cppo.ml b/src/machdep.cppo.ml index 45d734e93..b00ef8cfc 100644 --- a/src/machdep.cppo.ml +++ b/src/machdep.cppo.ml @@ -56,4 +56,11 @@ let gcc = { #ext machdep #endext } + +let gcc32 = +#include "machdep32" + +let gcc64 = +#include "machdep64" + let theMachine : mach ref = ref gcc diff --git a/src/machdepArchConfigure.ml b/src/machdepArchConfigure.ml new file mode 100644 index 000000000..29a249cd0 --- /dev/null +++ b/src/machdepArchConfigure.ml @@ -0,0 +1,21 @@ +module C = Configurator.V1 + +let () = + let real_gcc = ref "" in + let m = ref "" in + let args = Arg.[ + ("--real-gcc", Set_string real_gcc, ""); + ("-m", Set_string m, ""); + ] + in + C.main ~name:"model" ~args (fun c -> + let exe = "./machdep" ^ !m ^ "-ml.exe" in + let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in + if exit_code = 0 then ( + let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe [] in + assert (exit_code = 0); + Printf.printf "Some {%s}" stdout + ) + else + Printf.printf "None" + ) diff --git a/src/mergecil.ml b/src/mergecil.ml index 028649c7b..6de3abc4a 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -701,9 +701,11 @@ (* We check that they are defined in the same way. This is a fairly conservative check. *) List.iter2 - (fun (old_iname, old_iv, _) (iname, iv, _) -> + (fun (old_iname, old_attrs, old_iv, _) (iname, attrs, iv, _) -> if old_iname <> iname then raise (Failure "(different names for enumeration items)"); + if old_attrs <> attrs then + raise (Failure "(different enumerator attributes)"); let samev = match (constFold true old_iv, constFold true iv) with | Const (CInt (oldi, _, _)), Const (CInt (i, _, _)) -> @@ -1545,12 +1547,12 @@ as the variables *) ei.eitems <- Util.list_map - (fun (n, i, loc) -> + (fun (n, attrs, i, loc) -> let newname, _ = A.newAlphaName ~alphaTable:vtAlpha ~undolist:None ~lookupname:n ~data:!currentLoc in - (newname, i, loc)) + (newname, attrs, i, loc)) ei.eitems; mergePushGlobals (visitCilGlobal renameVisitor g) | Some (ei', _) -> diff --git a/src/modelConfigure.ml b/src/modelConfigure.ml index 5b0e8a4ac..a161e703a 100644 --- a/src/modelConfigure.ml +++ b/src/modelConfigure.ml @@ -13,6 +13,7 @@ let () = let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in if exit_code = 0 then ( let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe ["--env"] in + assert (exit_code = 0); print_string stdout; ) else 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 diff --git a/test/small1/attr-assign.c b/test/small1/attr-assign.c new file mode 100755 index 000000000..ae7712d98 --- /dev/null +++ b/test/small1/attr-assign.c @@ -0,0 +1,14 @@ +// 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; +} + +// 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; +} diff --git a/test/small1/attr-enumerator.c b/test/small1/attr-enumerator.c new file mode 100755 index 000000000..2c8f55ecd --- /dev/null +++ b/test/small1/attr-enumerator.c @@ -0,0 +1,8 @@ +// From some new MacOS headers + +enum { + A, + B __attribute__((availability(macos,introduced=10.15))), + C = 5, + D __attribute__((availability(macos,introduced=10.15))) = 7 +} E; 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 a33e9af7a..db75b5b4c 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -222,6 +222,8 @@ sub addToGroup { addTest("test/attr11 _GNUCC=1"); addTest("test/attr12 _GNUCC=1"); addTest("test/attr13 _GNUCC=1"); +# addTest("test/attr-assign"); # TODO: only on OSX, Linux GCC errors on introduced +# addTest("test/attr-enumerator"); # 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"); @@ -657,7 +659,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");