1use std::{
3 fmt, fs,
4 io::{self, Write},
5 path::Path,
6};
7
8use flux_config as config;
9use flux_macros::DebugAsJson;
10use rustc_hir::def_id::DefId;
11use rustc_middle::ty::TyCtxt;
12use rustc_span::Span;
13use serde::Serialize;
14
15#[derive(Serialize, DebugAsJson)]
16pub struct SpanTrace {
17 file: Option<String>,
18 start_line: usize,
19 start_col: usize,
20 end_line: usize,
21 end_col: usize,
22}
23
24impl SpanTrace {
25 fn span_file(tcx: TyCtxt, span: Span) -> Option<String> {
26 let sm = tcx.sess.source_map();
27 let current_dir = &tcx.sess.opts.working_dir;
28 let current_dir = current_dir.local_path()?;
29 if let rustc_span::FileName::Real(file_name) = sm.span_to_filename(span) {
30 let file_path = file_name.local_path()?;
31 let full_path = current_dir.join(file_path);
32 Some(full_path.display().to_string())
33 } else {
34 None
35 }
36 }
37 pub fn new(tcx: TyCtxt, span: Span) -> Self {
38 let sm = tcx.sess.source_map();
39 let (_, start_line, start_col, end_line, end_col) = sm.span_to_location_info(span);
40 let file = SpanTrace::span_file(tcx, span);
41 SpanTrace { file, start_line, start_col, end_line, end_col }
42 }
43 pub fn from_path(path: &Path, start_line: usize, start_col: usize, len: usize) -> Self {
44 SpanTrace {
45 file: Some(path.display().to_string()),
46 start_line,
47 start_col,
48 end_line: start_line,
49 end_col: start_col + len,
50 }
51 }
52}
53
54pub fn writer_for_item(
55 tcx: TyCtxt,
56 def_id: DefId,
57 ext: impl AsRef<str>,
58) -> io::Result<impl io::Write> {
59 fs::create_dir_all(config::log_dir())?;
60 let path = config::log_dir().join(dump_base_name(tcx, def_id, ext));
61 let file = fs::File::create(path)?;
62 let buf = std::io::BufWriter::new(file);
63 Ok(buf)
64}
65
66pub fn dump_item_info<T: fmt::Debug>(
67 tcx: TyCtxt,
68 def_id: impl Into<DefId>,
69 ext: impl AsRef<str>,
70 val: T,
71) -> io::Result<()> {
72 let mut writer = writer_for_item(tcx, def_id.into(), ext)?;
73 writeln!(writer, "{val:#?}")
74}
75
76#[macro_export]
77macro_rules! _shape_mode_span {
78 ($tcx:expr, $def_id:expr) => {{
79 let path = $tcx.def_path_str(rustc_hir::def_id::DefId::from($def_id));
80 tracing::info_span!("shape", def_id = path.as_str())
81 }};
82}
83pub use crate::_shape_mode_span as shape_mode_span;
84
85#[macro_export]
86macro_rules! _refine_mode_span {
87 ($tcx:expr, $def_id:expr, $bb_envs:expr) => {{
88 let path = $tcx.def_path_str(rustc_hir::def_id::DefId::from($def_id));
89 tracing::info_span!("refine", def_id = path.as_str(), bb_envs = ?$bb_envs)
90 }};
91}
92pub use crate::_refine_mode_span as refine_mode_span;
93
94#[macro_export]
95macro_rules! _check_fn_span {
96 ($tcx:expr, $def_id:expr) => {{
97 let path = $tcx.def_path_str(rustc_hir::def_id::DefId::from($def_id));
98 tracing::info_span!("check_fn", def_id = path.as_str())
99 }};
100}
101pub use crate::_check_fn_span as check_fn_span;
102
103#[macro_export]
104macro_rules! _basic_block_start {
105 ($bb:expr, $rcx:expr, $env:expr) => {{
106 tracing::debug!(event = "basic_block_start", bb = ?$bb, rcx = ?$rcx, env = ?$env)
107 }};
108}
109pub use crate::_basic_block_start as basic_block_start;
110
111#[macro_export]
112macro_rules! _solution {
113 ($genv:expr, $sol:expr, $span:expr) => {{
114 if config::dump_checker_trace_info() {
115 let genv = $genv;
116 let sol_json = SolutionTrace::new(genv, $sol);
117 let span_json = SpanTrace::new(genv.tcx(), $span);
118 tracing::info!(event = "solution", span = ?span_json, solution = ?sol_json)
119 }
120 }};
121}
122pub use crate::_solution as solution;
123
124#[macro_export]
125macro_rules! _statement{
126 ($pos:literal, $stmt:expr, $infcx:expr, $env:expr, $span:expr, $checker:expr) => {{
127 if config::dump_checker_trace_info() {
128 let rcx = $infcx.cursor();
129 let ck = $checker;
130 let genv = ck.genv;
131 let local_names = &ck.body.local_names;
132 let local_decls = &ck.body.local_decls;
133 let mut cx = PrettyCx::default(genv).show_kvar_args();
134 let rcx_json = RefineCtxtTrace::new(&mut cx, rcx);
135 let env_json = TypeEnvTrace::new(genv, local_names, local_decls, cx, $env);
136 let span_json = SpanTrace::new(genv.tcx(), $span);
137 tracing::info!(event = concat!("statement_", $pos), stmt = ?$stmt, stmt_span = ?$span, rcx = ?rcx, env = ?$env, rcx_json = ?rcx_json, env_json = ?env_json, stmt_span_json = ?span_json)
138 }
139 }};
140}
141pub use crate::_statement as statement;
142
143#[macro_export]
144macro_rules! _terminator{
145 ($pos:literal, $terminator:expr, $rcx:expr, $env:expr) => {{
146 tracing::debug!(event = concat!("terminator_", $pos), terminator = ?$terminator, rcx = ?$rcx, env = ?$env)
147 }};
148}
149pub use crate::_terminator as terminator;
150
151#[macro_export]
152macro_rules! _refine_goto {
153 ($target:expr, $rcx:expr, $env:expr, $bb_env:expr) => {{
154 tracing::debug!(event = "refine_goto", target = ?$target, rcx = ?$rcx, env = ?$env, bb_env = ?$bb_env)
155 }};
156}
157pub use crate::_refine_goto as refine_goto;
158
159#[macro_export]
160macro_rules! _shape_goto_enter {
161 ($target:expr, $env:expr, $bb_env:expr) => {{
162 if let Some(bb_env) = &$bb_env {
163 tracing::debug!(event = "shape_goto_enter", target = ?$target, env = ?&$env, ?bb_env)
164 } else {
165 tracing::debug!(event = "shape_goto_enter", target = ?$target, env = ?&$env, bb_env = "empty")
166 }
167 }};
168}
169pub use crate::_shape_goto_enter as shape_goto_enter;
170
171#[macro_export]
172macro_rules! _shape_goto_exit {
173 ($target:expr, $bb_env:expr) => {{
174 tracing::debug!(event = "shape_goto_exit", target = ?$target, bb_env = ?&$bb_env)
175 }};
176}
177pub use crate::_shape_goto_exit as shape_goto_exit;
178
179#[macro_export]
180macro_rules! _hyperlink {
181 ($tcx:expr, $src_span:expr, $dst_span:expr) => {{
182 let src_json = SpanTrace::new($tcx, $src_span);
183 let dst_json = SpanTrace::new($tcx, $dst_span);
184 tracing::warn!(event = "hyperlink", src_span = ?src_json, dst_span = ?dst_json)
185 }};
186}
187pub use crate::_hyperlink as hyperlink;
188
189#[macro_export]
190macro_rules! _hyperlink_json {
191 ($tcx:expr, $src_span:expr, $dst_json:expr) => {{
192 let src_json = SpanTrace::new($tcx, $src_span);
193 tracing::warn!(event = "hyperlink", src_span = ?src_json, dst_span = ?$dst_json)
194 }};
195}
196pub use crate::_hyperlink_json as hyperlink_json;
197
198fn dump_base_name(tcx: TyCtxt, def_id: DefId, ext: impl AsRef<str>) -> String {
199 let crate_name = tcx.crate_name(def_id.krate);
200 let item_name = tcx.def_path(def_id).to_filename_friendly_no_crate();
201 format!("{crate_name}.{item_name}.{}", ext.as_ref())
202}
203
204#[macro_export]
205macro_rules! _debug_assert_eq3 {
206 ($e1:expr, $e2:expr, $e3:expr) => {{
207 debug_assert!($e1 == $e2 && $e2 == $e3, "{:?} != {:?} != {:?}", $e1, $e2, $e3);
208 }};
209}
210pub use crate::_debug_assert_eq3 as debug_assert_eq3;
211
212pub fn as_subscript<T: ToString>(n: T) -> String {
213 n.to_string()
214 .chars()
215 .map(|c| {
216 match c {
217 '0' => '₀',
218 '1' => '₁',
219 '2' => '₂',
220 '3' => '₃',
221 '4' => '₄',
222 '5' => '₅',
223 '6' => '₆',
224 '7' => '₇',
225 '8' => '₈',
226 '9' => '₉',
227 _ => c,
228 }
229 })
230 .collect()
231}