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

charon_lib/ast/
llbc_ast.rs
