charon_lib/ast/bodies/
asm.rs

1//! Inline assembly inside a function body.
2//!
3//! See the [Rust Reference](https://doc.rust-lang.org/reference/inline-assembly.html) for the
4//! meaning of operands and options.
5use crate::ast::*;
6use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
7use macros::EnumIsA;
8use serde_state::{DeserializeState, SerializeState};
9use ustr::Ustr;
10
11generate_index_type!(AsmOperandId, "AsmOperand");
12
13/// Contents of an inline assembly block.
14#[derive(Debug, Clone, PartialEq, Eq)]
15#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
16pub struct InlineAsm {
17    /// Whether this is an `asm!` or `naked_asm!` assembly block.
18    pub kind: AsmKind,
19    /// The assembly code, parsed into a series of text fragments interspersed with placeholders.
20    pub template: Vec<AsmTemplatePiece>,
21    /// Input/outputs of the asm block. Not all of them may be referred to by placeholders, e.g.
22    /// explicit register operands may not.
23    pub operands: IndexVec<AsmOperandId, AsmOperand>,
24    /// The flags set in `options(...)`.
25    pub options: AsmOptions,
26}
27
28/// The kind of assembly block this is.
29#[derive(Debug, Copy, Clone, PartialEq, Eq)]
30#[derive(EnumIsA)]
31#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
32pub enum AsmKind {
33    /// Assembly generated by the `asm!` macro.
34    Asm,
35    /// Assembly generated by the `naked_asm!` macro. This forms the entire function body and only
36    /// accepts `const` and `sym` operands.
37    NakedAsm,
38}
39
40/// A fragment of assembly code.
41#[derive(Debug, Clone, PartialEq, Eq)]
42#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
43#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("AsmTemplate"))]
44pub enum AsmTemplatePiece {
45    /// Literal assembly text.
46    Text(#[serde_state(stateless)] Ustr),
47    /// Substitutes an operand, optionally with an architecture-specific register modifier.
48    Placeholder {
49        operand_id: AsmOperandId,
50        modifier: Option<char>,
51        span: Span,
52    },
53}
54
55/// An explicit register (such as `"rax"`) or a register class (such as `reg`).
56#[derive(Debug, Clone, PartialEq, Eq)]
57#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
58#[serde_state(stateless)]
59pub enum AsmRegister {
60    Explicit(Ustr),
61    Class(Ustr),
62}
63
64/// An operand supplied to inline assembly.
65#[derive(Debug, Clone, PartialEq, Eq)]
66#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
67pub enum AsmOperand {
68    /// `in(reg) value`: read `value` into the register before running the assembly.
69    In { reg: AsmRegister, value: Operand },
70    /// `out(reg) place` or `lateout(reg) place`: the contents of the register are written to
71    /// `place` at the end of the block, or discarded if `place` is `None` (essentially acting as a
72    /// clobber).
73    Out {
74        reg: AsmRegister,
75        late: bool,
76        place: Option<Place>,
77    },
78    /// `inout(reg) value => place` or `inlateout(reg) value => place`. Combines `in(reg) value`
79    /// and `out/lateout(reg) place`. The input and output places may be the same.
80    InOut {
81        reg: AsmRegister,
82        late: bool,
83        in_value: Operand,
84        out_place: Option<Place>,
85    },
86    /// An integer constant substituted into the template.
87    Const(ConstantExpr),
88    /// A function symbol substituted into the template.
89    SymFn(FnPtr),
90    /// A static symbol substituted into the template.
91    SymStatic(GlobalDeclRef),
92    /// The address of a block that the assembly may jump to. That `BranchId` corresponds to the
93    /// targets listed in [`ullbc_ast::TerminatorKind::InlineAsm`] and
94    /// [`llbc_ast::StatementKind::InlineAsm`].
95    Label(BranchId),
96}
97
98/// The flags set in `options(...)`. These flags constrain the assembly's effects; they do not
99/// describe instructions in the template itself.
100#[derive(Debug, Copy, Clone, PartialEq, Eq)]
101#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
102pub struct AsmOptions {
103    /// The assembly code has no side effects, must eventually return, and its outputs depend only
104    /// on its direct inputs or values read from memory.
105    pub pure: bool,
106    /// The assembly code does not read from or write to any memory accessible outside of the
107    /// assembly code.
108    pub nomem: bool,
109    /// The assembly code does not write to any memory accessible outside of the assembly code.
110    pub readonly: bool,
111    /// The assembly code does not modify the flags register.
112    pub preserves_flags: bool,
113    /// The assembly code does not fall through; it may still jump to label blocks.
114    pub noreturn: bool,
115    /// The assembly code does not push data to the stack, or write to the stack red-zone.
116    pub nostack: bool,
117    /// Only valid on x86; causes the assembler to use the .att_syntax prefix mode of the GNU assembler.
118    pub att_syntax: bool,
119    /// Allows unwinding out of an `asm!` block (unstable, see
120    /// https://github.com/rust-lang/rust/issues/93334). `naked_asm!` may unwind regardless of this
121    /// option.
122    pub may_unwind: bool,
123}
charon_lib/ast/bodies/asm.rs

charon_lib/ast/bodies/
asm.rs
