charon_lib/transform/simplify_output/
simplify_constants.rs

1//! The MIR constant expressions lead to a lot of duplication: there are
2//! for instance constant ADTs which duplicate the "regular" aggregated
3//! ADTs in the operands, constant references, etc. This reduces the number
4//! of cases to handle and eases the function translation in Aeneas.
5//!
6//! This pass removes all those occurrences, leaving only primitive constant expressions. It does
7//! so by introducing intermediate statements.
8//!
9//! A small remark about the intermediate statements we introduce for the globals:
10//! we do so because, when evaluating the code in "concrete" mode, it allows to
11//! handle the globals like function calls.
12
13use itertools::Itertools;
14
15use crate::transform::TransformCtx;
16use crate::transform::ctx::{BodyTransformCtx, UllbcPass, UllbcStatementTransformCtx};
17use crate::ullbc_ast::*;
18
19/// Add a global holding `value`, named like the promoted constants of the current item, and return its place.
20/// `ptr_metadata` is the metadata of pointers to the global.
21fn new_promoted_global(
22    ctx: &mut UllbcStatementTransformCtx<'_>,
23    value: ConstantExpr,
24    ptr_metadata: ConstantExpr,
25) -> GlobalDeclRef {
26    let krate = &mut ctx.ctx.translated;
27    let id = ItemId::Fun(*ctx.def_id);
28    let mut name = krate.item_names.get(&id).unwrap().clone();
29    let promoted_count = krate
30        .item_names
31        .values()
32        .filter_map(|n| n.name.split_last())
33        .filter(|(last, prefix)| {
34            matches!(last, PathElem::Builtin(BuiltinPathElem::PromotedConst, _))
35                && *prefix == name.name.as_slice()
36        })
37        .count();
38    let disambiguator = Disambiguator::new(promoted_count);
39    name.name.push(PathElem::Builtin(
40        BuiltinPathElem::PromotedConst,
41        disambiguator,
42    ));
43    let ty = value.ty().clone();
44    let id = krate.global_decls.push_with(|def_id| GlobalDecl {
45        def_id,
46        item_meta: ItemMeta::dummy_public(ctx.span, name.clone(), true, ItemOpacity::Transparent),
47        generics: GenericParams::empty(),
48        ty: ty.clone(),
49        size: Size::from_expr(SizeExpr::size_of(&ty)),
50        align: Size::from_expr(SizeExpr::align_of(&ty)),
51        ptr_metadata,
52        src: GlobalSource::Normal,
53        global_kind: GlobalKind::AnonConst,
54        value,
55    });
56    krate.item_names.insert(id.into(), name);
57    GlobalDeclRef {
58        id,
59        generics: Box::new(GenericArgs::empty()),
60    }
61}
62
63/// If the constant value is a constant ADT, push `Assign::Aggregate` statements
64/// to the vector of statements, that bind new variables to the ADT parts and
65/// the variable assigned to the complete ADT.
66///
67/// Goes fom e.g. `f(T::A(x, y))` to `let a = T::A(x, y); f(a)`.
68/// The function is recursively called on the aggregate fields (e.g. here x and y).
69fn transform_constant_expr(
70    ctx: &mut UllbcStatementTransformCtx<'_>,
71    mut val: ConstantExpr,
72) -> Operand {
73    let rval = match val.kind() {
74        // Here we use a copy, rather than a move -- moving a global would leave it uninitialized.
75        ConstantExprKind::Global(global_ref) => {
76            return Operand::Copy(Place::new_global(global_ref.clone(), val.ty().clone()));
77        }
78        ConstantExprKind::PtrNoProvenance(ptr) => {
79            let usize_ty = Ty::mk_usize();
80            let ptr_usize = ConstantExprKind::Integer(IntegerValue::Unsigned(UIntTy::Usize, *ptr));
81            let cast = UnOp::Cast(CastKind::RawPtr(val.ty().clone()));
82            Rvalue::UnaryOp(cast, Operand::Const(ConstantExpr::new(ptr_usize, usize_ty)))
83        }
84        cexpr @ (ConstantExprKind::Ref(gplace, metadata)
85        | ConstantExprKind::Ptr(_, gplace, metadata)) => {
86            let rk = cexpr.as_ptr().map(|(rk, _, _)| *rk);
87            let bval_is_sized = gplace.ty.get_ptr_metadata(ctx.get_crate()).is_none();
88
89            // Peel off the projections, from the outermost one.
90            let mut projs = vec![];
91            let mut base = gplace;
92            while let GlobalPlaceKind::Projection(sub, proj) = &base.kind {
93                projs.push((proj, &base.ty));
94                base = sub;
95            }
96            let mut place = match &base.kind {
97                // We view a vtable at type `()`, so we go through a pointer cast.
98                GlobalPlaceKind::Global(GlobalProvenance::Global(global_ref))
99                    if let Some(decl) = ctx.ctx.translated.global_decls.get(global_ref.id)
100                        && matches!(decl.src, GlobalSource::VTableInstance { .. }) =>
101                {
102                    let decl_ty = decl.ty.clone().substitute(&global_ref.generics);
103                    let vtable = Place::new_global(global_ref.clone(), decl_ty);
104                    let vtable_ptr = ctx.raw_borrow_to_new_var(vtable, RefKind::Shared, None);
105                    let ptr_ty = TyKind::RawPtr(base.ty.clone(), RefKind::Shared).into_ty();
106                    let cast = UnOp::Cast(CastKind::RawPtr(ptr_ty.clone()));
107                    let rval = Rvalue::UnaryOp(cast, Operand::Move(vtable_ptr));
108                    ctx.rval_to_place(rval, ptr_ty).deref()
109                }
110                GlobalPlaceKind::Global(GlobalProvenance::Global(global_ref)) => {
111                    Place::new_global(global_ref.clone(), base.ty.clone())
112                }
113                GlobalPlaceKind::Global(GlobalProvenance::Function(fn_ptr, fn_ptr_ty)) => {
114                    let fn_ptr = ConstantExpr::new(
115                        ConstantExprKind::FnPtr(fn_ptr.clone()),
116                        fn_ptr_ty.clone(),
117                    );
118                    let fn_ptr = transform_constant_expr(ctx, fn_ptr);
119                    let ptr_ty = TyKind::RawPtr(base.ty.clone(), RefKind::Shared).into_ty();
120                    let cast = UnOp::Cast(CastKind::RawPtr(ptr_ty.clone()));
121                    ctx.rval_to_place(Rvalue::UnaryOp(cast, fn_ptr), ptr_ty)
122                        .deref()
123                }
124                GlobalPlaceKind::Global(GlobalProvenance::TypeId(_)) => {
125                    let kind = ConstantExprKind::Opaque("pointer into a `TypeId`".into());
126                    return Operand::Const(ConstantExpr::new(kind, val.ty().clone()));
127                }
128                GlobalPlaceKind::Projection(..) => unreachable!(),
129                // A local can't be unsized, so we put it in a new global
130                GlobalPlaceKind::Value(bval) if !bval_is_sized => {
131                    let meta = match metadata.as_ref().unwrap() {
132                        UnsizingMetadata::Length(meta) | UnsizingMetadata::VTable(_, meta) => meta,
133                        UnsizingMetadata::VTableUpcast(..) | UnsizingMetadata::Unknown => {
134                            unreachable!("unexpected const metadata")
135                        }
136                    };
137                    let global_ref = new_promoted_global(ctx, bval.clone(), meta.clone());
138                    Place::new_global(global_ref, bval.ty().clone())
139                }
140                GlobalPlaceKind::Value(bval) => {
141                    // Recurse on the borrowed value
142                    let bval = transform_constant_expr(ctx, bval.clone());
143
144                    // Evaluate the referenced value
145                    let bval_ty = bval.ty().clone();
146                    ctx.rval_to_place(Rvalue::Use(bval, WithRetag::No), bval_ty)
147                }
148            };
149            for (proj, proj_ty) in projs.into_iter().rev() {
150                let op = |n: IntegerValue| Box::new(Operand::Const(n.to_constant()));
151                let proj = match *proj {
152                    ConstProjectionElem::Field(variant_id, field_id) => {
153                        ProjectionElem::Field(variant_id, field_id)
154                    }
155                    ConstProjectionElem::Index(i) => ProjectionElem::Index {
156                        offset: op(i),
157                        from_end: false,
158                    },
159                    ConstProjectionElem::Subslice { from, to } => ProjectionElem::Subslice {
160                        from: op(from),
161                        to: op(to),
162                        from_end: false,
163                    },
164                    ConstProjectionElem::Offset {
165                        count,
166                        ref ty,
167                        in_bounds,
168                        ref pointee_is_sized,
169                    } => ctx.offset_projection(
170                        *op(count),
171                        ty.as_ref(),
172                        in_bounds,
173                        proj_ty.clone(),
174                        pointee_is_sized.clone(),
175                    ),
176                };
177                place = place.project(proj, proj_ty.clone());
178            }
179            // A sized place is unsized after being borrowed, if there's metadata.
180            let mut rval = match (rk, metadata.clone().filter(|_| bval_is_sized)) {
181                // Borrow the place.
182                (None, None) => ctx.borrow(place, BorrowKind::Shared),
183                (Some(rk), None) => ctx.raw_borrow(place, rk),
184                // Unsizing borrow.
185                (None, Some(metadata)) => {
186                    let sized_ref = ctx.borrow_to_new_var(place, BorrowKind::Shared, None);
187                    Rvalue::UnaryOp(
188                        UnOp::Cast(CastKind::Unsize(val.ty().clone(), metadata, vec![])),
189                        Operand::Move(sized_ref),
190                    )
191                }
192                (Some(rk), Some(metadata)) => {
193                    let sized_raw_ref = ctx.raw_borrow_to_new_var(place, rk, None);
194                    Rvalue::UnaryOp(
195                        UnOp::Cast(CastKind::Unsize(val.ty().clone(), metadata, vec![])),
196                        Operand::Move(sized_raw_ref),
197                    )
198                }
199            };
200            // The metadata of an unsized global may be a vtable reference, which we lower too.
201            if let Rvalue::Ref { ptr_metadata, .. } | Rvalue::RawPtr { ptr_metadata, .. } =
202                &mut rval
203            {
204                transform_operand(ctx, ptr_metadata);
205            }
206            rval
207        }
208        ConstantExprKind::Adt(..) if val.ty().is_unit() => {
209            // Keep unit constants to avoid adding countless unit locals.
210            return Operand::Const(val);
211        }
212        ConstantExprKind::Adt(variant, fields) => {
213            let fields = fields
214                .iter()
215                .cloned()
216                .map(|x| transform_constant_expr(ctx, x))
217                .collect();
218
219            // Build an `Aggregate` rvalue.
220            let tref = val.ty().kind().as_adt().unwrap();
221            let aggregate_kind = AggregateKind::Adt(tref.clone(), *variant, None);
222            Rvalue::Aggregate(aggregate_kind, fields)
223        }
224        ConstantExprKind::Array(fields)
225            if let TyKind::Array(ty, _, ty_is_sized) = val.ty().kind() =>
226        {
227            let fields = fields
228                .iter()
229                .cloned()
230                .map(|x| transform_constant_expr(ctx, x))
231                .collect_vec();
232            let len = ConstantExpr::mk_usize(fields.len() as u128);
233            Rvalue::Aggregate(
234                AggregateKind::Array(ty.clone(), len, ty_is_sized.clone()),
235                fields,
236            )
237        }
238        ConstantExprKind::Cast(value, kind) => {
239            let value = transform_constant_expr(ctx, value.clone());
240            if let TyKind::Ref(_, pointee, rk) = val.ty().kind() {
241                // Cast to the corresponding raw pointer, then reborrow it as a reference.
242                let raw_ty = TyKind::RawPtr(pointee.clone(), *rk).into_ty();
243                let mut kind = kind.clone();
244                match &mut kind {
245                    CastKind::RawPtr(tgt) | CastKind::Unsize(tgt, ..) => *tgt = raw_ty.clone(),
246                    _ => unreachable!("unexpected cast to a reference: {kind:?}"),
247                }
248                let raw_ptr = ctx.rval_to_place(Rvalue::UnaryOp(UnOp::Cast(kind), value), raw_ty);
249                ctx.borrow(raw_ptr.deref(), (*rk).into())
250            } else {
251                Rvalue::UnaryOp(UnOp::Cast(kind.clone()), value)
252            }
253        }
254        ConstantExprKind::VTableRef(tref)
255            if let Some(vtable_ref) = tref.vtable_ref(&ctx.ctx.translated)
256                && let TyKind::Ref(_, vtable_ty, _) = val.ty().kind() =>
257        {
258            let inner = GlobalPlace::new_global(vtable_ref.clone(), vtable_ty.clone());
259            val.with_contents_mut(|kind, _| *kind = ConstantExprKind::Ref(inner, None));
260            // Normalize further into a place access.
261            return transform_constant_expr(ctx, val);
262        }
263        _ => return Operand::Const(val),
264    };
265    Operand::Move(ctx.rval_to_place(rval, val.ty().clone()))
266}
267
268fn transform_operand(ctx: &mut UllbcStatementTransformCtx<'_>, op: &mut Operand) {
269    // Transform the constant operands (otherwise do nothing)
270    take_mut::take(op, |op| {
271        if let Operand::Const(val) = op {
272            transform_constant_expr(ctx, val)
273        } else {
274            op
275        }
276    })
277}
278
279pub struct Transform;
280impl UllbcPass for Transform {
281    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
282        !options.raw_consts
283    }
284
285    fn transform_function(&self, ctx: &mut TransformCtx, fun_decl: &mut FunDecl) {
286        fun_decl.transform_ullbc_statements(ctx, |ctx, st| {
287            let assigns_const = matches!(
288                st.kind,
289                StatementKind::Assign(_, Rvalue::Use(Operand::Const(_), _))
290            );
291            st.kind
292                .dyn_visit_in_body_mut(|op: &mut Operand| transform_operand(ctx, op));
293            // If we turned `x = const c` into `tmp = rval; x = move tmp`, assign `rval` directly.
294            if assigns_const
295                && let StatementKind::Assign(_, rval) = &mut st.kind
296                && let Rvalue::Use(Operand::Move(tmp), _) = rval
297                && let Some(last) = ctx.statements.last()
298                && let StatementKind::Assign(last_dest, last_rval) = &last.kind
299                && last_dest == tmp
300            {
301                *rval = last_rval.clone();
302                ctx.statements.pop();
303            }
304        });
305        fun_decl.transform_ullbc_terminators(ctx, |ctx, term| {
306            term.kind
307                .dyn_visit_in_body_mut(|op: &mut Operand| transform_operand(ctx, op));
308        });
309        if let Some(body) = fun_decl.body.as_unstructured_mut() {
310            for block in body.body.iter_mut() {
311                // Normalize unit constants into unit aggregates.
312                block.dyn_visit_in_body_mut(|rvalue: &mut Rvalue| {
313                    take_mut::take(rvalue, |rvalue| match rvalue {
314                        Rvalue::Use(Operand::Const(e), _)
315                            if e.kind().is_adt() && e.ty().is_unit() =>
316                        {
317                            Rvalue::unit_value()
318                        }
319                        _ => rvalue,
320                    });
321                });
322            }
323        }
324    }
325}
charon_lib/transform/simplify_output/simplify_constants.rs

charon_lib/transform/simplify_output/
simplify_constants.rs
