-
Notifications
You must be signed in to change notification settings - Fork 62
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: Add support for the trivially false permission #1543
Conversation
In order to correctly support Rust types, we actually need a bit more than what this PR originally contained. Namely, we need a notion of a "false shape". I'll be removing the ready-to-merge label and updating the title to reflect this is a WIP. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It looks like this does not have a recombinePermConj
case for recombining a shape that contains false. This is needed in order to have calls to Rust functions with !
return type not continue type-checking after the function returns (because it doesn't return).
…tion of false elimination implication rules
…typecheck currently
… byte-sized eq perms instead of one giant eq perm for the whole string, which seems to fix some endianness issues
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me!
This PR adds a new
ValuePerm
,ValPerm_False
, which represents the trivially false value permission. It furthermore contains the relevant translations, additions to the implication prover, and conversions from Rust types (i.e. the never type,!
).The one thing I'm unsure of is the weight I've assigned to the success of a
PermImpl
step that is false elimination - or whether it matters as long as the weight is non-zero. Guidance on this for future reference is most welcome :)