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

charon_lib/ast/
llbc_ast.rs
