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

charon_lib/ast/
ullbc_ast.rs
