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 std::collections::HashMap;
7
8use crate::transform::TransformCtx;
9use crate::ullbc_ast::*;
10
11use crate::transform::ctx::UllbcPass;
12
13pub struct Transform;
14impl UllbcPass for Transform {
15    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
16        options.reconstruct_asserts
17    }
18
19    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
20        // Start by computing the set of blocks which are actually panics.
21        // Remark: doing this in two steps because reading the blocks at random
22        // while doing in-place updates is not natural to do in Rust.
23        let panics: HashMap<BlockId, AbortKind> = b
24            .body
25            .iter_indexed()
26            .filter_map(|(bid, block)| {
27                if block.statements.iter().all(|st| st.kind.is_storage_live())
28                    && let TerminatorKind::Abort(abort) = &block.terminator.kind
29                {
30                    Some((bid, abort.clone()))
31                } else {
32                    None
33                }
34            })
35            .collect();
36
37        for block in b.body.iter_mut() {
38            match &block.terminator.kind {
39                TerminatorKind::Switch {
40                    discr: _,
41                    targets: SwitchTargets::If(bid0, bid1),
42                } => {
43                    let (nbid, expected, abort) = if let Some(abort) = panics.get(bid0) {
44                        (*bid1, false, abort)
45                    } else if let Some(abort) = panics.get(bid1) {
46                        (*bid0, true, abort)
47                    } else {
48                        continue;
49                    };
50
51                    let kind = std::mem::replace(
52                        &mut block.terminator.kind,
53                        TerminatorKind::Goto { target: nbid },
54                    );
55                    let (discr, _) = kind.as_switch().unwrap();
56                    block.statements.push(Statement::new(
57                        block.terminator.span,
58                        StatementKind::Assert(Assert {
59                            cond: discr.clone(),
60                            expected,
61                            on_failure: abort.clone(),
62                        }),
63                    ));
64                }
65                _ => (),
66            }
67        }
68    }
69}
charon_lib/transform/resugar/reconstruct_asserts.rs

charon_lib/transform/resugar/
reconstruct_asserts.rs
