Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use hax::FullDef more #420

Merged
merged 2 commits into from
Oct 15, 2024
Merged

Use hax::FullDef more #420

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5ef01bb
Update hax
Nadrieril Oct 15, 2024
e941634
Use `FullDef` more
Nadrieril Oct 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions charon/Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 3 additions & 4 deletions charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,13 +129,13 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
};

// If this is a trait implementation, register it
if let hax::ImplSubject::Trait(..) = impl_subject {
if let hax::ImplSubject::Trait { .. } = impl_subject {
let _ = self.register_trait_impl_id(&None, def_id);
}

// Explore the items
for item in items {
let def_id = (&item.def_id).into();
for (item, item_def) in items {
let def_id = item_def.rust_def_id();
// Match on the impl item kind
match &item.kind {
hax::AssocKind::Const => {
Expand Down Expand Up @@ -410,7 +410,6 @@ pub fn translate<'tcx, 'ctx>(options: &CliOpts, tcx: TyCtxt<'tcx>) -> TransformC
reverse_id_map: Default::default(),
priority_queue: Default::default(),
translate_stack: Default::default(),
cached_defs: Default::default(),
cached_path_elems: Default::default(),
cached_names: Default::default(),
};
Expand Down
29 changes: 9 additions & 20 deletions charon/src/bin/charon-driver/translate/translate_ctx.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,8 +186,6 @@ pub struct TranslateCtx<'tcx, 'ctx> {
/// Stack of the translations currently happening. Used to avoid cycles where items need to
/// translate themselves transitively.
pub translate_stack: Vec<AnyTransId>,
/// Cache the `hax::FullDef`s to compute them only once each.
pub cached_defs: HashMap<DefId, Arc<hax::FullDef>>,
/// Cache the `PathElem`s to compute them only once each. It's an `Option` because some
/// `DefId`s (e.g. `extern {}` blocks) don't appear in the `Name`.
pub cached_path_elems: HashMap<DefId, Option<PathElem>>,
Expand Down Expand Up @@ -364,7 +362,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
ImplElem::Ty(generics, ty)
}
// Trait implementation
hax::ImplSubject::Trait(..) => {
hax::ImplSubject::Trait { .. } => {
let impl_id = self.register_trait_impl_id(&None, def_id);
ImplElem::Trait(impl_id)
}
Expand Down Expand Up @@ -495,12 +493,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {

pub fn hax_def(&mut self, def_id: impl Into<DefId>) -> Arc<hax::FullDef> {
let def_id: DefId = def_id.into();
// We return an `Arc` because keeping a borrow would prevent us from doing anything useful
// with `self`.
self.cached_defs
.entry(def_id)
.or_insert_with(|| Arc::new(def_id.sinto(&self.hax_state)))
.clone()
// Hax takes care of caching the translation.
def_id.sinto(&self.hax_state)
}

pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
Expand Down Expand Up @@ -542,14 +536,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
name: Name,
opacity: ItemOpacity,
) -> Result<ItemMeta, Error> {
let def_id: DefId = (&def.def_id).into();
// TODO: upstream to hax
let span = def_id
.as_local()
.map(|local_def_id| self.tcx.source_span(local_def_id))
.unwrap_or(def.span.rust_span_data.unwrap().span());
let source_text = self.tcx.sess.source_map().span_to_snippet(span.into()).ok();
let span = self.translate_span_from_hax(&span.sinto(&self.hax_state));
let def_id = def.rust_def_id();
let span = def.source_span.as_ref().unwrap_or(&def.span);
let span = self.translate_span_from_hax(span);
let attr_info = self.translate_attr_info(def);
let is_local = def.def_id.is_local;

Expand All @@ -565,7 +554,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
Ok(ItemMeta {
name,
span,
source_text,
source_text: def.source_text.clone(),
attr_info,
is_local,
opacity,
Expand Down Expand Up @@ -685,7 +674,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
}

pub(crate) fn def_span(&mut self, def_id: impl Into<DefId>) -> Span {
let span = self.tcx.def_span(def_id.into()).sinto(&self.hax_state);
let span = &self.hax_def(def_id).span;
self.translate_span_from_hax(&span)
}

Expand Down Expand Up @@ -859,7 +848,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
{
let def = self.hax_def(id);
let hax::FullDefKind::Impl {
impl_subject: hax::ImplSubject::Trait(trait_pred),
impl_subject: hax::ImplSubject::Trait { trait_pred, .. },
..
} = def.kind()
else {
Expand Down
49 changes: 24 additions & 25 deletions charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -733,19 +733,17 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}

/// Checks whether the given id corresponds to a built-in function.
fn recognize_builtin_fun(&mut self, def_id: &hax::DefId) -> Result<Option<BuiltinFun>, Error> {
use rustc_hir::lang_items::LangItem;
let tcx = self.t_ctx.tcx;
let rust_id = DefId::from(def_id);
let name = self.t_ctx.hax_def_id_to_name(def_id)?;

let panic_lang_items = &[LangItem::Panic, LangItem::PanicFmt, LangItem::BeginPanic];
fn recognize_builtin_fun(&mut self, def: &hax::FullDef) -> Result<Option<BuiltinFun>, Error> {
let name = self.t_ctx.hax_def_id_to_name(&def.def_id)?;
let panic_lang_items = &["panic", "panic_fmt", "begin_panic"];
let panic_names = &[&["core", "panicking", "assert_failed"], EXPLICIT_PANIC_NAME];
if tcx.is_diagnostic_item(rustc_span::sym::box_new, rust_id) {

if def.diagnostic_item.as_deref() == Some("box_new") {
Ok(Some(BuiltinFun::BoxNew))
} else if panic_lang_items
.iter()
.any(|i| tcx.is_lang_item(rust_id, *i))
} else if def
.lang_item
.as_deref()
.is_some_and(|lang_it| panic_lang_items.iter().contains(&lang_it))
|| panic_names.iter().any(|panic| name.equals_ref_name(panic))
{
Ok(Some(BuiltinFun::Panic))
Expand Down Expand Up @@ -775,7 +773,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
trait_refs: &Vec<hax::ImplExpr>,
trait_info: &Option<hax::ImplExpr>,
) -> Result<SubstFunIdOrPanic, Error> {
let builtin_fun = self.recognize_builtin_fun(def_id)?;
let fun_def = self.t_ctx.hax_def(def_id);
let builtin_fun = self.recognize_builtin_fun(&fun_def)?;
if matches!(builtin_fun, Some(BuiltinFun::Panic)) {
let name = self.t_ctx.hax_def_id_to_name(def_id)?;
return Ok(SubstFunIdOrPanic::Panic(name));
Expand Down Expand Up @@ -1226,12 +1225,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}

/// Gather all the lines that start with `//` inside the given span.
fn translate_body_comments(&mut self, charon_span: Span) -> Vec<(usize, Vec<String>)> {
let rust_span = charon_span.rust_span();
let source_map = self.t_ctx.tcx.sess.source_map();
if rust_span.ctxt().is_root()
&& let Ok(body_text) = source_map.span_to_snippet(rust_span.into())
{
fn translate_body_comments(
&mut self,
def: &hax::FullDef,
charon_span: Span,
) -> Vec<(usize, Vec<String>)> {
if let Some(body_text) = &def.source_text {
let mut comments = body_text
.lines()
// Iter through the lines of this body in reverse order.
Expand Down Expand Up @@ -1271,14 +1270,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
/// declared opaque, and only translate non-local bodies if `extract_opaque_bodies` is set).
fn translate_body(
&mut self,
rust_id: DefId,
def: &hax::FullDef,
arg_count: usize,
item_meta: &ItemMeta,
) -> Result<Result<Body, Opaque>, Error> {
// Stopgap measure because there are still many panics in charon and hax.
let mut this = panic::AssertUnwindSafe(&mut *self);
let res =
panic::catch_unwind(move || this.translate_body_aux(rust_id, arg_count, item_meta));
let res = panic::catch_unwind(move || this.translate_body_aux(def, arg_count, item_meta));
match res {
Ok(Ok(body)) => Ok(body),
// Translation error
Expand All @@ -1295,7 +1293,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {

fn translate_body_aux(
&mut self,
rust_id: DefId,
def: &hax::FullDef,
arg_count: usize,
item_meta: &ItemMeta,
) -> Result<Result<Body, Opaque>, Error> {
Expand All @@ -1305,6 +1303,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}

// Retrieve the body
let rust_id = def.rust_def_id();
let Some(body) =
get_mir_for_def_id_and_level(self.t_ctx.tcx, rust_id, self.t_ctx.options.mir_level)
else {
Expand Down Expand Up @@ -1346,7 +1345,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
span,
arg_count,
locals: mem::take(&mut self.vars),
comments: self.translate_body_comments(span),
comments: self.translate_body_comments(def, span),
body: blocks,
})))
}
Expand Down Expand Up @@ -1481,7 +1480,7 @@ impl BodyTransCtx<'_, '_, '_> {
let body_id = if !is_trait_method_decl_without_default {
// Translate the body. This doesn't store anything if we can't/decide not to translate
// this body.
match self.translate_body(rust_id, signature.inputs.len(), &item_meta) {
match self.translate_body(def, signature.inputs.len(), &item_meta) {
Ok(Ok(body)) => Ok(self.t_ctx.translated.bodies.push(body)),
// Opaque declaration
Ok(Err(Opaque)) => Err(Opaque),
Expand Down Expand Up @@ -1538,7 +1537,7 @@ impl BodyTransCtx<'_, '_, '_> {

// Translate its body like the body of a function. This returns `Opaque if we can't/decide
// not to translate this body.
let body_id = match self.translate_body(rust_id, 0, &item_meta) {
let body_id = match self.translate_body(def, 0, &item_meta) {
Ok(Ok(body)) => Ok(self.t_ctx.translated.bodies.push(body)),
// Opaque declaration
Ok(Err(Opaque)) => Err(Opaque),
Expand Down
21 changes: 8 additions & 13 deletions charon/src/bin/charon-driver/translate/translate_traits.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,10 +106,9 @@ impl BodyTransCtx<'_, '_, '_> {
};
let items: Vec<(TraitItemName, &hax::AssocItem, Arc<hax::FullDef>)> = items
.iter()
.map(|item| {
.map(|(item, def)| {
let name = TraitItemName(item.name.clone());
let def = self.t_ctx.hax_def(&item.def_id);
(name, item, def)
(name, item, def.clone())
})
.collect_vec();

Expand Down Expand Up @@ -233,7 +232,7 @@ impl BodyTransCtx<'_, '_, '_> {
let generics = self.translate_def_generics(span, def)?;

let hax::FullDefKind::Impl {
impl_subject: hax::ImplSubject::Trait(trait_pred),
impl_subject: hax::ImplSubject::Trait { trait_pred, .. },
items: impl_items,
..
} = &def.kind
Expand Down Expand Up @@ -307,7 +306,7 @@ impl BodyTransCtx<'_, '_, '_> {
let mut types: HashMap<TraitItemName, Ty> = HashMap::new();
let mut methods = HashMap::new();

for item in impl_items {
for (item, item_def) in impl_items {
let name = TraitItemName(item.name.clone());
let item_span = self.def_span(&item.def_id);
match &item.kind {
Expand All @@ -325,17 +324,13 @@ impl BodyTransCtx<'_, '_, '_> {
consts.insert(name, gref);
}
hax::AssocKind::Type => {
// Warning: don't call `hax_def` on associated functions because this triggers
// hax crashes on functions with higher-kinded predicates like
// `Iterator::scan`.
let item_def = self.t_ctx.hax_def(&item.def_id);
let hax::FullDefKind::AssocTy {
value: Some(ty), ..
} = item_def.kind()
else {
unreachable!()
};
let ty = self.translate_ty(item_span, erase_regions, ty)?;
let ty = self.translate_ty(item_span, erase_regions, &ty)?;
types.insert(name, ty);
}
}
Expand All @@ -352,9 +347,9 @@ impl BodyTransCtx<'_, '_, '_> {
let mut required_methods = Vec::new();
let mut provided_methods = Vec::new();

for decl_item in decl_items {
let item_def_id = (&decl_item.def_id).into();
let item_span = self.def_span(item_def_id);
for (decl_item, decl_item_def) in decl_items {
let item_def_id = decl_item_def.rust_def_id();
let item_span = self.translate_span_from_hax(&decl_item_def.span);
let name = TraitItemName(decl_item.name.to_string());
match &decl_item.kind {
hax::AssocKind::Fn => {
Expand Down
16 changes: 8 additions & 8 deletions charon/src/bin/charon-driver/translate/translate_types.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ use charon_lib::pretty::FmtWithCtx;
use core::convert::*;
use hax::Visibility;
use hax_frontend_exporter as hax;
use rustc_hir::def_id::DefId;

/// Small helper: we ignore some region names (when they are equal to "'_")
fn check_region_name(s: Option<String>) -> Option<String> {
Expand Down Expand Up @@ -420,10 +419,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {

/// Checks whether the given id corresponds to a built-in type.
fn recognize_builtin_type(&mut self, def_id: &hax::DefId) -> Result<Option<BuiltinTy>, Error> {
use rustc_hir::lang_items::LangItem;
let tcx = self.t_ctx.tcx;
let rust_id = DefId::from(def_id);
let ty = if tcx.is_lang_item(rust_id, LangItem::OwnedBox) {
let def = self.t_ctx.hax_def(def_id);
let ty = if def.lang_item.as_deref() == Some("owned_box") {
Some(BuiltinTy::Box)
} else {
None
Expand Down Expand Up @@ -664,7 +661,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
// Add the self trait clause.
match &def.kind {
FullDefKind::Impl {
impl_subject: hax::ImplSubject::Trait(self_predicate),
impl_subject:
hax::ImplSubject::Trait {
trait_pred: self_predicate,
..
},
..
}
| FullDefKind::Trait { self_predicate, .. } => {
Expand Down Expand Up @@ -709,8 +710,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
if let hax::FullDefKind::Trait { items, .. } = &def.kind
&& !is_parent
{
for item in items {
let item_def = self.t_ctx.hax_def(&item.def_id);
for (item, item_def) in items {
if let hax::FullDefKind::AssocTy { predicates, .. } = &item_def.kind {
let name = TraitItemName(item.name.clone());
self.register_predicates(
Expand Down
Loading