RFC for Function and Method Stubbing

[aaronbembenek-aws]

Description of changes:

Create an RFC for the UX and backend implementation of function and method stubbing. This would allow users to specify that, during verification, some functions/methods should be replaced with other functions/methods. These substitutions would help Kani handle code that has unsupported features (like inline assembly) or leads to bad verification performance.

I have created a proof-of-concept of the backend MIR-to-MIR transformation; the stub mapping is read from a file.

You can also find a rendered version of this document here.

Related issues:

Resolves #1695

Related to #1809

Call-outs:

Testing:

• How is this change tested?

• Is this a refactor change?

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]

Awesome! I haven't reviewed everything, but I left a few comments. Thanks

[adpaco-aws]

Thanks, this looks great overall! Just have a couple more comments.

[celinval]

Do we want to make any change to the results report to highlight that a stub was used?

[celinval]

This is pretty cool.

[celinval]

We will likely need some changes to the metadata so we can tell kani-driver which files were generated.

[aaronbembenek-aws]

Yes, that makes sense. I will add this.

[celinval]

I would highlight that another benefit is that we can extend our compiler to integrate --concrete-playback with the abstractions. But that this is out of the scope for this work.

[adpaco-aws]

Nice! Makes sense to explicitly write stub_by(...) because of this.

[adpaco-aws]

Not sure if it's good for all cases, but one possible approach here is instrumentation.

[tedinski]

Even without stubbing types

purely as a readability / flow nit: this starts talking about a case before you've really defined what these different types of stubbing are.

As I read on, I think this RFC is missing a paragraph or section discussing exactly this. We mention "stubbing types" here and "stubbing function/methods" later, but what else might there be?

One pattern I like in design docs like this is to have a section clearly articulating what's in-scope and out-of-scope. This might be a way to do this. For example, in-scope are function/methods and stub sets, out-of-scope are replacing types.

And while I'm thinking about this, I wonder if (as part of this work) we should develop a library of safe stubs for standard library functions that users can opt-into. e.g. #[kani::stubs(kani::std_stubs)] or something. Another idea besides Vec::with_capacity might be how HashMap::new works (e.g. removing/mitigating the randomness and thread local?)

[aaronbembenek-aws]

We will clarify this.

In scope:

• Replacing function bodies
• Replacing method bodies (which means that the new method body will be executed, whether the method is invoked directly or through a vtable)

Out of scope:

• Replacing type definitions
• Replacing macro definitions
• Mocking traits

[tedinski]

This should be understood as a change to kani-driver as well.

[aaronbembenek-aws]

Yes! I'll clarify that.

[tedinski]

I don't understand the downside. We don't lose the ability to still "cherry-pick" things from a module right? Stub-sets are just as "remote" as a module like this, no?

It seems like this might be a "nicer" and more Rust-friendly way of writing stub-sets and not actually have any real downsides that I can see...

[aaronbembenek-aws]

Some stronger downsides with this approach:

1. How do you mock multiple functions with the same stub? (Especially if, say, harness A wants to use stub1 to mock foo, and harness B wants to use stub1 to mock bar.)
2. How do you combine stub sets defined via modules? (This is probably possible, but would need to be fleshed out.)
3. Is it a regular module or not? Modules can contain other things than functions - how should we interpret them?

[tedinski]

we would need to figure out how to inject the AST/HIR from one crate into another

I'm not sure this is true?

[zhassan-aws]

The RFC is focused on function stubbing. Can we add examples of method stubbing?

[aaronbembenek-aws]

@tedinski We don't know until we compile later crates that earlier crates would need to have their HIR modified. Relatedly, a local abstraction would not be available while compiling a dependency.

@zhassan-aws We still need to iterate on exactly what the user experience for stubbing methods will be like. However, we can add an example of one approach to the Open Questions section.

[zhassan-aws]

How can the user verify that the stub is an abstraction of the original function/method?

[aaronbembenek-aws]

I'll add this - a good open question.

[celinval]

Should we add a limitations section? E.g.:

• This won't work with --concrete-playback for now.
• We are only able to apply abstractions to dependencies if user enables MIR Linker.

[camshaft]

If I understand this correctly, something like this would not be supported:

Say I had both the rand crate dependency and a local module:

mod rand {
    pub fn random() ...
}

#[kani::stub_by("rand::random", "mock_random")] // resolves to `self::rand::random`, not `::rand::random`

In the same vein, we won't handle imports either?

use path::to::rand_thing as rand;

#[kani::stub_by("rand::random", "mock_random")] // resolves to `path::to::rand_thing::random`, not `::rand::random`

To me, using the existing Rust scoping rules would be the most natural way to reference things.

[celinval]

Oh, that's a good point. I don't know why we have this restriction here. @aaronbembenek-aws can please clarify?

[aaronbembenek-aws]

The restriction was there so that the provided names would match the identifiers as they appear in the MIR. However, I agree that it would be a better UX to use the Rust scoping rules. So, I think we should target that approach, and try to resolve names on our end.

[camshaft]

Are you planning on enforcing visibility rules? In other words, are we going to allow stubbing a private function?

mod thing {
    pub fn foo() {
        bar();
    }

    fn bar() {
        ...
    }
}

#[kani::stub_by("thing::bar", "my_bar")]

[aaronbembenek-aws]

Yes, you will be able to stub a private function.

[camshaft]

