From fdc4070691d3a3409ff9bdac643f592583e185c9 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 5 Dec 2024 11:14:06 -0800 Subject: [PATCH 1/9] get GlobalEnv inside PrettyCx --- crates/flux-common/src/dbg.rs | 17 +++++++++++++++-- crates/flux-infer/src/refine_tree.rs | 6 +++++- crates/flux-middle/src/pretty.rs | 27 ++++++++++++++++++--------- crates/flux-middle/src/rty/pretty.rs | 2 ++ crates/flux-refineck/src/checker.rs | 8 ++++---- 5 files changed, 44 insertions(+), 16 deletions(-) diff --git a/crates/flux-common/src/dbg.rs b/crates/flux-common/src/dbg.rs index aeeae8c93d..cc7ce53912 100644 --- a/crates/flux-common/src/dbg.rs +++ b/crates/flux-common/src/dbg.rs @@ -68,11 +68,24 @@ macro_rules! _basic_block_start { } 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) => {{ +// if config::dump_checker_trace() { +// let rcx_json = RefineCtxtTrace::new($rcx); +// let env_json = TypeEnvTrace::new($env); +// tracing::info!(event = concat!("statement_", $pos), stmt = ?$stmt, stmt_span = ?$span, rcx = ?$rcx, env = ?$env, rcx_json = ?rcx_json, env_json = ?env_json) +// } +// }}; +// } +// pub use crate::_statement as statement; + #[macro_export] macro_rules! _statement{ - ($pos:literal, $stmt:expr, $rcx:expr, $env:expr, $span:expr) => {{ + ($pos:literal, $stmt:expr, $rcx:expr, $env:expr, $span:expr, $genv:expr) => {{ if config::dump_checker_trace() { - let rcx_json = RefineCtxtTrace::new($rcx); + let genv = $genv; + let rcx_json = RefineCtxtTrace::new(genv, $rcx); let env_json = TypeEnvTrace::new($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-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs index a845e4e65a..63574142e3 100644 --- a/crates/flux-infer/src/refine_tree.rs +++ b/crates/flux-infer/src/refine_tree.rs @@ -8,6 +8,7 @@ use flux_common::{index::IndexVec, iter::IterExt}; use flux_macros::DebugAsJson; use flux_middle::{ global_env::GlobalEnv, + pretty::{PrettyCx, WithCx}, queries::QueryResult, rty::{ canonicalize::{Hoister, HoisterDelegate}, @@ -792,10 +793,12 @@ struct RcxBind { sort: String, } impl RefineCtxtTrace { - pub fn new(rcx: &RefineCtxt) -> Self { + pub fn new(genv: GlobalEnv, rcx: &RefineCtxt) -> Self { let parents = ParentsIter::new(NodePtr::clone(&rcx.ptr)).collect_vec(); let mut bindings = vec![]; let mut exprs = vec![]; + let cx = PrettyCx::default(genv.tcx()).with_genv(genv); + parents.into_iter().rev().for_each(|ptr| { let node = ptr.borrow(); match &node.kind { @@ -804,6 +807,7 @@ impl RefineCtxtTrace { bindings.push(bind); } NodeKind::Assumption(e) if !e.simplify().is_trivially_true() => { + let e = WithCx::new(&cx, e); exprs.push(format!("{e:?}")); } _ => (), diff --git a/crates/flux-middle/src/pretty.rs b/crates/flux-middle/src/pretty.rs index e09b91f4e4..c05185e5f2 100644 --- a/crates/flux-middle/src/pretty.rs +++ b/crates/flux-middle/src/pretty.rs @@ -149,7 +149,10 @@ pub fn pprint_with_default_cx( } pub use crate::_impl_debug_with_default_cx as impl_debug_with_default_cx; -use crate::rty::{BoundReft, BoundReftKind, BoundVariableKind}; +use crate::{ + global_env::GlobalEnv, + rty::{BoundReft, BoundReftKind, BoundVariableKind}, +}; #[derive(Copy, Clone)] pub enum KVarArgs { @@ -158,8 +161,9 @@ pub enum KVarArgs { Hide, } -pub struct PrettyCx<'tcx> { +pub struct PrettyCx<'genv, 'tcx> { pub tcx: TyCtxt<'tcx>, + pub genv: Option>, pub kvar_args: KVarArgs, pub fully_qualified_paths: bool, pub simplify_exprs: bool, @@ -210,9 +214,9 @@ impl Env { } } -pub struct WithCx<'a, 'tcx, T> { +pub struct WithCx<'a, 'genv, 'tcx, T> { data: T, - cx: &'a PrettyCx<'tcx>, + cx: &'a PrettyCx<'genv, 'tcx>, } pub struct Join<'a, I> { @@ -255,10 +259,15 @@ macro_rules! set_opts { }; } -impl PrettyCx<'_> { - pub fn default(tcx: TyCtxt) -> PrettyCx { +impl<'genv, 'tcx> PrettyCx<'genv, 'tcx> { + pub fn with_genv(self, genv: GlobalEnv<'genv, 'tcx>) -> Self { + Self { genv: Some(genv), ..self } + } + + pub fn default(tcx: TyCtxt<'tcx>) -> Self { PrettyCx { tcx, + genv: None, kvar_args: KVarArgs::SelfOnly, fully_qualified_paths: false, simplify_exprs: true, @@ -380,8 +389,8 @@ impl PrettyCx<'_> { } } -impl<'a, 'tcx, T> WithCx<'a, 'tcx, T> { - pub fn new(cx: &'a PrettyCx<'tcx>, data: T) -> Self { +impl<'a, 'genv, 'tcx, T> WithCx<'a, 'genv, 'tcx, T> { + pub fn new(cx: &'a PrettyCx<'genv, 'tcx>, data: T) -> Self { Self { data, cx } } } @@ -451,7 +460,7 @@ where } } -impl fmt::Debug for WithCx<'_, '_, T> { +impl fmt::Debug for WithCx<'_, '_, '_, T> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { ::fmt(&self.data, self.cx, f) } diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index 90da338581..359402f5f7 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -557,3 +557,5 @@ impl_debug_with_default_cx!( BvSize, ExistentialPredicate, ); + + diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 2ff690acfc..49e4a2494e 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); + dbg::statement!("start", stmt, &infcx, &env, span, self.genv); self.check_statement(&mut infcx, &mut env, stmt)?; - dbg::statement!("end", stmt, &infcx, &env, span); + dbg::statement!("end", stmt, &infcx, &env, span, self.genv); 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); + dbg::statement!("start", stmt, infcx, env, span, self.genv); 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); + dbg::statement!("end", stmt, infcx, env, span, self.genv); Ok(()) } From 0196c30e39e1c0ef30c45d23729ae60e82f33178 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 5 Dec 2024 13:53:41 -0800 Subject: [PATCH 2/9] done pretty record --- crates/flux-common/src/dbg.rs | 2 +- crates/flux-infer/src/refine_tree.rs | 6 ++++ crates/flux-middle/src/pretty.rs | 8 +++--- crates/flux-middle/src/rty/expr.rs | 42 +++++++++++++++++++++++++--- crates/flux-middle/src/rty/pretty.rs | 24 +++++++++++++--- crates/flux-refineck/src/type_env.rs | 7 +++-- tools/vscode/src/extension.ts | 2 +- 7 files changed, 75 insertions(+), 16 deletions(-) diff --git a/crates/flux-common/src/dbg.rs b/crates/flux-common/src/dbg.rs index cc7ce53912..861b2d081e 100644 --- a/crates/flux-common/src/dbg.rs +++ b/crates/flux-common/src/dbg.rs @@ -86,7 +86,7 @@ macro_rules! _statement{ if config::dump_checker_trace() { let genv = $genv; let rcx_json = RefineCtxtTrace::new(genv, $rcx); - let env_json = TypeEnvTrace::new($env); + let env_json = TypeEnvTrace::new(genv, $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-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs index 63574142e3..d20170b477 100644 --- a/crates/flux-infer/src/refine_tree.rs +++ b/crates/flux-infer/src/refine_tree.rs @@ -810,6 +810,12 @@ impl RefineCtxtTrace { let e = WithCx::new(&cx, e); exprs.push(format!("{e:?}")); } + NodeKind::Root(binds) => { + for (name, sort) in binds { + let bind = RcxBind { name: format!("{name:?}"), sort: format!("{sort:?}") }; + bindings.push(bind); + } + } _ => (), } }); diff --git a/crates/flux-middle/src/pretty.rs b/crates/flux-middle/src/pretty.rs index c05185e5f2..4b308a01f9 100644 --- a/crates/flux-middle/src/pretty.rs +++ b/crates/flux-middle/src/pretty.rs @@ -260,10 +260,6 @@ macro_rules! set_opts { } impl<'genv, 'tcx> PrettyCx<'genv, 'tcx> { - pub fn with_genv(self, genv: GlobalEnv<'genv, 'tcx>) -> Self { - Self { genv: Some(genv), ..self } - } - pub fn default(tcx: TyCtxt<'tcx>) -> Self { PrettyCx { tcx, @@ -387,6 +383,10 @@ impl<'genv, 'tcx> PrettyCx<'genv, 'tcx> { pub fn hide_sorts(self, b: bool) -> Self { Self { hide_sorts: b, ..self } } + + pub fn with_genv(self, genv: GlobalEnv<'genv, 'tcx>) -> Self { + Self { genv: Some(genv), ..self } + } } impl<'a, 'genv, 'tcx, T> WithCx<'a, 'genv, 'tcx, T> { diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index 53fa701fca..c68997a487 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -28,6 +28,7 @@ use crate::{ big_int::BigInt, fhir::SpecFuncKind, global_env::GlobalEnv, + pretty::*, queries::QueryResult, rty::{ fold::{TypeFoldable, TypeFolder, TypeSuperFoldable}, @@ -1077,11 +1078,22 @@ impl From for Constant { impl_internable!(ExprKind); impl_slice_internable!(Expr, KVar); +#[derive(Debug)] +pub struct FieldBind { + pub name: Symbol, + pub value: T, +} + +impl Pretty for FieldBind { + fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { + define_scoped!(cx, f); + w!("{}: {:?}", ^self.name, &self.value) + } +} mod pretty { use flux_rustc_bridge::def_id_to_string; use super::*; - use crate::pretty::*; #[derive(PartialEq, Eq, PartialOrd, Ord)] enum Precedence { @@ -1163,10 +1175,20 @@ mod pretty { } } ExprKind::FieldProj(e, proj) => { + // base if e.is_atom() { - w!("{:?}.{:?}", e, ^proj.field_idx()) + w!("{:?}", e)?; } else { - w!("({:?}).{:?}", e, ^proj.field_idx()) + w!("({:?})", e)?; + }; + // proj + if let Some(genv) = cx.genv + && let FieldProj::Adt { def_id, field } = proj + && let Ok(adt_sort_def) = genv.adt_sort_def_of(def_id) + { + w!(".{}", ^adt_sort_def.field_names()[*field as usize]) + } else { + w!(".{:?}", ^proj.field_idx()) } } ExprKind::Aggregate(AggregateKind::Tuple(_), flds) => { @@ -1177,7 +1199,19 @@ mod pretty { } } ExprKind::Aggregate(AggregateKind::Adt(def_id), flds) => { - w!("{:?} {{ {:?} }}", def_id, join!(", ", flds)) + if let Some(genv) = cx.genv + && let Ok(adt_sort_def) = genv.adt_sort_def_of(def_id) + { + let field_binds = adt_sort_def + .field_names() + .iter() + .zip(flds) + .map(|(name, value)| FieldBind { name: *name, value: value.clone() }) + .collect_vec(); + w!("{{ {:?} }}", join!(", ", field_binds)) + } else { + w!("{:?} {{ {:?} }}", def_id, join!(", ", flds)) + } } ExprKind::PathProj(e, field) => { if e.is_atom() { diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index 359402f5f7..4f5a0a1195 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -1,5 +1,6 @@ use std::fmt; +use expr::FieldBind; use flux_rustc_bridge::ty::region_to_string; use rustc_type_ir::DebruijnIndex; use ty::{UnevaluatedConst, ValTree}; @@ -277,8 +278,25 @@ impl Pretty for Ty { } TyKind::Param(param_ty) => w!("{}", ^param_ty), TyKind::Downcast(adt, .., variant_idx, fields) => { - w!("{:?}::{}", adt.did(), ^adt.variant(*variant_idx).name)?; - if !fields.is_empty() { + let is_struct = adt.is_struct(); + // base-name + w!("{:?}", adt.did())?; + // variant-name: if it is not a struct + if !is_struct { + w!("::{}", ^adt.variant(*variant_idx).name)?; + } + // fields: use curly-braces + names for structs, otherwise use parens + if is_struct { + let field_binds = adt + .variant(*variant_idx) + .fields + .iter() + .zip(fields) + .map(|(field_def, value)| FieldBind { name: field_def.name, value }) + .collect_vec(); + + w!(" {{ {:?} }}", join!(", ", field_binds))?; + } else if !fields.is_empty() { w!("({:?})", join!(", ", fields))?; } Ok(()) @@ -557,5 +575,3 @@ impl_debug_with_default_cx!( BvSize, ExistentialPredicate, ); - - diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 9642762290..4876aa8194 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -11,6 +11,7 @@ use flux_infer::{ use flux_macros::DebugAsJson; use flux_middle::{ global_env::GlobalEnv, + pretty::{PrettyCx, WithCx}, queries::QueryResult, rty::{ canonicalize::{Hoister, LocalHoister}, @@ -886,8 +887,9 @@ struct TypeEnvBind { } impl TypeEnvTrace { - pub fn new(env: &TypeEnv) -> Self { + pub fn new(genv: GlobalEnv, env: &TypeEnv) -> Self { let mut bindings = vec![]; + let cx = PrettyCx::default(genv.tcx()).with_genv(genv); env.bindings .iter() .filter(|(_, binding)| !binding.ty.is_uninit()) @@ -895,7 +897,8 @@ impl TypeEnvTrace { .for_each(|(loc, binding)| { let loc = format!("{loc:?}"); let kind = format!("{:?}", binding.kind); - let ty = format!("{:?}", binding.ty); + let ty = WithCx::new(&cx, binding.ty.clone()); + let ty = format!("{:?}", ty); bindings.push(TypeEnvBind { loc, kind, ty }); }); diff --git a/tools/vscode/src/extension.ts b/tools/vscode/src/extension.ts index b70b5e5f8a..d19cbcb623 100644 --- a/tools/vscode/src/extension.ts +++ b/tools/vscode/src/extension.ts @@ -257,7 +257,7 @@ function collapseBindings(bindings: RcxBind[]): RcxBind[] { } } if (names.length > 0) { binds.push({name: names, sort: sort}) }; - console.log("collapsed bindings", binds); + // console.log("collapsed bindings", binds); return binds; } From 39b6006e01ea8d4b8abc03fe2482c0a865467a03 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 5 Dec 2024 15:16:59 -0800 Subject: [PATCH 3/9] done pretty record --- crates/flux-common/src/dbg.rs | 12 ------------ crates/flux-infer/src/refine_tree.rs | 2 +- crates/flux-middle/src/pretty.rs | 9 +++++---- crates/flux-refineck/src/type_env.rs | 2 +- 4 files changed, 7 insertions(+), 18 deletions(-) diff --git a/crates/flux-common/src/dbg.rs b/crates/flux-common/src/dbg.rs index 861b2d081e..f2a9485a6a 100644 --- a/crates/flux-common/src/dbg.rs +++ b/crates/flux-common/src/dbg.rs @@ -68,18 +68,6 @@ macro_rules! _basic_block_start { } 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) => {{ -// if config::dump_checker_trace() { -// let rcx_json = RefineCtxtTrace::new($rcx); -// let env_json = TypeEnvTrace::new($env); -// tracing::info!(event = concat!("statement_", $pos), stmt = ?$stmt, stmt_span = ?$span, rcx = ?$rcx, env = ?$env, rcx_json = ?rcx_json, env_json = ?env_json) -// } -// }}; -// } -// pub use crate::_statement as statement; - #[macro_export] macro_rules! _statement{ ($pos:literal, $stmt:expr, $rcx:expr, $env:expr, $span:expr, $genv:expr) => {{ diff --git a/crates/flux-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs index d20170b477..18f470ee11 100644 --- a/crates/flux-infer/src/refine_tree.rs +++ b/crates/flux-infer/src/refine_tree.rs @@ -797,7 +797,7 @@ impl RefineCtxtTrace { let parents = ParentsIter::new(NodePtr::clone(&rcx.ptr)).collect_vec(); let mut bindings = vec![]; let mut exprs = vec![]; - let cx = PrettyCx::default(genv.tcx()).with_genv(genv); + let cx = PrettyCx::default_with_genv(genv); parents.into_iter().rev().for_each(|ptr| { let node = ptr.borrow(); diff --git a/crates/flux-middle/src/pretty.rs b/crates/flux-middle/src/pretty.rs index 4b308a01f9..51ec855ce2 100644 --- a/crates/flux-middle/src/pretty.rs +++ b/crates/flux-middle/src/pretty.rs @@ -279,6 +279,11 @@ impl<'genv, 'tcx> PrettyCx<'genv, 'tcx> { } } + pub fn default_with_genv(genv: GlobalEnv<'genv, 'tcx>) -> Self { + let def = Self::default(genv.tcx()); + Self { genv: Some(genv), ..def } + } + pub fn merge(&mut self, opts: &config::Value) { set_opts!( self, @@ -383,10 +388,6 @@ impl<'genv, 'tcx> PrettyCx<'genv, 'tcx> { pub fn hide_sorts(self, b: bool) -> Self { Self { hide_sorts: b, ..self } } - - pub fn with_genv(self, genv: GlobalEnv<'genv, 'tcx>) -> Self { - Self { genv: Some(genv), ..self } - } } impl<'a, 'genv, 'tcx, T> WithCx<'a, 'genv, 'tcx, T> { diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 4876aa8194..131ecd2ea9 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -889,7 +889,7 @@ struct TypeEnvBind { impl TypeEnvTrace { pub fn new(genv: GlobalEnv, env: &TypeEnv) -> Self { let mut bindings = vec![]; - let cx = PrettyCx::default(genv.tcx()).with_genv(genv); + let cx = PrettyCx::default_with_genv(genv); env.bindings .iter() .filter(|(_, binding)| !binding.ty.is_uninit()) From a70354dcf924f1b9b96de10d6cbc0856dfed69b7 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 5 Dec 2024 19:49:39 -0800 Subject: [PATCH 4/9] only drop struct name for top-level index --- crates/flux-middle/src/rty/expr.rs | 2 +- crates/flux-middle/src/rty/pretty.rs | 26 +++++++++++++++++++++++++- tools/vscode/src/extension.ts | 1 - 3 files changed, 26 insertions(+), 3 deletions(-) diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index c68997a487..4cbbe65a82 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -1208,7 +1208,7 @@ mod pretty { .zip(flds) .map(|(name, value)| FieldBind { name: *name, value: value.clone() }) .collect_vec(); - w!("{{ {:?} }}", join!(", ", field_binds)) + w!("{:?} {{ {:?} }}", def_id, join!(", ", field_binds)) } else { w!("{:?} {{ {:?} }}", def_id, join!(", ", flds)) } diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index 4f5a0a1195..248d125527 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -236,6 +236,30 @@ impl Pretty for SubsetTy { } } +struct TopIndexExpr(Expr); + +impl Pretty for TopIndexExpr { + fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { + define_scoped!(cx, f); + let e = &self.0; + let e = if cx.simplify_exprs { e.simplify() } else { e.clone() }; + if let ExprKind::Aggregate(AggregateKind::Adt(def_id), flds) = e.kind() + && let Some(genv) = cx.genv + && let Ok(adt_sort_def) = genv.adt_sort_def_of(def_id) + { + let field_binds = adt_sort_def + .field_names() + .iter() + .zip(flds) + .map(|(name, value)| FieldBind { name: *name, value: value.clone() }) + .collect_vec(); + w!("{{ {:?} }}", join!(", ", field_binds)) + } else { + w!("{:?}", &self.0) + } + } +} + impl Pretty for Ty { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); @@ -250,7 +274,7 @@ impl Pretty for Ty { w!("[]")?; } } else { - w!("[{:?}]", idx)?; + w!("[{:?}]", TopIndexExpr(idx.clone()))?; } Ok(()) } diff --git a/tools/vscode/src/extension.ts b/tools/vscode/src/extension.ts index d19cbcb623..b0cec06321 100644 --- a/tools/vscode/src/extension.ts +++ b/tools/vscode/src/extension.ts @@ -366,7 +366,6 @@ class FluxViewProvider implements vscode.WebviewViewProvider { private _getHtmlForInfo() { const rcxBindings = this._currentRcx?.bindings.map(bind => { const name = typeof bind.name === 'string' ? bind.name : bind.name.join(' '); - console.log("bind", bind, name); return ` ${name} : ${bind.sort} From 915e6000f1e946ccff96ba1c0c9d4cb571eacc24 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 5 Dec 2024 19:52:42 -0800 Subject: [PATCH 5/9] add comment --- crates/flux-middle/src/rty/pretty.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index 248d125527..7d86c58173 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -236,6 +236,8 @@ impl Pretty for SubsetTy { } } +// This is a trick to avoid pretty printing `S [S { x: 10, y: 20}]` +// and instead just print `S[{x: 10, y: 20}]` for struct-valued indices. struct TopIndexExpr(Expr); impl Pretty for TopIndexExpr { From 5853ea40d16014f40bd6d6b843a6d13f22267b1a Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 6 Dec 2024 05:40:35 -0800 Subject: [PATCH 6/9] add comment --- crates/flux-common/src/dbg.rs | 8 +++++--- crates/flux-refineck/src/checker.rs | 8 ++++---- crates/flux-refineck/src/type_env.rs | 23 +++++++++++++++++------ crates/flux-rustc-bridge/src/lowering.rs | 18 ++++++++++++++++-- crates/flux-rustc-bridge/src/mir.rs | 4 ++++ tools/vscode/src/extension.ts | 3 ++- 6 files changed, 48 insertions(+), 16 deletions(-) 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..15f36e21ef 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; @@ -886,8 +888,16 @@ struct TypeEnvBind { ty: String, } +fn loc_string(local_names: &UnordMap, loc: &Loc) -> Option { + if let Loc::Local(local) = loc { + let name = local_names.get(local)?; + return Some(format!("{}", name)); + } + return Some(format!("{:?}", loc)); +} + 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); env.bindings @@ -895,11 +905,12 @@ impl TypeEnvTrace { .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 }); + 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) diff --git a/crates/flux-rustc-bridge/src/lowering.rs b/crates/flux-rustc-bridge/src/lowering.rs index 6a8af49d61..5b9ea75716 100644 --- a/crates/flux-rustc-bridge/src/lowering.rs +++ b/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) } diff --git a/crates/flux-rustc-bridge/src/mir.rs b/crates/flux-rustc-bridge/src/mir.rs index ccd7a440f2..2b248d660d 100644 --- a/crates/flux-rustc-bridge/src/mir.rs +++ b/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, body_with_facts: BodyWithBorrowckFacts<'tcx>, + pub local_names: UnordMap, } #[derive(Debug)] @@ -371,6 +373,7 @@ impl<'tcx> Body<'tcx> { local_decls: IndexVec, body_with_facts: BodyWithBorrowckFacts<'tcx>, infcx: rustc_infer::infer::InferCtxt<'tcx>, + local_names: UnordMap, ) -> 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, } } diff --git a/tools/vscode/src/extension.ts b/tools/vscode/src/extension.ts index b0cec06321..7091188ea6 100644 --- a/tools/vscode/src/extension.ts +++ b/tools/vscode/src/extension.ts @@ -381,7 +381,8 @@ class FluxViewProvider implements vscode.WebviewViewProvider { const envBindings = this._currentEnv?.map(bind => ` - ${bind.loc} : ${bind.ty} + ${bind.loc} + : ${bind.ty} `).join(''); From 52aba72379cc846be91e63d4e012f043c9d98bb8 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 6 Dec 2024 06:10:57 -0800 Subject: [PATCH 7/9] remove lifetimes from json trace --- crates/flux-refineck/src/type_env.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index dd54bd0c24..995cd56115 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -899,7 +899,7 @@ fn loc_string(local_names: &UnordMap, loc: &Loc) -> Option, 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()) From 6fc4b30552b7958045efd9c3b302c0ce10f5fe17 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 6 Dec 2024 06:16:35 -0800 Subject: [PATCH 8/9] clippy --- crates/flux-refineck/src/type_env.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 995cd56115..ee002d9f1d 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -893,7 +893,7 @@ fn loc_string(local_names: &UnordMap, loc: &Loc) -> Option Date: Fri, 6 Dec 2024 10:21:20 -0800 Subject: [PATCH 9/9] move local_names into Body::new --- crates/flux-refineck/src/type_env.rs | 33 +++++++++++++++++------- crates/flux-rustc-bridge/src/lowering.rs | 18 ++----------- crates/flux-rustc-bridge/src/mir.rs | 17 +++++++++--- tools/vscode/src/extension.ts | 12 ++++----- 4 files changed, 45 insertions(+), 35 deletions(-) diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index ee002d9f1d..ac65183e95 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -883,17 +883,31 @@ pub struct TypeEnvTrace(Vec); #[derive(Serialize)] struct TypeEnvBind { - loc: String, + local: LocInfo, + name: Option, kind: String, ty: String, } -fn loc_string(local_names: &UnordMap, loc: &Loc) -> Option { +#[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)); } - Some(format!("{:?}", loc)) + None } impl TypeEnvTrace { @@ -905,13 +919,12 @@ impl TypeEnvTrace { .filter(|(_, binding)| !binding.ty.is_uninit()) .sorted_by(|(loc1, _), (loc2, _)| loc1.cmp(loc2)) .for_each(|(loc, binding)| { - // 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 }); - } + 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 { name, local, kind, ty }); }); TypeEnvTrace(bindings) diff --git a/crates/flux-rustc-bridge/src/lowering.rs b/crates/flux-rustc-bridge/src/lowering.rs index 5b9ea75716..6a8af49d61 100644 --- a/crates/flux-rustc-bridge/src/lowering.rs +++ b/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, VarDebugInfoContents}, + mir::{self as rustc_mir, ConstValue}, traits::{ImplSource, ObligationCause}, ty::{ self as rustc_ty, adjustment as rustc_adjustment, GenericArgKind, ParamConst, ParamEnv, @@ -151,21 +151,7 @@ impl<'sess, 'tcx> MirLoweringCtxt<'_, 'sess, 'tcx> { .map(|local_decl| lower.lower_local_decl(local_decl)) .try_collect()?; - 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); + let body = Body::new(basic_blocks, local_decls, body_with_facts, infcx); Ok(body) } diff --git a/crates/flux-rustc-bridge/src/mir.rs b/crates/flux-rustc-bridge/src/mir.rs index 2b248d660d..d1c2be90f0 100644 --- a/crates/flux-rustc-bridge/src/mir.rs +++ b/crates/flux-rustc-bridge/src/mir.rs @@ -18,7 +18,7 @@ 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::{ @@ -373,7 +373,6 @@ impl<'tcx> Body<'tcx> { local_decls: IndexVec, body_with_facts: BodyWithBorrowckFacts<'tcx>, infcx: rustc_infer::infer::InferCtxt<'tcx>, - local_names: UnordMap, ) -> Self { let fake_predecessors = mk_fake_predecessors(&basic_blocks); @@ -385,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, diff --git a/tools/vscode/src/extension.ts b/tools/vscode/src/extension.ts index 7091188ea6..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,7 @@ class FluxViewProvider implements vscode.WebviewViewProvider { const envBindings = this._currentEnv?.map(bind => ` - ${bind.loc} + ${bind.name} : ${bind.ty} `).join(''); @@ -510,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[];