Skip to content

Add tests for forget#1041

Merged
adpaco-aws merged 6 commits intomodel-checking:mainfrom
adpaco-aws:disable-forget
Apr 13, 2022
Merged

Add tests for forget#1041
adpaco-aws merged 6 commits intomodel-checking:mainfrom
adpaco-aws:disable-forget

Conversation

@adpaco-aws
Copy link
Contributor

@adpaco-aws adpaco-aws commented Apr 13, 2022

Description of changes:

Adds a positive and a negative test case for forget and updates the support table accordingly.

Resolved issues:

Part of #727

Call-outs:

PR was originally "Disable forget intrinsic" but was changed after discussion below. Description included below for reference.

Removes the implementation for forget, which was being encoded as a no-op.

Note that this is not the well-known forget which calls ManuallyDrop, but an alternative that moves the value out of scope without calling drop functions (used by mem::forget_unsized): https://doc.rust-lang.org/std/intrinsics/fn.forget.html

Testing:

  • How is this change tested? Existing regression.

  • Is this a refactor change? No.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@adpaco-aws adpaco-aws requested a review from a team as a code owner April 13, 2022 16:12
@zhassan-aws
Copy link
Contributor

It seems to me that using a no-op for forget is sound since the only effect of using the forget intrinsic is to produce a compiler error if the value is referenced after "forgetting" it. I cannot think of any other verification-related effects of calling it.

@adpaco-aws
Copy link
Contributor Author

Thanks @zhassan-aws for the detailed explanation!

To be clear, I was under the impression this was not sound because I thought we had to generate code for "forgetting" the value in CBMC. But as you explained we do not need to do anything during code generation, so a no-op would be fine.

Now, instead of removing it, I was thinking of adding two tests similar to the example found here but using this forget.

fn main() {
let mut v = vec![65, 122];
let s = unsafe { String::from_raw_parts(v.as_mut_ptr(), v.len(), v.capacity()) };
std::intrinsics::forget(v);
assert!(v[0] == 65); // this causes failure to codegen
assert_eq!(s, "Az");
}

This should fail to codegen, and another test not including the first assertion should pass. What do you think?

@adpaco-aws adpaco-aws changed the title Disable forget intrinsic Add tests for forget Apr 13, 2022
@adpaco-aws
Copy link
Contributor Author

Just pushed the changes I was proposing because I figured it's something we would like to have anyway. Updated title and description as well.

Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

Makes sense to me (technically it would be a compilation error as opposed to a codegen failure with the first assert, but I guess for the purpose of compiletest, it's the same thing).

@adpaco-aws
Copy link
Contributor Author

Right, switched to kani-check-fail which is used to indicate errors before codegen.

@adpaco-aws adpaco-aws merged commit 227bbe7 into model-checking:main Apr 13, 2022
@adpaco-aws adpaco-aws mentioned this pull request Apr 14, 2022
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
* Disable `forget` intrinsic

* Restore `forget`

* Add two tests for `forget`

* Update `forget` status in support table

* Use `check-fail` instead of `codegen-fail`
tedinski pushed a commit that referenced this pull request Apr 27, 2022
* Disable `forget` intrinsic

* Restore `forget`

* Add two tests for `forget`

* Update `forget` status in support table

* Use `check-fail` instead of `codegen-fail`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants