charon_lib/ast/bodies/
structured.rs

1//! Bodies with structured control-flow (`if ... then ... else ...`,
2//! `loop { ... }`, etc).
3//!
4//! We reconstruct this structure from the unstructured ast in an optional translation pass.
5use derive_generic_visitor::*;
6use macros::{EnumAsGetters, EnumIsA, EnumToGetters};
7use serde_state::{DeserializeState, SerializeState};
8use std::mem;
9use std::sync::atomic::{AtomicUsize, Ordering};
10
11use crate::ast::*;
12
13// Globally-unique identifier for each statement.
14generate_index_type!(StatementId);
15// Globally-unique identifier for each block.
16generate_index_type!(BlockId);
17
18pub type ExprBody = GExprBody<Block>;
19
20/// A sequence of statements.
21#[derive(Debug, Clone, Eq)]
22#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
23#[serde_state(state_implements = DedupSerializerState)] // Avoid corecursive impls due to perfect derive
24pub struct Block {
25    pub span: Span,
26    /// An integer uniquely identifying this block.
27    #[cfg_attr(feature = "charon_on_charon", charon::rename("block_id"))]
28    pub id: BlockId,
29    pub statements: Vec<Statement>,
30}
31
32/// A statement, which can contain nested statements inside loops or switchers.
33#[derive(Debug, Clone, Eq)]
34#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
35pub struct Statement {
36    pub span: Span,
37    /// An integer uniquely identifying this statement.
38    #[cfg_attr(feature = "charon_on_charon", charon::rename("statement_id"))]
39    pub id: StatementId,
40    pub kind: StatementKind,
41    /// Comments that precede this statement.
42    // This is filled in a late pass after all the control-flow manipulation.
43    pub comments_before: Vec<String>,
44}
45
46#[derive(Debug, Clone, PartialEq, Eq)]
47#[derive(EnumIsA, EnumToGetters, EnumAsGetters)]
48#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
49pub enum StatementKind {
50    /// Assigns an `Rvalue` to a `Place`. e.g. `let y = x;` could become
51    /// `y := move x` which is represented as `Assign(y, Rvalue::Use(Operand::Move(x)))`.
52    Assign(Place, Rvalue),
53    /// Not used today because we take MIR built.
54    SetDiscriminant(Place, VariantId),
55    /// Indicates that this local should be allocated; if it is already allocated, this frees
56    /// the local and re-allocates it. The arguments do not receive a `StorageLive`. We ensure in
57    /// the micro-pass `insert_storage_statements` that all other locals have a `StorageLive`
58    /// associated with them.
59    StorageLive(LocalId),
60    /// Deallocates the given local; if it is already deallocated, this is
61    /// a no-op. Not all local deallocations are explicit: if a non-return local is still live at
62    /// function end (return or unwind), it is implicitly deallocated.
63    /// If `--deallocate-all-locals` is set, all local deallocations are made explicit.
64    StorageDead(LocalId),
65    /// A place is mentioned, but not accessed. The place itself must still be valid though, so
66    /// this statement is not a no-op: it can trigger UB if the place's projections are not valid
67    /// (e.g. because they go out of bounds).
68    PlaceMention(Place),
69    /// Statements that only affect borrow-checking.
70    Borrowck(BorrowckStatement),
71    /// Drop the value at the given place.
72    ///
73    /// Depending on `DropKind`, this may be a real call to `drop_glue`, or a conditional call
74    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
75    /// for more details; to get precise drops use `--precise-drops`.
76    Drop {
77        place: Place,
78        /// Reference to the `drop_glue` code to call on drop.
79        fn_ptr: FnPtr,
80        kind: DropKind,
81        on_unwind: Block,
82    },
83    Assert {
84        assert: Assert,
85        on_failure: AbortKind,
86        on_unwind: Block,
87    },
88    /// An inline assembly block.
89    InlineAsm {
90        asm: InlineAsm,
91        /// Next block if the control-flow continues without jumping. Absent for `naked_asm!` and `noreturn`.
92        fallthrough: Option<Block>,
93        /// Targets of [`AsmOperand::Label`] operands.
94        labels: IndexVec<BranchId, Block>,
95        /// Action to be taken if the inline assembly unwinds.
96        on_unwind: Block,
97    },
98    Call {
99        call: Call,
100        on_unwind: Block,
101    },
102    Switch {
103        data: SwitchData,
104        branches: IndexVec<BranchId, Block>,
105    },
106
107    Loop(Block),
108    /// Break out of one or more loops.
109    /// The `usize` gives the index of the loop to break from, counting inside-out:
110    /// * 0: break from the innermost loop (the current loop)
111    /// * 1: break from the second innermost loop
112    /// * ...
113    Break(usize),
114    /// Continue to the start of a loop.
115    /// The `usize` gives the index of the loop to continue to, counting inside-out:
116    /// * 0: continue to the start of the innermost loop (the current loop)
117    /// * 1: continue to the start of the second innermost loop
118    /// * ...
119    Continue(usize),
120
121    /// Call to a built-in panicking function. Only if `--reconstruct-panic-calls` is passed.
122    Panic {
123        /// The name of the function that was called.
124        name: Name,
125        on_unwind: Block,
126    },
127    /// Unwinding must stop for ABI reasons or because cleanup code panicked again.
128    UnwindTerminate,
129    /// Unwind out of the current function into its caller.
130    UnwindResume,
131
132    Return,
133    /// Reaching this point is undefined behavior in the Rust abstract machine.
134    UndefinedBehavior,
135    /// No-op.
136    Nop,
137}
138
139/// Ignores statement ids.
140impl PartialEq for Statement {
141    fn eq(&self, other: &Self) -> bool {
142        self.span == other.span
143            && self.kind == other.kind
144            && self.comments_before == other.comments_before
145    }
146}
147
148/// Ignores block ids.
149impl PartialEq for Block {
150    fn eq(&self, other: &Self) -> bool {
151        self.span == other.span && self.statements == other.statements
152    }
153}
154
155impl Block {
156    pub fn new(span: Span, statements: Vec<Statement>) -> Self {
157        Block {
158            span,
159            id: BlockId::fresh(),
160            statements,
161        }
162    }
163
164    pub fn new_unreachable(span: Span) -> Self {
165        Statement::new(span, StatementKind::UndefinedBehavior).into_block()
166    }
167
168    pub fn from_seq(seq: Vec<Statement>) -> Option<Self> {
169        if seq.is_empty() {
170            None
171        } else {
172            let span = seq
173                .iter()
174                .map(|st| st.span)
175                .reduce(|a, b| meta::combine_span(&a, &b))
176                .unwrap();
177            Some(Block::new(span, seq))
178        }
179    }
180
181    pub fn merge(mut self, mut other: Self) -> Self {
182        self.span = meta::combine_span(&self.span, &other.span);
183        self.statements.append(&mut other.statements);
184        self
185    }
186
187    pub fn then(mut self, r: Statement) -> Self {
188        self.span = meta::combine_span(&self.span, &r.span);
189        self.statements.push(r);
190        self
191    }
192
193    pub fn then_opt(self, other: Option<Statement>) -> Self {
194        if let Some(other) = other {
195            self.then(other)
196        } else {
197            self
198        }
199    }
200
201    /// Apply a function to all the statements, in a top-down manner.
202    pub fn visit_statements<F: FnMut(&mut Statement)>(&mut self, f: F) {
203        self.visit_helper(|_| {}, f);
204    }
205
206    /// Apply a transformer to all the statements, in a bottom-up manner. Compared to `transform`,
207    /// this also gives access to the following statements if any. Statements that are not part of
208    /// a sequence will be traversed as `[st]`. Statements that are will be traversed twice: once
209    /// as `[st]`, and then as `[st, ..]` with the following statements if any.
210    ///
211    /// The transformer should:
212    /// - mutate the current statements in place
213    /// - return the sequence of statements to introduce before the current statements
214    pub fn transform_sequences<F: FnMut(&mut [Statement]) -> Vec<Statement>>(&mut self, mut f: F) {
215        self.visit_blocks_bwd(|blk: &mut Block| {
216            let mut final_len = blk.statements.len();
217            let mut to_insert = vec![];
218            for i in (0..blk.statements.len()).rev() {
219                let new_to_insert = f(&mut blk.statements[i..]);
220                final_len += new_to_insert.len();
221                to_insert.push((i, new_to_insert));
222            }
223            if !to_insert.is_empty() {
224                to_insert.sort_by_key(|(i, _)| *i);
225                // Make it so the first element is always at the end so we can pop it.
226                to_insert.reverse();
227                // Construct the merged list of statements.
228                let old_statements =
229                    mem::replace(&mut blk.statements, Vec::with_capacity(final_len));
230                for (i, stmt) in old_statements.into_iter().enumerate() {
231                    while let Some((j, _)) = to_insert.last()
232                        && *j == i
233                    {
234                        let (_, mut stmts) = to_insert.pop().unwrap();
235                        blk.statements.append(&mut stmts);
236                    }
237                    blk.statements.push(stmt);
238                }
239            }
240        })
241    }
242
243    /// Visit `self` and its sub-blocks in a bottom-up (post-order) traversal.
244    pub fn visit_blocks_bwd<F: FnMut(&mut Block)>(&mut self, f: F) {
245        self.visit_helper(f, |_| {});
246    }
247
248    /// Small visitor helper to visit statements and blocks.
249    fn visit_helper<F: FnMut(&mut Block), G: FnMut(&mut Statement)>(
250        &mut self,
251        exit_blk: F,
252        enter_stmt: G,
253    ) {
254        #[derive(Visitor)]
255        pub struct BlockVisitor<F: FnMut(&mut Block), G: FnMut(&mut Statement)> {
256            exit_blk: F,
257            enter_stmt: G,
258        }
259
260        impl<F: FnMut(&mut Block), G: FnMut(&mut Statement)> VisitBodyMut for BlockVisitor<F, G> {
261            fn exit_llbc_block(&mut self, x: &mut Block) {
262                (self.exit_blk)(x)
263            }
264            fn enter_llbc_statement(&mut self, x: &mut Statement) {
265                (self.enter_stmt)(x)
266            }
267        }
268        BlockVisitor {
269            exit_blk,
270            enter_stmt,
271        }
272        .visit_by_val_infallible(self);
273    }
274}
275
276impl BlockId {
277    pub fn fresh() -> BlockId {
278        static COUNTER: AtomicUsize = AtomicUsize::new(0);
279        let id = COUNTER.fetch_add(1, Ordering::Relaxed);
280        BlockId::new(id)
281    }
282}
283
284impl Statement {
285    pub fn new(span: Span, kind: StatementKind) -> Self {
286        Statement {
287            span,
288            id: StatementId::fresh(),
289            kind,
290            comments_before: vec![],
291        }
292    }
293
294    pub fn into_box(self) -> Box<Self> {
295        Box::new(self)
296    }
297
298    pub fn into_block(self) -> Block {
299        Block::new(self.span, vec![self])
300    }
301}
302
303impl StatementId {
304    pub fn fresh() -> StatementId {
305        static COUNTER: AtomicUsize = AtomicUsize::new(0);
306        let id = COUNTER.fetch_add(1, Ordering::Relaxed);
307        StatementId::new(id)
308    }
309}
charon_lib/ast/bodies/structured.rs

charon_lib/ast/bodies/
structured.rs
