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

charon_lib/ast/bodies/
unstructured.rs
