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

Correct function type for vtable shim (fix some boxed closures) #335

Merged

Conversation

avanhatt
Copy link
Contributor

@avanhatt avanhatt commented Jul 19, 2021

Description of changes:

RMC currently fails to verify boxed dynamic FnOnce closures, like this:

let f: Box<dyn FnOnce()> = Box::new(|x| {
    assert(x == 2); // should fail
});
f(1);

The issue is somewhat specific to FnOnce::call_once, which takes a self pointer instead of a self * pointer at the source language level. Vtable calls expect a pointer as the first argument, so Rust itself repairs vtable shims of this type to take an argument:

    /// `<T as Trait>::method` where `method` receives unsizeable `self: Self` (part of the
    /// `unsized_locals` feature).
    ///
    /// The generated shim will take `Self` via `*mut Self` - conceptually this is `&owned Self` -
    /// and dereference the argument to call the original function.
    VtableShim(DefId),

...
if let ty::InstanceDef::VtableShim(..) = self.def {
    // Modify `fn(self, ...)` to `fn(self: *mut Self, ...)`.
    sig = sig.map_bound(|mut sig| {
        let mut inputs_and_output = sig.inputs_and_output.to_vec();
        inputs_and_output[0] = tcx.mk_mut_ptr(inputs_and_output[0]);
        sig.inputs_and_output = tcx.intern_type_list(&inputs_and_output);
        sig
    });
}

We need to do the same fix.

Resolved issues:

Resolves #367

Call-outs:

Known remaining issues: #240

Broader concerns are tracked in: #299.

Testing:

  • How is this change tested?
  • 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.

Comment on lines +218 to +225
ty::Adt(def, _) if def.is_box() => {
let boxed_ty = self.codegen_ty(ty);
self.codegen_local_fndef(ty.boxed_ty())
.map(|f| self.box_value(f.address_of(), boxed_ty))
}
Copy link
Contributor

Choose a reason for hiding this comment

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

Can you update the function-level comment regarding this case?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Done!

// We use `--no-memory-safety-checks` in this test to avoid getting
// a verification failure:
// [pointer_dereference.7] invalid function pointer: FAILURE
// Tracking issue: https://github.com/model-checking/rmc/issues/307
Copy link
Contributor

Choose a reason for hiding this comment

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

Let's not forget to mark this one as "done" in #307 once this PR is merged.

pub fn codegen_local_fndef(&mut self, l: Local) -> Option<Expr> {
let t = self.local_ty(l);
match t.kind() {
pub fn codegen_local_fndef(&mut self, ty: &'tcx ty::TyS<'tcx>) -> Option<Expr> {
Copy link
Contributor Author

Choose a reason for hiding this comment

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

DSN note: write a test for recursive Boxed box case

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Added _fixme test; but actual fix to support it is involved and will be split off into a different PR.

@avanhatt avanhatt marked this pull request as draft July 22, 2021 13:43
@avanhatt
Copy link
Contributor Author

Found a new test that still fails, converting to draft while I work on the fix.

@danielsn danielsn changed the base branch from main-153-2021-07-15 to main-153-2021-07-26 July 27, 2021 21:45
@avanhatt avanhatt force-pushed the vtable-shim-closure branch 3 times, most recently from eed88ff to c5ea34d Compare July 28, 2021 19:15
@avanhatt avanhatt marked this pull request as ready for review July 28, 2021 19:17
@avanhatt avanhatt changed the title Correct function type for vtable shim (fix boxed closures) Correct function type for vtable shim (fix some boxed closures) Jul 28, 2021
@avanhatt avanhatt merged commit 72c9b37 into model-checking:main-153-2021-07-26 Jul 29, 2021
adpaco-aws pushed a commit that referenced this pull request Aug 2, 2021
Correct vtable shim self type (add fixme for other cases)

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
@zhassan-aws zhassan-aws mentioned this pull request Aug 6, 2021
4 tasks
adpaco-aws pushed a commit that referenced this pull request Aug 6, 2021
Correct vtable shim self type (add fixme for other cases)

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
adpaco-aws pushed a commit that referenced this pull request Aug 17, 2021
Correct vtable shim self type (add fixme for other cases)

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
adpaco-aws pushed a commit that referenced this pull request Aug 24, 2021
Correct vtable shim self type (add fixme for other cases)

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
@avanhatt avanhatt deleted the vtable-shim-closure branch September 14, 2021 15:23
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 22, 2022
…l-checking#335)

Correct vtable shim self type (add fixme for other cases)

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 25, 2022
…l-checking#335)

Correct vtable shim self type (add fixme for other cases)

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
…l-checking#335)

Correct vtable shim self type (add fixme for other cases)

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
tedinski pushed a commit that referenced this pull request Apr 27, 2022
Correct vtable shim self type (add fixme for other cases)

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
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.

Correct function type for vtable shim
3 participants