charon_driver/translate/
translate_constants.rs

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

charon_driver/translate/
translate_constants.rs
