diff --git a/crates/flux-common/src/dbg.rs b/crates/flux-common/src/dbg.rs index f2a9485a6a..73ed4cd53c 100644 --- a/crates/flux-common/src/dbg.rs +++ b/crates/flux-common/src/dbg.rs @@ -70,11 +70,13 @@ pub use crate::_basic_block_start as basic_block_start; #[macro_export] macro_rules! _statement{ - ($pos:literal, $stmt:expr, $rcx:expr, $env:expr, $span:expr, $genv:expr) => {{ + ($pos:literal, $stmt:expr, $rcx:expr, $env:expr, $span:expr, $checker:expr) => {{ if config::dump_checker_trace() { - let genv = $genv; + let ck = $checker; + let genv = ck.genv; + let local_names = &ck.body.local_names; let rcx_json = RefineCtxtTrace::new(genv, $rcx); - let env_json = TypeEnvTrace::new(genv, $env); + let env_json = TypeEnvTrace::new(genv, local_names, $env); tracing::info!(event = concat!("statement_", $pos), stmt = ?$stmt, stmt_span = ?$span, rcx = ?$rcx, env = ?$env, rcx_json = ?rcx_json, env_json = ?env_json) } }}; diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 49e4a2494e..4c080ee3df 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -515,9 +515,9 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { span, )?; bug::track_span(span, || { - dbg::statement!("start", stmt, &infcx, &env, span, self.genv); + dbg::statement!("start", stmt, &infcx, &env, span, &self); self.check_statement(&mut infcx, &mut env, stmt)?; - dbg::statement!("end", stmt, &infcx, &env, span, self.genv); + dbg::statement!("end", stmt, &infcx, &env, span, &self); Ok(()) })?; if !stmt.is_nop() { @@ -1538,7 +1538,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { stmt: &GhostStatement, span: Span, ) -> Result { - dbg::statement!("start", stmt, infcx, env, span, self.genv); + dbg::statement!("start", stmt, infcx, env, span, &self); match stmt { GhostStatement::Fold(place) => { env.fold(&mut infcx.at(span), place).with_span(span)?; @@ -1553,7 +1553,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { .with_span(span)?; } } - dbg::statement!("end", stmt, infcx, env, span, self.genv); + dbg::statement!("end", stmt, infcx, env, span, &self); Ok(()) } diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 131ecd2ea9..ac65183e95 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -30,8 +30,10 @@ use flux_rustc_bridge::{ ty, }; use itertools::{izip, Itertools}; +use rustc_data_structures::unord::UnordMap; use rustc_index::IndexSlice; use rustc_middle::{mir::RETURN_PLACE, ty::TyCtxt}; +use rustc_span::Symbol; use rustc_type_ir::BoundVar; use serde::Serialize; @@ -881,25 +883,48 @@ pub struct TypeEnvTrace(Vec); #[derive(Serialize)] struct TypeEnvBind { - loc: String, + local: LocInfo, + name: Option, kind: String, ty: String, } +#[derive(Serialize)] +enum LocInfo { + Local(String), + Var(String), +} + +fn loc_info(loc: &Loc) -> LocInfo { + match loc { + Loc::Local(local) => LocInfo::Local(format!("{local:?}")), + Loc::Var(var) => LocInfo::Var(format!("{var:?}")), + } +} + +fn loc_name(local_names: &UnordMap, loc: &Loc) -> Option { + if let Loc::Local(local) = loc { + let name = local_names.get(local)?; + return Some(format!("{}", name)); + } + None +} + impl TypeEnvTrace { - pub fn new(genv: GlobalEnv, env: &TypeEnv) -> Self { + pub fn new(genv: GlobalEnv, local_names: &UnordMap, env: &TypeEnv) -> Self { let mut bindings = vec![]; - let cx = PrettyCx::default_with_genv(genv); + let cx = PrettyCx::default_with_genv(genv).hide_regions(true); env.bindings .iter() .filter(|(_, binding)| !binding.ty.is_uninit()) .sorted_by(|(loc1, _), (loc2, _)| loc1.cmp(loc2)) .for_each(|(loc, binding)| { - let loc = format!("{loc:?}"); + let name = loc_name(local_names, loc); + let local = loc_info(loc); let kind = format!("{:?}", binding.kind); let ty = WithCx::new(&cx, binding.ty.clone()); let ty = format!("{:?}", ty); - bindings.push(TypeEnvBind { loc, kind, ty }); + bindings.push(TypeEnvBind { name, local, kind, ty }); }); TypeEnvTrace(bindings) diff --git a/crates/flux-rustc-bridge/src/mir.rs b/crates/flux-rustc-bridge/src/mir.rs index ccd7a440f2..d1c2be90f0 100644 --- a/crates/flux-rustc-bridge/src/mir.rs +++ b/crates/flux-rustc-bridge/src/mir.rs @@ -11,13 +11,14 @@ use rustc_borrowck::consumers::{BodyWithBorrowckFacts, BorrowIndex}; use rustc_data_structures::{ fx::FxIndexMap, graph::{self, dominators::Dominators, DirectedGraph, StartNode}, + unord::UnordMap, }; use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_index::IndexSlice; use rustc_infer::infer::TyCtxtInferExt; use rustc_macros::{TyDecodable, TyEncodable}; use rustc_middle::{ - mir, + mir::{self, VarDebugInfoContents}, ty::{FloatTy, IntTy, ParamConst, TyCtxt, TypingMode, UintTy}, }; pub use rustc_middle::{ @@ -75,6 +76,7 @@ pub struct Body<'tcx> { /// See [`mk_fake_predecessors`] fake_predecessors: IndexVec, body_with_facts: BodyWithBorrowckFacts<'tcx>, + pub local_names: UnordMap, } #[derive(Debug)] @@ -382,7 +384,19 @@ impl<'tcx> Body<'tcx> { for (rank, bb) in (0u32..).zip(reverse_post_order) { dominator_order_rank[bb] = rank; } - + let local_names = body_with_facts + .body + .var_debug_info + .iter() + .flat_map(|var_debug_info| { + if let VarDebugInfoContents::Place(place) = var_debug_info.value { + let local = place.as_local()?; + Some((local, var_debug_info.name)) + } else { + None + } + }) + .collect(); Self { basic_blocks, local_decls, @@ -390,6 +404,7 @@ impl<'tcx> Body<'tcx> { fake_predecessors, body_with_facts, dominator_order_rank, + local_names, } } diff --git a/tools/vscode/src/extension.ts b/tools/vscode/src/extension.ts index b0cec06321..e2452fa58f 100644 --- a/tools/vscode/src/extension.ts +++ b/tools/vscode/src/extension.ts @@ -257,7 +257,6 @@ function collapseBindings(bindings: RcxBind[]): RcxBind[] { } } if (names.length > 0) { binds.push({name: names, sort: sort}) }; - // console.log("collapsed bindings", binds); return binds; } @@ -269,7 +268,7 @@ function parseRcx(rcx: string): Rcx { } function parseEnv(env: string): TypeEnv { - return JSON.parse(env); + return JSON.parse(env).filter((bind: TypeEnvBind) => bind.name) } class FluxViewProvider implements vscode.WebviewViewProvider { @@ -381,7 +380,8 @@ class FluxViewProvider implements vscode.WebviewViewProvider { const envBindings = this._currentEnv?.map(bind => ` - ${bind.loc} : ${bind.ty} + ${bind.name} + : ${bind.ty} `).join(''); @@ -509,10 +509,11 @@ async function readFluxCheckerTrace(): Promise> { } } +// TODO: add local-info to TypeEnvBind type TypeEnvBind = { - loc: String, - kind: String, - ty: String, + name: string | null, + kind: string, + ty: string, } type TypeEnv = TypeEnvBind[];