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

charon_lib/ast/
ullbc_ast.rs
