charon_lib/transform/resugar/
move_asserts_to_statements.rs

1//! # Micro-pass: if we want to reconstruct fallible operations, the first step
2//! is to move all assert terminators that correspond do dynamic checks into
3//! statements, to make them easier to recognize and transform in the next pass.
4//! It's important this pass runs before [`crate::transform::control_flow::merge_goto_chains`], to
5//! ensure the gotos we substitute the asserts with get merged, but before
6//! [`crate::transform::resugar::reconstruct_fallible_operations`], since it will expect the
7//! asserts to be in statements.
8
9use crate::ast::*;
10use crate::transform::TransformCtx;
11use crate::ullbc_ast::{ExprBody, Statement, StatementKind, TerminatorKind};
12
13use crate::transform::ctx::UllbcPass;
14
15pub struct Transform;
16impl UllbcPass for Transform {
17    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
18        options.reconstruct_fallible_operations
19    }
20
21    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
22        // Start by computing the set of blocks which are actually panics.
23        // Remark: doing this in two steps because reading the blocks at random
24        // while doing in-place updates is not natural to do in Rust.
25        let panics = b.as_abort_map();
26
27        for block in b.body.iter_mut() {
28            let TerminatorKind::Assert {
29                assert:
30                    Assert {
31                        check_kind: Some(_),
32                        ..
33                    },
34                target,
35                ..
36            } = &block.terminator.kind
37            else {
38                continue;
39            };
40
41            let new_terminator = TerminatorKind::Goto { target: *target };
42            let old_terminator = std::mem::replace(&mut block.terminator.kind, new_terminator);
43            let TerminatorKind::Assert {
44                assert, on_unwind, ..
45            } = old_terminator
46            else {
47                unreachable!();
48            };
49
50            let on_failure = panics
51                .get(&on_unwind)
52                .cloned()
53                .unwrap_or(AbortKind::Panic(None));
54
55            block.statements.push(Statement {
56                kind: StatementKind::Assert { assert, on_failure },
57                span: block.terminator.span,
58                comments_before: block.terminator.comments_before.clone(),
59            });
60        }
61    }
62}
charon_lib/transform/resugar/move_asserts_to_statements.rs

charon_lib/transform/resugar/
move_asserts_to_statements.rs
