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

charon_lib/transform/
reconstruct_asserts.rs
