Account for `use` statements when resolving paths in `kani::stub` attributes #2003

aaronbembenek-aws · 2022-12-15T15:10:40Z

Description of changes:

This PR follows up on #1999.

Currently, when we resolve paths appearing in kani::stub attributes, we do not take into account any use statements that might be in play. This PR fixes this gap by accounting for these types of imports:

use XXX;
use XXX as YYY;
use XXX::*
extern crate XXX as YYY;

Resolved issues:

Resolves #1998

Related #1866
Related #1997

Call-outs:

Some care had to be taken so that we handle glob imports correctly, as paths resolved through them essentially have a lower priority than paths resolved other ways.

Testing:

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

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.

aaronbembenek-aws · 2022-12-19T20:55:10Z

@celinval FYI, this is ready for review, but a maintainer needs to start the CI job.

celinval

Sorry, I haven't had time to go through the entire PR yet. FYI, I'll be off next week.

celinval · 2022-12-21T21:32:32Z

kani-compiler/src/kani_middle/resolve.rs

+fn module_to_string(tcx: TyCtxt, current_module: LocalDefId) -> String {
+    let def_id = current_module.to_def_id();
+    if def_id.is_crate_root() {
+        "crate root".to_string()


Can you either change this to be the name of the current create or something like crate $root? It could get confusing if the user has a crate named "root"

I changed this to the name of the root module.

celinval · 2022-12-21T21:38:02Z

kani-compiler/src/kani_middle/resolve.rs

+        // TODO: We should make this consistent with error handling for other
+        // cases (see <https://github.com/model-checking/kani/issues/2013>).
+        let location = module_to_string(tcx, current_module);
+        let mut msg = format!(


Maybe change this to:

Unable to resolve `{stub name}`. Ambiguous de definitions found due to the following imports: ...

Also, do we have the span from the stub declaration? I think that would really help here.

We currently don't have the span available anywhere in this module, and at this point in the code we don't even have the full name of the original function we're trying to resolve. We could potentially pass this information around all the different resolution functions so that we can produce helpful error messages here. However, I think it would be cleaner to change the resolution functions to return a Result and then leave it up to the client of this module to produce error messages.

You could wrap these functions into a type that holds that information so you can generate more helpful error messages. Not on this PR though. :)

Okay, sounds like we're holding off on making changes here until later. I think it probably makes most sense to go with the approach of returning a Result, so that this resolve module does not become specialized to stubbing, but can also be used in other parts of Kani.

BTW, my suggestion is to keep it independent from stubbing. I'm OK with returning a result too, and letting the user to decide whether the failure to resolve is an error or not.

My main point is that the message should give more context on the exact path that we are trying to resolve and in which level it has failed.

aaronbembenek-aws · 2022-12-23T16:40:30Z

Thanks for taking an initial look! I will also be off until mid-January.

rahulku · 2023-01-09T21:57:13Z

updates on this?

celinval · 2023-01-09T23:33:28Z

I don't think @aaronbembenek is back yet.

aaronbembenek · 2023-01-11T03:44:59Z

That’s right - I’m currently on vacation, but I’ll have some time to make updates starting next week.

…

On Tue, Jan 10, 2023 at 10:33 AM Celina G. Val ***@***.***> wrote: I don't think @aaronbembenek <https://github.com/aaronbembenek> is back yet. — Reply to this email directly, view it on GitHub <#2003 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABSS5S732XP5UWUFABHYAEDWRSN5JANCNFSM6AAAAAAS724WRA> . You are receiving this because you were mentioned.Message ID: ***@***.***>

aaronbembenek · 2023-01-17T21:40:11Z

Okay, I'm back now! Let me know what other changes to make...

aaronbembenek · 2023-01-17T21:43:52Z

Also, looks like I need someone to approve this workflow...

celinval

Thanks

aaronbembenek · 2023-01-19T21:14:38Z

Thanks @celinval for taking a look! You might have to merge this for me (I don't think I have permissions to).

aaronbembenek-aws added this to the Function/method stubbing milestone Dec 15, 2022

aaronbembenek-aws force-pushed the resolve-uses branch 2 times, most recently from 8a0a9d4 to 8d82d81 Compare December 16, 2022 20:55

aaronbembenek force-pushed the resolve-uses branch from 8d82d81 to fa6a70f Compare December 19, 2022 14:04

aaronbembenek-aws marked this pull request as ready for review December 19, 2022 14:08

aaronbembenek-aws requested a review from a team as a code owner December 19, 2022 14:08

aaronbembenek force-pushed the resolve-uses branch from 8946d5a to 3c101d3 Compare December 19, 2022 20:54

celinval reviewed Dec 23, 2022

View reviewed changes

aaronbembenek force-pushed the resolve-uses branch from 3c101d3 to d3f87d8 Compare January 17, 2023 21:36

aaronbembenek-aws and others added 3 commits January 17, 2023 16:39

Take into account use statements when resolving paths.

042230c

Fix?

e7658ce

Update error message.

b9e314c

aaronbembenek force-pushed the resolve-uses branch from d3f87d8 to b9e314c Compare January 17, 2023 21:39

celinval approved these changes Jan 19, 2023

View reviewed changes

Merge branch 'main' into resolve-uses

90318d3

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

adpaco-aws mentioned this pull request Feb 8, 2023

Name resolution falls into a cycle on local modules #2201

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Account for `use` statements when resolving paths in `kani::stub` attributes #2003

Account for `use` statements when resolving paths in `kani::stub` attributes #2003

aaronbembenek-aws commented Dec 15, 2022 •

edited

Loading

aaronbembenek-aws commented Dec 19, 2022

celinval left a comment

celinval Dec 21, 2022

aaronbembenek Jan 17, 2023

celinval Dec 21, 2022

aaronbembenek-aws Dec 23, 2022

celinval Dec 23, 2022

aaronbembenek Jan 17, 2023

celinval Jan 19, 2023

aaronbembenek-aws commented Dec 23, 2022

rahulku commented Jan 9, 2023

celinval commented Jan 9, 2023

aaronbembenek commented Jan 11, 2023 via email

aaronbembenek commented Jan 17, 2023

aaronbembenek commented Jan 17, 2023

celinval left a comment

aaronbembenek commented Jan 19, 2023

Account for use statements when resolving paths in kani::stub attributes #2003

Account for use statements when resolving paths in kani::stub attributes #2003

Conversation

aaronbembenek-aws commented Dec 15, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

aaronbembenek-aws commented Dec 19, 2022

celinval left a comment

Choose a reason for hiding this comment

celinval Dec 21, 2022

Choose a reason for hiding this comment

aaronbembenek Jan 17, 2023

Choose a reason for hiding this comment

celinval Dec 21, 2022

Choose a reason for hiding this comment

aaronbembenek-aws Dec 23, 2022

Choose a reason for hiding this comment

celinval Dec 23, 2022

Choose a reason for hiding this comment

aaronbembenek Jan 17, 2023

Choose a reason for hiding this comment

celinval Jan 19, 2023

Choose a reason for hiding this comment

aaronbembenek-aws commented Dec 23, 2022

rahulku commented Jan 9, 2023

celinval commented Jan 9, 2023

aaronbembenek commented Jan 11, 2023 via email

aaronbembenek commented Jan 17, 2023

aaronbembenek commented Jan 17, 2023

celinval left a comment

Choose a reason for hiding this comment

aaronbembenek commented Jan 19, 2023

Account for `use` statements when resolving paths in `kani::stub` attributes #2003

Account for `use` statements when resolving paths in `kani::stub` attributes #2003

aaronbembenek-aws commented Dec 15, 2022 •

edited

Loading