Wrap returned value from codegen_place in a Result to account for the possibility of an error due to unsupported operations#1057
Conversation
… possibility of an error due to unsupported operations
| /// A convenience macro that unwraps a `Result<ProjectPlace<'tcx>, | ||
| /// Err<UnimplementedData>` if it is Ok and returns an `codegen_unimplemented` | ||
| /// expression otherwise |
There was a problem hiding this comment.
quick question: why macro and not function?
There was a problem hiding this comment.
For this to have minimal changes on the caller side, it has to do a return, which cannot be done using a function (since it will return from that function, and not from the caller function). I hope the explanation is not too confusing.
| /// A convenience macro that unwraps a `Result<ProjectPlace<'tcx>, | ||
| /// Err<UnimplementedData>` if it is Ok and returns an `codegen_unimplemented` | ||
| /// expression otherwise |
There was a problem hiding this comment.
quick question: why macro and not function?
danielsn
left a comment
There was a problem hiding this comment.
Like the general idea, but we need a better name for the macro
| // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html | ||
| match before.mir_typ().kind() { | ||
| ty::Array(..) => unimplemented!(), | ||
| ty::Array(ty, len) => { |
There was a problem hiding this comment.
Should this be a separate PR? Or change the title of this PR?
There was a problem hiding this comment.
Makes sense to do in a separate PR. I took it out (along with the expected test that was added).
| /// Err<UnimplementedData>` if it is Ok and returns an `codegen_unimplemented` | ||
| /// expression otherwise | ||
| #[macro_export] | ||
| macro_rules! unwrap_or_codegen_unimplemented { |
There was a problem hiding this comment.
This macro affects control flow where it is called; we should make sure to call that our clearly in the name.
There was a problem hiding this comment.
I added return in the macro name: unwrap_or_return_codegen_unimplemented. Let me know if you have other suggestions.
|
|
||
| /// Same as the above macro, but returns a goto program `Stmt` instead | ||
| #[macro_export] | ||
| macro_rules! unwrap_or_codegen_unimplemented_stmt { |
There was a problem hiding this comment.
Same, call out that this returns
| e.as_stmt(Location::none()) | ||
| } else { | ||
| self.codegen_place(&p).goto_expr.assign(e, Location::none()) | ||
| unwrap_or_codegen_unimplemented_stmt!(self, self.codegen_place(&p)) |
There was a problem hiding this comment.
Is there a way to avoid repeating self, self.codegen_place
There was a problem hiding this comment.
I had the same thought, but couldn't figure out a way to do it. I initially tried not passing self in, and just calling it from inside the macro, but that didn't work due to macro hygiene: https://stackoverflow.com/a/44124477.
|
It looks good to me. Can you please check what kind of error the user will get when we fail to generate a projection Thanks! |
|
LGTM module @celinval comment |
I used the following small program as an example: #[kani::proof]
fn main() {
let mut x = 5;
let y = &mut x;
*y = 9;
assert!(x == 9);
}and replaced the implementation of Err(UnimplementedData {
operation: "deref".to_string(),
bug_url: "".to_string(),
goto_type: self.codegen_ty(inner_mir_typ).to_pointer(),
loc: Location::None,With that, Kani reported a single failure: and neither Kani nor CBMC produced any other warnings/errors. The This is because the callers to |
… possibility of an error due to unsupported operations (model-checking#1057)
… possibility of an error due to unsupported operations (#1057)
We should probably turn this into an assert and revert the logic added by model-checking#1057. But this is a much larger change that I prefer creating a separate PR for.
* Fix how we handle niche optimization with ZST The compiler uses niche optimization when there is only one variant that contains nonzero sized fields. This variant is represented as the dataful variant. However, other variants may have one or more ZST fields that can be deconstructed and referenced in the code. Before this change, we were not generating code for them and it generate type mismatch issues when the user tried to access them. This change ensures that we represent all variants that have any field, so their access is valid. * Enable debug assert inside projection mismatch We should probably turn this into an assert and revert the logic added by #1057. But this is a much larger change that I prefer creating a separate PR for. Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Description of changes:
Currently,
codegen_placereturns aProjectedPlace. For projections that are currently not supported, Kani panics since it's not possible to return acodegen_unimplementedexpression as aProjectedPlace. This PR changes the return type ofcodegen_placeto aResult<ProjectedPlace, Err(...)>so that it can return an error for those cases that is then handled by the caller through callingcodegen_unimplemented.Resolved issues:
Part of #707.
Call-outs:
Testing:
How is this change tested? A new test for sub-array binding was added that checks that Kani doesn't crash, and instead reports that the construct is not supported.
Is this a refactor change? Part of it is.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.