charon_lib/transform/resugar/
reconstruct_asserts.rs

1//! In the MIR AST, it seems `assert` are introduced to check preconditions
2//! (for the binops for example). The `assert!` introduced by the user
3//! introduce `if ... then { panic!(...) } else { ...}`.
4//! This pass introduces `assert` instead in order to make the code shorter.
5
6use crate::transform::TransformCtx;
7use crate::ullbc_ast::*;
8
9use crate::transform::ctx::UllbcPass;
10
11pub struct Transform;
12impl UllbcPass for Transform {
13    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
14        options.reconstruct_asserts
15    }
16
17    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
18        // Start by computing the set of blocks which are actually panics.
19        // Remark: doing this in two steps because reading the blocks at random
20        // while doing in-place updates is not natural to do in Rust.
21        let panics = b.as_abort_map();
22
23        for block in b.body.iter_mut() {
24            if let TerminatorKind::Switch { data, branches } = &block.terminator.kind
25                && let Some((true_id, false_id)) = data.as_if()
26                && let SwitchScrutinee::Value(discr) = data.scrutinee.clone()
27            {
28                let (true_bid, false_bid) = (branches[true_id], branches[false_id]);
29                let (nbid, expected, abort) = if let Some(abort) = panics.get(&true_bid) {
30                    (false_bid, false, abort)
31                } else if let Some(abort) = panics.get(&false_bid) {
32                    (true_bid, true, abort)
33                } else {
34                    continue;
35                };
36
37                let _ = std::mem::replace(
38                    &mut block.terminator.kind,
39                    TerminatorKind::Goto { target: nbid },
40                );
41                block.statements.push(Statement::new(
42                    block.terminator.span,
43                    StatementKind::Assert {
44                        assert: Assert {
45                            cond: discr,
46                            expected,
47                            check_kind: None,
48                        },
49                        on_failure: abort.clone(),
50                    },
51                ));
52            }
53        }
54    }
55}
charon_lib/transform/resugar/reconstruct_asserts.rs

charon_lib/transform/resugar/
reconstruct_asserts.rs
