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

charon_lib/ast/
ullbc_ast.rs
