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: more rust bugfixes #1574

Merged
merged 30 commits into from
Feb 9, 2022
Merged

Heapster: more rust bugfixes #1574

merged 30 commits into from
Feb 9, 2022

Conversation

eddywestbrook
Copy link
Contributor

This PR makes a number of bug fixes for running Heapster on code compiled from Rust.

Eddy Westbrook and others added 29 commits January 4, 2022 07:15
…dMods to introduce an eliminate just the modalities on named shapes
…a time; added a FIXME for only storing whole multiples of bytes
…f the lowned permission with the actual permissions that are borrowed
…ission, which has the same permissions on input and output
…irst; also changed implLLVMFieldTryProveWordEq to not drop equality permissions
…id out as pointers to values, the return permissions need to give back the memory where they were as an empty memblock permission
… stop deciding option-like-ness if no such element is found
…s lowned permission contains undetermined vars, not just when the lifetime itself is not determined
…ype; and added an assumption for the clone method for Box<List20<u64>>
@eddywestbrook
Copy link
Contributor Author

The main changes in this PR are:

  • Changed equality shapes to be indexed by their lengths, so that llvmShapeLen can be defined for equality shapes
  • Added simple lowned permissions as a new form of lifetime ownership permission, with a simpler, non-higher-order translation
  • Added implication rules to add and remove modalities from named shapes
  • Removed implication prover logic for sub-byte-sized fields (e.g., a pointer to a single bit), since this does not really work well with the logic
  • Added debug level 2 with more info
  • Fixed some issues with laying out Rust types
  • Added logic for handling Rust's optimizations for Option-like enums
  • Fixed bvSplit, which had endianness switched
  • Added logic to end lifetimes instead of just dropping them during inference of input permissions for a jump when the lifetime permissions contain undetermined variables

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.

LGTM, with the usual caveat that I wasn't able to fully understand the changes in Implication.hs and RustTypes.hs, so I mostly just looked over those files for style. If all the tests pass though, this is good to merge.

@m-yac m-yac added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Feb 9, 2022
@mergify mergify bot merged commit 81287fb into master Feb 9, 2022
@mergify mergify bot deleted the heapster/more-rust-bugfixes branch February 9, 2022 23:02
@m-yac m-yac added the subsystem: heapster Issues specifically related to memory verification using Heapster label Feb 24, 2022
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.

3 participants