Skip to content

Commit

Permalink
feat(exporter): add rustc default feature
Browse files Browse the repository at this point in the history
The `rustc` feature enables the conversion bridges from rustc types
(and AST) to the ones defined in `hax-frontend-exporter`. Enabling
`rustc` adds a dependency to `librustc_driver`.
  • Loading branch information
Lucas Franceschino committed Jul 2, 2024
1 parent 7cbb332 commit 2a72e1d
Show file tree
Hide file tree
Showing 28 changed files with 1,155 additions and 982 deletions.
1 change: 1 addition & 0 deletions Cargo.lock

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

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ bincode = "2.0.0-rc.3"
annotate-snippets = "0.11"

# Crates in this repository
hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-pre.1" }
hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-pre.1", default-features = false }
hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-pre.1" }
hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-pre.1" }
hax-phase-debug-webapp = { path = "engine/utils/phase-debug-webapp", version = "=0.1.0-pre.1" }
Expand Down
4 changes: 2 additions & 2 deletions cli/driver/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ serde.workspace = true
serde_json.workspace = true
clap.workspace = true
colored.workspace = true
hax-frontend-exporter.workspace = true
hax-types.workspace = true
hax-frontend-exporter = {workspace = true, features = ["rustc"]}
hax-types = {workspace = true, features = ["rustc"]}
hax-frontend-exporter-options.workspace = true
hax-lib-macros-types.workspace = true
itertools.workspace = true
Expand Down
1 change: 1 addition & 0 deletions engine/names/extract/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ use std::process::{Command, Stdio};
/// impls), we just inline a small module here that contains the three
/// type definition we need. See the module for complementary
/// informations.
#[allow(unexpected_cfgs)]
#[path = "../../../frontend/exporter/src/types/def_id.rs"]
mod hax_frontend_exporter_def_id;
use hax_frontend_exporter_def_id::*;
Expand Down
6 changes: 6 additions & 0 deletions frontend/exporter/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,12 @@ paste = "1.0.11"
extension-traits = "1.0.1"
lazy_static = "1.4.0"
bincode.workspace = true
cfg-if = "1.0.0"

[features]
default = ["rustc"]
extract_names_mode = []
# Enables the conversion bridges from rustc types (and AST) to the
# ones defined in this crate. Enabling `rustc` adds a dependency to
# `librustc_driver`.
rustc = []
1 change: 1 addition & 0 deletions frontend/exporter/adt-into/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -384,6 +384,7 @@ pub fn adt_into(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
};

