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, VariantIndexArity, VariantName};
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, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
22#[serde_state(state_implements = HashConsSerializerState)] // Avoid corecursive impls due to perfect derive
23pub struct Block {
24    pub span: Span,
25    /// Integer uniquely identifying this block. To simplify things we generate globally-fresh ids
26    /// when creating a new `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, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
34pub struct Statement {
35    pub span: Span,
36    /// Integer uniquely identifying this statement among the statmeents in the current body. To
37    /// simplify things we generate globally-fresh ids when creating a new `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    #[drive(skip)]
44    pub comments_before: Vec<String>,
45}
46
47#[derive(
48    Debug,
49    PartialEq,
50    Eq,
51    Clone,
52    EnumIsA,
53    EnumToGetters,
54    EnumAsGetters,
55    SerializeState,
56    DeserializeState,
57    Drive,
58    DriveMut,
59    DriveTwo,
60)]
61pub enum StatementKind {
62    /// Assigns an `Rvalue` to a `Place`. e.g. `let y = x;` could become
63    /// `y := move x` which is represented as `Assign(y, Rvalue::Use(Operand::Move(x)))`.
64    Assign(Place, Rvalue),
65    /// Not used today because we take MIR built.
66    SetDiscriminant(Place, VariantId),
67    /// Indicates that this local should be allocated; if it is already allocated, this frees
68    /// the local and re-allocates it. The arguments do not receive a `StorageLive`. We ensure in
69    /// the micro-pass `insert_storage_statements` that all other locals have a `StorageLive`
70    /// associated with them.
71    StorageLive(LocalId),
72    /// Deallocates the given local; if it is already deallocated, this is
73    /// a no-op. Not all local deallocations are explicit: if a non-return local is still live at
74    /// function end (return or unwind), it is implicitly deallocated.
75    /// If `--deallocate-all-locals` is set, all local deallocations are made explicit.
76    StorageDead(LocalId),
77    /// A place is mentioned, but not accessed. The place itself must still be valid though, so
78    /// this statement is not a no-op: it can trigger UB if the place's projections are not valid
79    /// (e.g. because they go out of bounds).
80    PlaceMention(Place),
81    /// Statements that only affect borrow-checking.
82    Borrowck(BorrowckStatement),
83    /// Drop the value at the given place.
84    ///
85    /// Depending on `DropKind`, this may be a real call to `drop_glue`, or a conditional call
86    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
87    /// for more details; to get precise drops use `--precise-drops`.
88    Drop {
89        place: Place,
90        /// Reference to the `drop_glue` code to call on drop.
91        fn_ptr: FnPtr,
92        #[drive(skip)]
93        kind: DropKind,
94        on_unwind: Block,
95    },
96    Assert {
97        assert: Assert,
98        on_failure: AbortKind,
99        on_unwind: Block,
100    },
101    /// An inline assembly block. For now we only preserve the template string.
102    InlineAsm {
103        asm: String,
104        targets: Vec<Block>,
105        on_unwind: Block,
106    },
107    Call {
108        call: Call,
109        on_unwind: Block,
110    },
111    /// Panic also handles "unreachable". We keep the name of the panicking function that was
112    /// called.
113    Abort(AbortKind),
114    Return,
115    /// Unwind out of the current function into its caller.
116    UnwindResume,
117    /// Break to outer loops.
118    /// The `usize` gives the index of the outer loop to break to:
119    /// * 0: break to first outer loop (the current loop)
120    /// * 1: break to second outer loop
121    /// * ...
122    #[drive(skip)]
123    Break(usize),
124    /// Continue to outer loops.
125    /// The `usize` gives the index of the outer loop to continue to:
126    /// * 0: continue to first outer loop (the current loop)
127    /// * 1: continue to second outer loop
128    /// * ...
129    #[drive(skip)]
130    Continue(usize),
131    /// No-op.
132    Nop,
133    Switch(Switch),
134    Loop(Block),
135    #[drive(skip)]
136    Error(String),
137}
138
139#[derive(
140    Debug,
141    PartialEq,
142    Eq,
143    Clone,
144    EnumIsA,
145    EnumToGetters,
146    EnumAsGetters,
147    SerializeState,
148    DeserializeState,
149    Drive,
150    DriveMut,
151    DriveTwo,
152    VariantName,
153    VariantIndexArity,
154)]
155pub enum Switch {
156    /// Gives the `if` block and the `else` block. The `Operand` is the condition of the `if`, e.g. `if (y == 0)` could become
157    /// ```text
158    /// v@3 := copy y; // Represented as `Assign(v@3, Use(Copy(y))`
159    /// v@2 := move v@3 == 0; // Represented as `Assign(v@2, BinOp(BinOp::Eq, Move(y), Const(0)))`
160    /// if (move v@2) { // Represented as `If(Move(v@2), <then branch>, <else branch>)`
161    /// ```
162    If(Operand, Block, Block),
163    /// Gives the integer type, a map linking values to switch branches, and the
164    /// otherwise block. Note that matches over enumerations are performed by
165    /// switching over the discriminant, which is an integer.
166    /// Also, we use a `Vec` to make sure the order of the switch
167    /// branches is preserved.
168    ///
169    /// Rk.: we use a vector of values, because some of the branches may
170    /// be grouped together, like for the following code:
171    /// ```text
172    /// match e {
173    ///   E::V1 | E::V2 => ..., // Grouped
174    ///   E::V3 => ...
175    /// }
176    /// ```
177    SwitchInt(Operand, LiteralTy, Vec<(Vec<Literal>, Block)>, Block),
178    /// A match over an ADT.
179    ///
180    /// The match statement is introduced in [crate::transform::resugar::reconstruct_matches]
181    /// (whenever we find a discriminant read, we merge it with the subsequent
182    /// switch into a match).
183    Match(Place, Vec<(Vec<VariantId>, Block)>, Option<Block>),
184}
185
186/// Ignores statement ids.
187impl PartialEq for Statement {
188    fn eq(&self, other: &Self) -> bool {
189        self.span == other.span
190            && self.kind == other.kind
191            && self.comments_before == other.comments_before
192    }
193}
194
195/// Ignores block ids.
196impl PartialEq for Block {
197    fn eq(&self, other: &Self) -> bool {
198        self.span == other.span && self.statements == other.statements
199    }
200}
201
202impl Block {
203    pub fn new(span: Span, statements: Vec<Statement>) -> Self {
204        Block {
205            span,
206            id: BlockId::fresh(),
207            statements,
208        }
209    }
210
211    pub fn new_abort(span: Span, kind: AbortKind) -> Self {
212        Statement::new(span, StatementKind::Abort(kind)).into_block()
213    }
214
215    pub fn new_unreachable(span: Span) -> Self {
216        Self::new_abort(span, AbortKind::UndefinedBehavior)
217    }
218
219    pub fn from_seq(seq: Vec<Statement>) -> Option<Self> {
220        if seq.is_empty() {
221            None
222        } else {
223            let span = seq
224                .iter()
225                .map(|st| st.span)
226                .reduce(|a, b| meta::combine_span(&a, &b))
227                .unwrap();
228            Some(Block::new(span, seq))
229        }
230    }
231
232    pub fn merge(mut self, mut other: Self) -> Self {
233        self.span = meta::combine_span(&self.span, &other.span);
234        self.statements.append(&mut other.statements);
235        self
236    }
237
238    pub fn then(mut self, r: Statement) -> Self {
239        self.span = meta::combine_span(&self.span, &r.span);
240        self.statements.push(r);
241        self
242    }
243
244    pub fn then_opt(self, other: Option<Statement>) -> Self {
245        if let Some(other) = other {
246            self.then(other)
247        } else {
248            self
249        }
250    }
251
252    /// Apply a function to all the statements, in a top-down manner.
253    pub fn visit_statements<F: FnMut(&mut Statement)>(&mut self, f: F) {
254        self.visit_helper(|_| {}, f);
255    }
256
257    /// Apply a transformer to all the statements, in a bottom-up manner. Compared to `transform`,
258    /// this also gives access to the following statements if any. Statements that are not part of
259    /// a sequence will be traversed as `[st]`. Statements that are will be traversed twice: once
260    /// as `[st]`, and then as `[st, ..]` with the following statements if any.
261    ///
262    /// The transformer should:
263    /// - mutate the current statements in place
264    /// - return the sequence of statements to introduce before the current statements
265    pub fn transform_sequences<F: FnMut(&mut [Statement]) -> Vec<Statement>>(&mut self, mut f: F) {
266        self.visit_blocks_bwd(|blk: &mut Block| {
267            let mut final_len = blk.statements.len();
268            let mut to_insert = vec![];
269            for i in (0..blk.statements.len()).rev() {
270                let new_to_insert = f(&mut blk.statements[i..]);
271                final_len += new_to_insert.len();
272                to_insert.push((i, new_to_insert));
273            }
274            if !to_insert.is_empty() {
275                to_insert.sort_by_key(|(i, _)| *i);
276                // Make it so the first element is always at the end so we can pop it.
277                to_insert.reverse();
278                // Construct the merged list of statements.
279                let old_statements =
280                    mem::replace(&mut blk.statements, Vec::with_capacity(final_len));
281                for (i, stmt) in old_statements.into_iter().enumerate() {
282                    while let Some((j, _)) = to_insert.last()
283                        && *j == i
284                    {
285                        let (_, mut stmts) = to_insert.pop().unwrap();
286                        blk.statements.append(&mut stmts);
287                    }
288                    blk.statements.push(stmt);
289                }
290            }
291        })
292    }
293
294    /// Visit `self` and its sub-blocks in a bottom-up (post-order) traversal.
295    pub fn visit_blocks_bwd<F: FnMut(&mut Block)>(&mut self, f: F) {
296        self.visit_helper(f, |_| {});
297    }
298
299    /// Small visitor helper to visit statements and blocks.
300    fn visit_helper<F: FnMut(&mut Block), G: FnMut(&mut Statement)>(
301        &mut self,
302        exit_blk: F,
303        enter_stmt: G,
304    ) {
305        #[derive(Visitor)]
306        pub struct BlockVisitor<F: FnMut(&mut Block), G: FnMut(&mut Statement)> {
307            exit_blk: F,
308            enter_stmt: G,
309        }
310
311        impl<F: FnMut(&mut Block), G: FnMut(&mut Statement)> VisitBodyMut for BlockVisitor<F, G> {
312            fn exit_llbc_block(&mut self, x: &mut Block) {
313                (self.exit_blk)(x)
314            }
315            fn enter_llbc_statement(&mut self, x: &mut Statement) {
316                (self.enter_stmt)(x)
317            }
318        }
319        BlockVisitor {
320            exit_blk,
321            enter_stmt,
322        }
323        .visit_by_val_infallible(self);
324    }
325}
326
327impl BlockId {
328    pub fn fresh() -> BlockId {
329        static COUNTER: AtomicUsize = AtomicUsize::new(0);
330        let id = COUNTER.fetch_add(1, Ordering::Relaxed);
331        BlockId::new(id)
332    }
333}
334
335impl Statement {
336    pub fn new(span: Span, kind: StatementKind) -> Self {
337        Statement {
338            span,
339            id: StatementId::fresh(),
340            kind,
341            comments_before: vec![],
342        }
343    }
344
345    pub fn into_box(self) -> Box<Self> {
346        Box::new(self)
347    }
348
349    pub fn into_block(self) -> Block {
350        Block::new(self.span, vec![self])
351    }
352}
353
354impl StatementId {
355    pub fn fresh() -> StatementId {
356        static COUNTER: AtomicUsize = AtomicUsize::new(0);
357        let id = COUNTER.fetch_add(1, Ordering::Relaxed);
358        StatementId::new(id)
359    }
360}
361
362impl Switch {
363    pub fn iter_targets(&self) -> impl Iterator<Item = &Block> {
364        use itertools::Either;
365        match self {
366            Switch::If(_, exp1, exp2) => Either::Left([exp1, exp2].into_iter()),
367            Switch::SwitchInt(_, _, targets, otherwise) => Either::Right(Either::Left(
368                targets.iter().map(|(_, tgt)| tgt).chain([otherwise]),
369            )),
370            Switch::Match(_, targets, otherwise) => Either::Right(Either::Right(
371                targets.iter().map(|(_, tgt)| tgt).chain(otherwise.as_ref()),
372            )),
373        }
374    }
375
376    pub fn iter_targets_mut(&mut self) -> impl Iterator<Item = &mut Block> {
377        use itertools::Either;
378        match self {
379            Switch::If(_, exp1, exp2) => Either::Left([exp1, exp2].into_iter()),
380            Switch::SwitchInt(_, _, targets, otherwise) => Either::Right(Either::Left(
381                targets.iter_mut().map(|(_, tgt)| tgt).chain([otherwise]),
382            )),
383            Switch::Match(_, targets, otherwise) => Either::Right(Either::Right(
384                targets
385                    .iter_mut()
386                    .map(|(_, tgt)| tgt)
387                    .chain(otherwise.as_mut()),
388            )),
389        }
390    }
391
392    /// Combine the span information from a [Switch]
393    pub fn combine_targets_span(&self) -> Span {
394        match self {
395            Switch::If(_, st1, st2) => meta::combine_span(&st1.span, &st2.span),
396            Switch::SwitchInt(_, _, branches, otherwise) => {
397                let branches = branches.iter().map(|b| &b.1.span);
398                let mbranches = meta::combine_span_iter(branches);
399                meta::combine_span(&mbranches, &otherwise.span)
400            }
401            Switch::Match(_, branches, otherwise) => {
402                let branches = branches.iter().map(|b| &b.1.span);
403                let mbranches = meta::combine_span_iter(branches);
404                if let Some(otherwise) = otherwise {
405                    meta::combine_span(&mbranches, &otherwise.span)
406                } else {
407                    mbranches
408                }
409            }
410        }
411    }
412}
charon_lib/ast/bodies/structured.rs

charon_lib/ast/bodies/
structured.rs
