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};
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#[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)]
33pub enum StatementKind {
34    Assign(Place, Rvalue),
35    /// A call. For now, we don't support dynamic calls (i.e. to a function pointer in memory).
36    SetDiscriminant(Place, VariantId),
37    /// Equivalent to std::intrinsics::copy_nonoverlapping; this is not modelled as a function
38    /// call as it cannot diverge
39    CopyNonOverlapping(Box<CopyNonOverlapping>),
40    /// Indicates that this local should be allocated; if it is already allocated, this frees
41    /// the local and re-allocates it. The return value and arguments do not receive a
42    /// `StorageLive`. We ensure in the micro-pass `insert_storage_lives` that all other locals
43    /// have a `StorageLive` associated with them.
44    StorageLive(LocalId),
45    /// Indicates that this local should be deallocated; if it is already deallocated, this is
46    /// a no-op. A local may not have a `StorageDead` in the function's body, in which case it
47    /// is implicitly deallocated at the end of the function.
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    /// A non-diverging runtime check for a condition. This can be either:
54    /// - Emitted for inlined "assumes" (which cause UB on failure)
55    /// - Reconstructed from `if b { panic() }` if `--reconstruct-asserts` is set.
56    ///
57    /// This statement comes with the effect that happens when the check fails
58    /// (rather than representing it as an unwinding edge).
59    Assert {
60        assert: Assert,
61        on_failure: AbortKind,
62    },
63    /// Does nothing. Useful for passes.
64    Nop,
65}
66
67#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
68pub struct Statement {
69    pub span: Span,
70    pub kind: StatementKind,
71    /// Comments that precede this statement.
72    // This is filled in a late pass after all the control-flow manipulation.
73    #[drive(skip)]
74    pub comments_before: Vec<String>,
75}
76
77#[derive(
78    Debug,
79    PartialEq,
80    Eq,
81    Clone,
82    EnumIsA,
83    EnumAsGetters,
84    VariantName,
85    VariantIndexArity,
86    SerializeState,
87    DeserializeState,
88    Drive,
89    DriveMut,
90)]
91#[charon::rename("Switch")]
92pub enum SwitchTargets {
93    /// Gives the `if` block and the `else` block
94    If(BlockId, BlockId),
95    /// Gives the integer type, a map linking values to switch branches, and the
96    /// otherwise block. Note that matches over enumerations are performed by
97    /// switching over the discriminant, which is an integer.
98    SwitchInt(LiteralTy, Vec<(Literal, BlockId)>, BlockId),
99}
100
101/// A raw terminator: a terminator without meta data.
102#[derive(
103    Debug,
104    PartialEq,
105    Eq,
106    Clone,
107    EnumIsA,
108    EnumAsGetters,
109    SerializeState,
110    DeserializeState,
111    Drive,
112    DriveMut,
113)]
114pub enum TerminatorKind {
115    Goto {
116        target: BlockId,
117    },
118    Switch {
119        discr: Operand,
120        targets: SwitchTargets,
121    },
122    Call {
123        call: Call,
124        target: BlockId,
125        on_unwind: BlockId,
126    },
127    /// Drop the value at the given place.
128    ///
129    /// Depending on `DropKind`, this may be a real call to `drop_in_place`, or a conditional call
130    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
131    /// for more details; to get precise drops use `--precise-drops`.
132    Drop {
133        #[drive(skip)]
134        kind: DropKind,
135        place: Place,
136        tref: TraitRef,
137        target: BlockId,
138        on_unwind: BlockId,
139    },
140    /// Assert that the given condition holds, and if not, unwind to the given block. This is used for
141    /// bounds checks, overflow checks, etc.
142    #[charon::rename("TAssert")]
143    Assert {
144        assert: Assert,
145        target: BlockId,
146        on_unwind: BlockId,
147    },
148    /// Handles panics and impossible cases.
149    Abort(AbortKind),
150    Return,
151    UnwindResume,
152}
153
154#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
155pub struct Terminator {
156    pub span: Span,
157    pub kind: TerminatorKind,
158    /// Comments that precede this terminator.
159    // This is filled in a late pass after all the control-flow manipulation.
160    #[drive(skip)]
161    pub comments_before: Vec<String>,
162}
163
164#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
165#[charon::rename("Block")]
166pub struct BlockData {
167    pub statements: Vec<Statement>,
168    pub terminator: Terminator,
169}
charon_lib/ast/ullbc_ast.rs

charon_lib/ast/
ullbc_ast.rs
