Skip to content

Commit

Permalink
Merge pull request #420 from Nadrieril/more-fulldef
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril authored Oct 15, 2024
2 parents 355ce1b + e941634 commit 43644cd
Show file tree
Hide file tree
Showing 7 changed files with 72 additions and 100 deletions.
6 changes: 3 additions & 3 deletions charon/Cargo.lock
View file

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
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
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
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
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
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

0 comments on commit 43644cd

Please sign in to comment.