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

charon_lib/transform/simplify_output/
simplify_constants.rs
