Rename functions with `gnu_inline` attribute when inline merging is off by stilscher · Pull Request #85 · goblint/cil

stilscher · 2022-03-23T16:00:59Z

With gcc 4.3 the semantic of extern inline was changed to conform with the ISO C99 standard (https://gcc.gnu.org/gcc-4.3/porting_to.html). Functions that should still have the GNU extern inline behavior have the attribute __attribute__((__gnu_inline__)). A function with this attribute in a header that is included in multiple different translation units leads to multiple function variables with the same name. This violates the check that was added with goblint/analyzer@39d7288. By renaming function variables, that have this gnu_inline attribute, whenever inline functions are not merged, fixes this. Below is an example where the problem can be observed:

./goblint --enable incremental.save --disable incremental.load file1.c file2.c
./goblint --disable incremental.save --enable incremental.load file1.c file2.c
or alternatively using --set pre.cppflags[+] -fgnu89-inline instead of the __attribute__((__gnu_inline__)) in the function definition

//file.h
extern inline __attribute__((__gnu_inline__)) int foo()
{ return 5; }

//file1.c
#include "file.h"
int goo() {
    return 2;
}

//file2.c
#include <assert.h>
#include "file.h"
int main() {
    int x = goo();
    assert(x == 2);
    return 0;
}

sim642 · 2022-03-24T15:01:51Z

src/mergecil.ml

      else begin
        (* Maybe it is static. Rename it then *)
-        if vi.vstorage = Static then begin
+        if vi.vstorage = Static || (not !merge_inlines && hasAttribute "gnu_inline" (typeAttrs vi.vtype)) then begin


I'm a bit confused why this fix is here, instead of where all the other no-merge_inlines code is:

cil/src/mergecil.ml

Lines 1549 to 1586 in d07f7db

(* either the function is not inline, or we're not attempting to

* merge inlines *)

if (mergeGlobals &&

not fdec'.svar.vinline &&

fdec'.svar.vstorage <> Static) then

begin

(* sm: this is a non-inline, non-static function. I want to

* consider dropping it if a same-named function has already

* been put into the merged file *)

let curSum = (functionChecksum fdec') in

(*(trace "mergeGlob" (P.dprintf "I see extern function %s, sum is %d\n"*)

(* fdec'.svar.vname curSum));*)

try

let prevFun, prevLoc, prevSum =

(H.find emittedFunDefn fdec'.svar.vname) in

(* previous was found *)

if (curSum = prevSum) then

(trace "mergeGlob"

(P.dprintf "dropping duplicate def'n of func %s at %a in favor of that at %a\n"

fdec'.svar.vname d_loc l d_loc prevLoc))

else begin

(* the checksums differ, so print a warning but keep the

* older one to avoid a link error later. I think this is

* a reasonable approximation of what ld does. *)

(ignore (warn "def'n of func %s at %a (sum %d) conflicts with the one at %a (sum %d); keeping the one at %a."

fdec'.svar.vname d_loc l curSum d_loc prevLoc

prevSum d_loc prevLoc))

end

with Not_found -> begin

(* there was no previous definition *)

(mergePushGlobal g');

(H.add emittedFunDefn fdec'.svar.vname (fdec', l, curSum))

end

end else begin

(* not attempting to merge global functions, or it was static

* or inline *)

mergePushGlobal g'

end

None of that code deals with inlines though (not fdec'.svar.vinline), and it makes sense to treat these functions as if they were static when the gnu_inline attribute is set.

The code I linked is in the else branch of the actual inlines merging. And the else branch of this at the very end is where everything else is considered, so it seems to me like the fix should be there.

The bigger issue with it being in processVarinfo is related to #84 (where variables get merged, but functions don't), just in the other direction (here we avoid merging variables with __gnu_inline__, but the renaming is distinct from the merging itself). The logic of whether to merge or not is duplicated and different between processVarinfo and below, where I linked, and this is just deepening the difference. It's not helping anything to avoid inconsistencies.

Bump goblint-cil (goblint/cil#85)

CHANGES: * Wrap library into `GoblintCil` module (goblint/cil#107). * Remove all MSVC support (goblint/cil#52, goblint/cil#88). * Port entire build process from configure/make to dune (goblint/cil#104). * Add C11 `_Generic` support (goblint/cil#48). * Add C11 `_Noreturn` support (goblint/cil#58). * Add C11 `_Static_assert` support (goblint/cil#62). * Add C11 `_Alignof` support (goblint/cil#66). * Add C11 `_Alignas` support (goblint/cil#93, goblint/cil#108). * Add partial C11 `_Atomic` support (goblint/cil#61). * Add `_Float32`, `_Float64`, `_Float32x` and `_Float64x` type support (goblint/cil#8, goblint/cil#60). * Add Universal Character Names, `char16_t` and `char32_t` type support (goblint/cil#80). * Change locations to location spans and add additional expression locations (goblint/cil#51). * Add synthetic marking for CIL-inserted statement locations (goblint/cil#98). * Expose list of files from line control directives (goblint/cil#73). * Add parsed location transformation hook (goblint/cil#89). * Use Zarith for integer constants (goblint/cil#47, goblint/cil#53). * Fix constant folding overflows (goblint/cil#59). * Add option to disable constant branch removal (goblint/cil#103). * Add standalone expression parsing and checking (goblint/cil#97, goblint/cil#96). * Improve inline function merging (goblint/cil#72, goblint/cil#85, goblint/cil#84, goblint/cil#86). * Fix some attribute parsing cases (goblint/cil#71, goblint/cil#75, goblint/cil#76, goblint/cil#77). * Fix global NaN initializers (goblint/cil#78, goblint/cil#79). * Fix `cilly` binary installation (goblint/cil#99, goblint/cil#100, goblint/cil#102). * Remove batteries dependency to support OCaml 5 (goblint/cil#106).

rename gnu_inline functions if not merging

2c78d00

michael-schwarz self-requested a review March 23, 2022 16:36

stilscher changed the title ~~rename gnu_inline functions if not merging~~ Rename gnu_inline functions if inline merging turned off Mar 23, 2022

michael-schwarz changed the title ~~Rename gnu_inline functions if inline merging turned off~~ Rename functions with gnu_inline attribute if inline merging turned off Mar 24, 2022

michael-schwarz changed the title ~~Rename functions with gnu_inline attribute if inline merging turned off~~ Rename functions with gnu_inline attribute when inline merging is off Mar 24, 2022

Add test

9fa623f

michael-schwarz marked this pull request as ready for review March 24, 2022 13:57

michael-schwarz approved these changes Mar 24, 2022

View reviewed changes

michael-schwarz merged commit d07f7db into develop Mar 24, 2022

michael-schwarz added a commit to goblint/analyzer that referenced this pull request Mar 24, 2022

Bump goblint-cil (goblint/cil#85)

2e2b02b

michael-schwarz mentioned this pull request Mar 24, 2022

Bump goblint-cil (https://github.com/goblint/cil/pull/85) goblint/analyzer#665

Merged

sim642 reviewed Mar 24, 2022

View reviewed changes

michael-schwarz added a commit to goblint/analyzer that referenced this pull request Mar 29, 2022

Merge pull request #665 from goblint/bump_cil_85

fe5c98d

Bump goblint-cil (goblint/cil#85)

sim642 deleted the fix_extern_inline branch May 30, 2022 07:12

sim642 added this to the 2.0.0 milestone Aug 12, 2022

sim642 mentioned this pull request Aug 12, 2022

[new release] goblint-cil (2.0.0) ocaml/opam-repository#21975

Merged

sim642 mentioned this pull request May 18, 2023

Extern inline functions are handled incorrectly when merge_inlines is false #142

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rename functions with `gnu_inline` attribute when inline merging is off#85

Rename functions with `gnu_inline` attribute when inline merging is off#85
michael-schwarz merged 2 commits intodevelopfrom
fix_extern_inline

stilscher commented Mar 23, 2022 •

edited

Loading

Uh oh!

sim642 Mar 24, 2022

Uh oh!

michael-schwarz Mar 24, 2022 •

edited

Loading

Uh oh!

sim642 Mar 24, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

	(* either the function is not inline, or we're not attempting to
	* merge inlines *)
	if (mergeGlobals &&
	not fdec'.svar.vinline &&
	fdec'.svar.vstorage <> Static) then
	begin
	(* sm: this is a non-inline, non-static function. I want to
	* consider dropping it if a same-named function has already
	* been put into the merged file *)
	let curSum = (functionChecksum fdec') in
	((trace "mergeGlob" (P.dprintf "I see extern function %s, sum is %d\n")
	(* fdec'.svar.vname curSum));*)
	try
	let prevFun, prevLoc, prevSum =
	(H.find emittedFunDefn fdec'.svar.vname) in
	(* previous was found *)
	if (curSum = prevSum) then
	(trace "mergeGlob"
	(P.dprintf "dropping duplicate def'n of func %s at %a in favor of that at %a\n"
	fdec'.svar.vname d_loc l d_loc prevLoc))
	else begin
	(* the checksums differ, so print a warning but keep the
	* older one to avoid a link error later. I think this is
	* a reasonable approximation of what ld does. *)
	(ignore (warn "def'n of func %s at %a (sum %d) conflicts with the one at %a (sum %d); keeping the one at %a."
	fdec'.svar.vname d_loc l curSum d_loc prevLoc
	prevSum d_loc prevLoc))
	end
	with Not_found -> begin
	(* there was no previous definition *)
	(mergePushGlobal g');
	(H.add emittedFunDefn fdec'.svar.vname (fdec', l, curSum))
	end
	end else begin
	(* not attempting to merge global functions, or it was static
	* or inline *)
	mergePushGlobal g'
	end

Conversation

stilscher commented Mar 23, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sim642 Mar 24, 2022

Choose a reason for hiding this comment

Uh oh!

michael-schwarz Mar 24, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sim642 Mar 24, 2022

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

stilscher commented Mar 23, 2022 •

edited

Loading

michael-schwarz Mar 24, 2022 •

edited

Loading