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;
14use std::assert_matches::assert_matches;
15
16use crate::transform::TransformCtx;
17use crate::ullbc_ast::*;
18
19use crate::transform::ctx::UllbcPass;
20
21/// If the constant value is a constant ADT, push `Assign::Aggregate` statements
22/// to the vector of statements, that bind new variables to the ADT parts and
23/// the variable assigned to the complete ADT.
24///
25/// Goes fom e.g. `f(T::A(x, y))` to `let a = T::A(x, y); f(a)`.
26/// The function is recursively called on the aggregate fields (e.g. here x and y).
27fn transform_constant_expr(
28    span: &Span,
29    val: Box<ConstantExpr>,
30    new_var: &mut impl FnMut(Rvalue, Ty) -> Place,
31) -> Operand {
32    match val.kind {
33        ConstantExprKind::Literal(_)
34        | ConstantExprKind::Var(_)
35        | ConstantExprKind::RawMemory(..)
36        | ConstantExprKind::TraitConst(..)
37        | ConstantExprKind::FnPtr(..)
38        | ConstantExprKind::Opaque(_) => {
39            // Nothing to do
40            // TODO: for trait const: might come from a top-level impl, so we might
41            // want to introduce an intermediate statement to be able to evaluate
42            // it as a function call, like for globals.
43            Operand::Const(val)
44        }
45        // Here we use a copy, rather than a move -- moving a global would leave it uninitialized,
46        // which would e.g. make the following code fail:
47        //     const GLOBAL: usize = 0;
48        //     let x = GLOBAL;
49        //     let y = GLOBAL; // if moving, at this point GLOBAL would be uninitialized
50        ConstantExprKind::Global(global_ref) => {
51            Operand::Copy(Place::new_global(global_ref, val.ty))
52        }
53        ConstantExprKind::PtrNoProvenance(ptr) => {
54            let usize_ty = TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)).into_ty();
55            let ptr_usize = ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned(
56                UIntTy::Usize,
57                ptr,
58            )));
59            let cast = UnOp::Cast(CastKind::RawPtr(usize_ty.clone(), val.ty.clone()));
60            let uvar = new_var(
61                Rvalue::UnaryOp(
62                    cast,
63                    Operand::Const(Box::new(ConstantExpr {
64                        kind: ptr_usize,
65                        ty: usize_ty,
66                    })),
67                ),
68                val.ty,
69            );
70            Operand::Move(uvar)
71        }
72        ConstantExprKind::Ref(bval) => {
73            match bval.kind {
74                ConstantExprKind::Global(global_ref) => {
75                    let unit_metadata = new_var(Rvalue::unit_value(), Ty::mk_unit());
76                    Operand::Move(new_var(
77                        // This is a reference to a global constant, which must be Sized, so no metadata
78                        Rvalue::Ref {
79                            place: Place::new_global(global_ref, bval.ty),
80                            kind: BorrowKind::Shared,
81                            ptr_metadata: Operand::Move(unit_metadata),
82                        },
83                        val.ty,
84                    ))
85                }
86                _ => {
87                    // Recurse on the borrowed value
88                    let bval_ty = bval.ty.clone();
89                    let bval = transform_constant_expr(span, bval, new_var);
90
91                    // Evaluate the referenced value
92                    let bvar = new_var(Rvalue::Use(bval), bval_ty);
93
94                    let unit_metadata = new_var(Rvalue::unit_value(), Ty::mk_unit());
95
96                    // Borrow the value
97                    // As the value is originally an argument, it must be Sized
98                    let ref_var = new_var(
99                        Rvalue::Ref {
100                            place: bvar,
101                            kind: BorrowKind::Shared,
102                            ptr_metadata: Operand::Move(unit_metadata),
103                        },
104                        val.ty,
105                    );
106
107                    Operand::Move(ref_var)
108                }
109            }
110        }
111        ConstantExprKind::Ptr(rk, bval) => {
112            match bval.kind {
113                ConstantExprKind::Global(global_ref) => {
114                    let unit_metadata = new_var(Rvalue::unit_value(), Ty::mk_unit());
115                    Operand::Move(new_var(
116                        // This is a raw pointer to a global constant, which must be Sized, so no metadata
117                        Rvalue::RawPtr {
118                            place: Place::new_global(global_ref, bval.ty),
119                            kind: rk,
120                            ptr_metadata: Operand::Move(unit_metadata),
121                        },
122                        val.ty,
123                    ))
124                }
125                _ => {
126                    // Recurse on the borrowed value
127                    let bval_ty = bval.ty.clone();
128                    let bval = transform_constant_expr(span, bval, new_var);
129
130                    // Evaluate the referenced value
131                    let bvar = new_var(Rvalue::Use(bval), bval_ty);
132
133                    let unit_metadata = new_var(Rvalue::unit_value(), Ty::mk_unit());
134
135                    // Borrow the value
136                    // As the value is originally an argument, it must be Sized, hence no metadata
137                    let ref_var = new_var(
138                        Rvalue::RawPtr {
139                            place: bvar,
140                            kind: rk,
141                            ptr_metadata: Operand::Move(unit_metadata),
142                        },
143                        val.ty,
144                    );
145
146                    Operand::Move(ref_var)
147                }
148            }
149        }
150        ConstantExprKind::Adt(variant, fields) => {
151            let fields = fields
152                .into_iter()
153                .map(|x| transform_constant_expr(span, Box::new(x), new_var))
154                .collect();
155
156            // Build an `Aggregate` rvalue.
157            let rval = {
158                let tref = val.ty.kind().as_adt().unwrap();
159                let aggregate_kind = AggregateKind::Adt(tref.clone(), variant, None);
160                Rvalue::Aggregate(aggregate_kind, fields)
161            };
162            let var = new_var(rval, val.ty);
163
164            Operand::Move(var)
165        }
166        ConstantExprKind::Array(fields) => {
167            let fields = fields
168                .into_iter()
169                .map(|x| transform_constant_expr(span, Box::new(x), new_var))
170                .collect_vec();
171
172            let len = ConstGeneric::Value(Literal::Scalar(ScalarValue::Unsigned(
173                UIntTy::Usize,
174                fields.len() as u128,
175            )));
176            let tref = val.ty.kind().as_adt().unwrap();
177            assert_matches!(
178                *tref.id.as_builtin().unwrap(),
179                BuiltinTy::Array | BuiltinTy::Slice
180            );
181            let ty = tref.generics.types[0].clone();
182            let rval = Rvalue::Aggregate(AggregateKind::Array(ty, len), fields);
183            let var = new_var(rval, val.ty);
184
185            Operand::Move(var)
186        }
187    }
188}
189
190fn transform_operand(span: &Span, locals: &mut Locals, nst: &mut Vec<Statement>, op: &mut Operand) {
191    // Transform the constant operands (otherwise do nothing)
192    take_mut::take(op, |op| {
193        if let Operand::Const(val) = op {
194            let mut new_var = |rvalue, ty| {
195                if let Rvalue::Use(Operand::Move(place)) = rvalue {
196                    place
197                } else {
198                    let var = locals.new_var(None, ty);
199                    nst.push(Statement::new(
200                        *span,
201                        StatementKind::StorageLive(var.as_local().unwrap()),
202                    ));
203                    nst.push(Statement::new(
204                        *span,
205                        StatementKind::Assign(var.clone(), rvalue),
206                    ));
207                    var
208                }
209            };
210            transform_constant_expr(span, val, &mut new_var)
211        } else {
212            op
213        }
214    })
215}
216
217pub struct Transform;
218impl UllbcPass for Transform {
219    fn transform_body(&self, _ctx: &mut TransformCtx, body: &mut ExprBody) {
220        for block in body.body.iter_mut() {
221            // Deconstruct some constants into series of MIR assignments.
222            block.transform_operands(|span, nst, op| {
223                transform_operand(span, &mut body.locals, nst, op)
224            });
225
226            // Simplify array with repeated constants into array repeats.
227            block.dyn_visit_in_body_mut(|rvalue: &mut Rvalue| {
228                take_mut::take(rvalue, |rvalue| match rvalue {
229                    Rvalue::Aggregate(AggregateKind::Array(ty, len), ref fields)
230                        if fields.len() >= 2
231                            && fields.iter().all(|x| x.is_const())
232                            && let Ok(op) = fields.iter().dedup().exactly_one() =>
233                    {
234                        Rvalue::Repeat(op.clone(), ty.clone(), len)
235                    }
236                    _ => rvalue,
237                });
238            });
239        }
240    }
241}
charon_lib/transform/simplify_output/simplify_constants.rs

charon_lib/transform/simplify_output/
simplify_constants.rs
