Skip to content

Commit

Permalink
Merge pull request #442 from Nadrieril/eager-fulldef
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril authored Oct 29, 2024
2 parents 4e66d01 + 6b6dc1a commit 2b71c3c
Show file tree
Hide file tree
Showing 6 changed files with 121 additions and 161 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.

221 changes: 84 additions & 137 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 @@ -5,164 +5,113 @@ use charon_lib::transform::ctx::TransformOptions;
use charon_lib::transform::TransformCtx;
use hax_frontend_exporter as hax;
use rustc_hir::def_id::DefId;
use rustc_hir::{ForeignItemKind, ItemId, ItemKind};
use rustc_middle::ty::TyCtxt;
use std::collections::{HashMap, HashSet};
use std::path::PathBuf;

impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
/// Register a HIR item and all its children. We call this on the crate root items and end up
/// exploring the whole crate.
fn register_local_hir_item(&mut self, item_id: ItemId) {
let mut ctx_ref = std::panic::AssertUnwindSafe(&mut *self);
// Catch panics that could happen during registration.
let res = std::panic::catch_unwind(move || ctx_ref.register_local_hir_item_inner(item_id));
if res.is_err() {
let hir_map = self.tcx.hir();
let item = hir_map.item(item_id);
let def_id = item.owner_id.to_def_id();
let span = self.tcx.def_span(def_id);
self.errors
.span_err_no_register(span, &format!("panicked while registering `{def_id:?}`"));
self.errors.error_count += 1;
}
}
fn register_local_item(&mut self, def_id: DefId) {
use hax::FullDefKind;
trace!("Registering {def_id:?}");

fn register_local_hir_item_inner(&mut self, item_id: ItemId) {
let hir_map = self.tcx.hir();
let item = hir_map.item(item_id);
let def_id = item.owner_id.to_def_id();
trace!("Registering {:?}", def_id);
let Ok(def) = self.hax_def(def_id) else {
return; // Error has already been emitted
};

let Ok(name) = self.hax_def_id_to_name(&def.def_id) else {
return; // Error has already been emitted
};
let opacity = self.opacity_for_name(&name);
// Use `item_meta` to take into account the `charon::opaque` attribute.
let opacity = self.translate_item_meta(&def, name, opacity).opacity;
let explore_inside = !(opacity.is_opaque() || opacity.is_invisible());

// Case disjunction on the item kind.
match &item.kind {
ItemKind::Enum(..)
| ItemKind::Struct(..)
| ItemKind::Union(..)
| ItemKind::TyAlias(..) => {
match def.kind() {
FullDefKind::Enum { .. }
| FullDefKind::Struct { .. }
| FullDefKind::Union { .. }
| FullDefKind::TyAlias { .. }
| FullDefKind::AssocTy { .. }
| FullDefKind::ForeignTy => {
let _ = self.register_type_decl_id(&None, def_id);
}
ItemKind::Fn(..) => {

FullDefKind::Fn { .. } | FullDefKind::AssocFn { .. } => {
let _ = self.register_fun_decl_id(&None, def_id);
}
ItemKind::Trait(..) => {
let _ = self.register_trait_decl_id(&None, def_id);
}
ItemKind::Const(..) | ItemKind::Static(..) => {
FullDefKind::Const { .. }
| FullDefKind::Static { .. }
| FullDefKind::AssocConst { .. } => {
let _ = self.register_global_decl_id(&None, def_id);
}
ItemKind::Impl(..) => {
trace!("impl");
let Ok(def) = self.hax_def(def_id) else {
return; // Error has already been emitted
};
let hax::FullDefKind::Impl {
items,
impl_subject,
..
} = &def.kind
else {
unreachable!()
};

match impl_subject {
hax::ImplSubject::Trait { .. } => {
let _ = self.register_trait_impl_id(&None, def_id);
}
hax::ImplSubject::Inherent { .. } => {
// Register the items
for (item, item_def) in items {
let def_id = item_def.rust_def_id();
// Match on the impl item kind
match &item.kind {
// Associated constant:
// ```
// impl Bar {
// const C = 32;
// }
// ```
hax::AssocKind::Const => {
let _ = self.register_global_decl_id(&None, def_id);
}
// Associated type:
// ```
// impl Bar {
// type T = bool;
// }
// ```
hax::AssocKind::Type => {
let _ = self.register_type_decl_id(&None, def_id);
}
// Inherent method
// ```
// impl Bar {
// fn is_foo() -> bool { false }
// }
// ```
hax::AssocKind::Fn => {
let _ = self.register_fun_decl_id(&None, def_id);
}
}
FullDefKind::Trait { .. } => {
let _ = self.register_trait_decl_id(&None, def_id);
}
FullDefKind::Impl {
items,
impl_subject,
..
} => match impl_subject {
hax::ImplSubject::Trait { .. } => {
let _ = self.register_trait_impl_id(&None, def_id);
}
hax::ImplSubject::Inherent { .. } => {
if explore_inside {
for (item, _) in items {
self.register_local_item((&item.def_id).into());
}
}
}
}
ItemKind::Mod(module) => {
trace!("module");
},
// TODO: trait aliases (https://github.com/AeneasVerif/charon/issues/366)
FullDefKind::TraitAlias { .. } => {}

FullDefKind::Mod { items, .. } => {
// Explore the module, only if it was not marked as "opaque"
// TODO: we may want to accumulate the set of modules we found,
// to check that all the opaque modules given as arguments actually
// exist
trace!("{:?}", def_id);
let Ok(name) = self.def_id_to_name(def_id) else {
return; // Error has already been emitted
};
let Ok(def) = self.hax_def(def_id) else {
return; // Error has already been emitted
};
let opacity = self.opacity_for_name(&name);
// Go through `item_meta` to get take into account the `charon::opaque` attribute.
let item_meta = self.translate_item_meta(&def, name, opacity);
if item_meta.opacity.is_opaque() || opacity.is_invisible() {
// Ignore
trace!(
"Ignoring module [{:?}] \
because it is marked as opaque",
def_id
);
} else {
trace!("Diving into module [{:?}]", def_id);
// Lookup and register the items
for item_id in module.item_ids {
self.register_local_hir_item(*item_id);
// TODO: we may want to accumulate the set of modules we found, to check that all
// the opaque modules given as arguments actually exist
if explore_inside {
for def_id in items {
self.register_local_item(def_id.into());
}
}
}
ItemKind::ForeignMod { items, .. } => {
trace!("Diving into `extern` block [{:?}]", def_id);
for item in *items {
// Lookup and register the item
let item = hir_map.foreign_item(item.id);
let def_id = item.owner_id.to_def_id();
match item.kind {
ForeignItemKind::Fn(..) => {
let _ = self.register_fun_decl_id(&None, def_id);
}
ForeignItemKind::Static(..) => {
let _ = self.register_global_decl_id(&None, def_id);
}
ForeignItemKind::Type => {
let _ = self.register_type_decl_id(&None, def_id);
}
}
FullDefKind::ForeignMod { items, .. } => {
// Foreign modules can't be named or have attributes, so we can't mark them opaque.
for def_id in items {
self.register_local_item(def_id.into());
}
}
// TODO: trait aliases (https://github.com/AeneasVerif/charon/issues/366)
ItemKind::TraitAlias(..) => {}
// Macros are already expanded.
ItemKind::Macro(..) => {}
ItemKind::ExternCrate(..) | ItemKind::GlobalAsm(..) | ItemKind::Use(..) => {}

// We skip these
FullDefKind::ExternCrate { .. }
| FullDefKind::GlobalAsm { .. }
| FullDefKind::Macro { .. }
| FullDefKind::Use { .. } => {}
// We cannot encounter these since they're not top-level items.
FullDefKind::AnonConst { .. }
| FullDefKind::Closure { .. }
| FullDefKind::ConstParam { .. }
| FullDefKind::Ctor { .. }
| FullDefKind::Field { .. }
| FullDefKind::InlineConst { .. }
| FullDefKind::LifetimeParam { .. }
| FullDefKind::OpaqueTy { .. }
| FullDefKind::SyntheticCoroutineBody { .. }
| FullDefKind::TyParam { .. }
| FullDefKind::Variant { .. } => {
let span = self.def_span(def_id);
self.errors.span_err(
span,
&format!(
"Cannot register this item: `{def_id:?}` with kind `{:?}`",
def.kind()
),
);
}
}
}

Expand Down Expand Up @@ -336,13 +285,11 @@ pub fn translate<'tcx, 'ctx>(
cached_names: Default::default(),
};

// Recursively register all the items in the crate, starting from the root module. We could
// Recursively register all the items in the crate, starting from the crate root. We could
// instead ask rustc for the plain list of all items in the crate, but we wouldn't be able to
// skip items inside modules annotated with `#[charon::opaque]`.
let hir = tcx.hir();
for item_id in hir.root_module().item_ids {
ctx.register_local_hir_item(*item_id);
}
let crate_def_id = rustc_span::def_id::CRATE_DEF_ID.to_def_id();
ctx.register_local_item(crate_def_id);

trace!(
"Queue after we explored the crate:\n{:?}",
Expand Down
4 changes: 4 additions & 0 deletions charon/tests/ui/opacity.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,5 +130,9 @@ fn test_crate::module::dont_translate_body()

fn test_crate::exclude_me()

struct test_crate::Struct = {}

unsafe fn test_crate::extern_fn(@1: i32)



17 changes: 17 additions & 0 deletions charon/tests/ui/opacity.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@
//@ charon-args=--include crate::keep_names_of_excluded::{crate::keep_names_of_excluded::Trait<_>}
// Note: we don't use the `impl Trait for T` syntax above because we can't have spaces in these
// options.
#![feature(register_tool)]
#![register_tool(charon)]

fn foo() {
let _ = Some(0).is_some();
Expand Down Expand Up @@ -47,3 +49,18 @@ mod keep_names_of_excluded {
}
}
}

struct Struct;

#[charon::opaque]
impl Struct {
fn method() {
let _ = 0;
}
}

// Foreign modules can't be named or have attributes, so we can't mark them opaque.
#[charon::opaque]
extern "C" {
fn extern_fn(x: i32);
}
2 changes: 1 addition & 1 deletion charon/tests/ui/rename_attribute_failure.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,4 +36,4 @@ error: Error parsing attribute: Unrecognized attribute: `charon::something_else(

error: aborting due to 6 previous errors

ERROR Compilation encountered 6 errors
ERROR Compilation encountered 12 errors
32 changes: 12 additions & 20 deletions charon/tests/ui/unsupported/advanced-const-generics.out
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,3 @@
error: Constant parameters of non-literal type are not supported
--> tests/ui/unsupported/advanced-const-generics.rs:14:8
|
14 | fn foo<const X: Foo>() -> Foo {
| ^^^^^^^^^^^^

error: Ignoring the following item due to a previous error: test_crate::foo
--> tests/ui/unsupported/advanced-const-generics.rs:14:1
|
14 | fn foo<const X: Foo>() -> Foo {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

disabled backtrace
error[E9999]: Supposely unreachable place in the Rust AST. The label is "TranslateUneval".
This error report happend because some assumption about the Rust AST was broken.
Expand Down Expand Up @@ -40,14 +28,18 @@ error: Hax panicked when translating `test_crate::bar`.
20 | | [(); N + 1]:,
| |_________________^

error: Ignoring the following item due to a previous error: test_crate::bar
--> tests/ui/unsupported/advanced-const-generics.rs:18:1
error: Constant parameters of non-literal type are not supported
--> tests/ui/unsupported/advanced-const-generics.rs:14:8
|
18 | / fn bar<const N: usize>()
19 | | where
20 | | [(); N + 1]:,
| |_________________^
14 | fn foo<const X: Foo>() -> Foo {
| ^^^^^^^^^^^^

error: Ignoring the following item due to a previous error: test_crate::foo
--> tests/ui/unsupported/advanced-const-generics.rs:14:1
|
14 | fn foo<const X: Foo>() -> Foo {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: aborting due to 5 previous errors
error: aborting due to 4 previous errors

ERROR Compilation encountered 4 errors
ERROR Compilation encountered 3 errors

0 comments on commit 2b71c3c

Please sign in to comment.