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

charon_lib/ast/bodies/
unstructured.rs
