Tracking issue for #[ffi_pure]

[gnzlbg]

Annotates an extern C function with C pure attribute.

[nagisa]

This corresponds to the readonly LLVM attribute.

[joshtriplett]

Is this fully implemented and ready for potential stabilization, or is there any blocker?

[workingjubilee]

I am not sure but I believe that this and its cousin, #58328, are of interest to the opsem team, as they significantly affect what optimizations the codegen backend is allowed to perform (and declaring them is probably very unsafe!). cc @rust-lang/opsem

[RalfJung]

Yes this sounds very unsafe. I assume it works a lot like asm! annotations? Are the requirements the same as what the Reference says about pure there?

[CAD97]

Interestingly, I see LLVM readonly is applied to the @llvm.type.checked.load.relative intrinsic but I don't actually see it defined for functions, only for parameters. I presume it means the same as memory(read). IIUC, GCC's pure is close to but more permissive than¹ LLVM's memory(read, inaccessiblemem: readwrite) and GCC's const is close to but more permissive than² LLVM's memory(none).

We do already expose a similar feature, in that asm! blocks can be annotated with options(pure, nomem) or options(pure, readonly). IIUC, these would correspond to GCC const and pure, respectively. Even though the purpose of the Rust attribute is to match C headers using __attribute__(), I think it'd be preferable to spell them something like #[pure(nomem)]/#[pure(readonly)] instead, to make the Rust semantic more clear.

With the removal of #[ffi_returns_twice], I don't think we want #[ffi_*] style attributes. If we want this, it should apply just as much without any FFI involved. The one advantage of applying to extern declared functions is that the point of unsafe for their signature being accurate is calling them. If allowed on fn items, either the attribute would need to similarly defer the safety of the annotation to the caller or be itself unsafe to use.

However, I can't come up with a way to define the semantics operationally in a way Miri could check. Even a brute force attempt that retags all globally accessible locations as Frozen and makes the called function use the new tag for global loads isn't sufficient, as a pointer loaded out of a global still has its existing provenance (thus can validly be used for writes).

Well, except for a shim that calls the actual symbol from an asm! block and uses those options annotations.

Footnotes

1. GCC says that “functions declared with the pure attribute can safely [...] modify the value of objects in a way that does not affect their return value or the observable state of the program.” LLVM's inaccessiblemem: readwrite permits e.g. encapsulated usage of malloc/free, but I don't know how exactly to interpret GCC's notion of writes that exist but aren't observable. ↩

2. GCC says that “functions declared with the [const] attribute can safely read objects that do not change their return value, such as non-volatile constants.” LLVM doesn't expose a knob for allowing reads of runtime constant memory but not runtime mutable memory. ↩

[workingjubilee]

hmm, cc @antoyo Do you by any chance have any insight into the question about GCC's semantics for the pure and const attributes?

[RalfJung]

However, I can't come up with a way to define the semantics operationally in a way Miri could check. Even a brute force attempt that retags all globally accessible locations as Frozen and makes the called function use the new tag for global loads isn't sufficient, as a pointer loaded out of a global still has its existing provenance (thus can validly be used for writes).

I think we can get most of pure, readonly with a per-thread flag indicating that this thread is currently in "pure" mode, and rejecting all sorts of operations if the current thread is in "pure" mode -- in particular, writes and fences. I guess we'd have to allow writes to the locals of the stack pure frame itself (and functions it calls), but that should be doable. Something similar could work for pure, nomem.

The part that is obviously impossible to check is the requirement that this function must terminate.