Add hook for overriding compiler builtin macros

[AlexanderPortland]

It would be useful for compiler plugins to be able to override the functionality of builtin macros, so this PR attempts to implement that. This is my first real attempt at contributing to Rust, so I’m looking to improve my skills and am very open to feedback or criticism!

This feature would specifically be very useful for us in Kani, as it would allow us to stub out the std library's panic!() macro when we’re doing codegen for verification and avoid having to verify the complicated string formatting from certain calls of that macro.

r? @oli-obk

[rustbot]

oli-obk is not on the review rotation at the moment.
They may take a while to respond.

[rustbot]

These commits modify the Cargo.lock file. Unintentional changes to Cargo.lock can be introduced when switching branches and rebasing PRs.

If this was unintentional then you should revert the changes before this PR is merged.
Otherwise, you can ignore this comment.

Some changes occurred to the CTFE machinery

cc @RalfJung, @oli-obk, @lcnr

[RalfJung]

What does this have to do with const-eval...?

[AlexanderPortland]

Sorry, nothing lol. I was trying to figure out which crate's provide() function a default implementation should go under, and am not very familiar with the compiler's layout. Is this the right way to do that, and if so which provide() would be the right one to add it to?

[RalfJung]

which provide() would be the right one to add it to?

I'm not sure either, I'm just a const-eval maintainer and was confused about what showed up on "my turf" here. ;)

Something that deals with macros, probably... or rustc_middle if nothing else fits, I guess.

[bjorn3]

This feature would specifically be very useful for us in Kani, as it would allow us to stub out the std library's panic!() macro when we’re doing codegen for verification and avoid having to verify the complicated string formatting from certain calls of that macro.

Is this for the standard library verification? If so you can just define a panic macro inside compiler-builtins to override the builtin one, right? Aside from the standard library verification, I wouldn't expect Kani to do anything with compiler-builtins at all. There shouldn't be any MIR level calls to compiler-builtins except for memcpy, memset and memcmp which you did want to shim anyway.

[RalfJung]

The macro is not defined i compiler-builtins so I am not sure why you are bringing that up?

[bjorn3]

I mean that for the standard library verification I think they could just put

macro_rules! panic { ... }

at the top of compiler-builtins to shadow the builtin panic macro.

[AlexanderPortland]

Hey @bjorn3, this situation actually came up in the context of verifying user programs, not the standard library itself.

AFAIK, when compiling a user crate, Kani uses --extern to link against a slightly modified version of the standard library where we've overridden panic!() to call a kani::panic() intrinsic instead. That works fine for direct calls to panic!() in user code.

However, if the user writes something like Result::unwrap(), it goes through a dependency's internal implementation (in this case the standard library), which isn't affected by our --extern override. That ends up calling the built-in panic!() macro, which still expands into a bunch of formatting logic and, even though we stub out the final MIR call to core::panic(), we still have to verify all that intermediate string formatting logic.

(Here's the link to the original Kani issue for more context.)

[RalfJung]

You need to build the dependencies against the modified standard library as well, then they will use your macro. I wonder how anything can work if you are mixing different standard libraries...?

This PR sets a precedent for ad-hoc patching of the standard library through rustc itself -- today you need this for builtin macros, but who knows what you want to replace tomorrow? I don't see anything specific to panic or builtin macros that would make them harder to replace than any other part of the standard library. (Them being builtin just means the standard library macro has no body, but in terms of name resolution it should behave like any normal macro.)

[RalfJung]

(Here's the link to model-checking/kani#2835 for more context.)

Is model-checking/kani#4169 the PR implementing what you mentioned above? That is something completely different from "--extern to link against a slightly modified version of the standard library where we've overridden panic!() to call a kani::panic() intrinsic instead" though so I must be looking at the wrong thing.

[RalfJung]

Okay I have found https://github.com/model-checking/kani/blob/96eb502ffce80c3408c79d18620c84e364be9310/library/std/src/lib.rs#L203. But that's not a modified standard library. That's a tiny crate called std that you layer in between the standard library and the user crate. Of course what you do there does not affect the "real" std.

If you actually modified the standard library, you could change the macro in whatever way you please and it'd apply everywhere.

[bjorn3]

If you are not verifying compiler-builtins, can you just ignore all functions in compiler-builtins when translating from MIR to whatever Kani produces? 99% of compiler-builtins will never be called from MIR and the remaining 1% (memcpy, memmove, memset, ...) you almost certainly want to shim anyway as it is often provided by libc rather than compiler-builtins

[RalfJung]

@bjorn3 why do you keep talking about compiler-builtins? This is about builtin macros, which have nothing to do with compiler-builtins...

[bjorn3]

Add hook for overriding compiler builtin macros

I read that as compiler-builtins macros. As in macros invoked inside the compiler-builtins crate. Never mind I guess.

[zhassan-aws]

Kani's std layer was originally introduced to allow us to override the assert macro.

Our overriden assert macro serves two purposes:

1. It allows us to reliably instrument additional checks (what we call assertion reachability checks)
2. It allows us to remove the formatting code from the verification path

The mechanism we use for overrides is pretty hacky though, and relies on passing --extern noprelude:std:

https://github.com/model-checking/kani/blob/8b8b89724585b08980e6a363da48aec3ad7cc690/kani-driver/src/call_single_file.rs#L20

We were hoping that rustc can provide a more reliable mechanism for performing such overrides so that we can rid of this hack.

[RalfJung]

It is in general impossible to "overwrite" the macros in std without building your own std -- the std that is distributed is already fully macro-expanded.

In that sense I think actually this PR is pointless? @AlexanderPortland have you actually tried this with Kani? Even with this PR, I am fairly sure that if you call Result::unwrap you get the version with the normal macro, since it'll just load the MIR from the std in the sysroot and that one already has all the formatting.

We were hoping that rustc can provide a more reliable mechanism for performing such overrides so that we can rid of this hack.

If you want the changes to affect even std itself, I don't think there is any realistic alternative to patching the std sources and then building a custom std.