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        Ok(match v {
15            hax::ConstantLiteral::ByteStr(bs) => ConstantExprKind::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) => ConstantExprKind::Char(*c),
27            hax::ConstantLiteral::Bool(b) => ConstantExprKind::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                        IntegerValue::Signed(ty, *v)
34                    }
35                    ConstantInt::Uint(v, uint_type) => {
36                        let ty = Self::translate_hax_uint_ty(uint_type);
37                        IntegerValue::Unsigned(ty, *v)
38                    }
39                };
40                ConstantExprKind::Integer(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                ConstantExprKind::Float(FloatValue { value, ty })
51            }
52            hax::ConstantLiteral::PtrNoProvenance(v) => {
53                return Ok(ConstantExprKind::PtrNoProvenance(*v));
54            }
55        })
56    }
57
58    /// Remark: [hax::ConstantExpr] contains span information, but it is often
59    /// the default span (i.e., it is useless), hence the additional span argument.
60    /// TODO: the user_ty might be None because hax doesn't extract it (because
61    /// we are translating a [ConstantExpr] instead of a Constant. We need to
62    /// update hax.
63    pub(crate) fn translate_constant_expr(
64        &mut self,
65        span: Span,
66        v: &hax::ConstantExpr,
67    ) -> Result<ConstantExpr, Error> {
68        let ty = self.translate_ty(span, &v.ty)?;
69        let kind = match v.contents.as_ref() {
70            hax::ConstantExprKind::Literal(lit) => {
71                self.translate_constant_literal_to_constant_expr_kind(span, lit)?
72            }
73            hax::ConstantExprKind::Adt { kind, fields } => {
74                let fields: Vec<ConstantExpr> = fields
75                    .iter()
76                    .map(|f| self.translate_constant_expr(span, &f.value))
77                    .try_collect()?;
78                use crate::hax::VariantKind;
79                let vid = if let VariantKind::Enum { index, .. } = *kind {
80                    Some(self.translate_variant_id(index))
81                } else {
82                    None
83                };
84                ConstantExprKind::Adt(vid, fields)
85            }
86            hax::ConstantExprKind::Array { fields } => {
87                let fields: Vec<ConstantExpr> = fields
88                    .iter()
89                    .map(|x| self.translate_constant_expr(span, x))
90                    .try_collect()?;
91
92                ConstantExprKind::Array(fields)
93            }
94            hax::ConstantExprKind::Tuple { fields } => {
95                let fields: Vec<ConstantExpr> = fields
96                    .iter()
97                    // TODO: the user_ty is not always None
98                    .map(|f| self.translate_constant_expr(span, f))
99                    .try_collect()?;
100                ConstantExprKind::Adt(None, fields)
101            }
102            hax::ConstantExprKind::NamedGlobal(item) => match &item.in_trait {
103                Some(trait_proof) => {
104                    let trait_ref = self.translate_trait_proof(span, trait_proof)?;
105                    // Trait consts can't have their own generics.
106                    assert!(item.generic_args.is_empty());
107                    let const_id =
108                        self.translate_assoc_const_id(trait_ref.trait_id(), &item.def_id)?;
109                    ConstantExprKind::TraitConst(trait_ref, const_id)
110                }
111                None => {
112                    let global_ref = self.translate_global_decl_ref(span, item)?;
113                    ConstantExprKind::Global(global_ref)
114                }
115            },
116            hax::ConstantExprKind::Borrow(v)
117                if let hax::ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
118                    v.contents.as_ref()
119                    && !self.t_ctx.options.unsized_strings =>
120            {
121                ConstantExprKind::Str(s.clone())
122            }
123
124            hax::ConstantExprKind::Borrow(v) => {
125                let mut val = self.translate_constant_expr(span, v)?;
126                let (metadata, new_ty) = match (v.contents.as_ref(), val.ty().kind()) {
127                    (
128                        hax::ConstantExprKind::Array { fields },
129                        TyKind::Slice(subty, ty_is_sized),
130                    ) => {
131                        let len = ConstantExpr::mk_usize(fields.len() as u128);
132                        // the sub-constant is an array, that has it's reference unsized
133                        (
134                            Some(UnsizingMetadata::Length(len.clone())),
135                            Some(Ty::mk_array(subty.clone(), len, ty_is_sized.clone())),
136                        )
137                    }
138
139                    (hax::ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)), _) => {
140                        let len = ConstantExpr::mk_usize(s.len() as u128);
141                        let ty_is_sized = self.translate_sized_proof(span, self.tcx.types.u8)?;
142                        // the sub-constant is an array, that has it's reference unsized
143                        let subty =
144                            TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U8)))
145                                .into();
146                        (
147                            Some(UnsizingMetadata::Length(len.clone())),
148                            Some(Ty::mk_array(subty, len, ty_is_sized)),
149                        )
150                    }
151
152                    _ => (None, None),
153                };
154                if let Some(new_ty) = new_ty {
155                    val.with_contents_mut(|_, ty| *ty = new_ty);
156                }
157                ConstantExprKind::Ref(val, metadata)
158            }
159            hax::ConstantExprKind::RawBorrow { mutability, arg } => {
160                let arg = self.translate_constant_expr(span, arg)?;
161                let rk = RefKind::mutable(mutability.is_mut());
162                ConstantExprKind::Ptr(rk, arg, None)
163            }
164            hax::ConstantExprKind::ConstRef { id } => {
165                match self.lookup_const_generic_var(span, id) {
166                    Ok(var) => ConstantExprKind::Var(var),
167                    Err(err) => ConstantExprKind::Opaque(err.msg),
168                }
169            }
170            hax::ConstantExprKind::FnDef(item) => {
171                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
172                ConstantExprKind::FnDef(fn_ptr)
173            }
174            hax::ConstantExprKind::FnPtr(item) => {
175                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
176                ConstantExprKind::FnPtr(fn_ptr)
177            }
178            hax::ConstantExprKind::Memory(bytes) => {
179                ConstantExprKind::RawMemory(bytes.iter().map(|b| Byte::Value(*b)).collect())
180            }
181            hax::ConstantExprKind::Todo(msg) => {
182                register_error!(self, span, "Unsupported constant: {:?}", msg);
183                ConstantExprKind::Opaque(msg.into())
184            }
185        };
186
187        Ok(ConstantExpr::new(kind, ty))
188    }
189
190    pub(crate) fn translate_ty_constant_expr(
191        &mut self,
192        span: Span,
193        c: &ty::Const<'tcx>,
194    ) -> Result<ConstantExpr, Error> {
195        let c = self.catch_sinto(span, c)?;
196        self.translate_constant_expr(span, &c)
197    }
198
199    /// Evaluates a constant definition and returns the result as a [`ConstantExpr`], if one exists.
200    pub(crate) fn evaluate_const_def(
201        &mut self,
202        def: &hax::FullDef<'tcx>,
203    ) -> Option<hax::Decorated<hax::ConstantExprKind>> {
204        match def.kind() {
205            hax::FullDefKind::Const { .. } | hax::FullDefKind::AssocConst { .. } => {
206                def.const_value(self.hax_state_with_id())
207            }
208            hax::FullDefKind::Static { .. } => def.static_value(self.hax_state_with_id()),
209            _ => None,
210        }
211    }
212}
charon_driver/translate/translate_constants.rs

charon_driver/translate/
translate_constants.rs
