If that's what you want, then you'd probably need to run the bare opcodes, which you can do in Rust today. Otherwise, you're relying on the compiler having a mnemonic for the instruction.
I don't think this is correct; since assembly can affect the CPU state in arbitrary ways, I'm not sure that treating the assembly this way will be correct. In particular, if I have some inline assembly that mutates memory at some arbitrary location, and that location had been marked as being const
within a chunk of safe rust, then the assembly will have violated that claim, and the formal checker (which by your statement is ignoring the internals of all asm!
blocks) won't detect it.
The reason I'm hammering on this point so hard is because I just learned about separation logic, and its extension concurrent separation logic. This form of logic looks like it would fit rust's model of the universe (owners, mutable/immutable borrows) particularly well provided rust can be fully specified.
I don't think the problem you're describing here is fundamentally different from the fact that Rust has unsafe
blocks, or that Rust exposes tons of OS-specific APIs in std
. asm!
is just one more thing that "the compiler can't understand." IIUC, @RalfJung and others have already achieved an "extensible" formal proof that safe Rust is typesafe, and that correctly implemented unsafe Rust doesn't violate that (although each unsafe feature has to have the "correctly" proven separately). See https://www.ralfj.de/blog/2017/07/08/rustbelt.html or https://www.janestreet.com/tech-talks/rustbelt/.
The deep issues with stable inline assembly support lie elsewhere. To be honest, I think the actual biggest problem is that we don't seem to have any consensus on what any of the difficulties are, or what any of the precise functionality should be, much less which are more or less important for which use cases. It feels like we forgot to have any community discussion on this for years and just now finally noticed.
asm!
will necessarily be unsafe.
And to the extent that asm!
prevents the application of formal methods, so will an extern "C"
function defined elsewhere. Either one might scribble on some memory location as a side effect of its operation.
I agree on both points.
I understand what you're saying, but it is too limited. As a fairly obvious example:
fn foo() {
unsafe {
x = 4;
}
}
won't compile. That means that there is some chunk of code within the compiler that is enforcing the rules, proving that the code is incorrect. Now, I know that example was overly simplistic, but you can replace it with your own, arbitrarily complicated chunk of code that (although it is unsafe) still passes certain syntactic and semantic checks. In short, unsafe
doesn't mean 'do whatever you want to, all checks are off', it has a very specific meaning, and other checks are still enforced. I want to be sure that rust is specified in such a way that it is at least theoretically possible check all rust code (although you might disregard the results within unsafe
regions). With an asm!
block, this is no longer possible. At best, you can specify preconditions that can be checked, and postconditions that you guarantee are true, and hope that is enough for the proof checker. That is... unfortunate.
From a safety/soundness point of view an asm!
is exactly the same as calling an external C function which contains the same inline asm block.
This doesn't make any sense. The author has no control over which assembler the user has installed on their system.
And what's the solution with GCC inline assembly?
When inline asm is used in a library, then it's a requirement of the consumer of the library to meet the dependency on the assembler, just like it is for any other extern "C"
provider. The library can package this up in a neat interface, but ultimately it's just like any other system library dependency: you have to manage it somehow.
I like the idea of asm being a proc-macro-like interface to rustc. That then allows authors to provide asm macros that provide some more niceties on top, such as bundling an assembler or doing some analysis of the asm, without requiring rustc to know anything about asm. Instead of returning a TokenStream
, the asm-proc-macro would return a new structure representing the asm blob (with substitution tokens), the register constraints, and how to invoke the assembler. That assembler would most likely be linked by the asm-proc-macro, either by finding it on the system or bundling it.
From a safety point of view an
asm!
is exactly the same as calling an external C function
I think if we ever stabilize inline assembly, we should specify this. Because this is not true in C. (In C, inline assembly can branch, and we definitely don't want that.)
You're talking about asm goto
, which requires passing in a list of labels that the asm block can jump to (i.e. it can't jump to arbitrary places). Since Rust doesn't have labels (at least the kind that C uses) we simply won't support asm goto
.
If we do stabilize inline asm, I think we should add several restrictions:
(Quotes by @sunfishcode from Inline Assembly. · Issue #1041 · bytecodealliance/wasmtime · GitHub)
Beyond parsing, let's talk about all the directives. Besides having multiple macro expanders to implement, many directives do subtle things with sections and fragments, exposing a lot of what would otherwise be implementation details, so your compiler backends basically have to be architected according to how C compilers have traditionally been architected in order to support all the interactions between compiler code and assembly code.
We should only allow a subset of the directives, like .data or .ascii
Also, don't miss the section on goto labels, because this means that an inline asm is effectively an arbitrary branch instruction too, so it can also create arbitrary n-way control-flow constructs which the rest of your compiler backend now has to be able to understand, and which the register allocator has to be able to spill and reload around, to satisfy the already complex constraint systems, because it all wasn't complex enough already.
We should forbid goto labels across different asm blocks.
Can you do
.popsection
within an inline asm and get to a predictable place?
This is a kind of directive we should forbid.
Are the special labels the compiler emits to mark the end of the function and other things ok to use?
We should not make them visible.
Can the compiler inline functions containing inline asm sections? How about unroll loops containing inline asm sections?
I think we should forbid inline asm which doesnt support this. Having to rename labels to do it is fine though I think.
I personally am and have been interested in such things, not really for inline assembly but, for is this blob of .text compiled of valid instructions? I personally wouldn't work on it unless there was manufacturer buy in to some extent. I wouldn't consider predicating inline assembly on the existence of such, unless we seek to push it off indefinitely. That said, here is
- REMS has SAIL and models for various architectures.
- arm machine readable architecture XML specifying opcode encoding/decoding instruction set and behavior in asl
- arm specification language interpreter what they describe the behavior in.
- arm mra tools for extracting xml.
Excepting IBM POWER all the other sail models besides Arm are handwritten from the specification documents, and most of the models only cover the user-mode fragments (I'm unsure of where to find this POWER specification).
Licensing:
The main thing that has stopped me from putting more serious effort into this is the licensing terms of the model itself. "No part of this document may be reproduced in any form by any means without the express prior written permission of Arm."
Sail and it's models are largely BSD Licensed it appears. The specific model derived from the Arm XML specification being 3-clause. So it seems they have come to an agreement on licensing that allows distribution of derivative works.
If i could get one point across it would be that deriving a correct model from an English specification as a third party is difficult and error prone task, if first party models are becoming available it'd be great to encourage this behavior by making rust as friendly to those models as possible.
sorry that got kind of long
FWIW, my probe
crate is an example that does need to use section directives, because SystemTap SDT probes (sys/sdt.h
) are ultimately recorded in ELF notes.
I do have a desire to have functionality similar to asm goto
, but not fully generalized.
For the most common usages of asm goto
, it would suffice to have functionality equivalent to a static if
: a means of writing an if
-like statement where instead of a condition you have an asm block that may jump to one branch, or either jump or fall through to the other. That would fully address the most common usage of asm goto
without allowing general goto
.
Can you use a static put in the correct linker section using #[link_section]
instead?
That won't work because the static needs to point to a nop
instruction in the code (the label 990
).
Missed that nop. Would something like the following work?
extern "C" {
static $nop_label: u8;
}
#[link_section = "..."]
pub static THE_NOTE: Ty = Ty {
addr: &$nop_label,
// ...
};
asm!(concat_str!(
".globl", stringify!($nop_label),
stringify!($nop_label), ": nop"
):::);
Unfortunately that's incorrect if the compiler decides to duplicate the asm!
block (which it is allowed to do, e.g. if the function containing it is inlined in multiple places). You'll end up with duplicate definitions of the nop_label
symbol.
I understand.
I think this is the nub of Cranelift's concern; it doesn't seem at all non-trivial to me.
No; inline ASM is fundamentally different in the sense that operational semantics can be given for normal unsafe
and this can decide whether a specific execution trace has UB or not (e.g. in Miri). Meanwhile, Ralf notes that:
Absolutely
asm
needs to be specified eventually. However, to my knowledge, never before has anyone precisely specified a notion of "correct compilation" for inline assembly embedded in an optimized language. Like, I do literally not know of any industry or academic work that would do this. I appreciate any references anyone has here.
Except for the ABI aspect, extern "C"
is however distinctly "not our problem", whereas inline assembly is our problem in terms of e.g. register allocation and the actual function call.
Sounds like GitHub - CensoredUsername/dynasm-rs: A dynasm-like tool for rust. ?