Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix merging and renaming of inlines #124

Merged
merged 15 commits into from
Nov 23, 2022
Merged

Conversation

stilscher
Copy link
Member

@stilscher stilscher commented Nov 15, 2022

The renaming of inline functions was broken in that multiple functions with the same name were outputted in the merged CIL file. This also lead to difficulties with the incremental analysis in Goblint, because globals are expected to have a unique name (goblint/analyzer#836). Also, the merging of inline functions was not correct, because inline functions with different bodies would not be renamed and the wrong version of a function would be called.

This PR aims at fixing that. For this, a distinction is made which C Standard is used, i.e. whether the gnu89 or c99 inline semantics needs to be used. They differ in that for c99 inline functions have internal linkage by default, unless extern inline is used, whereas it is opposite for gnu89. They agree on static inline functions that can in both cases only be called from the same translation unit.

This is reflected in the following changes:

  • matchVarinfo is only called for functions that can be called from other translation units. It assumes that the respective global has a unique name and aligns multiple occurrences (for example declarations) and creates a single varinfo for it. For inline functions that have internal linkage only, we instead call getNode.
  • All internal inline functions are renamed to avoid duplicate names. When inline functions are successfully merged, this renaming is reverted.
  • To distinguish between the different inline semantics, a c standard option is introduced. One can choose between c90, c99, c11 and gnu89inline, which represent the group of language standards and dialects close to it. The old inline semantics is used when set to c90 or gnu89inline while the newer one is used in the other cases. When using cilly, the option is set based on the gcc language options specified (default: c99). Otherwise the option can also be set through the configuration of Goblint (Option to set the C language standard for CIL in Goblint analyzer#905).

Closes #120

@sim642
Copy link
Member

sim642 commented Nov 16, 2022

  • All internal inline functions are renamed to avoid duplicate names. When inline functions are successfully merged, this renaming is reverted.

That means if only a single file containing inline functions is involved, so no merging happens at all, then it won't have its original name even though it's the easiest case where it should have?

@stilscher
Copy link
Member Author

That means if only a single file containing inline functions is involved, so no merging happens at all, then it won't have its original name even though it's the easiest case where it should have?

No, that is not the case. Renaming here means, it finds a new name (e.g. add__0) only if another function with the same name was already encountered. Otherwise the original name (e.g. add) is just kept.

@michael-schwarz michael-schwarz self-requested a review November 22, 2022 13:24
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apart from my small comments above, this looks good to me!

@jerhard jerhard self-requested a review November 23, 2022 13:58
@michael-schwarz
Copy link
Member

LGTM!

@stilscher stilscher merged commit 56a58af into develop Nov 23, 2022
@stilscher stilscher deleted the fix-renaming-when-merging branch November 23, 2022 17:12
@sim642 sim642 added this to the 2.0.2 milestone Apr 5, 2023
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 11, 2023
CHANGES:

* Rename `Rmtmps` to `RmUnused` (goblint/cil#135).
* Add option to add return statement to `noreturn` functions (goblint/cil#129).
* Fix empty `if`s being removed (goblint/cil#140).
* Fix `_Float128` support (goblint/cil#118, goblint/cil#119).
* Fix C11 `_Alignas` computation (goblint/cil#130).
* Fix renaming and merging of `inline` functions based on C standard (goblint/cil#120, goblint/cil#124).
* Fix `Pretty` not resetting all global state between calls (goblint/cil#133, goblint/cil#134).
* Fix `fundec` location in merger (goblint/cil#139).
* Fix `cilly` patcher (goblint/cil#128).
* Disable basename by default in parser.
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
CHANGES:

* Rename `Rmtmps` to `RmUnused` (goblint/cil#135).
* Add option to add return statement to `noreturn` functions (goblint/cil#129).
* Fix empty `if`s being removed (goblint/cil#140).
* Fix `_Float128` support (goblint/cil#118, goblint/cil#119).
* Fix C11 `_Alignas` computation (goblint/cil#130).
* Fix renaming and merging of `inline` functions based on C standard (goblint/cil#120, goblint/cil#124).
* Fix `Pretty` not resetting all global state between calls (goblint/cil#133, goblint/cil#134).
* Fix `fundec` location in merger (goblint/cil#139).
* Fix `cilly` patcher (goblint/cil#128).
* Disable basename by default in parser.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Cil keeps inline and non-inline function with same name
4 participants