charon_driver/translate/
translate_constants.rs

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

charon_driver/translate/
translate_constants.rs
