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
24                    .statements
25                    .iter()
26                    .all(|st| st.content.is_storage_live())
27                    && let RawTerminator::Abort(abort) = &block.terminator.content
28                {
29                    Some((bid, abort.clone()))
30                } else {
31                    None
32                }
33            })
34            .collect();
35
36        for block in b.body.iter_mut() {
37            match &block.terminator.content {
38                RawTerminator::Switch {
39                    discr: _,
40                    targets: SwitchTargets::If(bid0, bid1),
41                } => {
42                    let (nbid, expected, abort) = if let Some(abort) = panics.get(bid0) {
43                        (*bid1, false, abort)
44                    } else if let Some(abort) = panics.get(bid1) {
45                        (*bid0, true, abort)
46                    } else {
47                        continue;
48                    };
49
50                    let content = std::mem::replace(
51                        &mut block.terminator.content,
52                        RawTerminator::Goto { target: nbid },
53                    );
54                    let (discr, _) = content.as_switch().unwrap();
55                    block.statements.push(Statement::new(
56                        block.terminator.span,
57                        RawStatement::Assert(Assert {
58                            cond: discr.clone(),
59                            expected,
60                            on_failure: abort.clone(),
61                        }),
62                    ));
63                }
64                _ => (),
65            }
66        }
67    }
68}
charon_lib/transform/reconstruct_asserts.rs

charon_lib/transform/
reconstruct_asserts.rs
