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    Deinit(Place),
48    /// A runtime check for a condition. This can be either:
49    /// - Emitted for bounds/overflow/etc checks if `--reconstruct-fallible-operations` is not set;
50    /// - Reconstructed from `if b { panic() }` if `--reconstruct-assets` is set.
51    Assert(Assert),
52    /// Does nothing. Useful for passes.
53    Nop,
54}
55
56#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
57pub struct Statement {
58    pub span: Span,
59    pub kind: StatementKind,
60    /// Comments that precede this statement.
61    // This is filled in a late pass after all the control-flow manipulation.
62    #[drive(skip)]
63    pub comments_before: Vec<String>,
64}
65
66#[derive(
67    Debug,
68    Clone,
69    EnumIsA,
70    EnumAsGetters,
71    VariantName,
72    VariantIndexArity,
73    SerializeState,
74    DeserializeState,
75    Drive,
76    DriveMut,
77)]
78#[charon::rename("Switch")]
79pub enum SwitchTargets {
80    /// Gives the `if` block and the `else` block
81    If(BlockId, BlockId),
82    /// Gives the integer type, a map linking values to switch branches, and the
83    /// otherwise block. Note that matches over enumerations are performed by
84    /// switching over the discriminant, which is an integer.
85    SwitchInt(LiteralTy, Vec<(Literal, BlockId)>, BlockId),
86}
87
88/// A raw terminator: a terminator without meta data.
89#[derive(
90    Debug, Clone, EnumIsA, EnumAsGetters, SerializeState, DeserializeState, Drive, DriveMut,
91)]
92pub enum TerminatorKind {
93    Goto {
94        target: BlockId,
95    },
96    Switch {
97        discr: Operand,
98        targets: SwitchTargets,
99    },
100    Call {
101        call: Call,
102        target: BlockId,
103        on_unwind: BlockId,
104    },
105    /// Drop the value at the given place.
106    ///
107    /// Depending on `DropKind`, this may be a real call to `drop_in_place`, or a conditional call
108    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
109    /// for more details; to get precise drops use `--precise-drops`.
110    Drop {
111        #[drive(skip)]
112        kind: DropKind,
113        place: Place,
114        tref: TraitRef,
115        target: BlockId,
116        on_unwind: BlockId,
117    },
118    /// Handles panics and impossible cases.
119    Abort(AbortKind),
120    Return,
121    UnwindResume,
122}
123
124#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
125pub struct Terminator {
126    pub span: Span,
127    pub kind: TerminatorKind,
128    /// Comments that precede this terminator.
129    // This is filled in a late pass after all the control-flow manipulation.
130    #[drive(skip)]
131    pub comments_before: Vec<String>,
132}
133
134#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
135#[charon::rename("Block")]
136pub struct BlockData {
137    pub statements: Vec<Statement>,
138    pub terminator: Terminator,
139}
charon_lib/ast/ullbc_ast.rs

charon_lib/ast/
ullbc_ast.rs
