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 derive_generic_visitor::{Drive, DriveMut};
5use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
6use serde_state::{DeserializeState, SerializeState};
7
8// Block identifier. Similar to rust's `BasicBlock`.
9generate_index_type!(BlockId, "Block");
10
11// The entry block of a function is always the block with id 0
12pub static START_BLOCK_ID: BlockId = BlockId::ZERO;
13
14#[charon::rename("Blocks")]
15pub type BodyContents = Vector<BlockId, BlockData>;
16pub type ExprBody = GExprBody<BodyContents>;
17
18/// A raw statement: a statement without meta data.
19#[derive(
20    Debug,
21    Clone,
22    EnumIsA,
23    EnumAsGetters,
24    VariantName,
25    SerializeState,
26    DeserializeState,
27    Drive,
28    DriveMut,
29)]
30pub enum StatementKind {
31    Assign(Place, Rvalue),
32    /// A call. For now, we don't support dynamic calls (i.e. to a function pointer in memory).
33    SetDiscriminant(Place, VariantId),
34    /// Equivalent to std::intrinsics::copy_nonoverlapping; this is not modelled as a function
35    /// call as it cannot diverge
36    CopyNonOverlapping(Box<CopyNonOverlapping>),
37    /// Indicates that this local should be allocated; if it is already allocated, this frees
38    /// the local and re-allocates it. The return value and arguments do not receive a
39    /// `StorageLive`. We ensure in the micro-pass `insert_storage_lives` that all other locals
40    /// have a `StorageLive` associated with them.
41    StorageLive(LocalId),
42    /// Indicates that this local should be deallocated; if it is already deallocated, this is
43    /// a no-op. A local may not have a `StorageDead` in the function's body, in which case it
44    /// is implicitly deallocated at the end of the function.
45    StorageDead(LocalId),
46    Deinit(Place),
47    /// A built-in assert, which corresponds to runtime checks that we remove, namely: bounds
48    /// checks, over/underflow checks, div/rem by zero checks, pointer alignement check.
49    Assert(Assert),
50    /// Does nothing. Useful for passes.
51    Nop,
52    #[charon::opaque]
53    #[drive(skip)]
54    Error(String),
55}
56
57#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
58pub struct Statement {
59    pub span: Span,
60    pub kind: StatementKind,
61    /// Comments that precede this statement.
62    // This is filled in a late pass after all the control-flow manipulation.
63    #[drive(skip)]
64    pub comments_before: Vec<String>,
65}
66
67#[derive(
68    Debug,
69    Clone,
70    EnumIsA,
71    EnumAsGetters,
72    VariantName,
73    VariantIndexArity,
74    SerializeState,
75    DeserializeState,
76    Drive,
77    DriveMut,
78)]
79#[charon::rename("Switch")]
80pub enum SwitchTargets {
81    /// Gives the `if` block and the `else` block
82    If(BlockId, BlockId),
83    /// Gives the integer type, a map linking values to switch branches, and the
84    /// otherwise block. Note that matches over enumerations are performed by
85    /// switching over the discriminant, which is an integer.
86    SwitchInt(LiteralTy, Vec<(Literal, BlockId)>, BlockId),
87}
88
89/// A raw terminator: a terminator without meta data.
90#[derive(
91    Debug, Clone, EnumIsA, EnumAsGetters, SerializeState, DeserializeState, Drive, DriveMut,
92)]
93pub enum TerminatorKind {
94    Goto {
95        target: BlockId,
96    },
97    Switch {
98        discr: Operand,
99        targets: SwitchTargets,
100    },
101    Call {
102        call: Call,
103        target: BlockId,
104        on_unwind: BlockId,
105    },
106    /// Drop the value at the given place.
107    ///
108    /// Depending on `DropKind`, this may be a real call to `drop_in_place`, or a conditional call
109    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
110    /// for more details; to get precise drops use `--precise-drops`.
111    Drop {
112        #[drive(skip)]
113        kind: DropKind,
114        place: Place,
115        tref: TraitRef,
116        target: BlockId,
117        on_unwind: BlockId,
118    },
119    /// Handles panics and impossible cases.
120    Abort(AbortKind),
121    Return,
122    UnwindResume,
123}
124
125#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
126pub struct Terminator {
127    pub span: Span,
128    pub kind: TerminatorKind,
129    /// Comments that precede this terminator.
130    // This is filled in a late pass after all the control-flow manipulation.
131    #[drive(skip)]
132    pub comments_before: Vec<String>,
133}
134
135#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
136#[charon::rename("Block")]
137pub struct BlockData {
138    pub statements: Vec<Statement>,
139    pub terminator: Terminator,
140}
charon_lib/ast/ullbc_ast.rs

charon_lib/ast/
ullbc_ast.rs
