charon_driver/translate/
translate_constants.rs

1//! Functions to translate constants to LLBC.
2use rustc_middle::ty;
3
4use crate::translate::translate_bodies::translate_variant_id;
5
6use super::translate_ctx::*;
7use charon_lib::ast::*;
8
9impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
10    fn translate_constant_literal_to_constant_expr_kind(
11        &mut self,
12        span: Span,
13        v: &hax::ConstantLiteral,
14    ) -> Result<ConstantExprKind, Error> {
15        let lit = match v {
16            hax::ConstantLiteral::ByteStr(bs) => Literal::ByteStr(bs.clone()),
17            hax::ConstantLiteral::Str(..) => {
18                // This should have been handled in the `&str` case. If we get here, there's a
19                // `str` value not behind a reference.
20                raise_error!(self, span, "found a `str` constants not behind a reference")
21            }
22            hax::ConstantLiteral::Char(c) => Literal::Char(*c),
23            hax::ConstantLiteral::Bool(b) => Literal::Bool(*b),
24            hax::ConstantLiteral::Int(i) => {
25                use hax::ConstantInt;
26                let scalar = match i {
27                    ConstantInt::Int(v, int_type) => {
28                        let ty = Self::translate_hax_int_ty(int_type);
29                        ScalarValue::Signed(ty, *v)
30                    }
31                    ConstantInt::Uint(v, uint_type) => {
32                        let ty = Self::translate_hax_uint_ty(uint_type);
33                        ScalarValue::Unsigned(ty, *v)
34                    }
35                };
36                Literal::Scalar(scalar)
37            }
38            hax::ConstantLiteral::Float(value, float_type) => {
39                let value = value.clone();
40                let ty = match float_type {
41                    hax::FloatTy::F16 => FloatTy::F16,
42                    hax::FloatTy::F32 => FloatTy::F32,
43                    hax::FloatTy::F64 => FloatTy::F64,
44                    hax::FloatTy::F128 => FloatTy::F128,
45                };
46                Literal::Float(FloatValue { value, ty })
47            }
48            hax::ConstantLiteral::PtrNoProvenance(v) => {
49                return Ok(ConstantExprKind::PtrNoProvenance(*v));
50            }
51        };
52        Ok(ConstantExprKind::Literal(lit))
53    }
54
55    /// Remark: [hax::ConstantExpr] contains span information, but it is often
56    /// the default span (i.e., it is useless), hence the additional span argument.
57    /// TODO: the user_ty might be None because hax doesn't extract it (because
58    /// we are translating a [ConstantExpr] instead of a Constant. We need to
59    /// update hax.
60    pub(crate) fn translate_constant_expr(
61        &mut self,
62        span: Span,
63        v: &hax::ConstantExpr,
64    ) -> Result<ConstantExpr, Error> {
65        let ty = self.translate_ty(span, &v.ty)?;
66        let kind = match v.contents.as_ref() {
67            hax::ConstantExprKind::Literal(lit) => {
68                self.translate_constant_literal_to_constant_expr_kind(span, lit)?
69            }
70            hax::ConstantExprKind::Adt { kind, fields } => {
71                let fields: Vec<ConstantExpr> = fields
72                    .iter()
73                    .map(|f| self.translate_constant_expr(span, &f.value))
74                    .try_collect()?;
75                use hax::VariantKind;
76                let vid = if let VariantKind::Enum { index, .. } = *kind {
77                    Some(translate_variant_id(index))
78                } else {
79                    None
80                };
81                ConstantExprKind::Adt(vid, fields)
82            }
83            hax::ConstantExprKind::Array { fields } => {
84                let fields: Vec<ConstantExpr> = fields
85                    .iter()
86                    .map(|x| self.translate_constant_expr(span, x))
87                    .try_collect()?;
88
89                if matches!(v.ty.kind(), hax::TyKind::Slice { .. }) {
90                    ConstantExprKind::Slice(fields)
91                } else {
92                    ConstantExprKind::Array(fields)
93                }
94            }
95            hax::ConstantExprKind::Tuple { fields } => {
96                let fields: Vec<ConstantExpr> = fields
97                    .iter()
98                    // TODO: the user_ty is not always None
99                    .map(|f| self.translate_constant_expr(span, f))
100                    .try_collect()?;
101                ConstantExprKind::Adt(None, fields)
102            }
103            hax::ConstantExprKind::NamedGlobal(item) => match &item.in_trait {
104                Some(impl_expr) => {
105                    let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
106                    // Trait consts can't have their own generics.
107                    assert!(item.generic_args.is_empty());
108                    let name = self.translate_trait_item_name(&item.def_id)?;
109                    ConstantExprKind::TraitConst(trait_ref, name)
110                }
111                None => {
112                    let global_ref = self.translate_global_decl_ref(span, item)?;
113                    ConstantExprKind::Global(global_ref)
114                }
115            },
116            hax::ConstantExprKind::Borrow(v)
117                if let hax::ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
118                    v.contents.as_ref() =>
119            {
120                ConstantExprKind::Literal(Literal::Str(s.clone()))
121            }
122            hax::ConstantExprKind::Borrow(v) => {
123                let val = self.translate_constant_expr(span, v)?;
124                ConstantExprKind::Ref(Box::new(val))
125            }
126            hax::ConstantExprKind::Cast { .. } => {
127                register_error!(
128                    self,
129                    span,
130                    "Unsupported constant: `ConstantExprKind::Cast {{..}}`",
131                );
132                ConstantExprKind::Opaque("`ConstantExprKind::Cast {{..}}`".into())
133            }
134            hax::ConstantExprKind::RawBorrow { mutability, arg } => {
135                let arg = self.translate_constant_expr(span, arg)?;
136                let rk = RefKind::mutable(mutability.is_mut());
137                ConstantExprKind::Ptr(rk, Box::new(arg))
138            }
139            hax::ConstantExprKind::ConstRef { id } => {
140                match self.lookup_const_generic_var(span, id) {
141                    Ok(var) => ConstantExprKind::Var(var),
142                    Err(err) => ConstantExprKind::Opaque(err.msg),
143                }
144            }
145            hax::ConstantExprKind::FnDef(item) => {
146                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
147                ConstantExprKind::FnDef(fn_ptr)
148            }
149            hax::ConstantExprKind::FnPtr(item) => {
150                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
151                ConstantExprKind::FnPtr(fn_ptr)
152            }
153            hax::ConstantExprKind::Memory(bytes) => {
154                ConstantExprKind::RawMemory(bytes.iter().map(|b| Byte::Value(*b)).collect())
155            }
156            hax::ConstantExprKind::Todo(msg) => {
157                register_error!(self, span, "Unsupported constant: {:?}", msg);
158                ConstantExprKind::Opaque(msg.into())
159            }
160        };
161
162        Ok(ConstantExpr { kind, ty })
163    }
164
165    pub(crate) fn translate_ty_constant_expr(
166        &mut self,
167        span: Span,
168        c: &ty::Const<'tcx>,
169    ) -> Result<ConstantExpr, Error> {
170        let c = self.catch_sinto(span, c)?;
171        self.translate_constant_expr(span, &c)
172    }
173}
charon_driver/translate/translate_constants.rs

charon_driver/translate/
translate_constants.rs
