charon_driver/translate/
translate_constants.rs

1//! Functions to translate constants to LLBC.
2use crate::hax;
3use rustc_middle::ty;
4
5use super::translate_ctx::*;
6use charon_lib::ast::*;
7
8impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
9    fn translate_constant_literal_to_constant_expr_kind(
10        &mut self,
11        _span: Span,
12        v: &hax::ConstantLiteral,
13    ) -> Result<ConstantExprKind, Error> {
14        let lit = match v {
15            hax::ConstantLiteral::ByteStr(bs) => Literal::ByteStr(bs.clone()),
16            hax::ConstantLiteral::Str(str) => {
17                // We should only get here if we actually want to translate the data
18                // backing the string, when we represent strings as unsized [u8]s
19                assert!(self.t_ctx.options.unsized_strings);
20
21                let str_bytes = str.as_bytes();
22                return Ok(ConstantExprKind::RawMemory(
23                    str_bytes.iter().map(|b| Byte::Value(*b)).collect(),
24                ));
25            }
26            hax::ConstantLiteral::Char(c) => Literal::Char(*c),
27            hax::ConstantLiteral::Bool(b) => Literal::Bool(*b),
28            hax::ConstantLiteral::Int(i) => {
29                use crate::hax::ConstantInt;
30                let scalar = match i {
31                    ConstantInt::Int(v, int_type) => {
32                        let ty = Self::translate_hax_int_ty(int_type);
33                        ScalarValue::Signed(ty, *v)
34                    }
35                    ConstantInt::Uint(v, uint_type) => {
36                        let ty = Self::translate_hax_uint_ty(uint_type);
37                        ScalarValue::Unsigned(ty, *v)
38                    }
39                };
40                Literal::Scalar(scalar)
41            }
42            hax::ConstantLiteral::Float(value, float_type) => {
43                let value = value.clone();
44                let ty = match float_type {
45                    hax::FloatTy::F16 => FloatTy::F16,
46                    hax::FloatTy::F32 => FloatTy::F32,
47                    hax::FloatTy::F64 => FloatTy::F64,
48                    hax::FloatTy::F128 => FloatTy::F128,
49                };
50                Literal::Float(FloatValue { value, ty })
51            }
52            hax::ConstantLiteral::PtrNoProvenance(v) => {
53                return Ok(ConstantExprKind::PtrNoProvenance(*v));
54            }
55        };
56        Ok(ConstantExprKind::Literal(lit))
57    }
58
59    /// Remark: [hax::ConstantExpr] contains span information, but it is often
60    /// the default span (i.e., it is useless), hence the additional span argument.
61    /// TODO: the user_ty might be None because hax doesn't extract it (because
62    /// we are translating a [ConstantExpr] instead of a Constant. We need to
63    /// update hax.
64    pub(crate) fn translate_constant_expr(
65        &mut self,
66        span: Span,
67        v: &hax::ConstantExpr,
68    ) -> Result<ConstantExpr, Error> {
69        let ty = self.translate_ty(span, &v.ty)?;
70        let kind = match v.contents.as_ref() {
71            hax::ConstantExprKind::Literal(lit) => {
72                self.translate_constant_literal_to_constant_expr_kind(span, lit)?
73            }
74            hax::ConstantExprKind::Adt { kind, fields } => {
75                let fields: Vec<ConstantExpr> = fields
76                    .iter()
77                    .map(|f| self.translate_constant_expr(span, &f.value))
78                    .try_collect()?;
79                use crate::hax::VariantKind;
80                let vid = if let VariantKind::Enum { index, .. } = *kind {
81                    Some(self.translate_variant_id(index))
82                } else {
83                    None
84                };
85                ConstantExprKind::Adt(vid, fields)
86            }
87            hax::ConstantExprKind::Array { fields } => {
88                let fields: Vec<ConstantExpr> = fields
89                    .iter()
90                    .map(|x| self.translate_constant_expr(span, x))
91                    .try_collect()?;
92
93                ConstantExprKind::Array(fields)
94            }
95            hax::ConstantExprKind::Tuple { fields } => {
96                let fields: Vec<ConstantExpr> = fields
97                    .iter()
98                    // TODO: the user_ty is not always None
99                    .map(|f| self.translate_constant_expr(span, f))
100                    .try_collect()?;
101                ConstantExprKind::Adt(None, fields)
102            }
103            hax::ConstantExprKind::NamedGlobal(item) => match &item.in_trait {
104                Some(impl_expr) => {
105                    let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
106                    // Trait consts can't have their own generics.
107                    assert!(item.generic_args.is_empty());
108                    let const_id =
109                        self.translate_assoc_const_id(trait_ref.trait_id(), &item.def_id)?;
110                    ConstantExprKind::TraitConst(trait_ref, const_id)
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
