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 so that only the
7//! `ConstantExpression::Literal`. It does 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, FusedUllbcPass, UllbcStatementTransformCtx};
17use crate::ullbc_ast::*;
18
19/// If the constant value is a constant ADT, push `Assign::Aggregate` statements
20/// to the vector of statements, that bind new variables to the ADT parts and
21/// the variable assigned to the complete ADT.
22///
23/// Goes fom e.g. `f(T::A(x, y))` to `let a = T::A(x, y); f(a)`.
24/// The function is recursively called on the aggregate fields (e.g. here x and y).
25fn transform_constant_expr(
26    ctx: &mut UllbcStatementTransformCtx<'_>,
27    mut val: Box<ConstantExpr>,
28) -> Operand {
29    let rval = match val.kind {
30        // Here we use a copy, rather than a move -- moving a global would leave it uninitialized.
31        ConstantExprKind::Global(global_ref) => {
32            return Operand::Copy(Place::new_global(global_ref, val.ty));
33        }
34        ConstantExprKind::PtrNoProvenance(ptr) => {
35            let usize_ty = TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)).into_ty();
36            let ptr_usize = ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned(
37                UIntTy::Usize,
38                ptr,
39            )));
40            let cast = UnOp::Cast(CastKind::RawPtr(usize_ty.clone(), val.ty.clone()));
41            Rvalue::UnaryOp(
42                cast,
43                Operand::Const(Box::new(ConstantExpr {
44                    kind: ptr_usize,
45                    ty: usize_ty,
46                })),
47            )
48        }
49        cexpr @ (ConstantExprKind::Ref(..) | ConstantExprKind::Ptr(..)) => {
50            let (rk, bval, metadata) = match cexpr {
51                ConstantExprKind::Ref(bval, metadata) => (None, bval, metadata),
52                ConstantExprKind::Ptr(rk, bval, metadata) => (Some(rk), bval, metadata),
53                _ => unreachable!(),
54            };
55
56            // As the value is originally an argument, it must be Sized, hence no metadata
57            let place = match bval.kind {
58                ConstantExprKind::Global(global_ref) => Place::new_global(global_ref, bval.ty),
59                _ => {
60                    // Recurse on the borrowed value
61                    let bval = transform_constant_expr(ctx, bval);
62
63                    // Evaluate the referenced value
64                    let bval_ty = bval.ty().clone();
65                    ctx.rval_to_place(Rvalue::Use(bval), bval_ty)
66                }
67            };
68            match (rk, metadata) {
69                // Borrow the place.
70                (None, None) => ctx.borrow(place, BorrowKind::Shared),
71                (Some(rk), None) => ctx.raw_borrow(place, rk),
72                // Unsizing borrow.
73                (None, Some(metadata)) => {
74                    let sized_ref = ctx.borrow_to_new_var(place, BorrowKind::Shared, None);
75                    Rvalue::UnaryOp(
76                        UnOp::Cast(CastKind::Unsize(
77                            sized_ref.ty.clone(),
78                            val.ty.clone(),
79                            metadata,
80                        )),
81                        Operand::Move(sized_ref),
82                    )
83                }
84                (Some(rk), Some(metadata)) => {
85                    let sized_raw_ref = ctx.raw_borrow_to_new_var(place, rk, None);
86                    Rvalue::UnaryOp(
87                        UnOp::Cast(CastKind::Unsize(
88                            sized_raw_ref.ty.clone(),
89                            val.ty.clone(),
90                            metadata,
91                        )),
92                        Operand::Move(sized_raw_ref),
93                    )
94                }
95            }
96        }
97        ConstantExprKind::Adt(..) if val.ty.is_unit() => {
98            // Keep unit constants to avoid adding countless unit locals.
99            return Operand::Const(val);
100        }
101        ConstantExprKind::Adt(variant, fields) => {
102            let fields = fields
103                .into_iter()
104                .map(|x| transform_constant_expr(ctx, Box::new(x)))
105                .collect();
106
107            // Build an `Aggregate` rvalue.
108            let tref = val.ty.kind().as_adt().unwrap();
109            let aggregate_kind = AggregateKind::Adt(tref.clone(), variant, None);
110            Rvalue::Aggregate(aggregate_kind, fields)
111        }
112        ConstantExprKind::Array(fields) if let TyKind::Array(ty, _) = val.ty.kind() => {
113            let fields = fields
114                .into_iter()
115                .map(|x| transform_constant_expr(ctx, Box::new(x)))
116                .collect_vec();
117            let len =
118                ConstantExpr::mk_usize(ScalarValue::Unsigned(UIntTy::Usize, fields.len() as u128));
119            Rvalue::Aggregate(AggregateKind::Array(ty.clone(), Box::new(len)), fields)
120        }
121        ConstantExprKind::FnPtr(fptr) if let TyKind::FnPtr(sig) = val.ty.kind() => {
122            let from_ty =
123                TyKind::FnDef(sig.clone().map(|_| fptr.clone().move_under_binder())).into_ty();
124            let to_ty = TyKind::FnPtr(sig.clone()).into_ty();
125            Rvalue::UnaryOp(
126                UnOp::Cast(CastKind::FnPtr(from_ty.clone(), to_ty)),
127                Operand::Const(Box::new(ConstantExpr {
128                    kind: ConstantExprKind::FnDef(fptr),
129                    ty: from_ty,
130                })),
131            )
132        }
133        ConstantExprKind::VTableRef(tref)
134            if let TraitRefKind::TraitImpl(impl_ref) = &tref.kind
135                && let Some(timpl) = ctx.ctx.translated.trait_impls.get(impl_ref.id)
136                && let Some(vtable_ref) = &timpl.vtable
137                && let TyKind::Ref(_, vtable_ty, _) = val.ty.kind() =>
138        {
139            let inner = Box::new(ConstantExpr {
140                kind: ConstantExprKind::Global(vtable_ref.clone()),
141                ty: vtable_ty.clone(),
142            });
143            val.kind = ConstantExprKind::Ref(inner, None);
144            // Normalize further into a place access.
145            return transform_constant_expr(ctx, val);
146        }
147        _ => return Operand::Const(val),
148    };
149    Operand::Move(ctx.rval_to_place(rval, val.ty.clone()))
150}
151
152fn transform_operand(ctx: &mut UllbcStatementTransformCtx<'_>, op: &mut Operand) {
153    // Transform the constant operands (otherwise do nothing)
154    take_mut::take(op, |op| {
155        if let Operand::Const(val) = op {
156            transform_constant_expr(ctx, val)
157        } else {
158            op
159        }
160    })
161}
162
163pub struct Transform;
164impl FusedUllbcPass for Transform {
165    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
166        !options.raw_consts
167    }
168
169    fn transform_function(&self, ctx: &mut TransformCtx, fun_decl: &mut FunDecl) {
170        fun_decl.transform_ullbc_operands(ctx, transform_operand);
171        if let Some(body) = fun_decl.body.as_unstructured_mut() {
172            for block in body.body.iter_mut() {
173                // Simplify array with repeated constants into array repeats.
174                block.dyn_visit_in_body_mut(|rvalue: &mut Rvalue| {
175                    take_mut::take(rvalue, |rvalue| match rvalue {
176                        Rvalue::Aggregate(AggregateKind::Array(ty, len), ref fields)
177                            if fields.len() >= 2
178                                && fields.iter().all(|x| x.is_const())
179                                && let Ok(op) = fields.iter().dedup().exactly_one() =>
180                        {
181                            Rvalue::Repeat(op.clone(), ty.clone(), len)
182                        }
183                        Rvalue::Use(Operand::Const(e)) if e.kind.is_adt() && e.ty.is_unit() => {
184                            Rvalue::unit_value()
185                        }
186                        _ => rvalue,
187                    });
188                });
189            }
190        }
191    }
192}
charon_lib/transform/simplify_output/simplify_constants.rs

charon_lib/transform/simplify_output/
simplify_constants.rs
