charon_lib/ast/
llbc_ast.rs

1//! LLBC
2//!
3//! MIR code where we have rebuilt the control-flow (`if ... then ... else ...`,
4//! `while ...`, ...).
5//!
6//! Also note that we completely break the definitions Statement and Terminator
7//! from MIR to use Statement only.
8
9pub use super::llbc_ast_utils::*;
10pub use crate::ast::*;
11use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
12use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
13use serde_state::{DeserializeState, SerializeState};
14
15// Globally-unique identifier for each statement.
16generate_index_type!(StatementId);
17// Globally-unique identifier for each block.
18generate_index_type!(BlockId);
19
20/// A raw statement: a statement without meta data.
21#[derive(
22    Debug,
23    PartialEq,
24    Eq,
25    Clone,
26    EnumIsA,
27    EnumToGetters,
28    EnumAsGetters,
29    SerializeState,
30    DeserializeState,
31    Drive,
32    DriveMut,
33    DriveTwo,
34)]
35pub enum StatementKind {
36    /// Assigns an `Rvalue` to a `Place`. e.g. `let y = x;` could become
37    /// `y := move x` which is represented as `Assign(y, Rvalue::Use(Operand::Move(x)))`.
38    Assign(Place, Rvalue),
39    /// Not used today because we take MIR built.
40    SetDiscriminant(Place, VariantId),
41    /// Indicates that this local should be allocated; if it is already allocated, this frees
42    /// the local and re-allocates it. The arguments do not receive a `StorageLive`. We ensure in
43    /// the micro-pass `insert_storage_statements` that all other locals have a `StorageLive`
44    /// associated with them.
45    StorageLive(LocalId),
46    /// Indicates that this local should be deallocated; if it is already deallocated, this is
47    /// a no-op. A local may not have a `StorageDead` in the function's body, in which case it
48    /// is implicitly deallocated at the end of the function. The return local does not receive a
49    /// `StorageDead`. We ensure in the micro-pass `insert_storage_statements` that all other locals
50    /// have a `StorageDead` before function exits.
51    StorageDead(LocalId),
52    /// A place is mentioned, but not accessed. The place itself must still be valid though, so
53    /// this statement is not a no-op: it can trigger UB if the place's projections are not valid
54    /// (e.g. because they go out of bounds).
55    PlaceMention(Place),
56    /// Statements that only affect borrow-checking.
57    Borrowck(BorrowckStatement),
58    /// Drop the value at the given place.
59    ///
60    /// Depending on `DropKind`, this may be a real call to `drop_glue`, or a conditional call
61    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
62    /// for more details; to get precise drops use `--precise-drops`.
63    Drop {
64        place: Place,
65        /// Reference to the `drop_glue` code to call on drop.
66        fn_ptr: FnPtr,
67        #[drive(skip)]
68        kind: DropKind,
69        on_unwind: Block,
70    },
71    Assert {
72        assert: Assert,
73        on_failure: AbortKind,
74        on_unwind: Block,
75    },
76    /// An inline assembly block. For now we only preserve the template string.
77    InlineAsm {
78        asm: String,
79        targets: Vec<Block>,
80        on_unwind: Block,
81    },
82    Call {
83        call: Call,
84        on_unwind: Block,
85    },
86    /// Panic also handles "unreachable". We keep the name of the panicking function that was
87    /// called.
88    Abort(AbortKind),
89    Return,
90    /// Unwind out of the current function into its caller.
91    UnwindResume,
92    /// Break to outer loops.
93    /// The `usize` gives the index of the outer loop to break to:
94    /// * 0: break to first outer loop (the current loop)
95    /// * 1: break to second outer loop
96    /// * ...
97    #[drive(skip)]
98    Break(usize),
99    /// Continue to outer loops.
100    /// The `usize` gives the index of the outer loop to continue to:
101    /// * 0: continue to first outer loop (the current loop)
102    /// * 1: continue to second outer loop
103    /// * ...
104    #[drive(skip)]
105    Continue(usize),
106    /// No-op.
107    Nop,
108    Switch(Switch),
109    Loop(Block),
110    #[drive(skip)]
111    Error(String),
112}
113
114#[derive(Debug, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
115pub struct Statement {
116    pub span: Span,
117    /// Integer uniquely identifying this statement among the statmeents in the current body. To
118    /// simplify things we generate globally-fresh ids when creating a new `Statement`.
119    #[cfg_attr(feature = "charon_on_charon", charon::rename("statement_id"))]
120    pub id: StatementId,
121    pub kind: StatementKind,
122    /// Comments that precede this statement.
123    // This is filled in a late pass after all the control-flow manipulation.
124    #[drive(skip)]
125    pub comments_before: Vec<String>,
126}
127
128/// Ignores statement ids.
129impl PartialEq for Statement {
130    fn eq(&self, other: &Self) -> bool {
131        self.span == other.span
132            && self.kind == other.kind
133            && self.comments_before == other.comments_before
134    }
135}
136
137#[derive(Debug, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
138#[serde_state(state_implements = HashConsSerializerState)] // Avoid corecursive impls due to perfect derive
139pub struct Block {
140    pub span: Span,
141    /// Integer uniquely identifying this block. To simplify things we generate globally-fresh ids
142    /// when creating a new `Block`.
143    #[cfg_attr(feature = "charon_on_charon", charon::rename("block_id"))]
144    pub id: BlockId,
145    pub statements: Vec<Statement>,
146}
147
148/// Ignores block ids.
149impl PartialEq for Block {
150    fn eq(&self, other: &Self) -> bool {
151        self.span == other.span && self.statements == other.statements
152    }
153}
154
155#[derive(
156    Debug,
157    PartialEq,
158    Eq,
159    Clone,
160    EnumIsA,
161    EnumToGetters,
162    EnumAsGetters,
163    SerializeState,
164    DeserializeState,
165    Drive,
166    DriveMut,
167    DriveTwo,
168    VariantName,
169    VariantIndexArity,
170)]
171pub enum Switch {
172    /// Gives the `if` block and the `else` block. The `Operand` is the condition of the `if`, e.g. `if (y == 0)` could become
173    /// ```text
174    /// v@3 := copy y; // Represented as `Assign(v@3, Use(Copy(y))`
175    /// v@2 := move v@3 == 0; // Represented as `Assign(v@2, BinOp(BinOp::Eq, Move(y), Const(0)))`
176    /// if (move v@2) { // Represented as `If(Move(v@2), <then branch>, <else branch>)`
177    /// ```
178    If(Operand, Block, Block),
179    /// Gives the integer type, a map linking values to switch branches, and the
180    /// otherwise block. Note that matches over enumerations are performed by
181    /// switching over the discriminant, which is an integer.
182    /// Also, we use a `Vec` to make sure the order of the switch
183    /// branches is preserved.
184    ///
185    /// Rk.: we use a vector of values, because some of the branches may
186    /// be grouped together, like for the following code:
187    /// ```text
188    /// match e {
189    ///   E::V1 | E::V2 => ..., // Grouped
190    ///   E::V3 => ...
191    /// }
192    /// ```
193    SwitchInt(Operand, LiteralTy, Vec<(Vec<Literal>, Block)>, Block),
194    /// A match over an ADT.
195    ///
196    /// The match statement is introduced in [crate::transform::resugar::reconstruct_matches]
197    /// (whenever we find a discriminant read, we merge it with the subsequent
198    /// switch into a match).
199    Match(Place, Vec<(Vec<VariantId>, Block)>, Option<Block>),
200}
201
202pub type ExprBody = GExprBody<Block>;
charon_lib/ast/llbc_ast.rs

charon_lib/ast/
llbc_ast.rs
