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::FusedUllbcPass;
10
11pub struct Transform;
12impl FusedUllbcPass 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 {
25                discr: _,
26                targets: SwitchTargets::If(bid0, bid1),
27            } = &block.terminator.kind
28            {
29                let (nbid, expected, abort) = if let Some(abort) = panics.get(bid0) {
30                    (*bid1, false, abort)
31                } else if let Some(abort) = panics.get(bid1) {
32                    (*bid0, true, abort)
33                } else {
34                    continue;
35                };
36
37                let kind = std::mem::replace(
38                    &mut block.terminator.kind,
39                    TerminatorKind::Goto { target: nbid },
40                );
41                let (discr, _) = kind.as_switch().unwrap();
42                block.statements.push(Statement::new(
43                    block.terminator.span,
44                    StatementKind::Assert {
45                        assert: Assert {
46                            cond: discr.clone(),
47                            expected,
48                            check_kind: None,
49                        },
50                        on_failure: abort.clone(),
51                    },
52                ));
53            }
54        }
55    }
56}
charon_lib/transform/resugar/reconstruct_asserts.rs

charon_lib/transform/resugar/
reconstruct_asserts.rs
