charon_lib/transform/resugar/
reconstruct_intrinsics.rs

1use crate::transform::TransformCtx;
2use crate::transform::ctx::{BodyTransformCtx, UllbcPass};
3use crate::ullbc_ast::*;
4
5pub struct Transform;
6impl UllbcPass for Transform {
7    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
8        decl.transform_ullbc_terminators(ctx, |ctx, term| {
9            let TerminatorKind::Call { call, target, .. } = &term.kind else {
10                return;
11            };
12            let FnOperand::Regular(fn_ptr) = &call.func else {
13                return;
14            };
15            let FnPtrKind::Fun(fun_id) = fn_ptr.kind.as_ref() else {
16                return;
17            };
18            let Some(fun_decl) = ctx.ctx.translated.fun_decls.get(*fun_id) else {
19                return;
20            };
21            if fun_decl.item_meta.lang_item.as_ref() == Some(&from_rustc::LangItem::OffsetOf)
22                && let generics = fn_ptr.pre_mono_generics(&ctx.ctx.translated)
23                && let Some(ty) = generics.types.get(TypeVarId::ZERO)
24                && let TyKind::Adt(tref) = ty.kind()
25                && let [Operand::Const(arg0), Operand::Const(arg1)] = call.args.as_slice()
26                && let ConstantExprKind::Integer(IntegerValue::Unsigned(UIntTy::U32, variant_id)) =
27                    arg0.kind()
28                && let ConstantExprKind::Integer(IntegerValue::Unsigned(UIntTy::U32, field_id)) =
29                    arg1.kind()
30                && let Some(tdecl) = ctx.ctx.translated.type_decls.get(tref.id)
31            {
32                let variant_id = if tdecl.kind.is_enum() {
33                    Some(VariantId::from_usize(*variant_id as usize))
34                } else {
35                    None
36                };
37                let field_id = FieldId::from_usize(*field_id as usize);
38                let constant = ConstantExpr::new(
39                    ConstantExprKind::OffsetOf(tref.clone(), variant_id, field_id),
40                    Ty::mk_usize(),
41                );
42                ctx.insert_assn_stmt(
43                    call.dest.clone(),
44                    Rvalue::Use(Operand::Const(constant), WithRetag::No),
45                );
46                term.kind = TerminatorKind::Goto { target: *target };
47            }
48        });
49    }
50}
charon_lib/transform/resugar/reconstruct_intrinsics.rs

charon_lib/transform/resugar/
reconstruct_intrinsics.rs
