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

charon_lib/transform/resugar/
move_asserts_to_statements.rs