quote! {
#[cfg(feature = "rustc")]
const _ : () = {
use #from as FROM_TYPE;
use #to as TO_TYPE;
Expand Down
166 changes: 88 additions & 78 deletions frontend/exporter/src/body.rs
Original file line number Diff line number Diff line change
@@ -1,99 +1,109 @@
use crate::prelude::*;
pub use module::*;

pub use rustc_hir::{
def_id::{DefId as RDefId, LocalDefId as RLocalDefId},
hir_id::OwnerId as ROwnerId,
};

pub fn get_thir<'tcx, S: UnderOwnerState<'tcx>>(
did: RLocalDefId,
s: &S,
) -> (
Rc<rustc_middle::thir::Thir<'tcx>>,
rustc_middle::thir::ExprId,
) {
let base = s.base();
let msg = || fatal!(s[base.tcx.def_span(did)], "THIR not found for {:?}", did);
base.cached_thirs.get(&did).unwrap_or_else(msg).clone()
#[cfg(not(feature = "rustc"))]
mod module {
pub trait IsBody: Sized + Clone + 'static {}
impl<T: Sized + Clone + 'static> IsBody for T {}
}

pub trait IsBody: Sized + Clone + 'static {
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self;
}
#[cfg(feature = "rustc")]
mod module {
pub use crate::prelude::*;
pub use rustc_hir::{
def_id::{DefId as RDefId, LocalDefId as RLocalDefId},
hir_id::OwnerId as ROwnerId,
};

pub fn make_fn_def<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>(
fn_sig: &rustc_hir::FnSig,
body_id: &rustc_hir::BodyId,
s: &S,
) -> FnDef<Body> {
let hir_id = body_id.hir_id;
let ldid = hir_id.clone().owner.def_id;
pub fn get_thir<'tcx, S: UnderOwnerState<'tcx>>(
did: RLocalDefId,
s: &S,
) -> (
Rc<rustc_middle::thir::Thir<'tcx>>,
rustc_middle::thir::ExprId,
) {
let base = s.base();
let msg = || fatal!(s[base.tcx.def_span(did)], "THIR not found for {:?}", did);
base.cached_thirs.get(&did).unwrap_or_else(msg).clone()
}

let (thir, expr_entrypoint) = get_thir(ldid, s);
let s = &with_owner_id(s.base(), thir.clone(), (), ldid.to_def_id());
FnDef {
params: thir.params.raw.sinto(s),
ret: thir.exprs[expr_entrypoint].ty.sinto(s),
body: Body::body(ldid, s),
sig_span: fn_sig.span.sinto(s),
header: fn_sig.header.sinto(s),
pub trait IsBody: Sized + Clone + 'static {
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self;
}
}

pub fn body_from_id<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>(
id: rustc_hir::BodyId,
s: &S,
) -> Body {
// **Important:**
// We need a local id here, and we get it from the owner id, which must
// be local. It is safe to do so, because if we have access to HIR objects,
// it necessarily means we are exploring a local item (we don't have
// access to the HIR of external objects, only their MIR).
Body::body(s.base().tcx.hir().body_owner_def_id(id), s)
}
pub fn make_fn_def<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>(
fn_sig: &rustc_hir::FnSig,
body_id: &rustc_hir::BodyId,
s: &S,
) -> FnDef<Body> {
let hir_id = body_id.hir_id;
let ldid = hir_id.clone().owner.def_id;

mod implementations {
use super::*;
impl IsBody for () {
fn body<'tcx, S: UnderOwnerState<'tcx>>(_did: RLocalDefId, _s: &S) -> Self {
()
let (thir, expr_entrypoint) = get_thir(ldid, s);
let s = &with_owner_id(s.base(), thir.clone(), (), ldid.to_def_id());
FnDef {
params: thir.params.raw.sinto(s),
ret: thir.exprs[expr_entrypoint].ty.sinto(s),
body: Body::body(ldid, s),
sig_span: fn_sig.span.sinto(s),
header: fn_sig.header.sinto(s),
}
}
impl IsBody for ThirBody {
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self {
let (thir, expr) = get_thir(did, s);
if *CORE_EXTRACTION_MODE {
let expr = &thir.exprs[expr.clone()];
Decorated {
contents: Box::new(ExprKind::Tuple { fields: vec![] }),
hir_id: None,
attributes: vec![],
ty: expr.ty.sinto(s),
span: expr.span.sinto(s),

pub fn body_from_id<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>(
id: rustc_hir::BodyId,
s: &S,
) -> Body {
// **Important:**
// We need a local id here, and we get it from the owner id, which must
// be local. It is safe to do so, because if we have access to HIR objects,
// it necessarily means we are exploring a local item (we don't have
// access to the HIR of external objects, only their MIR).
Body::body(s.base().tcx.hir().body_owner_def_id(id), s)
}

mod implementations {
use super::*;
impl IsBody for () {
fn body<'tcx, S: UnderOwnerState<'tcx>>(_did: RLocalDefId, _s: &S) -> Self {
()
}
}
impl IsBody for ThirBody {
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self {
let (thir, expr) = get_thir(did, s);
if *CORE_EXTRACTION_MODE {
let expr = &thir.exprs[expr.clone()];
Decorated {
contents: Box::new(ExprKind::Tuple { fields: vec![] }),
hir_id: None,
attributes: vec![],
ty: expr.ty.sinto(s),
span: expr.span.sinto(s),
}
} else {
expr.sinto(&with_owner_id(s.base(), thir, (), did.to_def_id()))
}
} else {
expr.sinto(&with_owner_id(s.base(), thir, (), did.to_def_id()))
}
}
}

impl<A: IsBody, B: IsBody> IsBody for (A, B) {
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self {
(A::body(did, s), B::body(did, s))
impl<A: IsBody, B: IsBody> IsBody for (A, B) {
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self {
(A::body(did, s), B::body(did, s))
}
}
}

impl<MirKind: IsMirKind + Clone + 'static> IsBody for MirBody<MirKind> {
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self {
let (thir, _) = get_thir(did, s);
let mir = Rc::new(s.base().tcx.mir_built(did).borrow().clone());
mir.sinto(&with_owner_id(s.base(), thir, mir.clone(), did.to_def_id()))
impl<MirKind: IsMirKind + Clone + 'static> IsBody for MirBody<MirKind> {
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self {
let (thir, _) = get_thir(did, s);
let mir = Rc::new(s.base().tcx.mir_built(did).borrow().clone());
mir.sinto(&with_owner_id(s.base(), thir, mir.clone(), did.to_def_id()))
}
}
}
}

impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, Body> for rustc_hir::BodyId {
fn sinto(&self, s: &S) -> Body {
body_from_id::<Body, _>(self.clone(), s)
impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto<S, Body> for rustc_hir::BodyId {
fn sinto(&self, s: &S) -> Body {
body_from_id::<Body, _>(self.clone(), s)
}
}
}
Loading

0 comments on commit 2a72e1d

Please sign in to comment.