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(FunId::Regular(fun_id)) = &fn_ptr.kind 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_deref() == Some("offset_of")
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 TypeId::Adt(type_id) = tref.id
26                && let [Operand::Const(arg0), Operand::Const(arg1)] = call.args.as_slice()
27                && let ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned(
28                    UIntTy::U32,
29                    variant_id,
30                ))) = &arg0.kind
31                && let ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned(
32                    UIntTy::U32,
33                    field_id,
34                ))) = &arg1.kind
35                && let Some(tdecl) = ctx.ctx.translated.type_decls.get(type_id)
36            {
37                // TODO: move into a pass, maybe also size_of/align_of? or remove the nullops.
38                // maybe this is a constant also.
39                let variant_id = if tdecl.kind.is_enum() {
40                    Some(VariantId::from_usize(*variant_id as usize))
41                } else {
42                    None
43                };
44                let field_id = FieldId::from_usize(*field_id as usize);
45                let rval = Rvalue::NullaryOp(
46                    NullOp::OffsetOf(tref.clone(), variant_id, field_id),
47                    Ty::mk_usize(),
48                );
49                ctx.insert_assn_stmt(call.dest.clone(), rval);
50                term.kind = TerminatorKind::Goto { target: *target };
51            }
52        });
53    }
54}
charon_lib/transform/resugar/reconstruct_intrinsics.rs

charon_lib/transform/resugar/
reconstruct_intrinsics.rs
