Skip to content

Commit

Permalink
[Refactor] Add HIR helpers (#163)
Browse files Browse the repository at this point in the history
* [Refactor] Add HIR helpers

* Update stainless version.
  • Loading branch information
yannbolliger authored Jun 24, 2021
1 parent 0857e6b commit 3096b8d
Show file tree
Hide file tree
Showing 5 changed files with 45 additions and 33 deletions.
2 changes: 1 addition & 1 deletion .stainless-version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
noxt-0.8.0-8-gf15f5b5
noxt-0.8.1
2 changes: 1 addition & 1 deletion stainless_extraction/src/expr/spec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
// extraction to directly translate them to the surrounding function's
// variables, instead of extracting new, unrelated identifiers.

let def_id = self.tcx().hir().local_def_id(hir_id).to_def_id();
let def_id = self.base.hir_to_def_id(hir_id);
let outer_fn_txtcx = &self.txtcx;
let outer_fn_params = self.dcx.params();
let f = self.factory();
Expand Down
22 changes: 17 additions & 5 deletions stainless_extraction/src/fns.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
use super::*;

use rustc_hir::def_id::DefId;
use rustc_middle::ty::FnSig;

use stainless_data::ast as st;

Expand All @@ -25,13 +26,28 @@ impl<'a> FnItem<'a> {
}
}

/// This does not include the tparams as they are contained in the generics.
#[derive(Clone, Debug)]
pub struct FnSignature<'l> {
pub id: &'l st::SymbolIdentifier<'l>,
pub tparams: Vec<&'l st::TypeParameterDef<'l>>,
pub params: Params<'l>,
pub return_tpe: st::Type<'l>,
}

impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
/// Panics if the given HirId does not own a HIR body.
pub(super) fn hir_body(&self, hir_id: HirId) -> &'tcx hir::Body<'tcx> {
let body_id = self.tcx.hir().body_owned_by(hir_id);
self.tcx.hir().body(body_id)
}

pub(super) fn ty_fn_sig(&self, def_id: DefId) -> FnSig<'tcx> {
let poly_fn_sig = self.tcx.fn_sig(def_id);
self.tcx.liberate_late_bound_regions(def_id, poly_fn_sig)
}
}

