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            // The data backing a string, when we represent strings as unsized [u8]s.
17            hax::ConstantLiteral::Str(str) if self.t_ctx.options.unsized_strings => {
18                ConstantExprKind::RawMemory(str.bytes().map(Byte::Value).collect())
19            }
20            // A `str` value not behind a reference, e.g. the tail of a `str`-tailed DST
21            hax::ConstantLiteral::Str(str) => {
22                let ty_is_sized = self.translate_sized_proof(span, self.tcx.types.u8)?;
23                let bytes = str
24                    .bytes()
25                    .map(|b| IntegerValue::Unsigned(UIntTy::U8, b.into()).to_constant())
26                    .collect();
27                let slice_ty = Ty::mk_slice(Ty::mk_u8(), ty_is_sized);
28                let bytes = ConstantExpr::new(ConstantExprKind::Array(bytes), slice_ty);
29                // we encode `str` as `struct { [u8] }`
30                ConstantExprKind::Adt(None, vec![bytes])
31            }
32            hax::ConstantLiteral::Char(c) => ConstantExprKind::Char(*c),
33            hax::ConstantLiteral::Bool(b) => ConstantExprKind::Bool(*b),
34            hax::ConstantLiteral::Int(i) => {
35                use crate::hax::ConstantInt;
36                let scalar = match i {
37                    ConstantInt::Int(v, int_type) => {
38                        let ty = Self::translate_hax_int_ty(int_type);
39                        IntegerValue::Signed(ty, *v)
40                    }
41                    ConstantInt::Uint(v, uint_type) => {
42                        let ty = Self::translate_hax_uint_ty(uint_type);
43                        IntegerValue::Unsigned(ty, *v)
44                    }
45                };
46                ConstantExprKind::Integer(scalar)
47            }
48            hax::ConstantLiteral::Float(value, float_type) => {
49                let value = value.clone();
50                let ty = match float_type {
51                    hax::FloatTy::F16 => FloatTy::F16,
52                    hax::FloatTy::F32 => FloatTy::F32,
53                    hax::FloatTy::F64 => FloatTy::F64,
54                    hax::FloatTy::F128 => FloatTy::F128,
55                };
56                ConstantExprKind::Float(FloatValue { value, ty })
57            }
58            hax::ConstantLiteral::PtrNoProvenance(v) => {
59                return Ok(ConstantExprKind::PtrNoProvenance(*v));
60            }
61        })
62    }
63
64    fn translate_constant_byte(
65        &mut self,
66        span: Span,
67        b: &hax::ConstantByte,
68    ) -> Result<Byte, Error> {
69        Ok(match b {
70            hax::ConstantByte::Uninit => Byte::Uninit,
71            hax::ConstantByte::Value(v) => Byte::Value(*v),
72            hax::ConstantByte::Provenance(prov, offset) => {
73                let prov = match prov {
74                    hax::ConstantByteProvenance::Global(item) => {
75                        Provenance::Global(self.translate_global_decl_ref(span, item)?)
76                    }
77                    hax::ConstantByteProvenance::Function(item) => Provenance::Function(
78                        self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?,
79                    ),
80                    hax::ConstantByteProvenance::ClosureAsFn(closure) => {
81                        let fn_ref = self.translate_stateless_closure_as_fn_ref(span, closure)?;
82                        Provenance::Function(self.erase_region_binder(fn_ref).into())
83                    }
84                    hax::ConstantByteProvenance::Unknown => Provenance::Unknown,
85                };
86                Byte::Provenance(prov, *offset)
87            }
88        })
89    }
90
91    /// Remark: [hax::ConstantExpr] contains span information, but it is often
92    /// the default span (i.e., it is useless), hence the additional span argument.
93    /// TODO: the user_ty might be None because hax doesn't extract it (because
94    /// we are translating a [ConstantExpr] instead of a Constant. We need to
95    /// update hax.
96    pub(crate) fn translate_constant_expr(
97        &mut self,
98        span: Span,
99        v: &hax::ConstantExpr,
100    ) -> Result<ConstantExpr, Error> {
101        let ty = self.translate_ty(span, &v.ty)?;
102        let kind = match v.contents.as_ref() {
103            hax::ConstantExprKind::Literal(lit) => {
104                self.translate_constant_literal_to_constant_expr_kind(span, lit)?
105            }
106            hax::ConstantExprKind::Adt { kind, fields } => {
107                let fields: Vec<ConstantExpr> = fields
108                    .iter()
109                    .map(|f| self.translate_constant_expr(span, &f.value))
110                    .try_collect()?;
111                use crate::hax::VariantKind;
112                let vid = if let VariantKind::Enum { index, .. } = *kind {
113                    Some(self.translate_variant_id(index))
114                } else {
115                    None
116                };
117                ConstantExprKind::Adt(vid, fields)
118            }
119            hax::ConstantExprKind::Array { fields } => {
120                let fields: Vec<ConstantExpr> = fields
121                    .iter()
122                    .map(|x| self.translate_constant_expr(span, x))
123                    .try_collect()?;
124
125                ConstantExprKind::Array(fields)
126            }
127            hax::ConstantExprKind::Tuple { fields } => {
128                let fields: Vec<ConstantExpr> = fields
129                    .iter()
130                    // TODO: the user_ty is not always None
131                    .map(|f| self.translate_constant_expr(span, f))
132                    .try_collect()?;
133                ConstantExprKind::Adt(None, fields)
134            }
135            hax::ConstantExprKind::NamedGlobal(item) => match &item.in_trait {
136                Some(trait_proof) => {
137                    let trait_ref = self.translate_trait_proof(span, trait_proof)?;
138                    // Trait consts can't have their own generics.
139                    assert!(item.generic_args.is_empty());
140                    let const_id =
141                        self.translate_assoc_const_id(trait_ref.trait_id(), &item.def_id)?;
142                    ConstantExprKind::TraitConst(trait_ref, const_id)
143                }
144                None => {
145                    let global_ref = self.translate_global_decl_ref(span, item)?;
146                    ConstantExprKind::Global(global_ref)
147                }
148            },
149            hax::ConstantExprKind::Borrow(v, _)
150                if let hax::ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
151                    v.contents.as_ref()
152                    && !self.t_ctx.options.unsized_strings =>
153            {
154                ConstantExprKind::Str(s.clone())
155            }
156
157            hax::ConstantExprKind::Borrow(v, metadata) => {
158                let mut val = self.translate_constant_expr(span, v)?;
159                // With `--unsized-strings`, a string literal is the `[u8; N]` behind the `&str`.
160                if let hax::ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
161                    v.contents.as_ref()
162                {
163                    let len = ConstantExpr::mk_usize(s.len() as u128);
164                    let ty_is_sized = self.translate_sized_proof(span, self.tcx.types.u8)?;
165                    let array_ty = Ty::mk_array(Ty::mk_u8(), len, ty_is_sized);
166                    val.with_contents_mut(|_, ty| *ty = array_ty);
167                }
168                let metadata = if let Some(metadata) = metadata {
169                    Some(self.translate_unsizing_metadata(span, metadata)?)
170                } else {
171                    None
172                };
173                ConstantExprKind::Ref(val, metadata)
174            }
175            hax::ConstantExprKind::RawBorrow {
176                mutability,
177                arg,
178                metadata,
179            } => {
180                let arg = self.translate_constant_expr(span, arg)?;
181                let rk = RefKind::mutable(mutability.is_mut());
182                let metadata = if let Some(metadata) = metadata {
183                    Some(self.translate_unsizing_metadata(span, metadata)?)
184                } else {
185                    None
186                };
187                ConstantExprKind::Ptr(rk, arg, metadata)
188            }
189            hax::ConstantExprKind::ConstRef { id } => {
190                match self.lookup_const_generic_var(span, id) {
191                    Ok(var) => ConstantExprKind::Var(var),
192                    Err(err) => ConstantExprKind::Opaque(err.msg),
193                }
194            }
195            hax::ConstantExprKind::FnDef(item) => {
196                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
197                ConstantExprKind::FnDef(fn_ptr)
198            }
199            hax::ConstantExprKind::FnPtr(item) => {
200                let fn_ptr = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?;
201                ConstantExprKind::FnPtr(fn_ptr)
202            }
203            hax::ConstantExprKind::Memory(bytes) => {
204                let bytes: Vec<Byte> = bytes
205                    .iter()
206                    .map(|b| self.translate_constant_byte(span, b))
207                    .try_collect()?;
208                ConstantExprKind::RawMemory(bytes)
209            }
210            hax::ConstantExprKind::Todo(msg) => {
211                register_error!(self, span, "Unsupported constant: {:?}", msg);
212                ConstantExprKind::Opaque(msg.into())
213            }
214        };
215
216        Ok(ConstantExpr::new(kind, ty))
217    }
218
219    pub(crate) fn translate_ty_constant_expr(
220        &mut self,
221        span: Span,
222        c: &ty::Const<'tcx>,
223    ) -> Result<ConstantExpr, Error> {
224        let c = self.catch_sinto(span, c)?;
225        self.translate_constant_expr(span, &c)
226    }
227
228    /// Evaluates a global definition to a [`ConstantExpr`], if possible.
229    pub(crate) fn evaluate_const_def(
230        &mut self,
231        def: &hax::FullDef<'tcx>,
232    ) -> Option<hax::Decorated<hax::ConstantExprKind>> {
233        match def.kind() {
234            hax::FullDefKind::Const(_) | hax::FullDefKind::AssocConst(_) => {
235                def.const_value(self.hax_state_with_id())
236            }
237            hax::FullDefKind::Static(_) => def.static_value(self.hax_state_with_id()),
238            _ => None,
239        }
240    }
241
242    /// Evaluates a global definition to its byte representation, if possible.
243    pub(crate) fn evaluate_const_def_as_bytes(
244        &mut self,
245        def: &hax::FullDef<'tcx>,
246    ) -> Option<hax::Decorated<hax::ConstantExprKind>> {
247        match def.kind() {
248            hax::FullDefKind::Const(_) | hax::FullDefKind::AssocConst(_) => {
249                def.const_value_as_raw_memory(self.hax_state_with_id())
250            }
251            hax::FullDefKind::Static(_) => def.static_value_as_raw_memory(self.hax_state_with_id()),
252            _ => None,
253        }
254    }
255}
charon_driver/translate/translate_constants.rs

charon_driver/translate/
translate_constants.rs
