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        let ty = self.translate_ty(span, &v.ty)?;
62        let kind = match v.contents.as_ref() {
63            hax::ConstantExprKind::Literal(lit) => {
64                self.translate_constant_literal_to_constant_expr_kind(span, lit)?
65            }
66            hax::ConstantExprKind::Adt { info, fields } => {
67                let fields: Vec<ConstantExpr> = fields
68                    .iter()
69                    .map(|f| self.translate_constant_expr_to_constant_expr(span, &f.value))
70                    .try_collect()?;
71                use hax::VariantKind;
72                let vid = if let VariantKind::Enum { index, .. } = info.kind {
73                    Some(VariantId::new(index))
74                } else {
75                    None
76                };
77                ConstantExprKind::Adt(vid, fields)
78            }
79            hax::ConstantExprKind::Array { fields } => {
80                let fields: Vec<ConstantExpr> = fields
81                    .iter()
82                    .map(|x| self.translate_constant_expr_to_constant_expr(span, x))
83                    .try_collect()?;
84
85                if matches!(v.ty.kind(), hax::TyKind::Slice { .. }) {
86                    ConstantExprKind::Slice(fields)
87                } else {
88                    ConstantExprKind::Array(fields)
89                }
90            }
91            hax::ConstantExprKind::Tuple { fields } => {
92                let fields: Vec<ConstantExpr> = fields
93                    .iter()
94                    // TODO: the user_ty is not always None
95                    .map(|f| self.translate_constant_expr_to_constant_expr(span, f))
96                    .try_collect()?;
97                ConstantExprKind::Adt(None, fields)
98            }
99            hax::ConstantExprKind::NamedGlobal(item) => match &item.in_trait {
100                Some(impl_expr) => {
101                    let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
102                    // Trait consts can't have their own generics.
103                    assert!(item.generic_args.is_empty());
104                    let name = self.translate_trait_item_name(&item.def_id)?;
105                    ConstantExprKind::TraitConst(trait_ref, name)
106                }
107                None => {
108                    let global_ref = self.translate_global_decl_ref(span, item)?;
109                    ConstantExprKind::Global(global_ref)
110                }
111            },
112            hax::ConstantExprKind::Borrow(v)
113                if let hax::ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
114                    v.contents.as_ref() =>
115            {
116                ConstantExprKind::Literal(Literal::Str(s.clone()))
117            }
118            hax::ConstantExprKind::Borrow(v) => {
119                let val = self.translate_constant_expr_to_constant_expr(span, v)?;
120                ConstantExprKind::Ref(Box::new(val))
121            }
122            hax::ConstantExprKind::Cast { .. } => {
123                register_error!(
124                    self,
125                    span,
126                    "Unsupported constant: `ConstantExprKind::Cast {{..}}`",
127                );
128                ConstantExprKind::Opaque("`ConstantExprKind::Cast {{..}}`".into())
129            }
130            hax::ConstantExprKind::RawBorrow { mutability, arg } => {
131                let arg = self.translate_constant_expr_to_constant_expr(span, arg)?;
132                let rk = RefKind::mutable(*mutability);
133                ConstantExprKind::Ptr(rk, Box::new(arg))
134            }
135            hax::ConstantExprKind::ConstRef { id } => {
136                match self.lookup_const_generic_var(span, id) {
137                    Ok(var) => ConstantExprKind::Var(var),
138                    Err(err) => ConstantExprKind::Opaque(err.msg),
139                }
140            }
141            hax::ConstantExprKind::FnDef(item) => {
142                let fn_ptr = self
143                    .translate_fn_ptr(span, item, TransItemSourceKind::Fun)?
144                    .erase();
145                ConstantExprKind::FnDef(fn_ptr)
146            }
147            hax::ConstantExprKind::FnPtr(item) => {
148                let fn_ptr = self
149                    .translate_fn_ptr(span, item, TransItemSourceKind::Fun)?
150                    .erase();
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    /// Remark: [hax::ConstantExpr] contains span information, but it is often
166    /// the default span (i.e., it is useless), hence the additional span argument.
167    pub(crate) fn translate_constant_expr_to_const_generic(
168        &mut self,
169        span: Span,
170        v: &hax::ConstantExpr,
171    ) -> Result<ConstGeneric, Error> {
172        // Remark: we can't user globals as constant generics (meaning
173        // the user provided type annotation should always be none).
174        let kind = self.translate_constant_expr_to_constant_expr(span, v)?.kind;
175        match kind {
176            ConstantExprKind::Var(v) => Ok(ConstGeneric::Var(v)),
177            ConstantExprKind::Literal(v) => Ok(ConstGeneric::Value(v)),
178            ConstantExprKind::Global(global_ref) => {
179                // TODO: handle constant arguments with generics (this can likely only happen with
180                // a feature gate).
181                error_assert!(self, span, global_ref.generics.is_empty());
182                Ok(ConstGeneric::Global(global_ref.id))
183            }
184            ConstantExprKind::Adt(..)
185            | ConstantExprKind::Array { .. }
186            | ConstantExprKind::Slice { .. }
187            | ConstantExprKind::RawMemory { .. }
188            | ConstantExprKind::TraitConst { .. }
189            | ConstantExprKind::Ref(_)
190            | ConstantExprKind::Ptr(..)
191            | ConstantExprKind::FnPtr { .. }
192            | ConstantExprKind::FnDef { .. }
193            | ConstantExprKind::Opaque(_)
194            | ConstantExprKind::PtrNoProvenance(..) => {
195                raise_error!(self, span, "Unexpected constant generic: {:?}", kind)
196            }
197        }
198    }
199}
charon_driver/translate/translate_constants.rs

charon_driver/translate/
translate_constants.rs
