Skip to content

remove_vector and remove_complex break all irep sharing even when the program doesn't use those features #275

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

Closed
smowton opened this issue Oct 27, 2016 · 4 comments
Assignees

Comments

@smowton
Copy link
Contributor

smowton commented Oct 27, 2016

Suggested patch smowton@274e2ea checks whether the features are in use at all before using subtype, Forall_operands and other functions that break sharing. Processing Sakai (a Java program that obviously can't use either feature) this saved at least 20% of goto-analyzer's memory usage (maybe more, it exhausted by available memory before completing).

One caveat: in programs that do make heavy use of complex and vector types and which have highly nested expressions this may be costly due to repeated re-checking of sub-expressions.

@kroening kroening self-assigned this Oct 27, 2016
@martin-cs
Copy link
Collaborator

On Thu, 2016-10-27 at 03:25 -0700, Chris Smowton wrote:

Suggested patch smowton@274e2ea checks whether the features are in use at all before using subtype, Forall_operands and other functions that break sharing. Processing Sakai (a Java program that obviously can't use either feature) this saved at least 20% of goto-analyzer's memory usage (maybe more, it exhausted by available memory before completing).

From what you've said it seems like this would also affect C and C++.

One caveat: in programs that do make heavy use of complex and vector types and which have highly nested expressions this may be costly due to repeated re-checking of sub-expressions.

More generally, we should be performing sharing-aware traversal and
modification of expressions. There was a move to use a visitor for
this; I think the infrastructure should still be there.

@tautschnig
Copy link
Collaborator

@smowton We should work out to what extent your proposed patch and #150 do exactly the same thing.

@smowton
Copy link
Contributor Author

smowton commented Jan 3, 2017

100%, looks like.

@smowton
Copy link
Contributor Author

smowton commented Mar 23, 2017

Duplicate of #150

@smowton smowton closed this as completed Mar 23, 2017
smowton pushed a commit to smowton/cbmc that referenced this issue May 9, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants