1use super::translate_crate::TransItemSource;
3use super::translate_generics::BindingLevel;
4use charon_lib::ast::*;
5use charon_lib::formatter::{FmtCtx, IntoFormatter};
6use charon_lib::ids::Vector;
7use charon_lib::options::TranslateOptions;
8use hax_frontend_exporter::{self as hax, DefId, SInto};
9use rustc_middle::ty::TyCtxt;
10use std::borrow::Cow;
11use std::cell::RefCell;
12use std::collections::{BTreeSet, HashMap, HashSet};
13use std::fmt::Debug;
14use std::path::PathBuf;
15use std::sync::Arc;
16use std::{fmt, mem};
17
18pub(crate) use charon_lib::errors::{
20 error_assert, raise_error, register_error, DepSource, ErrorCtx, Level,
21};
22
23pub struct TranslateCtx<'tcx> {
25 pub tcx: TyCtxt<'tcx>,
27 pub sysroot: PathBuf,
29 pub hax_state: hax::StateWithBase<'tcx>,
31
32 pub options: TranslateOptions,
34 pub translated: TranslatedCrate,
36
37 pub id_map: HashMap<TransItemSource, AnyTransId>,
39 pub reverse_id_map: HashMap<AnyTransId, TransItemSource>,
41 pub file_to_id: HashMap<FileName, FileId>,
43
44 pub errors: RefCell<ErrorCtx>,
46 pub items_to_translate: BTreeSet<TransItemSource>,
49 pub processed: HashSet<TransItemSource>,
51 pub cached_names: HashMap<hax::DefId, Name>,
53 pub cached_item_metas: HashMap<TransItemSource, ItemMeta>,
55}
56
57pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
60 pub item_src: TransItemSource,
62 pub item_id: Option<AnyTransId>,
64 pub t_ctx: &'ctx mut TranslateCtx<'tcx>,
66 pub error_on_impl_expr_error: bool,
69
70 pub binding_levels: BindingStack<BindingLevel>,
74 pub parent_trait_clauses: Vector<TraitClauseId, TraitClause>,
76 pub item_trait_clauses: HashMap<TraitItemName, Vector<TraitClauseId, TraitClause>>,
78 pub self_clause_id: Option<TraitClauseId>,
81}
82
83pub fn catch_sinto<S, T, U>(
85 s: &S,
86 err: &mut ErrorCtx,
87 krate: &TranslatedCrate,
88 span: Span,
89 x: &T,
90) -> Result<U, Error>
91where
92 T: Debug + SInto<S, U>,
93{
94 let unwind_safe_s = std::panic::AssertUnwindSafe(s);
95 let unwind_safe_x = std::panic::AssertUnwindSafe(x);
96 std::panic::catch_unwind(move || unwind_safe_x.sinto(*unwind_safe_s)).or_else(|_| {
97 raise_error!(
98 err,
99 crate(krate),
100 span,
101 "Hax panicked when translating `{x:?}`."
102 )
103 })
104}
105
106impl<'tcx, 'ctx> TranslateCtx<'tcx> {
107 pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
109 self.errors
110 .borrow_mut()
111 .span_err(&self.translated, span, msg, level)
112 }
113
114 pub fn catch_sinto<S, T, U>(&mut self, s: &S, span: Span, x: &T) -> Result<U, Error>
116 where
117 T: Debug + SInto<S, U>,
118 {
119 catch_sinto(s, &mut *self.errors.borrow_mut(), &self.translated, span, x)
120 }
121
122 pub fn hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
123 let span = self.def_span(def_id);
124 let unwind_safe_s = std::panic::AssertUnwindSafe(&self.hax_state);
126 std::panic::catch_unwind(move || def_id.full_def(*unwind_safe_s))
127 .or_else(|_| raise_error!(self, span, "Hax panicked when translating `{def_id:?}`."))
128 }
129
130 pub(crate) fn get_lang_item(&self, item: rustc_hir::LangItem) -> DefId {
131 self.tcx
132 .lang_items()
133 .get(item)
134 .unwrap()
135 .sinto(&self.hax_state)
136 }
137
138 pub(crate) fn with_def_id<F, T>(
139 &mut self,
140 def_id: &hax::DefId,
141 item_id: Option<AnyTransId>,
142 f: F,
143 ) -> T
144 where
145 F: FnOnce(&mut Self) -> T,
146 {
147 let mut errors = self.errors.borrow_mut();
148 let current_def_id = mem::replace(&mut errors.def_id, item_id);
149 let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local);
150 drop(errors); let ret = f(self);
152 let mut errors = self.errors.borrow_mut();
153 errors.def_id = current_def_id;
154 errors.def_id_is_local = current_def_id_is_local;
155 ret
156 }
157}
158
159impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
160 pub(crate) fn new(
162 item_src: TransItemSource,
163 item_id: Option<AnyTransId>,
164 t_ctx: &'ctx mut TranslateCtx<'tcx>,
165 ) -> Self {
166 ItemTransCtx {
167 item_src,
168 item_id,
169 t_ctx,
170 error_on_impl_expr_error: true,
171 binding_levels: Default::default(),
172 parent_trait_clauses: Default::default(),
173 item_trait_clauses: Default::default(),
174 self_clause_id: Default::default(),
175 }
176 }
177
178 pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
179 self.t_ctx.span_err(span, msg, level)
180 }
181
182 pub(crate) fn hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
183 self.t_ctx.hax_def(def_id)
184 }
185
186 pub(crate) fn get_lang_item(&self, item: rustc_hir::LangItem) -> DefId {
187 self.t_ctx.get_lang_item(item)
188 }
189}
190
191impl<'a> IntoFormatter for &'a TranslateCtx<'_> {
192 type C = FmtCtx<'a>;
193 fn into_fmt(self) -> Self::C {
194 self.translated.into_fmt()
195 }
196}
197
198impl<'a> IntoFormatter for &'a ItemTransCtx<'_, '_> {
199 type C = FmtCtx<'a>;
200 fn into_fmt(self) -> Self::C {
201 FmtCtx {
202 translated: Some(&self.t_ctx.translated),
203 generics: self.binding_levels.map_ref(|bl| Cow::Borrowed(&bl.params)),
204 locals: None,
205 indent_level: 0,
206 }
207 }
208}
209
210impl<'tcx, 'ctx> fmt::Display for TranslateCtx<'tcx> {
211 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
212 self.translated.fmt(f)
213 }
214}