charon_lib/ast/
ullbc_ast.rs

1//! "Unstructured LLBC" ast (ULLBC). This is LLBC before the control-flow
2//! reconstruction. In effect, this is a cleaned up version of MIR.
3pub use crate::ast::*;
4use crate::ids::IndexVec;
5use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
6use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
7use serde_state::{DeserializeState, SerializeState};
8
9// Block identifier. Similar to rust's `BasicBlock`.
10generate_index_type!(BlockId, "Block");
11
12// The entry block of a function is always the block with id 0
13pub static START_BLOCK_ID: BlockId = BlockId::ZERO;
14
15#[cfg_attr(feature = "charon_on_charon", charon::rename("Blocks"))]
16pub type BodyContents = IndexVec<BlockId, BlockData>;
17pub type ExprBody = GExprBody<BodyContents>;
18
19/// A raw statement: a statement without meta data.
20#[derive(
21    Debug,
22    PartialEq,
23    Eq,
24    Clone,
25    EnumIsA,
26    EnumAsGetters,
27    VariantName,
28    SerializeState,
29    DeserializeState,
30    Drive,
31    DriveMut,
32    DriveTwo,
33)]
34pub enum StatementKind {
35    Assign(Place, Rvalue),
36    /// A call. For now, we don't support dynamic calls (i.e. to a function pointer in memory).
37    SetDiscriminant(Place, VariantId),
38    /// Indicates that this local should be allocated; if it is already allocated, this frees
39    /// the local and re-allocates it. The arguments do not receive a `StorageLive`. We ensure in
40    /// the micro-pass `insert_storage_statements` that all other locals have a `StorageLive`
41    /// associated with them.
42    StorageLive(LocalId),
43    /// Indicates that this local should be deallocated; if it is already deallocated, this is
44    /// a no-op. A local may not have a `StorageDead` in the function's body, in which case it
45    /// is implicitly deallocated at the end of the function. The return local does not receive a
46    /// `StorageDead`. We ensure in the micro-pass `insert_storage_statements` that all other locals
47    /// have a `StorageDead` before function exits.
48    StorageDead(LocalId),
49    /// A place is mentioned, but not accessed. The place itself must still be valid though, so
50    /// this statement is not a no-op: it can trigger UB if the place's projections are not valid
51    /// (e.g. because they go out of bounds).
52    PlaceMention(Place),
53    /// Statements that only affect borrow-checking.
54    Borrowck(BorrowckStatement),
55    /// A non-diverging runtime check for a condition. This can be either:
56    /// - Emitted for inlined "assumes" (which cause UB on failure)
57    /// - Reconstructed from `if b { panic() }` if `--reconstruct-asserts` is set.
58    ///
59    /// This statement comes with the effect that happens when the check fails
60    /// (rather than representing it as an unwinding edge).
61    Assert {
62        assert: Assert,
63        on_failure: AbortKind,
64    },
65    /// Does nothing. Useful for passes.
66    Nop,
67}
68
69#[derive(
70    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
71)]
72pub struct Statement {
73    pub span: Span,
74    pub kind: StatementKind,
75    /// Comments that precede this statement.
76    // This is filled in a late pass after all the control-flow manipulation.
77    #[drive(skip)]
78    pub comments_before: Vec<String>,
79}
80
81#[derive(
82    Debug,
83    PartialEq,
84    Eq,
85    Clone,
86    EnumIsA,
87    EnumAsGetters,
88    VariantName,
89    VariantIndexArity,
90    SerializeState,
91    DeserializeState,
92    Drive,
93    DriveMut,
94    DriveTwo,
95)]
96#[cfg_attr(feature = "charon_on_charon", charon::rename("Switch"))]
97pub enum SwitchTargets {
98    /// Gives the `if` block and the `else` block
99    If(BlockId, BlockId),
100    /// Gives the integer type, a map linking values to switch branches, and the
101    /// otherwise block. Note that matches over enumerations are performed by
102    /// switching over the discriminant, which is an integer.
103    SwitchInt(LiteralTy, Vec<(Literal, BlockId)>, BlockId),
104}
105
106/// A raw terminator: a terminator without meta data.
107#[derive(
108    Debug,
109    PartialEq,
110    Eq,
111    Clone,
112    EnumIsA,
113    EnumAsGetters,
114    SerializeState,
115    DeserializeState,
116    Drive,
117    DriveMut,
118    DriveTwo,
119)]
120pub enum TerminatorKind {
121    Goto {
122        target: BlockId,
123    },
124    Switch {
125        discr: Operand,
126        targets: SwitchTargets,
127    },
128    Call {
129        call: Call,
130        target: BlockId,
131        on_unwind: BlockId,
132    },
133    /// Drop the value at the given place.
134    ///
135    /// Depending on `DropKind`, this may be a real call to `drop_glue`, or a conditional call
136    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
137    /// for more details; to get precise drops use `--precise-drops`.
138    Drop {
139        #[drive(skip)]
140        kind: DropKind,
141        place: Place,
142        /// Reference to the `drop_glue` code to call on drop.
143        fn_ptr: FnPtr,
144        target: BlockId,
145        on_unwind: BlockId,
146    },
147    /// Assert that the given condition holds, and if not, unwind to the given block. This is used for
148    /// bounds checks, overflow checks, etc.
149    #[cfg_attr(feature = "charon_on_charon", charon::rename("TAssert"))]
150    Assert {
151        assert: Assert,
152        target: BlockId,
153        on_unwind: BlockId,
154    },
155    /// An inline assembly block. For now we only preserve the template string.
156    InlineAsm {
157        asm: String,
158        targets: Vec<BlockId>,
159        on_unwind: BlockId,
160    },
161    /// Handles panics and impossible cases.
162    Abort(AbortKind),
163    Return,
164    /// Unwind out of the current function into its caller.
165    UnwindResume,
166}
167
168#[derive(
169    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
170)]
171pub struct Terminator {
172    pub span: Span,
173    pub kind: TerminatorKind,
174    /// Comments that precede this terminator.
175    // This is filled in a late pass after all the control-flow manipulation.
176    #[drive(skip)]
177    pub comments_before: Vec<String>,
178}
179
180#[derive(
181    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
182)]
183#[cfg_attr(feature = "charon_on_charon", charon::rename("Block"))]
184pub struct BlockData {
185    pub statements: Vec<Statement>,
186    pub terminator: Terminator,
187}
charon_lib/ast/ullbc_ast.rs

charon_lib/ast/
ullbc_ast.rs
