charon_lib/ast/bodies/
unstructured.rs

1//! Bodies with unstructured control-flow, i.e. with a control-flow graph and GOTOs.
2//!
3//! In effect, this is a cleaned up version of MIR.
4use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
5use macros::{EnumAsGetters, EnumIsA, VariantName};
6use serde_state::{DeserializeState, SerializeState};
7use smallvec::{SmallVec, smallvec};
8use std::collections::HashMap;
9use std::mem;
10use std::ops::{Index, IndexMut};
11
12use crate::ast::*;
13
14// Block identifier. Similar to rust's `BasicBlock`.
15generate_index_type!(BlockId, "Block");
16
17// The entry block of a function is always the block with id 0
18pub static START_BLOCK_ID: BlockId = BlockId::ZERO;
19
20#[cfg_attr(feature = "charon_on_charon", charon::rename("Blocks"))]
21pub type BodyContents = IndexVec<BlockId, BlockData>;
22pub type ExprBody = GExprBody<BodyContents>;
23
24/// A "basic block", which contains a linear sequence of statements, followed by a terminator, which
25/// is where non-linear control-flow happens.
26#[derive(
27    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
28)]
29#[cfg_attr(feature = "charon_on_charon", charon::rename("Block"))]
30pub struct BlockData {
31    pub statements: Vec<Statement>,
32    pub terminator: Terminator,
33}
34
35/// A statement.
36#[derive(
37    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
38)]
39pub struct Statement {
40    pub span: Span,
41    pub kind: StatementKind,
42    /// Comments that precede this statement.
43    // This is filled in a late pass after all the control-flow manipulation.
44    pub comments_before: Vec<String>,
45}
46
47#[derive(
48    Debug,
49    PartialEq,
50    Eq,
51    Clone,
52    EnumIsA,
53    EnumAsGetters,
54    VariantName,
55    SerializeState,
56    DeserializeState,
57    Drive,
58    DriveMut,
59    DriveTwo,
60)]
61pub enum StatementKind {
62    Assign(Place, Rvalue),
63    /// A call. For now, we don't support dynamic calls (i.e. to a function pointer in memory).
64    SetDiscriminant(Place, VariantId),
65    /// Indicates that this local should be allocated; if it is already allocated, this frees
66    /// the local and re-allocates it. The arguments do not receive a `StorageLive`. We ensure in
67    /// the micro-pass `insert_storage_statements` that all other locals have a `StorageLive`
68    /// associated with them.
69    StorageLive(LocalId),
70    /// Deallocates the given local; if it is already deallocated, this is
71    /// a no-op. Not all local deallocations are explicit: if a non-return local is still live at
72    /// function end (return or unwind), it is implicitly deallocated.
73    /// If `--deallocate-all-locals` is set, all local deallocations are made explicit.
74    StorageDead(LocalId),
75    /// A place is mentioned, but not accessed. The place itself must still be valid though, so
76    /// this statement is not a no-op: it can trigger UB if the place's projections are not valid
77    /// (e.g. because they go out of bounds).
78    PlaceMention(Place),
79    /// Statements that only affect borrow-checking.
80    Borrowck(BorrowckStatement),
81    /// A non-diverging runtime check for a condition. This can be either:
82    /// - Emitted for inlined "assumes" (which cause UB on failure)
83    /// - Reconstructed from `if b { panic() }` if `--reconstruct-asserts` is set.
84    ///
85    /// This statement comes with the effect that happens when the check fails
86    /// (rather than representing it as an unwinding edge).
87    Assert {
88        assert: Assert,
89        on_failure: AbortKind,
90    },
91    /// Does nothing. Useful for passes.
92    Nop,
93}
94
95#[derive(
96    Debug,
97    PartialEq,
98    Eq,
99    Clone,
100    EnumIsA,
101    EnumAsGetters,
102    SerializeState,
103    DeserializeState,
104    Drive,
105    DriveMut,
106    DriveTwo,
107)]
108pub enum TerminatorKind {
109    Goto {
110        target: BlockId,
111    },
112    Switch {
113        data: SwitchData,
114        branches: IndexVec<BranchId, BlockId>,
115    },
116    Call {
117        call: Call,
118        target: BlockId,
119        on_unwind: BlockId,
120    },
121    /// Drop the value at the given place.
122    ///
123    /// Depending on `DropKind`, this may be a real call to `drop_glue`, or a conditional call
124    /// that should only happen if the place has not been moved out of. See the docs of `DropKind`
125    /// for more details; to get precise drops use `--precise-drops`.
126    Drop {
127        kind: DropKind,
128        place: Place,
129        /// Reference to the `drop_glue` code to call on drop.
130        fn_ptr: FnPtr,
131        target: BlockId,
132        on_unwind: BlockId,
133    },
134    /// Assert that the given condition holds, and if not, unwind to the given block. This is used for
135    /// bounds checks, overflow checks, etc.
136    #[cfg_attr(feature = "charon_on_charon", charon::rename("TAssert"))]
137    Assert {
138        assert: Assert,
139        target: BlockId,
140        on_unwind: BlockId,
141    },
142    /// An inline assembly block. For now we only preserve the template string.
143    InlineAsm {
144        asm: String,
145        targets: Vec<BlockId>,
146        on_unwind: BlockId,
147    },
148    /// Handles panics and impossible cases.
149    Abort(AbortKind),
150    Return,
151    /// Unwind out of the current function into its caller.
152    UnwindResume,
153}
154
155/// A terminator: instruction to execute at the end of a block, which may jump to other blocks.
156#[derive(
157    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
158)]
159pub struct Terminator {
160    pub span: Span,
161    pub kind: TerminatorKind,
162    /// Comments that precede this terminator.
163    // This is filled in a late pass after all the control-flow manipulation.
164    pub comments_before: Vec<String>,
165}
166
167impl ExprBody {
168    /// Returns a map from blocks in this body to their abort kind, if they correspond to an
169    /// abort block (ie. a block with only bookkeeping statements and a
170    /// [TerminatorKind::Abort] terminator).
171    pub fn as_abort_map(&self) -> HashMap<BlockId, AbortKind> {
172        self.body
173            .iter_enumerated()
174            .filter_map(|(bid, block)| block.as_abort().map(|abort| (bid, abort)))
175            .collect()
176    }
177
178    pub fn transform_sequences_fwd<F>(&mut self, mut f: F)
179    where
180        F: FnMut(BlockId, &mut Locals, &mut [Statement]) -> Vec<(usize, Vec<Statement>)>,
181    {
182        for (id, block) in &mut self.body.iter_mut_enumerated() {
183            block.transform_sequences_fwd(|seq| f(id, &mut self.locals, seq));
184        }
185    }
186
187    pub fn transform_sequences_bwd<F>(&mut self, mut f: F)
188    where
189        F: FnMut(&mut Locals, &mut [Statement]) -> Vec<(usize, Vec<Statement>)>,
190    {
191        for block in &mut self.body {
192            block.transform_sequences_bwd(|seq| f(&mut self.locals, seq));
193        }
194    }
195
196    /// Apply a function to all the statements, in a bottom-up manner.
197    pub fn visit_statements<F: FnMut(&mut Statement)>(&mut self, mut f: F) {
198        for block in self.body.iter_mut().rev() {
199            for st in block.statements.iter_mut().rev() {
200                f(st);
201            }
202        }
203    }
204}
205
206impl BlockData {
207    /// Build a block that's just a goto terminator.
208    pub fn new_goto(span: Span, target: BlockId) -> Self {
209        BlockData {
210            statements: vec![],
211            terminator: Terminator::goto(span, target),
212        }
213    }
214    pub fn as_goto(&self) -> Option<BlockId> {
215        if let TerminatorKind::Goto { target } = self.terminator.kind {
216            Some(target)
217        } else {
218            None
219        }
220    }
221    pub fn as_trivial_goto(&self) -> Option<BlockId> {
222        self.as_goto().filter(|_| {
223            self.statements
224                .iter()
225                .all(|st| matches!(st.kind, StatementKind::Nop))
226        })
227    }
228
229    pub fn as_abort(&self) -> Option<AbortKind> {
230        if self.statements.iter().all(|st| {
231            matches!(
232                st.kind,
233                StatementKind::Nop | StatementKind::StorageLive(_) | StatementKind::StorageDead(_)
234            )
235        }) && let TerminatorKind::Abort(abort) = &self.terminator.kind
236        {
237            Some(abort.clone())
238        } else {
239            None
240        }
241    }
242
243    /// Build a block that's UB to reach.
244    pub fn new_unreachable() -> Self {
245        Terminator::new(
246            Span::dummy(),
247            TerminatorKind::Abort(AbortKind::UndefinedBehavior),
248        )
249        .into_block()
250    }
251
252    pub fn targets(&self) -> SmallVec<[BlockId; 2]> {
253        self.terminator.targets()
254    }
255    pub fn targets_ignoring_unwind(&self) -> SmallVec<[BlockId; 2]> {
256        self.terminator.targets_ignoring_unwind()
257    }
258
259    /// Apply a transformer to all the statements.
260    ///
261    /// The transformer should:
262    /// - mutate the current statement in place
263    /// - return the sequence of statements to introduce before the current statement
264    pub fn transform<F: FnMut(&mut Statement) -> Vec<Statement>>(&mut self, mut f: F) {
265        self.transform_sequences_fwd(|slice| {
266            let new_statements = f(&mut slice[0]);
267            if new_statements.is_empty() {
268                vec![]
269            } else {
270                vec![(0, new_statements)]
271            }
272        });
273    }
274
275    /// Helper, see `transform_sequences_fwd` and `transform_sequences_bwd`.
276    fn transform_sequences<F>(&mut self, mut f: F, forward: bool)
277    where
278        F: FnMut(&mut [Statement]) -> Vec<(usize, Vec<Statement>)>,
279    {
280        let mut to_insert = vec![];
281        let mut final_len = self.statements.len();
282        if forward {
283            for i in 0..self.statements.len() {
284                let new_to_insert = f(&mut self.statements[i..]);
285                to_insert.extend(new_to_insert.into_iter().map(|(j, stmts)| {
286                    final_len += stmts.len();
287                    (i + j, stmts)
288                }));
289            }
290        } else {
291            for i in (0..self.statements.len()).rev() {
292                let new_to_insert = f(&mut self.statements[i..]);
293                to_insert.extend(new_to_insert.into_iter().map(|(j, stmts)| {
294                    final_len += stmts.len();
295                    (i + j, stmts)
296                }));
297            }
298        }
299        if !to_insert.is_empty() {
300            to_insert.sort_by_key(|(i, _)| *i);
301            // Make it so the first element is always at the end so we can pop it.
302            to_insert.reverse();
303            // Construct the merged list of statements.
304            let old_statements = mem::replace(&mut self.statements, Vec::with_capacity(final_len));
305            for (i, stmt) in old_statements.into_iter().enumerate() {
306                while let Some((j, _)) = to_insert.last()
307                    && *j == i
308                {
309                    let (_, mut stmts) = to_insert.pop().unwrap();
310                    self.statements.append(&mut stmts);
311                }
312                self.statements.push(stmt);
313            }
314        }
315    }
316
317    /// Apply a transformer to all the statements.
318    ///
319    /// The transformer should:
320    /// - mutate the current statements in place
321    /// - return a list of `(i, statements)` where `statements` will be inserted before index `i`.
322    pub fn transform_sequences_fwd<F>(&mut self, f: F)
323    where
324        F: FnMut(&mut [Statement]) -> Vec<(usize, Vec<Statement>)>,
325    {
326        self.transform_sequences(f, true);
327    }
328
329    /// Apply a transformer to all the statements.
330    ///
331    /// The transformer should:
332    /// - mutate the current statements in place
333    /// - return a list of `(i, statements)` where `statements` will be inserted before index `i`.
334    pub fn transform_sequences_bwd<F>(&mut self, f: F)
335    where
336        F: FnMut(&mut [Statement]) -> Vec<(usize, Vec<Statement>)>,
337    {
338        self.transform_sequences(f, false);
339    }
340}
341
342impl Statement {
343    pub fn new(span: Span, kind: StatementKind) -> Self {
344        Statement {
345            span,
346            kind,
347            comments_before: vec![],
348        }
349    }
350}
351
352impl Terminator {
353    pub fn new(span: Span, kind: TerminatorKind) -> Self {
354        Terminator {
355            span,
356            kind,
357            comments_before: vec![],
358        }
359    }
360    pub fn goto(span: Span, target: BlockId) -> Self {
361        Self::new(span, TerminatorKind::Goto { target })
362    }
363    /// Whether this terminator is an unconditional error (panic).
364    pub fn is_error(&self) -> bool {
365        use TerminatorKind::*;
366        match &self.kind {
367            Abort(..) => true,
368            Goto { .. }
369            | Switch { .. }
370            | InlineAsm { .. }
371            | Return
372            | Call { .. }
373            | Drop { .. }
374            | UnwindResume
375            | Assert { .. } => false,
376        }
377    }
378
379    pub fn into_block(self) -> BlockData {
380        BlockData {
381            statements: vec![],
382            terminator: self,
383        }
384    }
385
386    pub fn targets(&self) -> SmallVec<[BlockId; 2]> {
387        match &self.kind {
388            TerminatorKind::Goto { target } => {
389                smallvec![*target]
390            }
391            TerminatorKind::Switch { branches, .. } => branches.iter().copied().collect(),
392            TerminatorKind::InlineAsm {
393                targets, on_unwind, ..
394            } => targets.iter().copied().chain([*on_unwind]).collect(),
395            TerminatorKind::Call {
396                target, on_unwind, ..
397            }
398            | TerminatorKind::Drop {
399                target, on_unwind, ..
400            }
401            | TerminatorKind::Assert {
402                target, on_unwind, ..
403            } => smallvec![*target, *on_unwind],
404            TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => {
405                smallvec![]
406            }
407        }
408    }
409    pub fn targets_mut(&mut self) -> SmallVec<[&mut BlockId; 2]> {
410        match &mut self.kind {
411            TerminatorKind::Goto { target } => {
412                smallvec![target]
413            }
414            TerminatorKind::Switch { branches, .. } => branches.iter_mut().collect(),
415            TerminatorKind::InlineAsm {
416                targets, on_unwind, ..
417            } => targets.iter_mut().chain([on_unwind]).collect(),
418            TerminatorKind::Call {
419                target, on_unwind, ..
420            }
421            | TerminatorKind::Drop {
422                target, on_unwind, ..
423            }
424            | TerminatorKind::Assert {
425                target, on_unwind, ..
426            } => smallvec![target, on_unwind],
427            TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => {
428                smallvec![]
429            }
430        }
431    }
432
433    pub fn targets_ignoring_unwind(&self) -> SmallVec<[BlockId; 2]> {
434        match &self.kind {
435            TerminatorKind::Goto { target } => {
436                smallvec![*target]
437            }
438            TerminatorKind::Switch { branches, .. } => branches.iter().copied().collect(),
439            TerminatorKind::InlineAsm { targets, .. } => targets.iter().copied().collect(),
440            TerminatorKind::Call { target, .. }
441            | TerminatorKind::Drop { target, .. }
442            | TerminatorKind::Assert { target, .. } => {
443                smallvec![*target]
444            }
445            TerminatorKind::Abort(..) | TerminatorKind::Return | TerminatorKind::UnwindResume => {
446                smallvec![]
447            }
448        }
449    }
450}
451
452/// A statement location within a body.
453#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
454pub struct StmtLoc {
455    pub block: BlockId,
456    pub statement: usize,
457}
458
459impl StmtLoc {
460    pub fn new(block: BlockId, statement: usize) -> Self {
461        StmtLoc { block, statement }
462    }
463
464    pub fn block_start(block: BlockId) -> Self {
465        StmtLoc {
466            block,
467            statement: 0,
468        }
469    }
470
471    pub fn after(self) -> Self {
472        StmtLoc {
473            block: self.block,
474            statement: self.statement + 1,
475        }
476    }
477}
478
479impl Index<StmtLoc> for ExprBody {
480    type Output = Statement;
481    fn index(&self, loc: StmtLoc) -> &Self::Output {
482        &self.body[loc.block].statements[loc.statement]
483    }
484}
485
486impl IndexMut<StmtLoc> for ExprBody {
487    fn index_mut(&mut self, loc: StmtLoc) -> &mut Self::Output {
488        &mut self.body[loc.block].statements[loc.statement]
489    }
490}
491
492/// Helper to construct a small ullbc body.
493pub struct BodyBuilder {
494    /// The span to use for everything.
495    pub span: Span,
496    /// Body under construction.
497    pub body: ExprBody,
498    /// Block onto which we're adding statements. Its terminator is always `Return`.
499    pub current_block: BlockId,
500    /// Block to unwind to; created on demand.
501    pub unwind_block: Option<BlockId>,
502}
503
504fn mk_block(span: Span, term: TerminatorKind) -> BlockData {
505    BlockData {
506        statements: vec![],
507        terminator: Terminator::new(span, term),
508    }
509}
510
511impl BodyBuilder {
512    pub fn new(span: Span, arg_count: usize) -> Self {
513        let mut body: ExprBody = GExprBody {
514            span,
515            locals: Locals::new(arg_count),
516            bound_body_regions: 0,
517            body: IndexVec::new(),
518            comments: vec![],
519        };
520        let current_block = body.body.push(BlockData {
521            statements: Default::default(),
522            terminator: Terminator::new(span, TerminatorKind::Return),
523        });
524        Self {
525            span,
526            body,
527            current_block,
528            unwind_block: None,
529        }
530    }
531
532    /// Finalize the builder by returning the built body.
533    pub fn build(mut self) -> ExprBody {
534        // Replace erased regions with fresh ones.
535        let mut freshener: IndexMap<RegionId, ()> = IndexMap::new();
536        self.body.dyn_visit_mut(|r: &mut Region| {
537            if r.is_erased() || r.is_body() {
538                *r = Region::Body(freshener.push(()));
539            }
540        });
541        self.body.bound_body_regions = freshener.slot_count();
542        // Return the built body.
543        self.body
544    }
545
546    /// Create a new local. Adds a `StorageLive` statement if the local is not one of the special
547    /// ones (return or function argument).
548    pub fn new_var(&mut self, name: Option<String>, ty: Ty) -> Place {
549        let place = self.body.locals.new_var(name, ty);
550        let local_id = place.as_local().unwrap();
551        if !self.body.locals.is_return_or_arg(local_id) {
552            self.push_statement(StatementKind::StorageLive(local_id));
553        }
554        place
555    }
556
557    /// Helper.
558    fn current_block(&mut self) -> &mut BlockData {
559        &mut self.body.body[self.current_block]
560    }
561
562    pub fn push_statement(&mut self, kind: StatementKind) {
563        let st = Statement::new(self.span, kind);
564        self.current_block().statements.push(st);
565    }
566
567    fn unwind_block(&mut self) -> BlockId {
568        *self.unwind_block.get_or_insert_with(|| {
569            self.body
570                .body
571                .push(mk_block(self.span, TerminatorKind::UnwindResume))
572        })
573    }
574
575    pub fn call(&mut self, call: Call) {
576        let next_block = self
577            .body
578            .body
579            .push(mk_block(self.span, TerminatorKind::Return));
580        let term = TerminatorKind::Call {
581            target: next_block,
582            call,
583            on_unwind: self.unwind_block(),
584        };
585        self.current_block().terminator.kind = term;
586        self.current_block = next_block;
587    }
588
589    pub fn insert_drop(&mut self, place: Place, fn_ptr: FnPtr) {
590        let next_block = self
591            .body
592            .body
593            .push(mk_block(self.span, TerminatorKind::Return));
594        let term = TerminatorKind::Drop {
595            kind: DropKind::Precise,
596            place,
597            fn_ptr,
598            target: next_block,
599            on_unwind: self.unwind_block(),
600        };
601        self.current_block().terminator.kind = term;
602        self.current_block = next_block;
603    }
604}
charon_lib/ast/bodies/unstructured.rs

charon_lib/ast/bodies/
unstructured.rs
