-
Notifications
You must be signed in to change notification settings - Fork 12.8k
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
upcall_call_shim_on_rust_stack has redundant call to record stack limit? #2680
Comments
This is necessary. When switching to the c stack sp_limit is set to 0, so it must be restored before going back to rust. The sp_limit needs to be 0 when running on the C stack, so that when crust functions get called, their wrappers don't inadvertently trigger while on the C stack (which can corrupt the "state machine" of saving prev_c_sp and prev_rust_sp, frighteningly). By the way, I am moving these to rust_task.h as part of the tls push. (#1857) |
… also include ZSTs (rust-lang#2794) This change considers another case for the code generation of scalar data. In particular, when the expected type is an ADT, we previously considered two cases: either there is no field or there is one. But in cases where the ADT includes a ZST, the ADT will contain multiple fields: one associated to the scalar data, and other fields associated to the ZSTs. In those cases, we ended up crashing as in rust-lang#2680: ```rust error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9: assertion failed: `(left == right)` left: `2`, right: `1`: Error in struct_expr; mismatch in number of fields and values. StructTag("tag-_161424092592971241517604180463813633314") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]. thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9: assertion failed: `(left == right)` left: `2`, right: `1`: Error in struct_expr; mismatch in number of fields and values. StructTag("tag-_161424092592971241517604180463813633314") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }] ``` With the changes in this PR, that's no longer the case. Resolves rust-lang#2364 Resolves rust-lang#2680
Unclear comment in this function in rust_upcall.cpp, but appears to be saying function does some redundant work. Clarify?
The text was updated successfully, but these errors were encountered: