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 the value at the given place.
39 ///
40 /// For MIR built and promoted, this is a conditional drop: the value will only be dropped if
41 /// it has not already been moved out. For MIR elaborated and optimized, this is a real drop.
42 ///
43 /// This drop is then equivalent to a call to `std::ptr::drop_in_place(&raw mut place)`.
44 Drop(Place),
45 Assert(Assert),
46 Call(Call),
47 /// Panic also handles "unreachable". We keep the name of the panicking function that was
48 /// called.
49 Abort(AbortKind),
50 Return,
51 /// Break to outer loops.
52 /// The `usize` gives the index of the outer loop to break to:
53 /// * 0: break to first outer loop (the current loop)
54 /// * 1: break to second outer loop
55 /// * ...
56 #[drive(skip)]
57 Break(usize),
58 /// Continue to outer loops.
59 /// The `usize` gives the index of the outer loop to continue to:
60 /// * 0: continue to first outer loop (the current loop)
61 /// * 1: continue to second outer loop
62 /// * ...
63 #[drive(skip)]
64 Continue(usize),
65 /// No-op.
66 Nop,
67 Switch(Switch),
68 Loop(Block),
69 #[drive(skip)]
70 Error(String),
71}
72
73#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
74pub struct Statement {
75 pub span: Span,
76 pub content: RawStatement,
77 /// Comments that precede this statement.
78 // This is filled in a late pass after all the control-flow manipulation.
79 #[drive(skip)]
80 pub comments_before: Vec<String>,
81}
82
83#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
84pub struct Block {
85 pub span: Span,
86 pub statements: Vec<Statement>,
87}
88
89#[derive(
90 Debug,
91 Clone,
92 EnumIsA,
93 EnumToGetters,
94 EnumAsGetters,
95 Serialize,
96 Deserialize,
97 Drive,
98 DriveMut,
99 VariantName,
100 VariantIndexArity,
101)]
102pub enum Switch {
103 /// Gives the `if` block and the `else` block. The `Operand` is the condition of the `if`, e.g. `if (y == 0)` could become
104 /// ```text
105 /// v@3 := copy y; // Represented as `Assign(v@3, Use(Copy(y))`
106 /// v@2 := move v@3 == 0; // Represented as `Assign(v@2, BinOp(BinOp::Eq, Move(y), Const(0)))`
107 /// if (move v@2) { // Represented as `If(Move(v@2), <then branch>, <else branch>)`
108 /// ```
109 If(Operand, Block, Block),
110 /// Gives the integer type, a map linking values to switch branches, and the
111 /// otherwise block. Note that matches over enumerations are performed by
112 /// switching over the discriminant, which is an integer.
113 /// Also, we use a `Vec` to make sure the order of the switch
114 /// branches is preserved.
115 ///
116 /// Rk.: we use a vector of values, because some of the branches may
117 /// be grouped together, like for the following code:
118 /// ```text
119 /// match e {
120 /// E::V1 | E::V2 => ..., // Grouped
121 /// E::V3 => ...
122 /// }
123 /// ```
124 SwitchInt(Operand, IntegerTy, Vec<(Vec<ScalarValue>, Block)>, Block),
125 /// A match over an ADT.
126 ///
127 /// The match statement is introduced in [crate::transform::remove_read_discriminant]
128 /// (whenever we find a discriminant read, we merge it with the subsequent
129 /// switch into a match).
130 Match(Place, Vec<(Vec<VariantId>, Block)>, Option<Block>),
131}
132
133pub type ExprBody = GExprBody<Block>;