charon_lib/transform/
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 super::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.value {
33        RawConstantExpr::Literal(_)
34        | RawConstantExpr::Var(_)
35        | RawConstantExpr::RawMemory(..)
36        | RawConstantExpr::TraitConst(..)
37        | RawConstantExpr::FnPtr(..)
38        | RawConstantExpr::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        RawConstantExpr::Global(global_ref) => {
46            Operand::Move(new_var(Rvalue::Global(global_ref), val.ty.clone()))
47        }
48        RawConstantExpr::Ref(bval) => {
49            match bval.value {
50                RawConstantExpr::Global(global_ref) => Operand::Move(new_var(
51                    Rvalue::GlobalRef(global_ref, RefKind::Shared),
52                    val.ty,
53                )),
54                _ => {
55                    // Recurse on the borrowed value
56                    let bval_ty = bval.ty.clone();
57                    let bval = transform_constant_expr(span, bval, new_var);
58
59                    // Evaluate the referenced value
60                    let bvar = new_var(Rvalue::Use(bval), bval_ty);
61
62                    // Borrow the value
63                    let ref_var = new_var(Rvalue::Ref(bvar, BorrowKind::Shared), val.ty);
64
65                    Operand::Move(ref_var)
66                }
67            }
68        }
69        RawConstantExpr::MutPtr(bval) => {
70            match bval.value {
71                RawConstantExpr::Global(global_ref) => {
72                    Operand::Move(new_var(Rvalue::GlobalRef(global_ref, RefKind::Mut), val.ty))
73                }
74                _ => {
75                    // Recurse on the borrowed value
76                    let bval_ty = bval.ty.clone();
77                    let bval = transform_constant_expr(span, bval, new_var);
78
79                    // Evaluate the referenced value
80                    let bvar = new_var(Rvalue::Use(bval), bval_ty);
81
82                    // Borrow the value
83                    let ref_var = new_var(Rvalue::RawPtr(bvar, RefKind::Mut), val.ty);
84
85                    Operand::Move(ref_var)
86                }
87            }
88        }
89        RawConstantExpr::Adt(variant, fields) => {
90            let fields = fields
91                .into_iter()
92                .map(|x| transform_constant_expr(span, Box::new(x), new_var))
93                .collect();
94
95            // Build an `Aggregate` rvalue.
96            let rval = {
97                let (adt_kind, generics) = val.ty.kind().as_adt().unwrap();
98                let aggregate_kind =
99                    AggregateKind::Adt(*adt_kind, variant, None, Box::new(generics.clone()));
100                Rvalue::Aggregate(aggregate_kind, fields)
101            };
102            let var = new_var(rval, val.ty);
103
104            Operand::Move(var)
105        }
106        RawConstantExpr::Array(fields) => {
107            let fields = fields
108                .into_iter()
109                .map(|x| transform_constant_expr(span, Box::new(x), new_var))
110                .collect_vec();
111
112            let len = ConstGeneric::Value(Literal::Scalar(ScalarValue::Usize(fields.len() as u64)));
113            let (adt_kind, generics) = val.ty.kind().as_adt().unwrap();
114            assert_matches!(
115                *adt_kind.as_builtin().unwrap(),
116                BuiltinTy::Array | BuiltinTy::Slice
117            );
118            let ty = generics.types[0].clone();
119            let rval = Rvalue::Aggregate(AggregateKind::Array(ty, len), fields);
120            let var = new_var(rval, val.ty);
121
122            Operand::Move(var)
123        }
124    }
125}
126
127fn transform_operand(span: &Span, locals: &mut Locals, nst: &mut Vec<Statement>, op: &mut Operand) {
128    // Transform the constant operands (otherwise do nothing)
129    take_mut::take(op, |op| {
130        if let Operand::Const(val) = op {
131            let mut new_var = |rvalue, ty| {
132                if let Rvalue::Use(Operand::Move(place)) = rvalue {
133                    place
134                } else {
135                    let var = locals.new_var(None, ty);
136                    nst.push(Statement::new(
137                        *span,
138                        RawStatement::Assign(var.clone(), rvalue),
139                    ));
140                    var
141                }
142            };
143            transform_constant_expr(span, val, &mut new_var)
144        } else {
145            op
146        }
147    })
148}
149
150pub struct Transform;
151impl UllbcPass for Transform {
152    fn transform_body(&self, _ctx: &mut TransformCtx, body: &mut ExprBody) {
153        for block in body.body.iter_mut() {
154            // Deconstruct some constants into series of MIR assignments.
155            block.transform_operands(|span, nst, op| {
156                transform_operand(span, &mut body.locals, nst, op)
157            });
158
159            // Simplify array with repeated constants into array repeats.
160            block.dyn_visit_in_body_mut(|rvalue: &mut Rvalue| {
161                take_mut::take(rvalue, |rvalue| match rvalue {
162                    Rvalue::Aggregate(AggregateKind::Array(ty, len), ref fields)
163                        if fields.len() >= 2
164                            && fields.iter().all(|x| x.is_const())
165                            && let Ok(op) = fields.iter().dedup().exactly_one() =>
166                    {
167                        Rvalue::Repeat(op.clone(), ty.clone(), len)
168                    }
169                    _ => rvalue,
170                });
171            });
172        }
173    }
174}
charon_lib/transform/simplify_constants.rs

charon_lib/transform/
simplify_constants.rs
