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                        use hax::IntTy;
26                        match int_type {
27                            IntTy::Isize => ScalarValue::Isize(*v as i64),
28                            IntTy::I8 => ScalarValue::I8(*v as i8),
29                            IntTy::I16 => ScalarValue::I16(*v as i16),
30                            IntTy::I32 => ScalarValue::I32(*v as i32),
31                            IntTy::I64 => ScalarValue::I64(*v as i64),
32                            IntTy::I128 => ScalarValue::I128(*v),
33                        }
34                    }
35                    ConstantInt::Uint(v, int_type) => {
36                        use hax::UintTy;
37                        match int_type {
38                            UintTy::Usize => ScalarValue::Usize(*v as u64),
39                            UintTy::U8 => ScalarValue::U8(*v as u8),
40                            UintTy::U16 => ScalarValue::U16(*v as u16),
41                            UintTy::U32 => ScalarValue::U32(*v as u32),
42                            UintTy::U64 => ScalarValue::U64(*v as u64),
43                            UintTy::U128 => ScalarValue::U128(*v),
44                        }
45                    }
46                };
47                Literal::Scalar(scalar)
48            }
49            hax::ConstantLiteral::Float(value, float_type) => {
50                let value = value.clone();
51                let ty = match float_type {
52                    hax::FloatTy::F16 => FloatTy::F16,
53                    hax::FloatTy::F32 => FloatTy::F32,
54                    hax::FloatTy::F64 => FloatTy::F64,
55                    hax::FloatTy::F128 => FloatTy::F128,
56                };
57                Literal::Float(FloatValue { value, ty })
58            }
59        };
60        Ok(RawConstantExpr::Literal(lit))
61    }
62
63    /// Remark: [hax::ConstantExpr] contains span information, but it is often
64    /// the default span (i.e., it is useless), hence the additional span argument.
65    /// TODO: the user_ty might be None because hax doesn't extract it (because
66    /// we are translating a [ConstantExpr] instead of a Constant. We need to
67    /// update hax.
68    pub(crate) fn translate_constant_expr_to_constant_expr(
69        &mut self,
70        span: Span,
71        v: &hax::ConstantExpr,
72    ) -> Result<ConstantExpr, Error> {
73        use hax::ConstantExprKind;
74        let ty = self.translate_ty(span, &v.ty)?;
75        let value = match v.contents.as_ref() {
76            ConstantExprKind::Literal(lit) => {
77                self.translate_constant_literal_to_raw_constant_expr(span, lit)?
78            }
79            ConstantExprKind::Adt { info, fields } => {
80                let fields: Vec<ConstantExpr> = fields
81                    .iter()
82                    .map(|f| self.translate_constant_expr_to_constant_expr(span, &f.value))
83                    .try_collect()?;
84                use hax::VariantKind;
85                let vid = if let VariantKind::Enum { index, .. } = info.kind {
86                    Some(VariantId::new(index))
87                } else {
88                    None
89                };
90                RawConstantExpr::Adt(vid, fields)
91            }
92            ConstantExprKind::Array { fields } => {
93                let fields: Vec<ConstantExpr> = fields
94                    .iter()
95                    .map(|x| self.translate_constant_expr_to_constant_expr(span, x))
96                    .try_collect()?;
97                RawConstantExpr::Array(fields)
98            }
99            ConstantExprKind::Tuple { fields } => {
100                let fields: Vec<ConstantExpr> = fields
101                    .iter()
102                    // TODO: the user_ty is not always None
103                    .map(|f| self.translate_constant_expr_to_constant_expr(span, f))
104                    .try_collect()?;
105                RawConstantExpr::Adt(None, fields)
106            }
107            ConstantExprKind::TraitConst { impl_expr, name } => {
108                let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
109                let name = TraitItemName(name.clone());
110                RawConstantExpr::TraitConst(trait_ref, name)
111            }
112            ConstantExprKind::GlobalName(item) => {
113                let global_ref = self.translate_global_decl_ref(span, item)?;
114                RawConstantExpr::Global(global_ref)
115            }
116            ConstantExprKind::Borrow(v)
117                if let ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
118                    v.contents.as_ref() =>
119            {
120                RawConstantExpr::Literal(Literal::Str(s.clone()))
121            }
122            ConstantExprKind::Borrow(v) => {
123                let val = self.translate_constant_expr_to_constant_expr(span, v)?;
124                RawConstantExpr::Ref(Box::new(val))
125            }
126            ConstantExprKind::Cast { .. } => {
127                register_error!(
128                    self,
129                    span,
130                    "Unsupported constant: `ConstantExprKind::Cast {{..}}`",
131                );
132                RawConstantExpr::Opaque("`ConstantExprKind::Cast {{..}}`".into())
133            }
134            ConstantExprKind::RawBorrow { mutability, arg } => {
135                let arg = self.translate_constant_expr_to_constant_expr(span, arg)?;
136                let rk = RefKind::mutable(*mutability);
137                RawConstantExpr::Ptr(rk, Box::new(arg))
138            }
139            ConstantExprKind::ConstRef { id } => {
140                let var = self.lookup_const_generic_var(span, id)?;
141                RawConstantExpr::Var(var)
142            }
143            ConstantExprKind::FnPtr(item) => {
144                let fn_ptr = self.translate_fn_ptr(span, item)?.erase();
145                RawConstantExpr::FnPtr(fn_ptr)
146            }
147            ConstantExprKind::Memory(bytes) => RawConstantExpr::RawMemory(bytes.clone()),
148            ConstantExprKind::Todo(msg) => {
149                register_error!(self, span, "Unsupported constant: {:?}", msg);
150                RawConstantExpr::Opaque(msg.into())
151            }
152        };
153
154        Ok(ConstantExpr { value, ty })
155    }
156
157    /// Remark: [hax::ConstantExpr] contains span information, but it is often
158    /// the default span (i.e., it is useless), hence the additional span argument.
159    pub(crate) fn translate_constant_expr_to_const_generic(
160        &mut self,
161        span: Span,
162        v: &hax::ConstantExpr,
163    ) -> Result<ConstGeneric, Error> {
164        // Remark: we can't user globals as constant generics (meaning
165        // the user provided type annotation should always be none).
166        let value = self
167            .translate_constant_expr_to_constant_expr(span, v)?
168            .value;
169        match value {
170            RawConstantExpr::Var(v) => Ok(ConstGeneric::Var(v)),
171            RawConstantExpr::Literal(v) => Ok(ConstGeneric::Value(v)),
172            RawConstantExpr::Global(global_ref) => {
173                // TODO: handle constant arguments with generics (this can likely only happen with
174                // a feature gate).
175                error_assert!(self, span, global_ref.generics.is_empty());
176                Ok(ConstGeneric::Global(global_ref.id))
177            }
178            RawConstantExpr::Adt(..)
179            | RawConstantExpr::Array { .. }
180            | RawConstantExpr::RawMemory { .. }
181            | RawConstantExpr::TraitConst { .. }
182            | RawConstantExpr::Ref(_)
183            | RawConstantExpr::Ptr(..)
184            | RawConstantExpr::FnPtr { .. }
185            | RawConstantExpr::Opaque(_) => {
186                raise_error!(self, span, "Unexpected constant generic: {:?}", value)
187            }
188        }
189    }
190}
charon_driver/translate/translate_constants.rs

charon_driver/translate/
translate_constants.rs
