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: Operand::Const(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(usize_ty.clone(), val.ty().clone()));
82            Rvalue::UnaryOp(cast, Operand::Const(ConstantExpr::new(ptr_usize, usize_ty)))
83        }
84        cexpr @ (ConstantExprKind::Ref(bval, metadata)
85        | ConstantExprKind::Ptr(_, bval, metadata)) => {
86            let rk = cexpr.as_ptr().map(|(rk, _, _)| *rk);
87            let bval_is_sized = bval.ty().get_ptr_metadata(ctx.get_crate()).is_none();
88
89            let place = match bval.kind() {
90                ConstantExprKind::Global(global_ref) => {
91                    Place::new_global(global_ref.clone(), bval.ty().clone())
92                }
93                // A local can't be unsized, so we put it in a new global
94                _ if !bval_is_sized => {
95                    let meta = match metadata.as_ref().unwrap() {
96                        UnsizingMetadata::Length(meta) | UnsizingMetadata::VTable(_, meta) => meta,
97                        UnsizingMetadata::VTableUpcast(..) | UnsizingMetadata::Unknown => {
98                            unreachable!("unexpected const metadata")
99                        }
100                    };
101                    let global_ref = new_promoted_global(ctx, bval.clone(), meta.clone());
102                    Place::new_global(global_ref, bval.ty().clone())
103                }
104                _ => {
105                    // Recurse on the borrowed value
106                    let bval = transform_constant_expr(ctx, bval.clone());
107
108                    // Evaluate the referenced value
109                    let bval_ty = bval.ty().clone();
110                    ctx.rval_to_place(Rvalue::Use(bval, WithRetag::No), bval_ty)
111                }
112            };
113            // A sized place is unsized after being borrowed, if there's metadata.
114            let mut rval = match (rk, metadata.clone().filter(|_| bval_is_sized)) {
115                // Borrow the place.
116                (None, None) => ctx.borrow(place, BorrowKind::Shared),
117                (Some(rk), None) => ctx.raw_borrow(place, rk),
118                // Unsizing borrow.
119                (None, Some(metadata)) => {
120                    let sized_ref = ctx.borrow_to_new_var(place, BorrowKind::Shared, None);
121                    Rvalue::UnaryOp(
122                        UnOp::Cast(CastKind::Unsize(
123                            sized_ref.ty.clone(),
124                            val.ty().clone(),
125                            metadata,
126                        )),
127                        Operand::Move(sized_ref),
128                    )
129                }
130                (Some(rk), Some(metadata)) => {
131                    let sized_raw_ref = ctx.raw_borrow_to_new_var(place, rk, None);
132                    Rvalue::UnaryOp(
133                        UnOp::Cast(CastKind::Unsize(
134                            sized_raw_ref.ty.clone(),
135                            val.ty().clone(),
136                            metadata,
137                        )),
138                        Operand::Move(sized_raw_ref),
139                    )
140                }
141            };
142            // The metadata of an unsized global may be a vtable reference, which we lower too.
143            if let Rvalue::Ref { ptr_metadata, .. } | Rvalue::RawPtr { ptr_metadata, .. } =
144                &mut rval
145            {
146                transform_operand(ctx, ptr_metadata);
147            }
148            rval
149        }
150        ConstantExprKind::Adt(..) if val.ty().is_unit() => {
151            // Keep unit constants to avoid adding countless unit locals.
152            return Operand::Const(val);
153        }
154        ConstantExprKind::Adt(variant, fields) => {
155            let fields = fields
156                .iter()
157                .cloned()
158                .map(|x| transform_constant_expr(ctx, x))
159                .collect();
160
161            // Build an `Aggregate` rvalue.
162            let tref = val.ty().kind().as_adt().unwrap();
163            let aggregate_kind = AggregateKind::Adt(tref.clone(), *variant, None);
164            Rvalue::Aggregate(aggregate_kind, fields)
165        }
166        ConstantExprKind::Array(fields)
167            if let TyKind::Array(ty, _, ty_is_sized) = val.ty().kind() =>
168        {
169            let fields = fields
170                .iter()
171                .cloned()
172                .map(|x| transform_constant_expr(ctx, x))
173                .collect_vec();
174            let len = ConstantExpr::mk_usize(fields.len() as u128);
175            Rvalue::Aggregate(
176                AggregateKind::Array(ty.clone(), len, ty_is_sized.clone()),
177                fields,
178            )
179        }
180        ConstantExprKind::FnPtr(fptr) if let TyKind::FnPtr(sig) = val.ty().kind() => {
181            let from_ty =
182                TyKind::FnDef(sig.clone().map(|_| fptr.clone().move_under_binder())).into_ty();
183            let to_ty = TyKind::FnPtr(sig.clone()).into_ty();
184            Rvalue::UnaryOp(
185                UnOp::Cast(CastKind::FnPtr(from_ty.clone(), to_ty)),
186                Operand::Const(ConstantExpr::new(
187                    ConstantExprKind::FnDef(fptr.clone()),
188                    from_ty,
189                )),
190            )
191        }
192        ConstantExprKind::VTableRef(tref)
193            if let Some(vtable_ref) = tref.vtable_ref(&ctx.ctx.translated)
194                && let TyKind::Ref(_, vtable_ty, _) = val.ty().kind() =>
195        {
196            let inner = ConstantExpr::new(
197                ConstantExprKind::Global(vtable_ref.clone()),
198                vtable_ty.clone(),
199            );
200            val.with_contents_mut(|kind, _| *kind = ConstantExprKind::Ref(inner, None));
201            // Normalize further into a place access.
202            return transform_constant_expr(ctx, val);
203        }
204        _ => return Operand::Const(val),
205    };
206    Operand::Move(ctx.rval_to_place(rval, val.ty().clone()))
207}
208
209fn transform_operand(ctx: &mut UllbcStatementTransformCtx<'_>, op: &mut Operand) {
210    // Transform the constant operands (otherwise do nothing)
211    take_mut::take(op, |op| {
212        if let Operand::Const(val) = op {
213            transform_constant_expr(ctx, val)
214        } else {
215            op
216        }
217    })
218}
219
220pub struct Transform;
221impl UllbcPass for Transform {
222    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
223        !options.raw_consts
224    }
225
226    fn transform_function(&self, ctx: &mut TransformCtx, fun_decl: &mut FunDecl) {
227        fun_decl.transform_ullbc_operands(ctx, transform_operand);
228        if let Some(body) = fun_decl.body.as_unstructured_mut() {
229            for block in body.body.iter_mut() {
230                // Normalize unit constants into unit aggregates.
231                block.dyn_visit_in_body_mut(|rvalue: &mut Rvalue| {
232                    take_mut::take(rvalue, |rvalue| match rvalue {
233                        Rvalue::Use(Operand::Const(e), _)
234                            if e.kind().is_adt() && e.ty().is_unit() =>
235                        {
236                            Rvalue::unit_value()
237                        }
238                        _ => rvalue,
239                    });
240                });
241            }
242        }
243    }
244}
charon_lib/transform/simplify_output/simplify_constants.rs

charon_lib/transform/simplify_output/
simplify_constants.rs