This is definitely a tradeoff of flexibility and maintainability. On the one hand, stubbing private functions makes it really easy for writing a new proof.

However, private functions don't have any guarantees on stability or behavior. Having to maintain a proof that stubs private functions could become really tedious every time you want to refactor or upgrade a dependency.

[aaronbembenek-aws]

These are good points, and I've added them to the RFC. We are still planning to support stubbing private functions/methods (we think users will ultimately demand it), but in the documentation we will discourage users from doing so unless absolutely necessary.

[camshaft]

Are these global symbols or resolved through the module path in which they're defined? I would prefer the latter.

[aaronbembenek-aws]

Thanks for the making this point - I agree that the latter is preferable, and that's what we'll target.

[camshaft]

I see it's in the open questions section, but we definitely need to know what "compatible" means. Arity is an obvious aspect. But things start getting tricky when we're talking about generic constraints. For example are these compatible?

pub fn random<T>() -> T
    where Standard: Distribution<T>

pub fn random<T>() -> T
    where T: kani::Arbitrary

[aaronbembenek-aws]

We need to iterate on this and see what is technically feasible. From my perspective, the optimal outcome would be that a stub is compatible if the monomorphized program is well typed. Our current prototype supports the example you give.

[zhassan-aws]

Very-well written! Great work, @aaronbembenek-aws!

[zhassan-aws]

Nit: Can we shorten it to stub? I think it's customary to drop the preposition from function names (e.g. copy as opposed to copy_to or swap as opposed to swap_with).

[aaronbembenek-aws]

Sure, I think that's a good idea.

[zhassan-aws]

This is a nice example, but it's a bit involved, and I don't think it's adding much value to the RFC. IMHO, the previous, example illustrates the idea well, and is simple enough to understand. This example would be nice for the documentation though.

[aaronbembenek-aws]

We've decided to move this to the end of the RFC, as an appendix.

[zhassan-aws]

The code below replaces foo with bar, but the description says the opposite: foo used in place of bar.

[aaronbembenek-aws]

Nice catch!

[zhassan-aws]

If this turns out to be an issue, the user can always stub the public methods that are calling private functions/methods replacing those calls with calls to another function/method.

[zhassan-aws]

This macro call has parentheses, whereas the previous one doesn't.

[aaronbembenek-aws]

Another good catch! We don't need parentheses here.

[zhassan-aws]

That would be very helpful!

[zhassan-aws]

I wouldn't say this is the key motivation because conceptually, it should be possible to allow contracts to be specified on external functions (which AFAIK, CBMC allows), but it hasn't been prioritized in the current implementation. I would say the key benefit of stubbing is the simplicity of replacing a function's implementation with another that is written in Rust. The replacement can be really be anything: an over-approximation, an under-approximation, or neither. On the other hand, the disadvantage of stubbing is that there's no easy mechanism to verify that a proof is sound with the specified stubs.

[aaronbembenek-aws]

These are good points; I've rephrased them this way:

• Function contracts could in principle be applied to external functions. Doing so would require some additional UX design decisions ("How do users specify this?"); with stubbing, we do not have to distinguish between local and external functions.
• Function contracts sometimes come with a mechanism for verifying that a function satisfies its contract. We do not provide this functionality; however, it is possible to emulate it by writing proof harnesses comparing the behavior of the original code and the stub. Our approach provides more flexibility: we do not enforce a stub to be an overapproximation, or to have the same behavior in all harnesses.

[tedinski]

Nice doc!

[tedinski]

nit/bike-shed: I think this syntax isn't ideal. How much control over it do you have? If I'm not mistaken you're suggesting that the first item in the list is the name of the stub set, right?

Can we do something like kani::stub_set!(my_io_stubs) { ... the contents ... } or similar?

[aaronbembenek-aws]

Exactly, the first item would be the name of the stub set. How about kani::stub_set!(my_io_stubs, { ... the contents ... });? We should be able to support that. I believe there needs to be a single outer set of parentheses or braces enclosing everything (the name, the contents, etc.).

[fzaiser]

How about: kani::stub_set! { my_io_stubs: ... }? This would avoid having two types of delimiters ({} and ()).

[aaronbembenek-aws]

Thanks @fzaiser! I think this is a pretty good solution. I'm going to go with it for now; we can always iterate on it.

[celinval]

I am actually not a big fan of using : as a separator. It looks like a typo for me. I would prefer regular rust separators, ,, or an aggregator: {} or (). E.g.: like:

kani::stub_set!{my_io_stubs {
 ... the contents ... 
}};

[camshaft]

Ideally we use something that rustfmt will accept too 🙂. It basically needs to look like an existing construct for it to work.

[aaronbembenek-aws]

@camshaft That's a good point about rustfmt. Apparently it doesn't format code in macro invocations between braces. This syntax (based on @celinval's) works well with rustfmt:

kani::stub_set!(my_io_stubs(
    stub(std::fs::read, my_read),
    stub(std::fs::write, my_write),
));

[celinval]

We should eventually add 3 types of automatic stub generation.

• unreachable: Assert the function is unreachable.
• havoc_locals: Return non-det values and assign non-det to all mutable argument.
• havoc: Similar to havoc_locals but also assign non-det to all mutable global.

[aaronbembenek-aws]

Another one is uninterpreted: treat function as an uninterpreted function (suggested by @weaversa here).

[celinval]

I think the RFC overall looks good. I'm OK iterating over some of the details (such as the stub set syntax) as we move along as long.