charon_driver/translate/
translate_constants.rs

1//! Functions to translate constants to LLBC.
2use rustc_middle::ty;
3
4use crate::translate::translate_bodies::translate_variant_id;
5
6use super::translate_ctx::*;
7use charon_lib::ast::*;
8
9impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
10    fn translate_constant_literal_to_constant_expr_kind(
11        &mut self,
12        _span: Span,
13        v: &hax::ConstantLiteral,
14    ) -> Result<ConstantExprKind, Error> {
15        let lit = match v {
16            hax::ConstantLiteral::ByteStr(bs) => Literal::ByteStr(bs.clone()),
17            hax::ConstantLiteral::Str(str) => {
18                // We should only get here if we actually want to translate the data
19                // backing the string, when we represent strings as unsized [u8]s
20                assert!(self.t_ctx.options.unsized_strings);
21
22                let str_bytes = str.as_bytes();
23                return Ok(ConstantExprKind::RawMemory(
24                    str_bytes.iter().map(|b| Byte::Value(*b)).collect(),
25                ));
26            }
27            hax::ConstantLiteral::Char(c) => Literal::Char(*c),
28            hax::ConstantLiteral::Bool(b) => Literal::Bool(*b),
29            hax::ConstantLiteral::Int(i) => {
30                use hax::ConstantInt;
31                let scalar = match i {
32                    ConstantInt::Int(v, int_type) => {
33                        let ty = Self::translate_hax_int_ty(int_type);
34                        ScalarValue::Signed(ty, *v)
35                    }
36                    ConstantInt::Uint(v, uint_type) => {
37                        let ty = Self::translate_hax_uint_ty(uint_type);
38                        ScalarValue::Unsigned(ty, *v)
39                    }
40                };
41                Literal::Scalar(scalar)
42            }
43            hax::ConstantLiteral::Float(value, float_type) => {
44                let value = value.clone();
45                let ty = match float_type {
46                    hax::FloatTy::F16 => FloatTy::F16,
47                    hax::FloatTy::F32 => FloatTy::F32,
48                    hax::FloatTy::F64 => FloatTy::F64,
49                    hax::FloatTy::F128 => FloatTy::F128,
50                };
51                Literal::Float(FloatValue { value, ty })
52            }
53            hax::ConstantLiteral::PtrNoProvenance(v) => {
54                return Ok(ConstantExprKind::PtrNoProvenance(*v));
55            }
56        };
57        Ok(ConstantExprKind::Literal(lit))
58    }
59
60    /// Remark: [hax::ConstantExpr] contains span information, but it is often
61    /// the default span (i.e., it is useless), hence the additional span argument.
62    /// TODO: the user_ty might be None because hax doesn't extract it (because
63    /// we are translating a [ConstantExpr] instead of a Constant. We need to
64    /// update hax.
65    pub(crate) fn translate_constant_expr(
66        &mut self,
67        span: Span,
68        v: &hax::ConstantExpr,
69    ) -> Result<ConstantExpr, Error> {
70        let ty = self.translate_ty(span, &v.ty)?;
71        let kind = match v.contents.as_ref() {
72            hax::ConstantExprKind::Literal(lit) => {
73                self.translate_constant_literal_to_constant_expr_kind(span, lit)?
74            }
75            hax::ConstantExprKind::Adt { kind, fields } => {
76                let fields: Vec<ConstantExpr> = fields
77                    .iter()
78                    .map(|f| self.translate_constant_expr(span, &f.value))
79                    .try_collect()?;
80                use hax::VariantKind;
81                let vid = if let VariantKind::Enum { index, .. } = *kind {
82                    Some(translate_variant_id(index))
83                } else {
84                    None
85                };
86                ConstantExprKind::Adt(vid, fields)
87            }
88            hax::ConstantExprKind::Array { fields } => {
89                let fields: Vec<ConstantExpr> = fields
90                    .iter()
91                    .map(|x| self.translate_constant_expr(span, x))
92                    .try_collect()?;
93
94                ConstantExprKind::Array(fields)
95            }
96            hax::ConstantExprKind::Tuple { fields } => {
97                let fields: Vec<ConstantExpr> = fields
98                    .iter()
99                    // TODO: the user_ty is not always None
100                    .map(|f| self.translate_constant_expr(span, f))
101                    .try_collect()?;
102                ConstantExprKind::Adt(None, fields)
103            }
104            hax::ConstantExprKind::NamedGlobal(item) => match &item.in_trait {
105                Some(impl_expr) => {
106                    let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
107                    // Trait consts can't have their own generics.
108                    assert!(item.generic_args.is_empty());
109                    let name = self.translate_trait_item_name(&item.def_id)?;
110                    ConstantExprKind::TraitConst(trait_ref, name)
111                }
112                None => {
113                    let global_ref = self.translate_global_decl_ref(span, item)?;
114                    ConstantExprKind::Global(global_ref)
115                }
116            },
117            hax::ConstantExprKind::Borrow(v)
118                if let hax::ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
119                    v.contents.as_ref()
120                    && !self.t_ctx.options.unsized_strings =>
121            {
122                ConstantExprKind::Literal(Literal::Str(s.clone()))
123            }
124
125            hax::ConstantExprKind::Borrow(v) => {
126                let mut val = self.translate_constant_expr(span, v)?;
127                let metadata = match (v.contents.as_ref(), val.ty.kind()) {
128                    (hax::ConstantExprKind::Array { fields }, TyKind::Slice(subty)) => {
129                        let len = ConstantExpr::mk_usize(ScalarValue::Unsigned(
130                            UIntTy::Usize,
131                            fields.len() as u128,
132                        ));
133                        // the sub-constant is an array, that has it's reference unsized
134                        val.ty = Ty::mk_array(subty.clone(), len.clone());
135                        Some(UnsizingMetadata::Length(Box::new(len)))
136                    }
137
138                    (hax::ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)), _) => {
139                        let len = ConstantExpr::mk_usize(ScalarValue::Unsigned(
140                            UIntTy::Usize,
141                            s.len() as u128,
142                        ));
143                        // the sub-constant is an array, that has it's reference unsized
144                        let subty = TyKind::Literal(LiteralTy::UInt(UIntTy::U8)).into();
145                        val.ty = Ty::mk_array(subty, len.clone());
146                        Some(UnsizingMetadata::Length(Box::new(len)))
147                    }
148
149                    _ => None,
150                };
151                ConstantExprKind::Ref(Box::new(val), metadata)
152            }
153            hax::ConstantExprKind::Cast { .. } => {
154                register_error!(
155                    self,
156                    span,
157                    "Unsupported constant: `ConstantExprKind::Cast {{..}}`",
158                );
159                ConstantExprKind::Opaque("`ConstantExprKind::Cast {{..}}`".into())
160            }
161            hax::ConstantExprKind::RawBorrow { mutability, arg } => {
162                let arg = self.translate_constant_expr(span, arg)?;
163                let rk = RefKind::mutable(mutability.is_mut());
164                ConstantExprKind::Ptr(rk, Box::new(arg), None)
165            }
166            hax::ConstantExprKind::ConstRef { id } => {
167                match self.lookup_const_generic_var(span, id) {
168                    Ok(var) => ConstantExprKind::Var(var),
169                    Err(err) => ConstantExprKind::Opaque(err.msg),
170                }
171            }
172            hax::ConstantExprKind::FnDef(item) => {
173                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
174                ConstantExprKind::FnDef(fn_ptr)
175            }
176            hax::ConstantExprKind::FnPtr(item) => {
177                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
178                ConstantExprKind::FnPtr(fn_ptr)
179            }
180            hax::ConstantExprKind::Memory(bytes) => {
181                ConstantExprKind::RawMemory(bytes.iter().map(|b| Byte::Value(*b)).collect())
182            }
183            hax::ConstantExprKind::Todo(msg) => {
184                register_error!(self, span, "Unsupported constant: {:?}", msg);
185                ConstantExprKind::Opaque(msg.into())
186            }
187        };
188
189        Ok(ConstantExpr { kind, ty })
190    }
191
192    pub(crate) fn translate_ty_constant_expr(
193        &mut self,
194        span: Span,
195        c: &ty::Const<'tcx>,
196    ) -> Result<ConstantExpr, Error> {
197        let c = self.catch_sinto(span, c)?;
198        self.translate_constant_expr(span, &c)
199    }
200}
charon_driver/translate/translate_constants.rs

charon_driver/translate/
translate_constants.rs
