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

charon_lib/ast/
llbc_ast.rs
