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            match &block.terminator.kind {
25                TerminatorKind::Switch {
26                    discr: _,
27                    targets: SwitchTargets::If(bid0, bid1),
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        }
57    }
58}
charon_lib/transform/resugar/reconstruct_asserts.rs

charon_lib/transform/resugar/
reconstruct_asserts.rs
