Add support to casting closure to function pointer by celinval · Pull Request #2124 · model-checking/kani

celinval · 2023-01-14T01:17:29Z

Description of changes:

Change function declaration and call to ignore arguments that are ZST, and implement the closure to function pointer by reifying it to its FnOnce implementation.

The casting of closures to function pointers rely on the fact that the closures do not capture anything. Those closures are represented by empty structures, which should get pruned from its argument list of the FnOnce::call_once implementation.

Resolved issues:

Resolves #274

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

This change is manually inspecting the arguments and ignoring the ZST ones. However, I believe the long term solution is to change how we gather information about the function signature. We currently use (fn_sig()), when we should be using fn_abi_of_instance() instead. Unfortunately, that is a big change. So I'll work on it separately as part of #1365.

Testing:

How is this change tested? New tests
Is this a refactor change? Kinda

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.

Change function declaration and call to ignore arguments that are ZST, and implement the closure to function pointer by reifying it to its FnOnce implementation. The casting of closures to function pointers rely on the fact that the closures do not capture anything. Those closures are represented by empty structures, which should get pruned from its argument list of the FnOnce::call_once implementation.

tedinski · 2023-01-17T16:01:04Z

The casting of closures to function pointers rely on the fact that the closures do not capture anything. Those closures are represented by empty structures, which should get pruned from its argument list of the FnOnce::call_once implementation.

Can you explain this a bit more? This is something Rust does, but we didn't do, but that deficiency wasn't exposed by anything until now?

We currently use (fn_sig()), when we should be using fn_abi_of_instance() instead. Unfortunately, that is a big change. So I'll work on it separately as part of #1365.

Looking forward to this

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

tests/script-based-pre/check-output/check-output.sh

tedinski

Is fn_abi... your next priority? I hope so, the only reservations I have here are really how complicated this code is getting.

celinval · 2023-01-17T17:49:44Z

The casting of closures to function pointers rely on the fact that the closures do not capture anything. Those closures are represented by empty structures, which should get pruned from its argument list of the FnOnce::call_once implementation.

Can you explain this a bit more? This is something Rust does, but we didn't do, but that deficiency wasn't exposed by anything until now?

Maybe I wasn't clear. The only closures that can be casted to function pointers are the ones that don't capture anything. Their FnOnce shim will have an empty structure as the first argument, which is ignored, and the final signature matches the signature of the function pointer that we are casting it to.

We didn't support closure to function pointer before, so this wasn't a problem. We also duplicate a lot of the code that is related to function ABI to overcome other issues.

celinval · 2023-01-17T17:54:28Z

Is fn_abi... your next priority? I hope so, the only reservations I have here are really how complicated this code is getting.

I totally agree, this is a temporary solution but it does unblock users that are currently affected by this issue.

danielsn · 2023-01-17T14:31:14Z

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

+            let var_ty = self.monomorphize(ldata.ty);
+            let var_type = self.codegen_ty(var_ty);


is ty vs type a standard convention to distinguish between MIR and GOTO?

Not a standard convention. I tend to used it often when I need to use both in the same function though.

I think it's much better than using t for both though. I think we should avoid shadowing variables, especially when they represent different things, not just a different state of same thing.

Do you have any other suggestion?

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

danielsn · 2023-01-17T17:56:51Z

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

-                let index_param = tupe.clone().member(&i.to_string(), &self.symbol_table);
-                fargs.push(index_param);
+            if let ty::Tuple(tupled_args) = tuple_ty.kind() {
+                for (idx, arg_ty) in tupled_args.iter().enumerate() {


Is this ordering deterministic?

I didn't dive deep into that since we already had this assumption in this code. I just merged the two loops together.

danielsn · 2023-01-17T17:57:24Z

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

-                if self.operand_ty(o).is_bool() {
-                    self.codegen_operand(o).cast_to(Type::c_bool())
+    /// When `skip_zst` is set to `true`, the return value will not include any argument that is ZST.
+    /// This is used because we ignore ZST arguments, except for intrinsics.


why can't we ignore them for instrinsics?

Because our intrinsics implementation have assumptions about the number of parameters. BTW, I think this is also true for other backends.

danielsn · 2023-01-17T17:59:01Z

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

-                        let (name, _) = self.codegen_spread_arg_name(&lc);
-                        ident = name;
+            .filter_map(|(i, t)| {
+                if self.is_zst(*t) && !(i == 0 && is_vtable_shim) {


This is a complicated check. Can we simplify?

I don't think it's worth it. I could split it, but it will just complicate the code flow. We should really be looking at the FnAbi to decide how to codegen parameters.

danielsn · 2023-01-17T17:59:17Z

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

+                    // See https://github.com/model-checking/kani/issues/274 for more details.
+                    None
+                } else {
+                    let lc = Local::from_usize(i + 1);


If I'm not wrong, that's because the variable 0 is the return value.

@danielsn is there anything else you would like me to change? Can I go ahead and merge it as is?

Conflicts: kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

celinval added 3 commits January 13, 2023 13:13

Fix intrinsics

f088d23

Polish the code and comments

c2c3ab9

celinval requested a review from a team as a code owner January 14, 2023 01:17

tedinski reviewed Jan 17, 2023

View reviewed changes

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs Show resolved Hide resolved

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs Show resolved Hide resolved

tests/script-based-pre/check-output/check-output.sh Outdated Show resolved Hide resolved

tedinski approved these changes Jan 17, 2023

View reviewed changes

Merge branch 'main' into issue-274-closure-ptr

f498c56

danielsn reviewed Jan 17, 2023

View reviewed changes

celinval added 2 commits January 18, 2023 12:57

Address PR feedback

dc159af

Merge remote-tracking branch 'origin/main' into issue-274-closure-ptr

b7a554f

Conflicts: kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

celinval merged commit afe238d into model-checking:main Jan 19, 2023

		let var_ty = self.monomorphize(ldata.ty);
		let var_type = self.codegen_ty(var_ty);

Conversation

celinval commented Jan 14, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Related RFC:

Call-outs:

Testing:

Checklist

Uh oh!

tedinski commented Jan 17, 2023

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tedinski left a comment

Choose a reason for hiding this comment

Uh oh!

celinval commented Jan 17, 2023

Uh oh!

celinval commented Jan 17, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

celinval Jan 18, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

celinval commented Jan 14, 2023 •

edited

Loading

celinval Jan 18, 2023 •

edited

Loading