charon_lib/transform/remove_read_discriminant.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 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
//! 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 crate::errors::register_error;
use crate::formatter::IntoFormatter;
use crate::llbc_ast::*;
use crate::name_matcher::NamePattern;
use crate::pretty::FmtWithCtx;
use crate::transform::TransformCtx;
use itertools::Itertools;
use std::collections::{HashMap, HashSet};
use super::ctx::LlbcPass;
/// Generate `match _y { 0 => { _x = 0 }, 1 => { _x = 1; }, .. }`.
fn generate_discr_assignment(
span: Span,
variants: &Vector<VariantId, Variant>,
scrutinee: &Place,
dest: &Place,
) -> RawStatement {
let targets = variants
.iter_indexed_values()
.map(|(id, variant)| {
let discr_value = Rvalue::Use(Operand::Const(variant.discriminant.to_constant()));
let statement = Statement::new(span, RawStatement::Assign(dest.clone(), discr_value));
(vec![id], statement.into_block())
})
.collect();
RawStatement::Switch(Switch::Match(scrutinee.clone(), targets, None))
}
pub struct Transform;
impl Transform {
fn update_block(
ctx: &mut TransformCtx,
block: &mut Block,
discriminant_intrinsic: Option<FunDeclId>,
) {
// Iterate through the statements.
for i in 0..block.statements.len() {
let suffix = &mut block.statements[i..];
match suffix {
[Statement {
content: RawStatement::Assign(dest, Rvalue::Discriminant(p, adt_id)),
span: span1,
..
}, rest @ ..] => {
// The destination should be a variable
assert!(dest.is_local());
// Lookup the type of the scrutinee
let tkind = ctx.translated.type_decls.get(*adt_id).map(|x| &x.kind);
let Some(TypeDeclKind::Enum(variants)) = tkind else {
match tkind {
// This can happen if the type was declared as invisible or opaque.
None | Some(TypeDeclKind::Opaque) => {
let name = ctx.translated.item_name(*adt_id).unwrap();
register_error!(
ctx,
block.span,
"reading the discriminant of an opaque enum. \
Add `--include {}` to the `charon` arguments \
to translate this enum.",
name.fmt_with_ctx(&ctx.into_fmt())
);
}
// Don't double-error
Some(TypeDeclKind::Error(..)) => {}
Some(_) => {
register_error!(
ctx,
block.span,
"reading the discriminant of a non-enum type"
);
}
}
block.statements[i].content = RawStatement::Error(
"error reading the discriminant of this type".to_owned(),
);
return;
};
// We look for a `SwitchInt` just after the discriminant read.
match rest {
[Statement {
content:
RawStatement::Switch(switch @ Switch::SwitchInt(Operand::Move(_), ..)),
..
}, ..] => {
// Convert between discriminants and variant indices. Remark: the discriminant can
// be of any *signed* integer type (`isize`, `i8`, etc.).
let discr_to_id: HashMap<ScalarValue, VariantId> = variants
.iter_indexed_values()
.map(|(id, variant)| (variant.discriminant, id))
.collect();
take_mut::take(switch, |switch| {
let (Operand::Move(op_p), _, targets, otherwise) =
switch.to_switch_int().unwrap()
else {
unreachable!()
};
assert!(op_p.is_local() && op_p.var_id() == dest.var_id());
let mut covered_discriminants: HashSet<ScalarValue> =
HashSet::default();
let targets = targets
.into_iter()
.map(|(v, e)| {
let targets = v
.into_iter()
.filter_map(|discr| {
covered_discriminants.insert(discr);
discr_to_id.get(&discr).or_else(|| {
register_error!(
ctx,
block.span,
"Found incorrect discriminant \
{discr} for enum {adt_id}"
);
None
})
})
.copied()
.collect_vec();
(targets, e)
})
.collect_vec();
// Filter the otherwise branch if it is not necessary.
let covers_all = covered_discriminants.len() == discr_to_id.len();
let otherwise = if covers_all { None } else { Some(otherwise) };
// Replace the old switch with a match.
Switch::Match(p.clone(), targets, otherwise)
});
// `Nop` the discriminant read.
block.statements[i].content = RawStatement::Nop;
}
_ => {
// The discriminant read is not followed by a `SwitchInt`. This can happen
// in optimized MIR. We replace `_x = Discr(_y)` with `match _y { 0 => { _x
// = 0 }, 1 => { _x = 1; }, .. }`.
block.statements[i].content =
generate_discr_assignment(*span1, variants, p, dest)
}
}
}
// Replace calls of `core::intrinsics::discriminant_value` on a known enum with the
// appropriate MIR.
[Statement {
content: RawStatement::Call(call),
span: span1,
..
}, ..]
if let Some(discriminant_intrinsic) = discriminant_intrinsic
// Detect a call to the intrinsic...
&& let FnOperand::Regular(fn_ptr) = &call.func
&& let FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)) = fn_ptr.func
&& fun_id == discriminant_intrinsic
// on a known enum...
&& let ty = &fn_ptr.generics.types[0]
&& let TyKind::Adt(TypeId::Adt(type_id), _) = *ty.kind()
&& let Some(TypeDeclKind::Enum(variants)) =
ctx.translated.type_decls.get(type_id).map(|x| &x.kind)
// passing it a reference.
&& let Operand::Move(p) = &call.args[0]
&& let TyKind::Ref(_, sub_ty, _) = p.ty().kind() =>
{
let p = p.clone().project(ProjectionElem::Deref, sub_ty.clone());
block.statements[i].content =
generate_discr_assignment(*span1, variants, &p, &call.dest)
}
_ => {}
}
}
}
}
const DISCRIMINANT_INTRINSIC: &str = "core::intrinsics::discriminant_value";
impl LlbcPass for Transform {
fn transform_ctx(&self, ctx: &mut TransformCtx) {
let pat = NamePattern::parse(DISCRIMINANT_INTRINSIC).unwrap();
let discriminant_intrinsic: Option<FunDeclId> = ctx
.translated
.item_names
.iter()
.find(|(_, name)| pat.matches(&ctx.translated, name))
.and_then(|(id, _)| id.as_fun())
.copied();
ctx.for_each_fun_decl(|ctx, decl| {
if let Ok(body) = &mut decl.body {
let body = body.as_structured_mut().unwrap();
self.log_before_body(ctx, &decl.item_meta.name, Ok(&*body));
body.body.visit_blocks_bwd(|block: &mut Block| {
Transform::update_block(ctx, block, discriminant_intrinsic);
});
};
});
}
}