charon_driver/translate/
translate_constants.rs

1//! Functions to translate constants to LLBC.
2use crate::hax;
3use crate::hax::state::UnderOwnerState;
4use itertools::Itertools;
5use rustc_middle::ty;
6
7use super::translate_ctx::*;
8use charon_lib::ast::*;
9
10impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
11    fn translate_constant_literal_to_constant_expr_kind(
12        &mut self,
13        v: &hax::ConstantLiteral,
14    ) -> Result<ConstantExprKind, Error> {
15        Ok(match v {
16            hax::ConstantLiteral::ByteStr(bs) => ConstantExprKind::ByteStr(bs.clone()),
17            hax::ConstantLiteral::Str(str) => ConstantExprKind::Str(str.clone()),
18            hax::ConstantLiteral::Char(c) => ConstantExprKind::Char(*c),
19            hax::ConstantLiteral::Bool(b) => ConstantExprKind::Bool(*b),
20            hax::ConstantLiteral::Int(i) => {
21                use crate::hax::ConstantInt;
22                let scalar = match i {
23                    ConstantInt::Int(v, int_type) => {
24                        let ty = Self::translate_hax_int_ty(int_type);
25                        IntegerValue::Signed(ty, *v)
26                    }
27                    ConstantInt::Uint(v, uint_type) => {
28                        let ty = Self::translate_hax_uint_ty(uint_type);
29                        IntegerValue::Unsigned(ty, *v)
30                    }
31                };
32                ConstantExprKind::Integer(scalar)
33            }
34            hax::ConstantLiteral::Float(value, bits, float_type) => {
35                let value = value.clone();
36                let bits = *bits;
37                let ty = match float_type {
38                    hax::FloatTy::F16 => FloatTy::F16,
39                    hax::FloatTy::F32 => FloatTy::F32,
40                    hax::FloatTy::F64 => FloatTy::F64,
41                    hax::FloatTy::F128 => FloatTy::F128,
42                };
43                ConstantExprKind::Float(FloatValue { value, bits, ty })
44            }
45            hax::ConstantLiteral::PtrNoProvenance(v) => {
46                return Ok(ConstantExprKind::PtrNoProvenance(*v));
47            }
48        })
49    }
50
51    fn translate_constant_byte(
52        &mut self,
53        span: Span,
54        b: &hax::ConstantByte<'tcx>,
55    ) -> Result<Byte, Error> {
56        Ok(match b {
57            hax::ConstantByte::Uninit => Byte::Uninit,
58            hax::ConstantByte::Value(v) => Byte::Value(*v),
59            hax::ConstantByte::Provenance(prov, offset, i) => Byte::Provenance(
60                self.translate_provenance(span, prov)?,
61                IntegerValue::mk_usize(*offset as u128),
62                *i,
63            ),
64        })
65    }
66
67    fn translate_provenance(
68        &mut self,
69        span: Span,
70        prov: &hax::ConstantByteProvenance<'tcx>,
71    ) -> Result<GlobalProvenance, Error> {
72        Ok(match prov {
73            hax::ConstantByteProvenance::Global(item) => {
74                GlobalProvenance::Global(self.translate_global_decl_ref(span, item)?)
75            }
76            hax::ConstantByteProvenance::Function(target, fn_ptr_ty) => {
77                let fn_ptr = self.translate_bound_fn_ptr_target(span, target)?;
78                GlobalProvenance::Function(
79                    self.erase_region_binder(fn_ptr),
80                    self.translate_ty(span, fn_ptr_ty)?,
81                )
82            }
83            hax::ConstantByteProvenance::TypeId(ty) => {
84                GlobalProvenance::TypeId(self.translate_ty(span, ty)?)
85            }
86            hax::ConstantByteProvenance::VTable(proof) => {
87                match self.translate_vtable_instance_const(span, proof)?.kind() {
88                    ConstantExprKind::Ref(vtable, None)
89                        if let GlobalPlaceKind::Global(prov) = &vtable.kind =>
90                    {
91                        prov.clone()
92                    }
93                    _ => raise_error!(self, span, "vtable without a global"),
94                }
95            }
96        })
97    }
98
99    /// The function pointed to by a function pointer.
100    fn translate_bound_fn_ptr_target(
101        &mut self,
102        span: Span,
103        target: &hax::FnPtrTarget<'tcx>,
104    ) -> Result<RegionBinder<FnPtr>, Error> {
105        Ok(match target {
106            hax::FnPtrTarget::Fn(item) => {
107                self.translate_bound_fn_ptr(span, item, TransItemSourceKind::Fun)?
108            }
109            hax::FnPtrTarget::ClosureAsFn(closure) => self
110                .translate_stateless_closure_as_fn_ref(span, closure)?
111                .map(FnPtr::from),
112        })
113    }
114
115    /// Translate a constant expression.
116    pub(crate) fn translate_constant_expr(
117        &mut self,
118        span: Span,
119        v: &hax::ConstantExpr<'tcx>,
120    ) -> Result<ConstantExpr, Error> {
121        let ty = self.translate_ty(span, &v.ty)?;
122        let kind = match v.kind.as_ref() {
123            hax::ConstantExprKind::Literal(lit) => {
124                self.translate_constant_literal_to_constant_expr_kind(lit)?
125            }
126            hax::ConstantExprKind::Adt { kind, fields } => {
127                let fields: IndexVec<FieldId, ConstantExpr> = fields
128                    .iter()
129                    .map(|f| self.translate_constant_expr(span, &f.value))
130                    .try_collect()?;
131                use crate::hax::VariantKind;
132                let vid = if let VariantKind::Enum { index, .. } = *kind {
133                    Some(self.translate_variant_id(index))
134                } else {
135                    None
136                };
137                ConstantExprKind::Adt(vid, fields)
138            }
139            hax::ConstantExprKind::Array { fields } => {
140                let fields: Vec<ConstantExpr> = fields
141                    .iter()
142                    .map(|x| self.translate_constant_expr(span, x))
143                    .try_collect()?;
144
145                if let TyKind::Array(_, count, value_is_sized) = ty.kind()
146                    && fields.len() >= 2
147                    && let Ok(value) = fields.iter().dedup().exactly_one()
148                {
149                    ConstantExprKind::Repeat {
150                        value: value.clone(),
151                        count: count.clone(),
152                        value_is_sized: value_is_sized.clone(),
153                    }
154                } else {
155                    ConstantExprKind::Array(fields)
156                }
157            }
158            hax::ConstantExprKind::Repeat { value } => {
159                let TyKind::Array(_, count, value_is_sized) = ty.kind() else {
160                    unreachable!("Unexpected type for a repeat constant: {ty:?}")
161                };
162                ConstantExprKind::Repeat {
163                    value: self.translate_constant_expr(span, value)?,
164                    count: count.clone(),
165                    value_is_sized: value_is_sized.clone(),
166                }
167            }
168            hax::ConstantExprKind::Tuple { fields } => {
169                let fields: IndexVec<FieldId, ConstantExpr> = fields
170                    .iter()
171                    .map(|f| self.translate_constant_expr(span, f))
172                    .try_collect()?;
173                ConstantExprKind::Adt(None, fields)
174            }
175            hax::ConstantExprKind::NamedGlobal(item) => match &item.in_trait {
176                Some(trait_proof) => {
177                    let trait_ref = self.translate_trait_proof(span, trait_proof)?.erase();
178                    // Trait consts can't have their own generics.
179                    assert!(item.generic_args.is_empty());
180                    let const_id =
181                        self.translate_assoc_const_id(trait_ref.trait_id(), &item.def_id)?;
182                    ConstantExprKind::TraitConst(trait_ref, const_id)
183                }
184                None => {
185                    let global_ref = self.translate_global_decl_ref(span, item)?;
186                    ConstantExprKind::Global(global_ref)
187                }
188            },
189            hax::ConstantExprKind::Ptr {
190                base,
191                projections,
192                metadata,
193            } => {
194                let mut place = match base {
195                    hax::ConstantPtrBase::Global(prov, base_ty) => GlobalPlace {
196                        kind: GlobalPlaceKind::Global(self.translate_provenance(span, prov)?),
197                        ty: self.translate_ty(span, base_ty)?,
198                    },
199                    hax::ConstantPtrBase::Value(arg) => {
200                        GlobalPlace::new_value(self.translate_constant_expr(span, arg)?)
201                    }
202                };
203                for (proj, proj_ty) in projections {
204                    let proj = match *proj {
205                        hax::ConstantProjectionElem::Field(variant, field) => {
206                            ConstProjectionElem::Field(
207                                variant.map(|v| self.translate_variant_id(v)),
208                                self.translate_field_id(field),
209                            )
210                        }
211                        hax::ConstantProjectionElem::Index(i) => {
212                            ConstProjectionElem::Index(IntegerValue::mk_usize(i as u128))
213                        }
214                        hax::ConstantProjectionElem::Subslice { from, to } => {
215                            ConstProjectionElem::Subslice {
216                                from: IntegerValue::mk_usize(from as u128),
217                                to: IntegerValue::mk_usize(to as u128),
218                            }
219                        }
220                        hax::ConstantProjectionElem::Offset {
221                            count,
222                            ref ty,
223                            in_bounds,
224                            ref pointee_is_sized,
225                        } => ConstProjectionElem::Offset {
226                            count: IntegerValue::Signed(IntTy::Isize, count as i128),
227                            ty: ty
228                                .as_ref()
229                                .map(|ty| self.translate_ty(span, ty))
230                                .transpose()?,
231                            in_bounds,
232                            pointee_is_sized: self
233                                .options
234                                .hide_marker_traits
235                                .then_some(self.translate_trait_proof(span, pointee_is_sized))
236                                .transpose()?
237                                .map(|p| p.no_bound_vars()),
238                        },
239                    };
240                    place = place.project(proj, self.translate_ty(span, proj_ty)?);
241                }
242                let metadata = metadata
243                    .as_ref()
244                    .map(|metadata| self.translate_unsizing_metadata(span, metadata))
245                    .transpose()?;
246                match ty.kind() {
247                    TyKind::RawPtr(_, rk) => ConstantExprKind::Ptr(*rk, place, metadata),
248                    _ => ConstantExprKind::Ref(place, metadata),
249                }
250            }
251            hax::ConstantExprKind::PtrCast(ptr, metadata) => {
252                let ptr = self.translate_constant_expr(span, ptr)?;
253                let kind = if let Some(metadata) = metadata {
254                    let metadata = self.translate_unsizing_metadata(span, metadata)?;
255                    CastKind::Unsize(ty.clone(), metadata, vec![])
256                } else {
257                    CastKind::RawPtr(ty.clone())
258                };
259                ConstantExprKind::Cast(ptr, kind)
260            }
261            hax::ConstantExprKind::ConstRef { id } => {
262                match self.lookup_const_generic_var(span, id) {
263                    Ok(var) => ConstantExprKind::Var(var),
264                    Err(err) => ConstantExprKind::Opaque(err.msg),
265                }
266            }
267            hax::ConstantExprKind::FnDef(item) => {
268                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
269                ConstantExprKind::FnDef(fn_ptr)
270            }
271            hax::ConstantExprKind::FnPtr(target) => {
272                let rustc_sig = match target {
273                    hax::FnPtrTarget::Fn(item) => {
274                        let args = item.rustc_args(self.hax_state_with_id());
275                        let sig = self.tcx.fn_sig(item.def_id.real_rust_def_id());
276                        hax::inst_binder(
277                            self.tcx,
278                            self.hax_state_with_id().typing_env(),
279                            Some(args),
280                            sig,
281                        )
282                    }
283                    hax::FnPtrTarget::ClosureAsFn(closure) => {
284                        let args = closure.item.rustc_args(self.hax_state_with_id());
285                        hax::closure_sig(self.tcx, args.as_closure())
286                    }
287                };
288                let rustc_fn_ptr = ty::Ty::new_fn_ptr(self.tcx, rustc_sig);
289                let source_ty = self.translate_rustc_ty(span, &rustc_fn_ptr)?;
290                let fn_ptr = self.translate_bound_fn_ptr_target(span, target)?;
291                let fn_def = ConstantExpr::new(
292                    ConstantExprKind::FnDef(self.erase_region_binder(fn_ptr.clone())),
293                    TyKind::FnDef(fn_ptr).into_ty(),
294                );
295                let kind = ConstantExprKind::Cast(fn_def, CastKind::FnDefToFnPtr);
296                let (TyKind::FnPtr(source), TyKind::FnPtr(target)) = (source_ty.kind(), ty.kind())
297                else {
298                    unreachable!("expected function pointer types")
299                };
300                if source.skip_binder.is_unsafe != target.skip_binder.is_unsafe {
301                    ConstantExprKind::Cast(
302                        ConstantExpr::new(kind, source_ty),
303                        CastKind::FnPtrToUnsafe,
304                    )
305                } else {
306                    kind
307                }
308            }
309            hax::ConstantExprKind::TypeId(ty) => {
310                ConstantExprKind::TypeId(self.translate_ty(span, ty)?)
311            }
312            hax::ConstantExprKind::Memory(bytes) => {
313                let bytes: Vec<Byte> = bytes
314                    .iter()
315                    .map(|b| self.translate_constant_byte(span, b))
316                    .try_collect()?;
317                ConstantExprKind::RawMemory(bytes)
318            }
319            hax::ConstantExprKind::Todo(msg) => {
320                register_error!(self, span, "Unsupported constant: {:?}", msg);
321                ConstantExprKind::Opaque(msg.into())
322            }
323        };
324
325        Ok(ConstantExpr::new(kind, ty))
326    }
327
328    pub(crate) fn translate_ty_constant_expr(
329        &mut self,
330        span: Span,
331        c: &ty::Const<'tcx>,
332    ) -> Result<ConstantExpr, Error> {
333        let c = self.catch_sinto(span, c)?;
334        self.translate_constant_expr(span, &c)
335    }
336}
charon_driver/translate/translate_constants.rs

charon_driver/translate/
translate_constants.rs
