charon_lib/transform/control_flow/
prettify_cfg.rs

1use crate::llbc_ast::*;
2use crate::transform::TransformCtx;
3
4use crate::transform::ctx::LlbcPass;
5
6pub struct Transform;
7
8impl Transform {
9    fn update_statements(locals: &Locals, seq: &mut [Statement]) -> Vec<Statement> {
10        // Remove consecutive unconditional errors. This can happen when a function call is
11        // replaced by a panic by `inline_local_panic_functions`.
12        if let [
13            Statement {
14                kind:
15                    StatementKind::Panic { .. }
16                    | StatementKind::UndefinedBehavior
17                    | StatementKind::UnwindTerminate,
18                ..
19            },
20            Statement {
21                kind:
22                    second_abort @ (StatementKind::Panic { .. }
23                    | StatementKind::UndefinedBehavior
24                    | StatementKind::UnwindTerminate),
25                ..
26            },
27            ..,
28        ] = seq
29        {
30            *second_abort = StatementKind::Nop;
31            return Vec::new();
32        }
33        if let [
34            Statement {
35                kind: StatementKind::Call { call, .. },
36                ..
37            },
38            Statement {
39                kind:
40                    second_abort @ (StatementKind::Panic { .. }
41                    | StatementKind::UndefinedBehavior
42                    | StatementKind::UnwindTerminate),
43                ..
44            },
45            ..,
46        ] = seq
47            && let Some(local_id) = call.dest.as_local()
48            && locals[local_id].ty.kind().is_never()
49        {
50            *second_abort = StatementKind::Nop;
51            return Vec::new();
52        }
53
54        Vec::new()
55    }
56}
57
58impl LlbcPass for Transform {
59    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
60        b.body
61            .transform_sequences(|seq| Transform::update_statements(&b.locals, seq))
62    }
63}
charon_lib/transform/control_flow/prettify_cfg.rs

charon_lib/transform/control_flow/
prettify_cfg.rs
