Make vscode-extension work on vtock (#945)

* add workspacePath to runFlux

* next: JSON the span

* update doc

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.
 

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

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

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<T = ()> = std::result::Result<T, CheckerError>;

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<String>,
+    start_line: usize,
+    start_col: usize,
+    end_line: usize,
+    end_col: usize,
+}
+
+impl SpanTrace {
+    fn span_file(tcx: TyCtxt, span: Span) -> Option<String> {
+        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 }
+    }
+}

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
 }
 
-/**********************************************************************************************/
+/**********************************************************************************************/