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

Principled fix for Apron-Domain Top #1380

Open
michael-schwarz opened this issue Mar 3, 2024 · 1 comment
Open

Principled fix for Apron-Domain Top #1380

michael-schwarz opened this issue Mar 3, 2024 · 1 comment
Labels
bug cleanup Refactoring, clean-up relational Relational analyses (Apron, affeq, lin2var)

Comments

@michael-schwarz
Copy link
Member

As discussed here

https://github.com/goblint/analyzer/pull/1354/files/05bd808ad40aea8555f53f1d235f257d26d67988#r1498877891

and in the GobCon.

A separate T is to be introduced that conceptually ranges over the entire environment. I gave it a shot today, but turns out it is a major rewrite that I don't have time for before wrapping up my thesis.
Among other things, it and also entails carefully thinking about where variable values are only forgotten as opposed to removed from the environment.

Creating this separate issue for the principled fix allows merging #1354 which is not the grand unified fix but a step in the right direction (and away from a setup which we know to be unsound) which also allows for experiments in a setting that is not unsound.

@michael-schwarz
Copy link
Member Author

Is this not just a workaround for the actual bug? Seems like escapes should also contribute to mutex_inits.
BasePriv.PerMutexPrivBase and BasePriv.PerMutexMeetTIDPriv side-effect escapes to mutex_inits at least.

Originally posted by @sim642 in #1354 (comment)

Is a further issue we should investigate while fixing the lattice here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug cleanup Refactoring, clean-up relational Relational analyses (Apron, affeq, lin2var)
Projects
None yet
Development

No branches or pull requests

1 participant