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

Fix closure untupling/retupling #373

Merged

Conversation

avanhatt
Copy link
Contributor

@avanhatt avanhatt commented Aug 2, 2021

Description of changes:

RMC currently fails to verify some nested boxed closures, such as this:

    let f: Box<Box<dyn FnOnce(f32, i32)>> = Box::new(Box::new(|x, y| { assert!(x == 1.0); assert!(y == 2) }));
    f(1.0, 2);

The problem is that we were checking whether to untuple closure arguments based on whether the function's type kind was a Closure, but this misses some cases (where the trait points to a defined function, or with vtable shims) where the type is a FnDef. The right way to check for untupling is via a check to the function's ABI. However, in that case, we also need to retuple arguments based on the MIR's spread_arg flag. See this Zulip for more discussion.

The trickiness here is that we need to insert both the tuple and its individual components into the symbol table, and then write the components out to the tuple at the start of a function. To do this, I added a new naming convention for the untupled args, avoiding naming conflicts based on the local index. Local index math determines what gets retupled when necessary.

Here is an example of the code we now generate (with renaming for clarity):

struct Unit call_once_vtable_shim(struct [boxed_closure.rs:8:49: 11:6] *var_1, float spread_2, int spread_3)
{
  struct (f32, i32) var_2={ .0=spread_2, .1=spread_3 }; // new: retuple since the body requires it
  struct Unit var_0;

bb0:
  ;
  boxed_closure_main(*var_1, var_2.0, var_2.1);

bb1:
  ;
  return var_0;
}

Resolved issues:

Resolves #240

Call-outs:

ignore_var_ty is mystifying, and there are some intrinsic cases where skipping FnDef there elides the environment argument of a call through a tuple. I don't like this, and we should probably eventually remove ignore_var_ty in favor of elides arguments only for specific, documented reasons (like the being Zero Sized Types that rust elides).

Testing:

  • How is this change tested?

Existing tests, including a fixme added in my last PR.

  • Is this a refactor change?

Somewhat.

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.

@adpaco-aws
Copy link
Contributor

Hi @avanhatt , can you please add the example to the description?

Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

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

Great work! A few minor comments and questions.

compiler/rustc_codegen_llvm/src/gotoc/mod.rs Outdated Show resolved Hide resolved
src/test/cbmc/DynTrait/dyn_fn_param.rs Show resolved Hide resolved
compiler/rustc_codegen_llvm/src/gotoc/metadata.rs Outdated Show resolved Hide resolved
Comment on lines 149 to 150
if self.symbol_table.contains(&sym.name) {
debug!("Skipping already-added local: {:?}", sym.name);
Copy link
Contributor

Choose a reason for hiding this comment

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

Why do we need this check?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The spread arg is added in the prelude, so we shouldn't re-add it to the table here. But I added a different, more explicit check and comment instead, thanks!

compiler/rustc_codegen_llvm/src/gotoc/statement.rs Outdated Show resolved Hide resolved
compiler/rustc_codegen_llvm/src/gotoc/utils.rs Outdated Show resolved Hide resolved
// compiler/rustc_codegen_llvm/src/gotoc/mod.rs:codegen_function_prelude
pub fn codegen_spread_arg_name(&self, l: &Local) -> String {
let fname = self.current_fn().name();
format!("{}::1::spread{:?}", fname, l)
Copy link
Contributor

Choose a reason for hiding this comment

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

Do we need to hard-code this?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I think so, the name spread is not special, we just need to name it something different from var and I chose this to try and help convey the purpose.

@avanhatt avanhatt changed the base branch from main-153-2021-07-26 to main-154-2021-08-02 August 2, 2021 15:42
Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

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

LGTM! Do you mind updating manually and fixing the typo below?

compiler/rustc_codegen_llvm/src/gotoc/mod.rs Outdated Show resolved Hide resolved
avanhatt and others added 2 commits August 3, 2021 14:53
Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
@avanhatt avanhatt merged commit 2986902 into model-checking:main-154-2021-08-02 Aug 3, 2021
adpaco-aws added a commit that referenced this pull request Aug 6, 2021
Use the rust-call ABI and MIR-level spread args flag to untuple/retuple closures and shims.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
adpaco-aws added a commit that referenced this pull request Aug 17, 2021
Use the rust-call ABI and MIR-level spread args flag to untuple/retuple closures and shims.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
adpaco-aws added a commit that referenced this pull request Aug 24, 2021
Use the rust-call ABI and MIR-level spread args flag to untuple/retuple closures and shims.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
@avanhatt avanhatt deleted the closure-retupling branch September 14, 2021 15:23
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 22, 2022
Use the rust-call ABI and MIR-level spread args flag to untuple/retuple closures and shims.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 25, 2022
Use the rust-call ABI and MIR-level spread args flag to untuple/retuple closures and shims.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
Use the rust-call ABI and MIR-level spread args flag to untuple/retuple closures and shims.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
tedinski pushed a commit that referenced this pull request Apr 27, 2022
Use the rust-call ABI and MIR-level spread args flag to untuple/retuple closures and shims.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@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.

Incorrect verification results for function/closure dyn traits
2 participants