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

Heapster/exponential code explosion #1528

Merged
merged 15 commits into from
Dec 1, 2021

Conversation

eddywestbrook
Copy link
Contributor

This PR addresses the problem of exponential explosion during code generation, by inserting let-bindings for the outputs of each TypedSetReg operation. This prevents Crucible code like

x2 = x1+x1; x3 = x2+x2; ...

from generated exponential-sized expressions in the generated Coq.

This PR also makes two other changes:

  • LLVM globals now generate SAW core definitions, so that their specifications are not copied each time they are used in a program

  • A simple translation of BVUndef was defined, that translates these poison values to the bitvector value 0, though this should probably be readdressed in the future

m-yac and others added 15 commits November 23, 2021 13:22
…s that could actually be used to prove a permission at the given offset
… its own SAW core definition, rather than having the entire global be copied into each spec when it is used
…ion translation, to avoid exponential code explosion
…ings for repeated terms; added a type ascription term to the Coq AST; changed the translation of the unit type to give it an explicit ascription to sort Type rather than Set
@eddywestbrook eddywestbrook requested a review from m-yac November 30, 2021 22:24
@eddywestbrook
Copy link
Contributor Author

Oops, and this PR also changes how implGetLLVMPermForOffset chooses a permission to use in proving another permission, making it more specialized to how the implication prover actually uses those left-hand size permissions as well making it choose more precisely to avoid having to do unnecessary proof search

Copy link
Contributor

@m-yac m-yac left a comment

Choose a reason for hiding this comment

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

This looks awesome, thanks Eddy!

@eddywestbrook eddywestbrook added subsystem: heapster Issues specifically related to memory verification using Heapster PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run labels Dec 1, 2021
@eddywestbrook eddywestbrook merged commit 04a599b into master Dec 1, 2021
@mergify mergify bot deleted the heapster/exponential-code-explosion branch December 1, 2021 17:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants