charon_lib/transform/
remove_drop_never.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
//! The MIR code often contains variables with type `Never`, and we want to get
//! rid of those. We proceed in two steps. First, we remove the instructions
//! `drop(v)` where `v` has type `Never` (it can happen - this module does the
//! filtering). Then, we filter the unused variables ([crate::remove_unused_locals]).

use derive_visitor::{visitor_enter_fn_mut, DriveMut};

use crate::llbc_ast::*;
use crate::transform::TransformCtx;

use super::ctx::LlbcPass;

pub struct Transform;
impl LlbcPass for Transform {
    fn transform_body(&self, _ctx: &mut TransformCtx<'_>, b: &mut ExprBody) {
        let locals = &b.locals;
        b.body
            .drive_mut(&mut visitor_enter_fn_mut(|st: &mut Statement| {
                // Filter the statement by replacing it with `Nop` if it is a `Drop(x)` where
                // `x` has type `Never`. Otherwise leave it unchanged.
                if let RawStatement::Drop(p) = &st.content
                    && p.projection.is_empty()
                    && locals.get(p.var_id).unwrap().ty.kind().is_never()
                {
                    st.content = RawStatement::Nop;
                }
            }));
    }
}