/// Identifies the specific implementation/instance of a type class that is
/// needed at a method call site.
#[derive(Debug, Eq, PartialEq)]
Expand All @@ -49,10 +65,6 @@ pub struct TypeClassKey<'l> {
impl PartialEq<st::ClassType<'_>> for TypeClassKey<'_> {
fn eq(&self, other: &st::ClassType<'_>) -> bool {
let st::ClassType { id, tps } = other;
let key = TypeClassKey {
id: *id,
recv_tps: tps.clone(),
};
key == *self
self.id == *id && self.recv_tps == *tps
}
}
19 changes: 7 additions & 12 deletions stainless_extraction/src/krate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {

impl<'xtor, 'l, 'tcx> ItemLikeVisitor<'tcx> for ItemVisitor<'xtor, 'l, 'tcx> {
fn visit_item(&mut self, item: &'tcx hir::Item<'tcx>) {
let def_id = self.xtor.tcx.hir().local_def_id(item.hir_id()).to_def_id();
let def_id = self.xtor.hir_to_def_id(item.hir_id());
let def_path_str = self.xtor.tcx.def_path_str(def_id);

match &item.kind {
Expand Down Expand Up @@ -120,7 +120,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
let fns = items
.filter_map(|(hir_id, kind, defaultness)| match kind {
AssocItemKind::Fn { .. } => {
let fn_id = self.xtor.tcx.hir().local_def_id(hir_id).to_def_id();
let fn_id = self.xtor.hir_to_def_id(hir_id);
Some(self.xtor.create_fn_item(fn_id, !defaultness.has_value()))
}
// ignore consts and type aliases in impl blocks
Expand Down Expand Up @@ -316,8 +316,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {

// Extract the function signature
let Generics { tparams, txtcx, .. } = self.get_or_extract_generics(def_id);
let poly_fn_sig = self.tcx.fn_sig(def_id);
let fn_sig = self.tcx.liberate_late_bound_regions(def_id, poly_fn_sig);
let fn_sig = self.ty_fn_sig(def_id);
let params: Params<'l> = fn_sig
.inputs()
.iter()
Expand Down Expand Up @@ -349,12 +348,9 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
/// Extract a local function
pub(super) fn extract_local_fn(&mut self, fn_item: &FnItem<'l>) -> &'l st::FunDef<'l> {
let f = self.factory();
let tcx = self.tcx;

assert!(fn_item.def_id.is_local());
let hir_id = tcx
.hir()
.local_def_id_to_hir_id(fn_item.def_id.expect_local());
let hir_id = self.ldef_to_hir_id(fn_item.def_id.expect_local());
let class_def = self.get_class_of_method(fn_item.fd_id);

// Extract flags
Expand Down Expand Up @@ -483,10 +479,9 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
let adt_def = self.tcx.adt_def(def_id);

// Extract flags for local def ids.
let (flags, mut flags_by_symbol, hir_id_opt) = def_id
.as_local()
.map(|local_def_id| {
let hir_id = self.tcx.hir().local_def_id_to_hir_id(local_def_id);
let (flags, mut flags_by_symbol, hir_id_opt) = self
.def_to_hir_id(def_id)
.map(|hir_id| {
let (carrier_flags, by_symbol) = self.extract_flags(hir_id);
(carrier_flags.to_stainless(f), by_symbol, Some(hir_id))
})
Expand Down
33 changes: 19 additions & 14 deletions stainless_extraction/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -303,6 +303,20 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
self.factory().Variable(new_id, var.tpe, flags)
}

fn hir_to_def_id(&self, hir_id: HirId) -> DefId {
self.tcx.hir().local_def_id(hir_id).to_def_id()
}

/// Returns None if the `def_id` is not local.
fn ldef_to_hir_id(&self, ldi: LocalDefId) -> HirId {
self.tcx.hir().local_def_id_to_hir_id(ldi)
}

/// Returns None if the `def_id` is not local.
fn def_to_hir_id(&self, def_id: DefId) -> Option<HirId> {
def_id.as_local().map(|ldi| self.ldef_to_hir_id(ldi))
}

/// Get a BodyExtractor for some item with a body (like a function)
fn enter_body<T, F>(
&mut self,
Expand Down Expand Up @@ -365,10 +379,7 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
let local_def_id = tcx.hir().local_def_id(hir_id);
assert!(tcx.has_typeck_results(local_def_id));
let tables = tcx.typeck(local_def_id);

// Fetch the body and the corresponding DefContext containing all bindings
let body_id = tcx.hir().body_owned_by(hir_id);
let body = tcx.hir().body(body_id);
let body = base.hir_body(hir_id);

BodyExtractor {
arena,
Expand Down Expand Up @@ -400,16 +411,10 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
}

fn return_tpe(&mut self) -> st::Type<'l> {
let hir_id = self
.tcx()
.hir()
.local_def_id_to_hir_id(self.tables.hir_owner);
let sigs = self.tables.liberated_fn_sigs();
let sig = sigs.get(hir_id).unwrap();
let decl = self.tcx().hir().fn_decl_by_hir_id(hir_id).unwrap();
self
.base
.extract_ty(sig.output(), &self.txtcx, decl.output.span())
let hir_id = self.base.ldef_to_hir_id(self.tables.hir_owner);
let span = self.tcx().hir().span(hir_id);
let sig = self.base.ty_fn_sig(self.tables.hir_owner.to_def_id());
self.base.extract_ty(sig.output(), &self.txtcx, span)
}

fn extract_body_expr(&mut self, ldi: LocalDefId) -> st::Expr<'l> {
Expand Down

0 comments on commit 3096b8d

Please sign in to comment.