charon_lib/transform/simplify_output/
simplify_constants.rs1use itertools::Itertools;
14
15use crate::transform::TransformCtx;
16use crate::transform::ctx::{BodyTransformCtx, FusedUllbcPass, UllbcStatementTransformCtx};
17use crate::ullbc_ast::*;
18
19fn transform_constant_expr(
26 ctx: &mut UllbcStatementTransformCtx<'_>,
27 mut val: Box<ConstantExpr>,
28) -> Operand {
29 let rval = match val.kind {
30 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 let place = match bval.kind {
58 ConstantExprKind::Global(global_ref) => Place::new_global(global_ref, bval.ty),
59 _ => {
60 let bval = transform_constant_expr(ctx, bval);
62
63 let bval_ty = bval.ty().clone();
65 ctx.rval_to_place(Rvalue::Use(bval), bval_ty)
66 }
67 };
68 match (rk, metadata) {
69 (None, None) => ctx.borrow(place, BorrowKind::Shared),
71 (Some(rk), None) => ctx.raw_borrow(place, rk),
72 (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 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 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 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 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}