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::{Deserialize, Serialize};
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, Clone, EnumIsA, EnumAsGetters, VariantName, Serialize, Deserialize, Drive, DriveMut,
21)]
22pub enum StatementKind {
23    Assign(Place, Rvalue),
24    /// A call. For now, we don't support dynamic calls (i.e. to a function pointer in memory).
25    SetDiscriminant(Place, VariantId),
26    /// Equivalent to std::intrinsics::copy_nonoverlapping; this is not modelled as a function
27    /// call as it cannot diverge
28    CopyNonOverlapping(Box<CopyNonOverlapping>),
29    /// Indicates that this local should be allocated; if it is already allocated, this frees
30    /// the local and re-allocates it. The return value and arguments do not receive a
31    /// `StorageLive`. We ensure in the micro-pass `insert_storage_lives` that all other locals
32    /// have a `StorageLive` associated with them.
33    StorageLive(LocalId),
34    /// Indicates that this local should be deallocated; if it is already deallocated, this is
35    /// a no-op. A local may not have a `StorageDead` in the function's body, in which case it
36    /// is implicitly deallocated at the end of the function.
37    StorageDead(LocalId),
38    Deinit(Place),
39    /// A built-in assert, which corresponds to runtime checks that we remove, namely: bounds
40    /// checks, over/underflow checks, div/rem by zero checks, pointer alignement check.
41    Assert(Assert),
42    /// Does nothing. Useful for passes.
43    Nop,
44    #[charon::opaque]
45    #[drive(skip)]
46    Error(String),
47}
48
49#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
50pub struct Statement {
51    pub span: Span,
52    pub kind: StatementKind,
53    /// Comments that precede this statement.
54    // This is filled in a late pass after all the control-flow manipulation.
55    #[drive(skip)]
56    pub comments_before: Vec<String>,
57}
58
59#[derive(
60    Debug,
61    Clone,
62    EnumIsA,
63    EnumAsGetters,
64    VariantName,
65    VariantIndexArity,
66    Serialize,
67    Deserialize,
68    Drive,
69    DriveMut,
70)]
71#[charon::rename("Switch")]
72pub enum SwitchTargets {
73    /// Gives the `if` block and the `else` block
74    If(BlockId, BlockId),
75    /// Gives the integer type, a map linking values to switch branches, and the
76    /// otherwise block. Note that matches over enumerations are performed by
77    /// switching over the discriminant, which is an integer.
78    SwitchInt(LiteralTy, Vec<(Literal, BlockId)>, BlockId),
79}
80
81/// A raw terminator: a terminator without meta data.
82#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
83pub enum TerminatorKind {
84    Goto {
85        target: BlockId,
86    },
87    Switch {
88        discr: Operand,
89        targets: SwitchTargets,
90    },
91    Call {
92        call: Call,
93        target: BlockId,
94        on_unwind: BlockId,
95    },
96    /// Drop the value at the given place.
97    ///
98    /// This calls `<T as Destruct>::drop_in_place(&raw mut place)` and marks the place as
99    /// moved-out-of. The `drop_in_place` method is added by Charon, it contains the same code as
100    /// the `core::ptr::drop_in_place<T>` builtin).
101    Drop {
102        place: Place,
103        tref: TraitRef,
104        target: BlockId,
105        on_unwind: BlockId,
106    },
107    /// Handles panics and impossible cases.
108    Abort(AbortKind),
109    Return,
110    UnwindResume,
111}
112
113#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
114pub struct Terminator {
115    pub span: Span,
116    pub kind: TerminatorKind,
117    /// Comments that precede this terminator.
118    // This is filled in a late pass after all the control-flow manipulation.
119    #[drive(skip)]
120    pub comments_before: Vec<String>,
121}
122
123#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
124#[charon::rename("Block")]
125pub struct BlockData {
126    pub statements: Vec<Statement>,
127    pub terminator: Terminator,
128}
charon_lib/ast/ullbc_ast.rs

charon_lib/ast/
ullbc_ast.rs
