Skip to main content

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(variant, fields) => {
98            let fields = fields
99                .into_iter()
100                .map(|x| transform_constant_expr(ctx, Box::new(x)))
101                .collect();
102
103            // Build an `Aggregate` rvalue.
104            let tref = val.ty.kind().as_adt().unwrap();
105            let aggregate_kind = AggregateKind::Adt(tref.clone(), variant, None);
106            Rvalue::Aggregate(aggregate_kind, fields)
107        }
108        ConstantExprKind::Array(fields) if let TyKind::Array(ty, _) = val.ty.kind() => {
109            let fields = fields
110                .into_iter()
111                .map(|x| transform_constant_expr(ctx, Box::new(x)))
112                .collect_vec();
113            let len =
114                ConstantExpr::mk_usize(ScalarValue::Unsigned(UIntTy::Usize, fields.len() as u128));
115            Rvalue::Aggregate(AggregateKind::Array(ty.clone(), Box::new(len)), fields)
116        }
117        ConstantExprKind::FnPtr(fptr) if let TyKind::FnPtr(sig) = val.ty.kind() => {
118            let from_ty =
119                TyKind::FnDef(sig.clone().map(|_| fptr.clone().move_under_binder())).into_ty();
120            let to_ty = TyKind::FnPtr(sig.clone()).into_ty();
121            Rvalue::UnaryOp(
122                UnOp::Cast(CastKind::FnPtr(from_ty.clone(), to_ty)),
123                Operand::Const(Box::new(ConstantExpr {
124                    kind: ConstantExprKind::FnDef(fptr),
125                    ty: from_ty,
126                })),
127            )
128        }
129        ConstantExprKind::VTableRef(tref)
130            if let TraitRefKind::TraitImpl(impl_ref) = &tref.kind
131                && let Some(timpl) = ctx.ctx.translated.trait_impls.get(impl_ref.id)
132                && let Some(vtable_ref) = &timpl.vtable
133                && let TyKind::Ref(_, vtable_ty, _) = val.ty.kind() =>
134        {
135            let inner = Box::new(ConstantExpr {
136                kind: ConstantExprKind::Global(vtable_ref.clone()),
137                ty: vtable_ty.clone(),
138            });
139            val.kind = ConstantExprKind::Ref(inner, None);
140            // Normalize further into a place access.
141            return transform_constant_expr(ctx, val);
142        }
143        _ => return Operand::Const(val),
144    };
145    Operand::Move(ctx.rval_to_place(rval, val.ty.clone()))
146}
147
148fn transform_operand(ctx: &mut UllbcStatementTransformCtx<'_>, op: &mut Operand) {
149    // Transform the constant operands (otherwise do nothing)
150    take_mut::take(op, |op| {
151        if let Operand::Const(val) = op {
152            transform_constant_expr(ctx, val)
153        } else {
154            op
155        }
156    })
157}
158
159pub struct Transform;
160impl FusedUllbcPass for Transform {
161    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
162        !options.raw_consts
163    }
164
165    fn transform_function(&self, ctx: &mut TransformCtx, fun_decl: &mut FunDecl) {
166        fun_decl.transform_ullbc_operands(ctx, transform_operand);
167        if let Some(body) = fun_decl.body.as_unstructured_mut() {
168            for block in body.body.iter_mut() {
169                // Simplify array with repeated constants into array repeats.
170                block.dyn_visit_in_body_mut(|rvalue: &mut Rvalue| {
171                    take_mut::take(rvalue, |rvalue| match rvalue {
172                        Rvalue::Aggregate(AggregateKind::Array(ty, len), ref fields)
173                            if fields.len() >= 2
174                                && fields.iter().all(|x| x.is_const())
175                                && let Ok(op) = fields.iter().dedup().exactly_one() =>
176                        {
177                            Rvalue::Repeat(op.clone(), ty.clone(), len)
178                        }
179                        _ => rvalue,
180                    });
181                });
182            }
183        }
184    }
185}