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

Function forward-declarations mishandled in incremental compare and update #627

Closed
sim642 opened this issue Mar 8, 2022 · 3 comments · Fixed by #836
Closed

Function forward-declarations mishandled in incremental compare and update #627

sim642 opened this issue Mar 8, 2022 · 3 comments · Fixed by #836
Assignees
Labels
Milestone

Comments

@sim642
Copy link
Member

sim642 commented Mar 8, 2022

See #609 (comment) and the following comments.

Special care should be taken of GVarDecls that also have corresponding GFuns. The CIL invariant is that if they refer to the same function, they should share a single physical instance of varinfo.
Currently incremental compare and update treats them separately and may update the ID twice, while also breaking the sharing. I suppose we'll have to group all the GVarDecls for a GFun together and do a single update to the varinfo, which is shared by all of them.

@sim642 sim642 added the bug label Mar 8, 2022
@sim642
Copy link
Member Author

sim642 commented Mar 25, 2022

@stilscher Actually the problem described here wasn't about comparing function declarations, although I guess with the uniqueness check it might already fail during comparison.
The issue was with updating the IDs, which is done by iterating over all the globals to number them sequentially, while the declarations and definitions (correctly) share a varinfo. I think here it's not possible to completely ignore them (and they're not updated when updating functions that reference them) because even unused declarations should get fresh IDs that don't accidentally collide with anything else.
Hence the fix to UpdateCil might have to be a bit more involved. For example, first grouping all the to-be-updated globals by their varinfos (which would put a definition together with all the connected declarations) and just update that once.

@stilscher stilscher self-assigned this May 31, 2022
@michael-schwarz
Copy link
Member

@stilscher Is this still the case or is it fixed now?

@stilscher
Copy link
Member

It is still an issue that needs to be fixed.

@sim642 sim642 added this to the v2.2.0 milestone Nov 25, 2022
sim642 added a commit to sim642/opam-repository that referenced this issue Sep 13, 2023
CHANGES:

* Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019).
* Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016).
* Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082).
* Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073).
* Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048).
* Add affine equalities analysis (goblint/analyzer#592).
* Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114).
* Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979).
* Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952).
* Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124).
* Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777).
* Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031).
* Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078).
* Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091).
* Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027).
* Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053).
* Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138).
* Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
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.

3 participants