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    Clone,
21    EnumIsA,
22    EnumToGetters,
23    EnumAsGetters,
24    SerializeState,
25    DeserializeState,
26    Drive,
27    DriveMut,
28)]
29pub enum StatementKind {
30    /// Assigns an `Rvalue` to a `Place`. e.g. `let y = x;` could become
31    /// `y := move x` which is represented as `Assign(y, Rvalue::Use(Operand::Move(x)))`.
32    Assign(Place, Rvalue),
33    /// Not used today because we take MIR built.
34    SetDiscriminant(Place, VariantId),
35    /// Equivalent to std::intrinsics::copy_nonoverlapping; this is not modelled as a function
36    /// call as it cannot diverge
37    CopyNonOverlapping(Box<CopyNonOverlapping>),
38    /// Indicates that this local should be allocated; if it is already allocated, this frees
39    /// the local and re-allocates it. The return value and arguments do not receive a
40    /// `StorageLive`. We ensure in the micro-pass `insert_storage_lives` that all other locals
41    /// have a `StorageLive` associated with them.
42    StorageLive(LocalId),
43    /// Indicates that this local should be deallocated; if it is already deallocated, this is
44    /// a no-op. A local may not have a `StorageDead` in the function's body, in which case it
45    /// is implicitly deallocated at the end of the function.
46    StorageDead(LocalId),
47    Deinit(Place),
48    /// Drop the value at the given place.
49    ///
50    /// Depending on `DropKind`, this may be a real call to `drop_in_place`, or a conditional call
51    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
52    /// for more details; to get precise drops use `--precise-drops`.
53    Drop(Place, TraitRef, #[drive(skip)] DropKind),
54    Assert(Assert),
55    Call(Call),
56    /// Panic also handles "unreachable". We keep the name of the panicking function that was
57    /// called.
58    Abort(AbortKind),
59    Return,
60    /// Break to outer loops.
61    /// The `usize` gives the index of the outer loop to break to:
62    /// * 0: break to first outer loop (the current loop)
63    /// * 1: break to second outer loop
64    /// * ...
65    #[drive(skip)]
66    Break(usize),
67    /// Continue to outer loops.
68    /// The `usize` gives the index of the outer loop to continue to:
69    /// * 0: continue to first outer loop (the current loop)
70    /// * 1: continue to second outer loop
71    /// * ...
72    #[drive(skip)]
73    Continue(usize),
74    /// No-op.
75    Nop,
76    Switch(Switch),
77    Loop(Block),
78    #[drive(skip)]
79    Error(String),
80}
81
82#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
83pub struct Statement {
84    pub span: Span,
85    /// Integer uniquely identifying this statement among the statmeents in the current body. To
86    /// simplify things we generate globally-fresh ids when creating a new `Statement`.
87    #[charon::rename("statement_id")]
88    pub id: StatementId,
89    pub kind: StatementKind,
90    /// Comments that precede this statement.
91    // This is filled in a late pass after all the control-flow manipulation.
92    #[drive(skip)]
93    pub comments_before: Vec<String>,
94}
95
96#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
97#[serde_state(state_implements = HashConsSerializerState)] // Avoid corecursive impls due to perfect derive
98pub struct Block {
99    pub span: Span,
100    pub statements: Vec<Statement>,
101}
102
103#[derive(
104    Debug,
105    Clone,
106    EnumIsA,
107    EnumToGetters,
108    EnumAsGetters,
109    SerializeState,
110    DeserializeState,
111    Drive,
112    DriveMut,
113    VariantName,
114    VariantIndexArity,
115)]
116pub enum Switch {
117    /// Gives the `if` block and the `else` block. The `Operand` is the condition of the `if`, e.g. `if (y == 0)` could become
118    /// ```text
119    /// v@3 := copy y; // Represented as `Assign(v@3, Use(Copy(y))`
120    /// v@2 := move v@3 == 0; // Represented as `Assign(v@2, BinOp(BinOp::Eq, Move(y), Const(0)))`
121    /// if (move v@2) { // Represented as `If(Move(v@2), <then branch>, <else branch>)`
122    /// ```
123    If(Operand, Block, Block),
124    /// Gives the integer type, a map linking values to switch branches, and the
125    /// otherwise block. Note that matches over enumerations are performed by
126    /// switching over the discriminant, which is an integer.
127    /// Also, we use a `Vec` to make sure the order of the switch
128    /// branches is preserved.
129    ///
130    /// Rk.: we use a vector of values, because some of the branches may
131    /// be grouped together, like for the following code:
132    /// ```text
133    /// match e {
134    ///   E::V1 | E::V2 => ..., // Grouped
135    ///   E::V3 => ...
136    /// }
137    /// ```
138    SwitchInt(Operand, LiteralTy, Vec<(Vec<Literal>, Block)>, Block),
139    /// A match over an ADT.
140    ///
141    /// The match statement is introduced in [crate::transform::resugar::reconstruct_matches]
142    /// (whenever we find a discriminant read, we merge it with the subsequent
143    /// switch into a match).
144    Match(Place, Vec<(Vec<VariantId>, Block)>, Option<Block>),
145}
146
147pub type ExprBody = GExprBody<Block>;
charon_lib/ast/llbc_ast.rs

charon_lib/ast/
llbc_ast.rs
