Skip to content

Re: Introduce Tracing into Chalk #409

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.

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

Closed
wants to merge 6 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
255 changes: 215 additions & 40 deletions Cargo.lock

Large diffs are not rendered by default.

2 changes: 2 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ rustyline = "1.0"
salsa = "0.10.0"
serde = "1.0"
serde_derive = "1.0"
tracing = "0.1"
tracing-subscriber = "0.2"

[dependencies.chalk-parse]
version = "0.1.0"
Expand Down
1 change: 1 addition & 0 deletions chalk-engine/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ default = []

[dependencies]
rustc-hash = { version = "1.0.0" }
tracing = "0.1"

[dependencies.chalk-macros]
version = "0.1.0"
Expand Down
2 changes: 2 additions & 0 deletions chalk-engine/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@

#[macro_use]
extern crate chalk_macros;
#[macro_use]
extern crate tracing;

use crate::context::Context;
use std::cmp::min;
Expand Down
53 changes: 21 additions & 32 deletions chalk-engine/src/logic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ impl<C: Context> Forest<C> {
mut test: impl FnMut(&C::InferenceNormalizedSubst) -> bool,
) -> bool {
if let Some(answer) = self.tables[table].answer(answer) {
info!("answer cached = {:?}", answer);
info!(?answer, "answer cached");
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Woah! what is happening here. I guess this is a different for how tracing works?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yup, in tracing the logging macros generate Events which may contain a number of fields. The ? sigil is a shorthand for creating a new field using the Debug implementation of answer.

return test(C::inference_normalized_subst_from_subst(&answer.subst));
}

Expand Down Expand Up @@ -171,14 +171,13 @@ impl<C: Context> Forest<C> {
/// In terms of the NFTD paper, creating a new table corresponds
/// to the *New Subgoal* step as well as the *Program Clause
/// Resolution* steps.
#[instrument(level = "debug", skip(self, context, infer))]
fn get_or_create_table_for_subgoal(
&mut self,
context: &impl ContextOps<C>,
infer: &mut dyn InferenceTable<C>,
subgoal: &Literal<C>,
) -> Option<(TableIndex, C::UniverseMap)> {
debug_heading!("get_or_create_table_for_subgoal(subgoal={:?})", subgoal);

// Subgoal abstraction:
let (ucanonical_subgoal, universe_map) = match subgoal {
Literal::Positive(subgoal) => {
Expand All @@ -204,23 +203,23 @@ impl<C: Context> Forest<C> {
/// In terms of the NFTD paper, creating a new table corresponds
/// to the *New Subgoal* step as well as the *Program Clause
/// Resolution* steps.
#[instrument(level = "debug", skip(self))]
pub(crate) fn get_or_create_table_for_ucanonical_goal(
&mut self,
context: &impl ContextOps<C>,
goal: C::UCanonicalGoalInEnvironment,
) -> TableIndex {
debug_heading!("get_or_create_table_for_ucanonical_goal({:?})", goal);

if let Some(table) = self.tables.index_of(&goal) {
debug!("found existing table {:?}", table);
return table;
}

info_heading!(
"creating new table {:?} and goal {:#?}",
self.tables.next_index(),
goal
let _ = info_span!(
"create new table and goal",
table_index = ?self.tables.next_index(),
?goal
);

let coinductive_goal = context.is_coinductive(&goal);
let table = self.tables.insert(goal, coinductive_goal);
self.push_initial_strands(context, table);
Expand Down Expand Up @@ -260,7 +259,7 @@ impl<C: Context> Forest<C> {
match context.program_clauses(&environment, &domain_goal, &mut infer) {
Ok(clauses) => {
for clause in clauses {
info!("program clause = {:#?}", clause);
info!(?clause, "program clause");
let mut infer = infer.clone();
if let Ok(resolvent) = infer.resolvent_clause(
context.interner(),
Expand All @@ -269,7 +268,7 @@ impl<C: Context> Forest<C> {
&subst,
&clause,
) {
info!("pushing initial strand with ex-clause: {:#?}", &resolvent,);
info!(?resolvent, "pushing initial strand with ex-clause");
let strand = Strand {
infer,
ex_clause: resolvent,
Expand All @@ -282,7 +281,7 @@ impl<C: Context> Forest<C> {
}
}
Err(Floundered) => {
debug!("Marking table {:?} as floundered!", table);
debug!(?table, "Marking table as floundered!");
table_ref.mark_floundered();
}
}
Expand All @@ -301,8 +300,8 @@ impl<C: Context> Forest<C> {
Self::simplify_hh_goal(context, &mut infer, subst, environment, hh_goal)
{
info!(
"pushing initial strand with ex-clause: {:#?}",
infer.debug_ex_clause(context.interner(), &ex_clause),
ex_clause = ?infer.debug_ex_clause(context.interner(), &ex_clause),
"pushing initial strand with ex-clause",
);
let strand = Strand {
infer,
Expand Down Expand Up @@ -423,27 +422,21 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
/// This function first attempts to fetch answer that is cached in
/// the table. If none is found, then it will recursively search
/// to find an answer.
#[instrument(level = "debug", skip(self))]
fn ensure_root_answer(
&mut self,
initial_table: TableIndex,
initial_answer: AnswerIndex,
) -> RootSearchResult<()> {
info_heading!(
"ensure_answer(table={:?}, answer={:?})",
initial_table,
initial_answer
);
info!(
"table goal = {:#?}",
self.forest.tables[initial_table].table_goal
);
let goal = &self.forest.tables[initial_table].table_goal;
info!(?goal, "table goal");
// Check if this table has floundered.
if self.forest.tables[initial_table].is_floundered() {
return Err(RootSearchFail::Floundered);
}
// Check for a tabled answer.
if let Some(answer) = self.forest.tables[initial_table].answer(initial_answer) {
info!("answer cached = {:?}", answer);
info!(?answer, "answer cached");
return Ok(());
}

Expand Down Expand Up @@ -839,7 +832,7 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for

// Check for a tabled answer.
if let Some(answer) = self.forest.tables[subgoal_table].answer(answer_index) {
info!("answer cached = {:?}", answer);
info!(?answer, "answer cached");

// There was a previous answer available for this table
// We need to check if we can merge it into the current `Strand`.
Expand Down Expand Up @@ -867,7 +860,7 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
// Next, check if the table is already active. If so, then we
// have a recursive attempt.
if let Some(cyclic_depth) = self.stack.is_active(subgoal_table) {
info!("cycle detected at depth {:?}", cyclic_depth);
info!(?cyclic_depth, "cycle detected at depth");
let minimums = Minimums {
positive: self.stack[cyclic_depth].clock,
negative: TimeStamp::MAX,
Expand Down Expand Up @@ -1426,8 +1419,8 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
}
}

#[instrument(skip(self))]
fn reconsider_floundered_subgoals(&mut self, ex_clause: &mut ExClause<impl Context>) {
info!("reconsider_floundered_subgoals(ex_clause={:#?})", ex_clause,);
let ExClause {
answer_time,
subgoals,
Expand All @@ -1445,12 +1438,8 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
/// Removes the subgoal at `subgoal_index` from the strand's
/// subgoal list and adds it to the strand's floundered subgoal
/// list.
#[instrument(level = "debug", skip(self))]
fn flounder_subgoal(&self, ex_clause: &mut ExClause<impl Context>, subgoal_index: usize) {
info_heading!(
"flounder_subgoal(answer_time={:?}, subgoal={:?})",
ex_clause.answer_time,
ex_clause.subgoals[subgoal_index],
);
let floundered_time = ex_clause.answer_time;
let floundered_literal = ex_clause.subgoals.remove(subgoal_index);
ex_clause.floundered_subgoals.push(FlounderedSubgoal {
Expand Down
6 changes: 3 additions & 3 deletions chalk-engine/src/table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -117,10 +117,10 @@ impl<C: Context> Table<C> {
/// tests trigger this case, and assumptions upstream assume that when
/// `true` is returned here, that a *new* answer was added (instead of an)
/// existing answer replaced.
#[instrument(level = "debug", skip(self))]
pub(super) fn push_answer(&mut self, answer: Answer<C>) -> Option<AnswerIndex> {
assert!(!self.floundered);

debug_heading!("push_answer(answer={:?})", answer);
debug!(
"pre-existing entry: {:?}",
self.answers_hash.get(&answer.subst)
Expand All @@ -142,8 +142,8 @@ impl<C: Context> Table<C> {
};

info!(
"new answer to table with goal {:?}: answer={:?}",
self.table_goal, answer,
goal = ?self.table_goal, answer=?answer,
"new answer to table with goal; answer"
);
if !added {
return None;
Expand Down
5 changes: 1 addition & 4 deletions chalk-integration/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ edition = "2018"
[dependencies]
lalrpop-intern = "0.15.1"
salsa = "0.10.0"
tracing = "0.1"

[dependencies.chalk-engine]
version = "0.9.0"
Expand All @@ -32,7 +33,3 @@ features = ["default-interner"]
[dependencies.chalk-rust-ir]
version = "0.1.0"
path = "../chalk-rust-ir"

[dependencies.chalk-macros]
version = "0.1.0"
path = "../chalk-macros"
2 changes: 1 addition & 1 deletion chalk-integration/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
#![cfg_attr(feature = "bench", feature(test))]

#[macro_use]
extern crate chalk_macros;
extern crate tracing;

pub mod db;
pub mod error;
Expand Down
3 changes: 1 addition & 2 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1247,14 +1247,13 @@ trait LowerImpl {
}

impl LowerImpl for Impl {
#[instrument(level = "debug", skip(self, empty_env, associated_ty_value_ids))]
fn lower_impl(
&self,
empty_env: &Env,
impl_id: ImplId<ChalkIr>,
associated_ty_value_ids: &AssociatedTyValueIds,
) -> LowerResult<rust_ir::ImplDatum<ChalkIr>> {
debug_heading!("LowerImpl::lower_impl(impl_id={:?})", impl_id);

let polarity = self.polarity.lower();
let binders = empty_env.in_binders(self.all_parameters(), |env| {
let trait_ref = self.trait_ref.lower(env)?;
Expand Down
2 changes: 1 addition & 1 deletion chalk-macros/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,4 @@ keywords = ["compiler", "traits", "prolog"]
edition = "2018"

[dependencies]
lazy_static = "1.1.0"
tracing = "0.1"
131 changes: 0 additions & 131 deletions chalk-macros/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,133 +1,2 @@
use std::cell::RefCell;

#[macro_use]
extern crate lazy_static;

#[macro_use]
mod index;

lazy_static! {
pub static ref DEBUG_ENABLED: bool = {
use std::env;
env::var("CHALK_DEBUG")
.ok()
.and_then(|s| s.parse::<u32>().ok())
.map(|x| x >= 2)
.unwrap_or(false)
};
pub static ref INFO_ENABLED: bool = {
use std::env;
env::var("CHALK_DEBUG")
.ok()
.and_then(|s| s.parse::<u32>().ok())
.map(|x| x >= 1)
.unwrap_or(false)
};
}

thread_local! {
pub(crate) static INDENT: RefCell<Vec<String>> = RefCell::new(vec![]);
}

// When CHALK_DEBUG is enabled, we only allow this many frames of
// nested processing, at which point we assume something has gone
// away.
const OVERFLOW_DEPTH: usize = 100;

#[macro_export]
macro_rules! debug {
($($t:tt)*) => {
if *$crate::DEBUG_ENABLED {
$crate::dump(&format!($($t)*), "");
}
}
}

#[macro_export]
macro_rules! debug_heading {
($($t:tt)*) => {
let _ = &if *$crate::DEBUG_ENABLED {
let string = format!($($t)*);
$crate::dump(&string, " {");
$crate::Indent::new(true, string)
} else {
$crate::Indent::new(false, String::new())
};
}
}

#[macro_export]
macro_rules! info {
($($t:tt)*) => {
if *$crate::INFO_ENABLED {
$crate::dump(&format!($($t)*), "");
}
}
}

#[macro_export]
macro_rules! info_heading {
($($t:tt)*) => {
let _ = &if *$crate::INFO_ENABLED {
let string = format!($($t)*);
$crate::dump(&string, " {");
$crate::Indent::new(true, string)
} else {
$crate::Indent::new(false, String::new())
};
}
}

pub fn dump(string: &str, suffix: &str) {
let indent = INDENT.with(|i| i.borrow().len());
let mut first = true;
for line in string.lines() {
if first {
for _ in 0..indent {
eprint!(": ");
}
eprint!("| ");
} else {
eprintln!();
for _ in 0..indent {
eprint!(": ");
}
eprint!(": ");
}
eprint!("{}", line);
first = false;
}

eprintln!("{}", suffix);
}

pub struct Indent {
enabled: bool,
}

impl Indent {
pub fn new(enabled: bool, value: String) -> Self {
if enabled {
INDENT.with(|i| {
i.borrow_mut().push(value);
if i.borrow().len() > OVERFLOW_DEPTH {
eprintln!("CHALK_DEBUG OVERFLOW:");
for v in i.borrow().iter().rev() {
eprintln!("- {}", v);
}
panic!("CHALK_DEBUG OVERFLOW")
}
});
}
Indent { enabled }
}
}

impl Drop for Indent {
fn drop(&mut self) {
if self.enabled {
INDENT.with(|i| i.borrow_mut().pop().unwrap());
dump("}", "");
}
}
}
Loading