Fix issue with value_of / align_of traits#1089
Conversation
We were trying to figure out the values of those properties during runtime, which is not possible. Emit a runtime error for now.
| let arg = fargs.remove(0); | ||
| let size_align = self.size_and_align_of_dst(tp_ty, arg); | ||
| self.codegen_expr_to_place(p, size_align.$which) | ||
| if size_align.is_some() { |
There was a problem hiding this comment.
if let Some instead of using unwrap?
There was a problem hiding this comment.
Yes, because this can be None.
| // https://github.com/model-checking/kani/issues/1074 | ||
| // The size of dyn T is only known at runtime. Thus, we need to retrieve that | ||
| // information from the object vtable. | ||
| None |
There was a problem hiding this comment.
Does arg.member("vtable").member("size") not work here?
There was a problem hiding this comment.
Probably. I just didn't have time to go figure it out. Let me try and maybe we can just fix this issue. :)
| let field_ty = layout.field(self, n).ty; | ||
| let SizeAlign { size: unsized_size, align: mut unsized_align } = | ||
| self.size_and_align_of_dst(field_ty, arg); | ||
| self.size_and_align_of_dst(field_ty, arg.clone())?; |
There was a problem hiding this comment.
Why is this clone now needed?
There was a problem hiding this comment.
This was probably some debug I removed and forgot to revert this. I'll remove it.
| fn check_align_simple() { | ||
| let a = A { id: 0 }; | ||
| let t: &dyn T = &a; | ||
| assert_eq!(align_of_val(t), 8); |
There was a problem hiding this comment.
Does this assume a particular architecture?
There was a problem hiding this comment.
This should hold for the architecture we currently support.
Use field in the vtable.
We were trying to figure out the values of those properties during runtime, which is not possible. Fix the code to look for the information in the vtable instead.
We were trying to figure out the values of those properties during runtime, which is not possible. Fix the code to look for the information in the vtable instead.
Description of changes:
We were trying to figure out the values of those properties during runtime, which is not possible. Fix the code to look for the information in the vtable instead.
Resolved issues:
Fixes #1074
Call-outs:
This is v2. The initial PR was trying to mitigate it but it turned out that the fix was straight forward.
Testing:
How is this change tested? New tests
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.