charon_lib/transform/
prettify_cfg.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
use crate::llbc_ast::*;
use crate::transform::TransformCtx;

use super::ctx::LlbcPass;

pub struct Transform;

impl Transform {
    fn update_statements(locals: &Locals, seq: &mut [Statement]) -> Vec<Statement> {
        // Remove double aborts. This can happen when a function call is turned into an `Abort` by
        // `inline_local_panic_functions`.
        if let [Statement {
            content: RawStatement::Abort(_),
            ..
        }, Statement {
            content: second_abort @ RawStatement::Abort(_),
            ..
        }, ..] = seq
        {
            *second_abort = RawStatement::Nop;
            return Vec::new();
        }
        if let [Statement {
            content: RawStatement::Call(call),
            ..
        }, Statement {
            content: second_abort @ RawStatement::Abort(_),
            ..
        }, ..] = seq
            && locals[call.dest.var_id()].ty.kind().is_never()
        {
            *second_abort = RawStatement::Nop;
            return Vec::new();
        }

        Vec::new()
    }
}

impl LlbcPass for Transform {
    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
        b.body
            .transform_sequences(|seq| Transform::update_statements(&b.locals, seq))
    }
}