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

charon_lib/ast/bodies/
structured.rs
