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, UllbcPass, 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    val: Box<ConstantExpr>,
28) -> Operand {
29    let mut val_ty = val.ty.clone();
30    let rval = match val.kind {
31        ConstantExprKind::Literal(_)
32        | ConstantExprKind::Var(_)
33        | ConstantExprKind::RawMemory(..)
34        | ConstantExprKind::TraitConst(..)
35        | ConstantExprKind::FnDef(..)
36        | ConstantExprKind::Opaque(_) => {
37            // Nothing to do
38            // TODO: for trait const: might come from a top-level impl, so we might
39            // want to introduce an intermediate statement to be able to evaluate
40            // it as a function call, like for globals.
41            return Operand::Const(val);
42        }
43        // Here we use a copy, rather than a move -- moving a global would leave it uninitialized,
44        // which would e.g. make the following code fail:
45        //     const GLOBAL: usize = 0;
46        //     let x = GLOBAL;
47        //     let y = GLOBAL; // if moving, at this point GLOBAL would be uninitialized
48        ConstantExprKind::Global(global_ref) => {
49            return Operand::Copy(Place::new_global(global_ref, val.ty));
50        }
51        ConstantExprKind::PtrNoProvenance(ptr) => {
52            let usize_ty = TyKind::Literal(LiteralTy::UInt(UIntTy::Usize)).into_ty();
53            let ptr_usize = ConstantExprKind::Literal(Literal::Scalar(ScalarValue::Unsigned(
54                UIntTy::Usize,
55                ptr,
56            )));
57            let cast = UnOp::Cast(CastKind::RawPtr(usize_ty.clone(), val.ty.clone()));
58            Rvalue::UnaryOp(
59                cast,
60                Operand::Const(Box::new(ConstantExpr {
61                    kind: ptr_usize,
62                    ty: usize_ty,
63                })),
64            )
65        }
66        ConstantExprKind::Ref(bval) if bval.ty.is_slice() => {
67            // We need to special-case slices; we don't take a reference to the slice,
68            // but an unsizing cast
69            // We generate the following code:
70            // let array: [T; N] = [...];
71            // let array_ref: &[T; N] = &array;
72            // return unsize::<&[T; N], &[T]>(array_ref);
73            let bval = transform_constant_expr(ctx, bval);
74            let bval_ty = bval.ty().clone();
75            let (_, len) = bval_ty.as_array().expect("Non-adt slice sub-constant");
76
77            let array_place = ctx.rval_to_place(Rvalue::Use(bval), bval_ty.clone());
78
79            let (_, _, rk) = val.ty.as_ref().unwrap();
80            let array_ref = ctx.borrow_to_new_var(array_place, rk.clone().into(), None);
81            Rvalue::UnaryOp(
82                UnOp::Cast(CastKind::Unsize(
83                    array_ref.ty.clone(),
84                    val.ty.clone(),
85                    UnsizingMetadata::Length(len.clone()),
86                )),
87                Operand::Move(array_ref),
88            )
89        }
90        ConstantExprKind::Ref(bval) => {
91            let place = match bval.kind {
92                ConstantExprKind::Global(global_ref) => Place::new_global(global_ref, bval.ty),
93                _ => {
94                    // Recurse on the borrowed value
95                    let bval = transform_constant_expr(ctx, bval);
96
97                    // Evaluate the referenced value
98                    let bval_ty = bval.ty().clone();
99                    ctx.rval_to_place(Rvalue::Use(bval), bval_ty)
100                }
101            };
102            // Borrow the place.
103            ctx.borrow(place, BorrowKind::Shared)
104        }
105        ConstantExprKind::Ptr(rk, bval) => {
106            // As the value is originally an argument, it must be Sized, hence no metadata
107            let place = match bval.kind {
108                ConstantExprKind::Global(global_ref) => Place::new_global(global_ref, bval.ty),
109                _ => {
110                    // Recurse on the borrowed value
111                    let bval = transform_constant_expr(ctx, bval);
112
113                    // Evaluate the referenced value
114                    let bval_ty = bval.ty().clone();
115                    ctx.rval_to_place(Rvalue::Use(bval), bval_ty)
116                }
117            };
118            // Borrow the value
119            ctx.raw_borrow(place, rk)
120        }
121        ConstantExprKind::Adt(variant, fields) => {
122            let fields = fields
123                .into_iter()
124                .map(|x| transform_constant_expr(ctx, Box::new(x)))
125                .collect();
126
127            // Build an `Aggregate` rvalue.
128            let tref = val.ty.kind().as_adt().unwrap();
129            let aggregate_kind = AggregateKind::Adt(tref.clone(), variant, None);
130            Rvalue::Aggregate(aggregate_kind, fields)
131        }
132        ConstantExprKind::Array(fields) | ConstantExprKind::Slice(fields) => {
133            let fields = fields
134                .into_iter()
135                .map(|x| transform_constant_expr(ctx, Box::new(x)))
136                .collect_vec();
137
138            let len =
139                ConstantExpr::mk_usize(ScalarValue::Unsigned(UIntTy::Usize, fields.len() as u128));
140            let ty = match val.ty.kind() {
141                TyKind::Array(ty, _) => ty.clone(),
142                TyKind::Slice(ty) => {
143                    val_ty = Ty::mk_array(ty.clone(), len.clone());
144                    ty.clone()
145                }
146                _ => unreachable!("Unexpected type in array/slice constant"),
147            };
148            Rvalue::Aggregate(AggregateKind::Array(ty, Box::new(len)), fields)
149        }
150        ConstantExprKind::FnPtr(fptr) => {
151            let TyKind::FnPtr(sig) = val.ty.kind() else {
152                unreachable!("FnPtr constant must have FnPtr type");
153            };
154            let from_ty =
155                TyKind::FnDef(sig.clone().map(|_| fptr.clone().move_under_binder())).into_ty();
156            let to_ty = TyKind::FnPtr(sig.clone()).into_ty();
157
158            Rvalue::UnaryOp(
159                UnOp::Cast(CastKind::FnPtr(from_ty.clone(), to_ty)),
160                Operand::Const(Box::new(ConstantExpr {
161                    kind: ConstantExprKind::FnDef(fptr),
162                    ty: from_ty,
163                })),
164            )
165        }
166    };
167    Operand::Move(ctx.rval_to_place(rval, val_ty))
168}
169
170fn transform_operand(ctx: &mut UllbcStatementTransformCtx<'_>, op: &mut Operand) {
171    // Transform the constant operands (otherwise do nothing)
172    take_mut::take(op, |op| {
173        if let Operand::Const(val) = op {
174            transform_constant_expr(ctx, val)
175        } else {
176            op
177        }
178    })
179}
180
181pub struct Transform;
182impl UllbcPass for Transform {
183    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
184        !options.raw_consts
185    }
186
187    fn transform_function(&self, ctx: &mut TransformCtx, fun_decl: &mut FunDecl) {
188        fun_decl.transform_ullbc_operands(ctx, transform_operand);
189        if let Some(body) = fun_decl.body.as_unstructured_mut() {
190            for block in body.body.iter_mut() {
191                // Simplify array with repeated constants into array repeats.
192                block.dyn_visit_in_body_mut(|rvalue: &mut Rvalue| {
193                    take_mut::take(rvalue, |rvalue| match rvalue {
194                        Rvalue::Aggregate(AggregateKind::Array(ty, len), ref fields)
195                            if fields.len() >= 2
196                                && fields.iter().all(|x| x.is_const())
197                                && let Ok(op) = fields.iter().dedup().exactly_one() =>
198                        {
199                            Rvalue::Repeat(op.clone(), ty.clone(), len)
200                        }
201                        _ => rvalue,
202                    });
203                });
204            }
205        }
206    }
207}
charon_lib/transform/simplify_output/simplify_constants.rs

charon_lib/transform/simplify_output/
simplify_constants.rs
