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

Not merging inlines breaks fundec invariant #84

Closed
sim642 opened this issue Feb 28, 2022 · 1 comment · Fixed by #86
Closed

Not merging inlines breaks fundec invariant #84

sim642 opened this issue Feb 28, 2022 · 1 comment · Fixed by #86
Labels
Milestone

Comments

@sim642
Copy link
Member

sim642 commented Feb 28, 2022

fundec claims the invariant that the physical objects are in one-to-one correspondence with varinfos:

cil/src/cil.ml

Lines 688 to 694 in c47bbbd

(** Function definitions. *)
and fundec =
{ mutable svar: varinfo;
(** Holds the name and type as a variable, so we can refer to it
* easily from the program. All references to this function either
* in a function call or in a prototype must point to the same
* varinfo. *)

And Goblint relies on this invariant by identifying functions by the underlying variable (ID).

In goblint/analyzer#603 (comment), I realized that #72 broke this invariant.
This is also easily seen in the code:

cil/src/mergecil.ml

Lines 1421 to 1425 in c47bbbd

| GFun (fdec, l) as g ->
currentLoc := l;
incr currentDeclIdx;
(* We apply the renaming *)
fdec.svar <- processVarinfo fdec.svar l;

where the underlying variable is replaced unconditionally (of merge_inlines).

@stilscher
Copy link
Member

What do you mean with physical object? The invariant just says, that all references to a function must point to the same varinfo. So different instances of a function (for example two instances of a static inline function that has not been merged) could still have different varinfos as long as they are consistent with the respective function calls, right?

@sim642 sim642 added this to the 2.0.0 milestone Aug 12, 2022
sim642 added a commit to sim642/opam-repository that referenced this issue Aug 12, 2022
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).
sim642 added a commit to sim642/opam-repository that referenced this issue Aug 12, 2022
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants