Source-level names in JSON trace

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)
         }
     }};

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(())
     }
 

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;
 
@@ -886,20 +888,30 @@ struct TypeEnvBind {
     ty: String,
 }
 
+fn loc_string(local_names: &UnordMap<Local, Symbol>, loc: &Loc) -> Option<String> {
+    if let Loc::Local(local) = loc {
+        let name = local_names.get(local)?;
+        return Some(format!("{}", name));
+    }
+    Some(format!("{:?}", loc))
+}
+
 impl TypeEnvTrace {
-    pub fn new(genv: GlobalEnv, env: &TypeEnv) -> Self {
+    pub fn new(genv: GlobalEnv, local_names: &UnordMap<Local, Symbol>, 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 kind = format!("{:?}", binding.kind);
-                let ty = WithCx::new(&cx, binding.ty.clone());
-                let ty = format!("{:?}", ty);
-                bindings.push(TypeEnvBind { loc, kind, ty });
+                // filtering out bindings that do not correspond to source-level names
+                if let Some(loc) = loc_string(local_names, loc) {
+                    let kind = format!("{:?}", binding.kind);
+                    let ty = WithCx::new(&cx, binding.ty.clone());
+                    let ty = format!("{:?}", ty);
+                    bindings.push(TypeEnvBind { loc, kind, ty });
+                }
             });
 
         TypeEnvTrace(bindings)

crates/flux-rustc-bridge/src/lowering.rs

@@ -8,7 +8,7 @@ use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_infer::{infer::TyCtxtInferExt, traits::Obligation};
 use rustc_macros::{Decodable, Encodable};
 use rustc_middle::{
-    mir::{self as rustc_mir, ConstValue},
+    mir::{self as rustc_mir, ConstValue, VarDebugInfoContents},
     traits::{ImplSource, ObligationCause},
     ty::{
         self as rustc_ty, adjustment as rustc_adjustment, GenericArgKind, ParamConst, ParamEnv,
@@ -151,7 +151,21 @@ impl<'sess, 'tcx> MirLoweringCtxt<'_, 'sess, 'tcx> {
             .map(|local_decl| lower.lower_local_decl(local_decl))
             .try_collect()?;
 
-        let body = Body::new(basic_blocks, local_decls, body_with_facts, infcx);
+        let local_names = lower
+            .rustc_mir
+            .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();
+
+        let body = Body::new(basic_blocks, local_decls, body_with_facts, infcx, local_names);
         Ok(body)
     }
 

crates/flux-rustc-bridge/src/mir.rs

@@ -11,6 +11,7 @@ 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;
@@ -75,6 +76,7 @@ pub struct Body<'tcx> {
     /// See [`mk_fake_predecessors`]
     fake_predecessors: IndexVec<BasicBlock, usize>,
     body_with_facts: BodyWithBorrowckFacts<'tcx>,
+    pub local_names: UnordMap<Local, Symbol>,
 }
 
 #[derive(Debug)]
@@ -371,6 +373,7 @@ impl<'tcx> Body<'tcx> {
         local_decls: IndexVec<Local, LocalDecl>,
         body_with_facts: BodyWithBorrowckFacts<'tcx>,
         infcx: rustc_infer::infer::InferCtxt<'tcx>,
+        local_names: UnordMap<Local, Symbol>,
     ) -> Self {
         let fake_predecessors = mk_fake_predecessors(&basic_blocks);
 
@@ -390,6 +393,7 @@ impl<'tcx> Body<'tcx> {
             fake_predecessors,
             body_with_facts,
             dominator_order_rank,
+            local_names,
         }
     }
 

tools/vscode/src/extension.ts

@@ -381,7 +381,8 @@ class FluxViewProvider implements vscode.WebviewViewProvider {
 
         const envBindings = this._currentEnv?.map(bind => `
             <tr>
-                <td><b style="color: #F26123">${bind.loc}</b> : ${bind.ty} </td>
+                <td><b style="color: #F26123">${bind.loc}</b></td>
+                <td>: ${bind.ty}</td>
             </tr>
           `).join('');