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 {
113                id,
114                generics,
115                trait_refs,
116                ..
117            } => {
118                trace!(
119                    "\n- generics: {:?}\n- trait_resf: {:?}\n",
120                    generics,
121                    trait_refs
122                );
123                let global_id = self.register_global_decl_id(span, id);
124                let generics = self.translate_generic_args(
125                    span,
126                    generics,
127                    trait_refs,
128                    None,
129                    GenericsSource::item(global_id),
130                )?;
131                RawConstantExpr::Global(GlobalDeclRef {
132                    id: global_id,
133                    generics: Box::new(generics),
134                })
135            }
136            ConstantExprKind::Borrow(v)
137                if let ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
138                    v.contents.as_ref() =>
139            {
140                RawConstantExpr::Literal(Literal::Str(s.clone()))
141            }
142            ConstantExprKind::Borrow(v) => {
143                let val = self.translate_constant_expr_to_constant_expr(span, v)?;
144                RawConstantExpr::Ref(Box::new(val))
145            }
146            ConstantExprKind::Cast { .. } => {
147                register_error!(
148                    self,
149                    span,
150                    "Unsupported constant: `ConstantExprKind::Cast {{..}}`",
151                );
152                RawConstantExpr::Opaque("`ConstantExprKind::Cast {{..}}`".into())
153            }
154            ConstantExprKind::RawBorrow {
155                mutability: false, ..
156            } => {
157                register_error!(
158                    self,
159                    span,
160                    "Unsupported constant: `ConstantExprKind::RawBorrow {{mutability: false, ..}}`",
161                );
162                RawConstantExpr::Opaque(
163                    "ConstantExprKind::RawBorrow {{mutability: false, ..}}".into(),
164                )
165            }
166            ConstantExprKind::RawBorrow {
167                mutability: true,
168                arg,
169            } => {
170                let arg = self.translate_constant_expr_to_constant_expr(span, arg)?;
171                RawConstantExpr::MutPtr(Box::new(arg))
172            }
173            ConstantExprKind::ConstRef { id } => {
174                let var = self.lookup_const_generic_var(span, id)?;
175                RawConstantExpr::Var(var)
176            }
177            ConstantExprKind::FnPtr {
178                def_id: fn_id,
179                generics: substs,
180                generics_impls: trait_refs,
181                method_impl: trait_info,
182            } => {
183                let fn_ptr = self.translate_fn_ptr(span, fn_id, substs, trait_refs, trait_info)?;
184                RawConstantExpr::FnPtr(fn_ptr)
185            }
186            ConstantExprKind::Memory(bytes) => RawConstantExpr::RawMemory(bytes.clone()),
187            ConstantExprKind::Todo(msg) => {
188                register_error!(self, span, "Unsupported constant: {:?}", msg);
189                RawConstantExpr::Opaque(msg.into())
190            }
191        };
192
193        Ok(ConstantExpr { value, ty })
194    }
195
196    /// Remark: [hax::ConstantExpr] contains span information, but it is often
197    /// the default span (i.e., it is useless), hence the additional span argument.
198    pub(crate) fn translate_constant_expr_to_const_generic(
199        &mut self,
200        span: Span,
201        v: &hax::ConstantExpr,
202    ) -> Result<ConstGeneric, Error> {
203        // Remark: we can't user globals as constant generics (meaning
204        // the user provided type annotation should always be none).
205        let value = self
206            .translate_constant_expr_to_constant_expr(span, v)?
207            .value;
208        match value {
209            RawConstantExpr::Var(v) => Ok(ConstGeneric::Var(v)),
210            RawConstantExpr::Literal(v) => Ok(ConstGeneric::Value(v)),
211            RawConstantExpr::Global(global_ref) => {
212                // TODO: handle constant arguments with generics (this can likely only happen with
213                // a feature gate).
214                error_assert!(self, span, global_ref.generics.is_empty());
215                Ok(ConstGeneric::Global(global_ref.id))
216            }
217            RawConstantExpr::Adt(..)
218            | RawConstantExpr::Array { .. }
219            | RawConstantExpr::RawMemory { .. }
220            | RawConstantExpr::TraitConst { .. }
221            | RawConstantExpr::Ref(_)
222            | RawConstantExpr::MutPtr(_)
223            | RawConstantExpr::FnPtr { .. }
224            | RawConstantExpr::Opaque(_) => {
225                raise_error!(self, span, "Unexpected constant generic: {:?}", value)
226            }
227        }
228    }
229}
charon_driver/translate/translate_constants.rs

charon_driver/translate/
translate_constants.rs
