Resolve paths in `kani::stub` attributes (ignoring `use` statements) #1999

aaronbembenek-aws · 2022-12-13T22:30:23Z

Description of changes:

Currently, when we resolve paths in kani::stub attributes we do not take into account the module of the harness and we do not support the path qualifiers crate, self, super, and initial ::. This PR improves our path resolution algorithm to take into account the module of the harness (so we resolve relative paths correctly) and adds support for those qualifiers.

It does not handle use statements (as in use XXX; or use XXX as YYY;); they will be addressed in a separate PR (tracked in #1998).

Resolved issues:

Related to #1866
Resolves #1894

Call-outs:

Previously, we represented a stub mapping (mapping original functions/methods to their replacements) as a FxHashMap<String, String>, and then did a linear lookup in the HIR during the MIR transformation to try to find a function/method with the same string representation. Since we are actually resolving paths now when processing the attributes (and constructing the stub mappings), this PR uses a FxHashMap<DefPathHash, DefPathHash> instead, which is more robust and removes the need for that linear lookup. A DefPathHash is stable across crate and compilation boundaries.

Testing:

How is this change tested? Existing tests and 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.

celinval

I still have to go through the tests in this PR, but overall I think this is a great improvement to the user experience.

The logic here is fairly complicated, so I would like to ask you to add some debug!() and trace!() statements to help future development. Especially when things go wrong. There are a lot of places inside resolve.rs that you return None, which basically means that we fail resolution. It would be great to know which path we took to get there.

Another thing to consider is to give a more informative error when resolution fails. Let's say we fail in the following resolution:

::my_crate::my_module::my_function

If we fail while processing my_crate, the error could say something like fail to find crate "my_crate". But if we have found my_crate, but not my_module, we can say couldn't find "my_module" inside "my_crate".

I'm OK if we leave the more detailed error for later, but you might want to consider at least what mechanism we should use to pass this error. For example, right now we discard whatever we process. We are also returning Option<> everywhere, should we consider using Result<> instead or should we just trigger the error whenever we find it?

celinval · 2022-12-15T20:49:24Z

kani-compiler/src/kani_middle/resolve.rs

+#[derive(Debug)]
+struct Path {
+    base: Base,
+    segments: Segments,


can you please document that if may_be_external_path is true, then segments cannot be empty?

celinval · 2022-12-15T20:51:40Z

kani-compiler/src/kani_middle/resolve.rs

+    // `self` may be followed be `super` (handled below).
+    let mut may_be_external_path = true;
+    let first = segments[0].as_str();
+    if first == ROOT {


Can you please replace this by match block?

match first { ROOT => {} SELF => {} ...

celinval · 2022-12-15T20:52:51Z

kani-compiler/src/kani_middle/resolve.rs

+/// structure, resolving qualifiers (like `crate`, etc.) along the way.
+fn to_path(tcx: TyCtxt, current_module: LocalDefId, name: &str) -> Option<Path> {
+    const CRATE: &str = "crate";
+    const ROOT: &str = "{{root}}";


Is this how the compiler maps initial "::"?

Exactly. I added a comment

celinval · 2022-12-15T21:19:57Z

kani-compiler/src/kani_middle/resolve.rs

+
+    // Resolve qualifiers `crate`, initial `::`, and `self`. The qualifier
+    // `self` may be followed be `super` (handled below).
+    let mut may_be_external_path = true;


For readability, I would recommend inspecting the first element and assigning the proper value here. Something like:

let may_be_external_path = !matches!(first, CRATE, SELF, SUPER);

This is cleaner! Done

celinval · 2022-12-15T21:28:37Z

kani-compiler/src/kani_middle/stubbing/transform.rs

+    type Item = (u64, u64);
+    let item_to_def_id = |item: Item| -> DefId {
+        let hash = DefPathHash(Fingerprint::new(item.0, item.1));
+        tcx.def_path_hash_to_def_id(hash, &mut || panic!())


Maybe a friendly error would be nice here. Something on the terms that this is likely due to a Kani issue, please file a bug report.

I checked, and the panic is caught by our panic handler, so the user does receive a message to that effect

celinval · 2022-12-15T21:59:18Z

kani-compiler/src/kani_middle/resolve.rs

@@ -0,0 +1,236 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains code for resolving strings to `DefId`s.


Can you please expand this description? What kind of strings are we talking about? Does this module cover any string that represents a path? Do we support fully qualified paths? Maybe adding a link to the path syntax might help too: https://doc.rust-lang.org/reference/paths.html.

Which brings me a question, do we support qualified paths?

Looking through the open issues kind of answers my last question about qualified paths: #1997

But I think it would be great if we can explicitly state that we are only handling simple paths and add a link to its definition: https://doc.rust-lang.org/reference/paths.html#simple-paths

I've updated some comments to make this clearer (and included the link for simple paths)

celinval

Thank you! BTW, great tests!

celinval · 2022-12-16T18:52:33Z

BTW, I create #2013 to track improvements to the stubbing error formats.

aaronbembenek-aws · 2022-12-16T19:19:30Z

Thanks for taking a look! I've added traces so that we now get debug output like this:

┐kani_compiler::kani_middle::resolve::path_resolution
├───0ms DEBUG kani_compiler::kani_middle::resolve Normalizing path `local_mod::pub_fn`
├───0ms DEBUG kani_compiler::kani_middle::resolve Resolving `local_mod::pub_fn` in local crate root
├───0ms DEBUG kani_compiler::kani_middle::resolve Resolving `pub_fn` in local module `local_mod`
├───0ms DEBUG kani_compiler::kani_middle::resolve Resolved `pub_fn` as a function in local module `local_mod`
┘

BTW, I create #2013 to track improvements to the stubbing error formats.

Thanks! I think we should be able to support better errors by (as you suggest) changing the Options to Results where the error case records where resolution gets stuck.

aaronbembenek-aws requested a review from a team as a code owner December 13, 2022 22:30

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

aaronbembenek-aws mentioned this pull request Dec 15, 2022

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

Merged

4 tasks

aaronbembenek-aws force-pushed the resolve-stub-names branch from f976d55 to b11edcd Compare December 15, 2022 20:01

celinval reviewed Dec 15, 2022

View reviewed changes

aaronbembenek-aws added 3 commits December 16, 2022 12:20

Resolve paths in kani::stub attributes.

2258810

Change how harnesses are specified in cargo-kani tests.

7b5ed54

Address PR feedback.

0aedf42

celinval approved these changes Dec 16, 2022

View reviewed changes

aaronbembenek-aws force-pushed the resolve-stub-names branch from bb5a0e2 to d58d896 Compare December 16, 2022 19:07

Add tracing.

ba93bc6

aaronbembenek-aws force-pushed the resolve-stub-names branch from d58d896 to ba93bc6 Compare December 16, 2022 19:11

aaronbembenek-aws merged commit 1d94b6b into model-checking:main Dec 16, 2022

aaronbembenek-aws deleted the resolve-stub-names branch December 16, 2022 20:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Resolve paths in `kani::stub` attributes (ignoring `use` statements) #1999

Resolve paths in `kani::stub` attributes (ignoring `use` statements) #1999

aaronbembenek-aws commented Dec 13, 2022

celinval left a comment •

edited

Loading

celinval Dec 15, 2022

aaronbembenek-aws Dec 16, 2022

celinval Dec 15, 2022

aaronbembenek-aws Dec 16, 2022

celinval Dec 15, 2022

aaronbembenek-aws Dec 16, 2022

celinval Dec 15, 2022

aaronbembenek-aws Dec 16, 2022

celinval Dec 15, 2022

aaronbembenek-aws Dec 16, 2022

celinval Dec 16, 2022

celinval Dec 15, 2022

celinval Dec 15, 2022

aaronbembenek-aws Dec 16, 2022

celinval left a comment

celinval commented Dec 16, 2022

aaronbembenek-aws commented Dec 16, 2022

Resolve paths in kani::stub attributes (ignoring use statements) #1999

Resolve paths in kani::stub attributes (ignoring use statements) #1999

Conversation

aaronbembenek-aws commented Dec 13, 2022

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

celinval left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

celinval commented Dec 16, 2022

aaronbembenek-aws commented Dec 16, 2022

Resolve paths in `kani::stub` attributes (ignoring `use` statements) #1999

Resolve paths in `kani::stub` attributes (ignoring `use` statements) #1999

celinval left a comment •

edited

Loading