charon_driver/translate/
translate_constants.rs1use super::translate_ctx::*;
3use charon_lib::ast::*;
4
5impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
6 fn translate_constant_literal_to_constant_expr_kind(
7 &mut self,
8 span: Span,
9 v: &hax::ConstantLiteral,
10 ) -> Result<ConstantExprKind, Error> {
11 let lit = match v {
12 hax::ConstantLiteral::ByteStr(bs) => Literal::ByteStr(bs.clone()),
13 hax::ConstantLiteral::Str(..) => {
14 raise_error!(self, span, "found a `str` constants not behind a reference")
17 }
18 hax::ConstantLiteral::Char(c) => Literal::Char(*c),
19 hax::ConstantLiteral::Bool(b) => Literal::Bool(*b),
20 hax::ConstantLiteral::Int(i) => {
21 use hax::ConstantInt;
22 let scalar = match i {
23 ConstantInt::Int(v, int_type) => {
24 let ty = Self::translate_hax_int_ty(int_type);
25 ScalarValue::Signed(ty, *v)
26 }
27 ConstantInt::Uint(v, uint_type) => {
28 let ty = Self::translate_hax_uint_ty(uint_type);
29 ScalarValue::Unsigned(ty, *v)
30 }
31 };
32 Literal::Scalar(scalar)
33 }
34 hax::ConstantLiteral::Float(value, float_type) => {
35 let value = value.clone();
36 let ty = match float_type {
37 hax::FloatTy::F16 => FloatTy::F16,
38 hax::FloatTy::F32 => FloatTy::F32,
39 hax::FloatTy::F64 => FloatTy::F64,
40 hax::FloatTy::F128 => FloatTy::F128,
41 };
42 Literal::Float(FloatValue { value, ty })
43 }
44 hax::ConstantLiteral::PtrNoProvenance(v) => {
45 return Ok(ConstantExprKind::PtrNoProvenance(*v));
46 }
47 };
48 Ok(ConstantExprKind::Literal(lit))
49 }
50
51 pub(crate) fn translate_constant_expr_to_constant_expr(
57 &mut self,
58 span: Span,
59 v: &hax::ConstantExpr,
60 ) -> Result<ConstantExpr, Error> {
61 use hax::ConstantExprKind;
62 let ty = self.translate_ty(span, &v.ty)?;
63 let value = match v.contents.as_ref() {
64 ConstantExprKind::Literal(lit) => {
65 self.translate_constant_literal_to_constant_expr_kind(span, lit)?
66 }
67 ConstantExprKind::Adt { info, fields } => {
68 let fields: Vec<ConstantExpr> = fields
69 .iter()
70 .map(|f| self.translate_constant_expr_to_constant_expr(span, &f.value))
71 .try_collect()?;
72 use hax::VariantKind;
73 let vid = if let VariantKind::Enum { index, .. } = info.kind {
74 Some(VariantId::new(index))
75 } else {
76 None
77 };
78 expressions::ConstantExprKind::Adt(vid, fields)
79 }
80 ConstantExprKind::Array { fields } => {
81 let fields: Vec<ConstantExpr> = fields
82 .iter()
83 .map(|x| self.translate_constant_expr_to_constant_expr(span, x))
84 .try_collect()?;
85 expressions::ConstantExprKind::Array(fields)
86 }
87 ConstantExprKind::Tuple { fields } => {
88 let fields: Vec<ConstantExpr> = fields
89 .iter()
90 .map(|f| self.translate_constant_expr_to_constant_expr(span, f))
92 .try_collect()?;
93 expressions::ConstantExprKind::Adt(None, fields)
94 }
95 ConstantExprKind::TraitConst { impl_expr, name } => {
96 let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
97 let name = TraitItemName(name.clone());
98 expressions::ConstantExprKind::TraitConst(trait_ref, name)
99 }
100 ConstantExprKind::GlobalName(item) => {
101 let global_ref = self.translate_global_decl_ref(span, item)?;
102 expressions::ConstantExprKind::Global(global_ref)
103 }
104 ConstantExprKind::Borrow(v)
105 if let ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
106 v.contents.as_ref() =>
107 {
108 expressions::ConstantExprKind::Literal(Literal::Str(s.clone()))
109 }
110 ConstantExprKind::Borrow(v) => {
111 let val = self.translate_constant_expr_to_constant_expr(span, v)?;
112 expressions::ConstantExprKind::Ref(Box::new(val))
113 }
114 ConstantExprKind::Cast { .. } => {
115 register_error!(
116 self,
117 span,
118 "Unsupported constant: `ConstantExprKind::Cast {{..}}`",
119 );
120 expressions::ConstantExprKind::Opaque("`ConstantExprKind::Cast {{..}}`".into())
121 }
122 ConstantExprKind::RawBorrow { mutability, arg } => {
123 let arg = self.translate_constant_expr_to_constant_expr(span, arg)?;
124 let rk = RefKind::mutable(*mutability);
125 expressions::ConstantExprKind::Ptr(rk, Box::new(arg))
126 }
127 ConstantExprKind::ConstRef { id } => {
128 let var = self.lookup_const_generic_var(span, id)?;
129 expressions::ConstantExprKind::Var(var)
130 }
131 ConstantExprKind::FnPtr(item) => {
132 let fn_ptr = self.translate_fn_ptr(span, item)?.erase();
133 expressions::ConstantExprKind::FnPtr(fn_ptr)
134 }
135 ConstantExprKind::Memory(bytes) => {
136 expressions::ConstantExprKind::RawMemory(bytes.clone())
137 }
138 ConstantExprKind::Todo(msg) => {
139 register_error!(self, span, "Unsupported constant: {:?}", msg);
140 expressions::ConstantExprKind::Opaque(msg.into())
141 }
142 };
143
144 Ok(ConstantExpr { value, ty })
145 }
146
147 pub(crate) fn translate_constant_expr_to_const_generic(
150 &mut self,
151 span: Span,
152 v: &hax::ConstantExpr,
153 ) -> Result<ConstGeneric, Error> {
154 let value = self
157 .translate_constant_expr_to_constant_expr(span, v)?
158 .value;
159 match value {
160 ConstantExprKind::Var(v) => Ok(ConstGeneric::Var(v)),
161 ConstantExprKind::Literal(v) => Ok(ConstGeneric::Value(v)),
162 ConstantExprKind::Global(global_ref) => {
163 error_assert!(self, span, global_ref.generics.is_empty());
166 Ok(ConstGeneric::Global(global_ref.id))
167 }
168 ConstantExprKind::Adt(..)
169 | ConstantExprKind::Array { .. }
170 | ConstantExprKind::RawMemory { .. }
171 | ConstantExprKind::TraitConst { .. }
172 | ConstantExprKind::Ref(_)
173 | ConstantExprKind::Ptr(..)
174 | ConstantExprKind::FnPtr { .. }
175 | ConstantExprKind::Opaque(_)
176 | ConstantExprKind::PtrNoProvenance(..) => {
177 raise_error!(self, span, "Unexpected constant generic: {:?}", value)
178 }
179 }
180 }
181}