diff --git a/book/src/guide/run.md b/book/src/guide/run.md index 320e77b0cb..51af7491f7 100644 --- a/book/src/guide/run.md +++ b/book/src/guide/run.md @@ -113,7 +113,7 @@ driver](https://rustc-dev-guide.rust-lang.org/rustc-driver.html?highlight=driver (similar to how clippy works) meaning it uses rustc as a library to "drive" compilation performing additional analysis along the way. Running the binary requires dynamically linking a correct version of `librustc`. Thus, to avoid the -hassle you should never execute it directly. Instead, use `rustc-flux` or `cargo-flux`. +hassle you should never execute it directly. Instead, use `rustc-flux` or `cargo-flux`. ## Editor Support @@ -142,21 +142,21 @@ Add this to the workspace settings i.e. `.vscode/settings.json` You can set various `env` variables to customize the behavior of `flux`. -* `FLUX_CONFIG` tells `flux` where to find a config file for these settings. - * By default, `flux` searches its directory for a `flux.toml` or `.flux.toml`. -* `FLUX_SYSROOT` tells `cargo-flux` and `rustc-flux` where to find the `flux-driver` binary. - * Defaults to the default installation location in `~/.flux`. -* `FLUX_LOG_DIR=path/to/log/` sets the directory where constraints, timing and cache are saved. Defaults to `./log/`. -* `FLUX_DUMP_CONSTRAINT=1` tell `flux` to dump constraints generated for each function. -* `FLUX_DUMP_CHECKER_TRACE=1` saves the checker's trace (useful for debugging!) -* `FLUX_DUMP_TIMINGS=1` saves the profile information -* `FLUX_DUMP_MIR=1` saves the low-level MIR for each analyzed function -* `FLUX_POINTER_WIDTH=N` the size of (either `32` or `64`), used to determine if an integer cast is lossy (default `64`). -* `FLUX_CHECK_DEF=name` only checks definitions containing `name` as a substring -* `FLUX_CHECK_FILES=path/to/file1.rs,path/to/file2.rs` only checks the specified files -* `FLUX_CACHE=1"` switches on query caching and saves the cache in `FLUX_CACHE_FILE` -* `FLUX_CACHE_FILE=file.json` customizes the cache file, default `FLUX_LOG_DIR/cache.json` -* `FLUX_CHECK_OVERFLOW=1` checks for over and underflow on arithmetic integer +- `FLUX_CONFIG` tells `flux` where to find a config file for these settings. + - By default, `flux` searches its directory for a `flux.toml` or `.flux.toml`. +- `FLUX_SYSROOT` tells `cargo-flux` and `rustc-flux` where to find the `flux-driver` binary. + - Defaults to the default installation location in `~/.flux`. +- `FLUX_LOG_DIR=path/to/log/` sets the directory where constraints, timing and cache are saved. Defaults to `./log/`. +- `FLUX_DUMP_CONSTRAINT=1` tell `flux` to dump constraints generated for each function. +- `FLUX_DUMP_CHECKER_TRACE=1` saves the checker's trace (useful for debugging!) +- `FLUX_DUMP_TIMINGS=1` saves the profile information +- `FLUX_DUMP_MIR=1` saves the low-level MIR for each analyzed function +- `FLUX_POINTER_WIDTH=N` the size of (either `32` or `64`), used to determine if an integer cast is lossy (default `64`). +- `FLUX_CHECK_DEF=name` only checks definitions containing `name` as a substring +- `FLUX_CHECK_FILES=/absolute/path/to/file1.rs,/absolute/path/to/file2.rs` only checks the specified files +- `FLUX_CACHE=1"` switches on query caching and saves the cache in `FLUX_CACHE_FILE` +- `FLUX_CACHE_FILE=file.json` customizes the cache file, default `FLUX_LOG_DIR/cache.json` +- `FLUX_CHECK_OVERFLOW=1` checks for over and underflow on arithmetic integer operations, default `0`. When set to `0`, it still checks for underflow on unsigned integer subtraction. diff --git a/crates/flux-common/src/dbg.rs b/crates/flux-common/src/dbg.rs index 73ed4cd53c..0f5722fb68 100644 --- a/crates/flux-common/src/dbg.rs +++ b/crates/flux-common/src/dbg.rs @@ -77,7 +77,8 @@ macro_rules! _statement{ let local_names = &ck.body.local_names; let rcx_json = RefineCtxtTrace::new(genv, $rcx); 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) + let span_json = SpanTrace::new(genv, $span); + 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) } }}; } diff --git a/crates/flux-driver/src/callbacks.rs b/crates/flux-driver/src/callbacks.rs index 0cad11d33a..0efcf46d68 100644 --- a/crates/flux-driver/src/callbacks.rs +++ b/crates/flux-driver/src/callbacks.rs @@ -159,9 +159,15 @@ impl<'genv, 'tcx> CrateChecker<'genv, 'tcx> { let tcx = self.genv.tcx(); let span = tcx.def_span(def_id); let sm = tcx.sess.source_map(); + let current_dir = tcx.sess.opts.working_dir.clone(); if let FileName::Real(file_name) = sm.span_to_filename(span) { - if let Some(path) = file_name.local_path() { - let file = path.to_string_lossy().to_string(); + if let Some(file_path) = file_name.local_path() + && let Some(current_dir_path) = current_dir.local_path() + { + let file = current_dir_path + .join(file_path) + .to_string_lossy() + .to_string(); return config::is_checked_file(&file); } } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index fadec34766..a7d6ca3ead 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -51,7 +51,9 @@ use crate::{ ghost_statements::{GhostStatement, GhostStatements, Point}, primops, queue::WorkQueue, - type_env::{BasicBlockEnv, BasicBlockEnvShape, PtrToRefBound, TypeEnv, TypeEnvTrace}, + type_env::{ + BasicBlockEnv, BasicBlockEnvShape, PtrToRefBound, SpanTrace, TypeEnv, TypeEnvTrace, + }, }; type Result = std::result::Result; diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 65931b723a..13775baf67 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -33,7 +33,7 @@ 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_span::{Span, Symbol}; use rustc_type_ir::BoundVar; use serde::Serialize; @@ -926,3 +926,34 @@ impl TypeEnvTrace { TypeEnvTrace(bindings) } } + +#[derive(Serialize, DebugAsJson)] +pub struct SpanTrace { + file: Option, + start_line: usize, + start_col: usize, + end_line: usize, + end_col: usize, +} + +impl SpanTrace { + fn span_file(tcx: TyCtxt, span: Span) -> Option { + let sm = tcx.sess.source_map(); + let current_dir = &tcx.sess.opts.working_dir; + let current_dir = current_dir.local_path()?; + if let rustc_span::FileName::Real(file_name) = sm.span_to_filename(span) { + let file_path = file_name.local_path()?; + let full_path = current_dir.join(file_path); + Some(full_path.display().to_string()) + } else { + None + } + } + pub fn new(genv: GlobalEnv, span: Span) -> Self { + let tcx = genv.tcx(); + let sm = tcx.sess.source_map(); + let (_, start_line, start_col, end_line, end_col) = sm.span_to_location_info(span); + let file = SpanTrace::span_file(tcx, span); + SpanTrace { file, start_line, start_col, end_line, end_col } + } +} diff --git a/tools/vscode/src/extension.ts b/tools/vscode/src/extension.ts index 345252c21b..c8e1e1a0db 100644 --- a/tools/vscode/src/extension.ts +++ b/tools/vscode/src/extension.ts @@ -39,7 +39,7 @@ export function activate(context: vscode.ExtensionContext) { fluxViewProvider.toggle(); const editor = vscode.window.activeTextEditor; if (editor) { - infoProvider.runFlux(editor.document.fileName, () => { fluxViewProvider.updateView(); }); + infoProvider.runFlux(workspacePath, editor.document.fileName, () => { fluxViewProvider.updateView(); }); } }); context.subscriptions.push(disposable); @@ -64,14 +64,14 @@ export function activate(context: vscode.ExtensionContext) { // Track the set of saved (updated) source files context.subscriptions.push( vscode.workspace.onDidSaveTextDocument((document) => { - fluxViewProvider.runFlux(document.fileName); + fluxViewProvider.runFlux(workspacePath, document.fileName); } )); // Track the set of opened files context.subscriptions.push( vscode.workspace.onDidOpenTextDocument((document) => { - fluxViewProvider.runFlux(document.fileName); + fluxViewProvider.runFlux(workspacePath, document.fileName); } )); @@ -80,9 +80,10 @@ export function activate(context: vscode.ExtensionContext) { // Reload the flux trace information for changedFiles const logFilePattern = new vscode.RelativePattern(workspacePath, checkerPath); const fileWatcher = vscode.workspace.createFileSystemWatcher(logFilePattern); + console.log(`fileWatcher at:`, logFilePattern); fileWatcher.onDidChange((uri) => { - // console.log(`checker trace changed: ${uri.fsPath}`); + console.log(`checker trace changed: ${uri.fsPath}`); infoProvider.loadFluxInfo() .then(() => fluxViewProvider.updateView()) }); @@ -94,6 +95,7 @@ const execPromise = promisify(child_process.exec); async function runShellCommand(env: NodeJS.ProcessEnv, command: string) { try { + console.log("Running command: ", command); const { stdout, stderr } = await execPromise(command, { env: env, cwd: vscode.workspace.workspaceFolders?.[0]?.uri.fsPath @@ -105,7 +107,7 @@ async function runShellCommand(env: NodeJS.ProcessEnv, command: string) { return stdout.trim(); } catch (error) { - console.log(`Command failed: ${error}`); + console.log(`Command failed:`, error); // vscode.window.showErrorMessage(`Command failed: ${error}`); // throw error; } @@ -122,14 +124,17 @@ async function runTouch(file: string) { await runShellCommand(process.env, command) } -// run `cargo flux` on the file -async function runCargoFlux(file: string) { +// run `cargo flux` on the file (absolute path) +async function runCargoFlux(workspacePath: string, file: string) { + const logDir = path.join(workspacePath, 'log'); const fluxEnv = { ...process.env, + FLUX_LOG_DIR : logDir, FLUX_DUMP_CHECKER_TRACE : '1', FLUX_CHECK_FILES : file, }; const command = `cargo flux`; + console.log("Running flux:", fluxEnv, command); await runShellCommand(fluxEnv, command); } @@ -158,7 +163,7 @@ class InfoProvider { } public setPosition(file: string, line: number, column: number, text: string) { - this.currentFile = this.relFile(file); + this.currentFile = file; // this.relFile(file); this.currentLine = line; this.currentColumn = column; this.currentPosition = text.slice(0, column - 1).trim() === '' ? Position.Start : Position.End; @@ -176,6 +181,7 @@ class InfoProvider { private updateInfo(fileName: string, fileInfo: LineInfo[]) { const startMap = this.positionMap(fileInfo, Position.Start); const endMap = this.positionMap(fileInfo, Position.End); + console.log("updateInfo:", fileName, startMap, endMap); this._StartMap.set(fileName, startMap); this._EndMap.set(fileName, endMap); } @@ -184,10 +190,15 @@ class InfoProvider { const file = this.currentFile; const pos = this.currentPosition; const line = this.currentLine; + const map = pos === Position.Start ? this._StartMap : this._EndMap; + console.log("getLineInfo (0):", file, pos, line, map); if (file) { - const map = pos === Position.Start ? this._StartMap : this._EndMap; - if (map.has(file)) { - return map.get(file)?.get(line); + const fileInfo = map.get(file); + console.log("getLineInfo (1):", fileInfo); + if (fileInfo) { + let lineInfo = fileInfo.get(line); + console.log("getLineInfo (2):", lineInfo); + return lineInfo; } else { return 'loading'; } @@ -198,7 +209,7 @@ class InfoProvider { return this.currentLine; } - public async runFlux(file: string, beforeLoad: () => void) { + public async runFlux(workspacePath: string, file: string, beforeLoad: () => void) { if (!file.endsWith('.rs')) { return; } const src = this.relFile(file); @@ -217,7 +228,8 @@ class InfoProvider { await runTouch(src); const curAt = getFileModificationTime(file); this._ModifiedAt.set(src, curAt); - await runCargoFlux(src) + // note we use `file` for the ABSOLUTE path due to odd cargo workspace behavior + await runCargoFlux(workspacePath, file) } public async loadFluxInfo() { @@ -320,8 +332,8 @@ class FluxViewProvider implements vscode.WebviewViewProvider { } } - public runFlux(file: string) { - this._infoProvider.runFlux(file, () => { this.updateView(); }) + public runFlux(workspacePath: string, file: string) { + this._infoProvider.runFlux(workspacePath, file, () => { this.updateView(); }) .then(() => this._infoProvider.loadFluxInfo()) .then(() => this.updateView()); } @@ -612,7 +624,7 @@ type Rcx = { } type StmtSpan = { - file: string; + file: string | null; start_line: number; start_col: number; end_line: number; @@ -644,15 +656,27 @@ function parseStatementSpan(span: string): StmtSpan | undefined { return undefined; } +function parseStatementSpanJSON(span: string): StmtSpan | undefined { + if (span) { + return JSON.parse(span); + } + return undefined; +} + + function parseEvent(event: any): [string, LineInfo] | undefined { + try { const position = event.fields.event === 'statement_start' ? Position.Start : (event.fields.event === 'statement_end' ? Position.End : undefined); if (position !== undefined) { - const stmt_span = parseStatementSpan(event.fields.stmt_span); - if (stmt_span /* && files.has(stmt_span.file) */) { + const stmt_span = parseStatementSpanJSON(event.fields.stmt_span_json); + if (stmt_span && stmt_span.file) { const info = {line: stmt_span.end_line, pos: position, rcx: event.fields.rcx_json, env: event.fields.env_json}; return [stmt_span.file, info]; } } + } catch (error) { + console.log(`Failed to parse event: ${error}`); + } return undefined; } @@ -728,4 +752,4 @@ function nestedStringHtml(node: NestedString) : string { return html } -/**********************************************************************************************/ \ No newline at end of file +/**********************************************************************************************/