-
Notifications
You must be signed in to change notification settings - Fork 84
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
Correct function type for vtable shim (fix some boxed closures) #335
Conversation
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)) | ||
} |
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.
Can you update the function-level comment regarding this case?
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.
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 |
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.
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> { |
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.
DSN note: write a test for recursive Boxed box case
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.
Added _fixme
test; but actual fix to support it is involved and will be split off into a different PR.
Found a new test that still fails, converting to draft while I work on the fix. |
8464638
to
952cc20
Compare
eed88ff
to
c5ea34d
Compare
c5ea34d
to
2a5afe0
Compare
Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
…l-checking#335) Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
…l-checking#335) Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
…l-checking#335) Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
Description of changes:
RMC currently fails to verify boxed dynamic
FnOnce
closures, like this:The issue is somewhat specific to
FnOnce::call_once
, which takes aself
pointer instead of aself *
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:We need to do the same fix.
Resolved issues:
Resolves #367
Call-outs:
Known remaining issues: #240
Broader concerns are tracked in: #299.
Testing:
--pointer-check
)._fixme
test to be fixed in Incorrect verification results for function/closure dyn traits #240No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.