updated gillian to work with main branch

GaloisInc · Jan 22, 2025 · 2df79d8 · 2df79d8
1 parent 8d33fec
commit 2df79d8
Show file tree

Hide file tree

Showing 6 changed files with 109 additions and 14 deletions.
diff --git a/cn-client/package.json b/cn-client/package.json
@@ -49,6 +49,11 @@
                     "default": null,
                     "description": "Location of the LSP server"
                 },
+                "CN.debugPath": {
+                    "type": "string",
+                    "default": null,
+                    "description": "Location of the CN-DAP executable"
+                },
                 "CN.showGillianDebugLenses": {
                     "type": "boolean",
                     "default": false,

diff --git a/cn-client/src/extension.ts b/cn-client/src/extension.ts
@@ -31,12 +31,20 @@ export async function activate(context: vsc.ExtensionContext): Promise<void> {
         // or retrieved in a server configuration, should we try again?
     }
 
+    const workspaceFolders = vsc.workspace.workspaceFolders;
+    let logPath = "CN-lsp-server.log";
+    if (workspaceFolders && workspaceFolders.length > 0) {
+        const workspaceRoot = workspaceFolders[0].uri.fsPath;
+        logPath = path.join(workspaceRoot, "CN-lsp-server.log");
+    }
+
     const serverOptions: ct.Executable = {
         command: serverContext.serverPath,
         transport: ct.TransportKind.pipe,
         options: {
             env,
         },
+        args: ["--log", logPath]
     };
 
     const clientOptions: ct.LanguageClientOptions = {
@@ -81,6 +89,13 @@ export async function activate(context: vsc.ExtensionContext): Promise<void> {
         client.sendRequest(req, params);
     });
 
+    context.subscriptions.push(
+        vsc.debug.registerDebugAdapterDescriptorFactory(
+            "CN",
+            new CNDebugAdaptorDescriptorFactory(serverContext.debugPath)
+        )
+    );
+
     client.start();
     console.log("started client");
 }
@@ -93,9 +108,45 @@ export function deactivate(): Thenable<void> | undefined {
     }
 }
 
+class CNDebugAdaptorDescriptorFactory
+    implements vsc.DebugAdapterDescriptorFactory {
+    private debugPath: string;
+
+    constructor(debugPath: string | undefined) {
+        this.debugPath = debugPath ?? "cn-debug";
+    }
+
+    createDebugAdapterDescriptor(
+        _session: vsc.DebugSession,
+        executable: vsc.DebugAdapterExecutable | undefined
+    ): vsc.ProviderResult<vsc.DebugAdapterDescriptor> {
+        let langCmd: string = this.debugPath;
+
+        const config = vsc.workspace.getConfiguration("gillianDebugger");
+        console.log("Configuring debugger!...", { config });
+
+        const workspaceFolders = vsc.workspace.workspaceFolders;
+        let logPath = "CN-debug.log";
+        if (workspaceFolders && workspaceFolders.length > 0) {
+            const workspaceRoot = workspaceFolders[0].uri.fsPath;
+            logPath = path.join(workspaceRoot, "CN-debug.log");
+        }
+
+        let args = [
+            "--log",
+            logPath
+        ];
+
+        executable = new vsc.DebugAdapterExecutable(langCmd, args);
+
+        return executable;
+    }
+}
+
 interface ServerContext {
     serverPath: string;
     cerbRuntime?: string;
+    debugPath?: string;
 }
 
 async function newServerContext(
@@ -122,40 +173,58 @@ async function newServerContext(
             }
 
             let serverPath = path.join(opamDir, "bin", "cn-lsp-server");
+            let debugPath = path.join(opamDir, "bin", "cn-debug");
             let cerbRuntime = path.join(opamDir, "lib", "cerberus", "runtime");
 
-            if (fs.existsSync(serverPath) && fs.existsSync(cerbRuntime)) {
+            if (fs.existsSync(serverPath) && fs.existsSync(debugPath) && fs.existsSync(cerbRuntime)) {
                 return {
                     serverPath,
                     cerbRuntime,
+                    debugPath
                 };
             }
         }
     }
 
+    let serverPath: Maybe<string> = undefined;
+    let debugPath: Maybe<string> = undefined;
+
     console.log("Looking in $CN_LSP_SERVER");
     console.log(process.env);
     let envPath = process.env.CN_LSP_SERVER;
     if (envPath !== undefined) {
-        return { serverPath: envPath };
+        serverPath = envPath;
     }
 
-    console.log("Looking on $PATH");
-    const out = child_process.spawnSync("which", ["cn-lsp-server"], {
-        encoding: "utf-8",
-    });
-    if (out.status === 0) {
-        let serverPath = out.stdout.trim();
-        return { serverPath };
+    if (serverPath === undefined) {
+        console.log("Looking on $PATH");
+        const out = child_process.spawnSync("which", ["cn-lsp-server"], {
+            encoding: "utf-8",
+        });
+        if (out.status === 0) {
+            serverPath = out.stdout.trim();
+        }
+    }
+
+    if (debugPath === undefined) {
+        console.log("Looking on $PATH");
+        const out = child_process.spawnSync("which", ["cn-debug"], {
+            encoding: "utf-8",
+        });
+        if (out.status === 0) {
+            debugPath = out.stdout.trim();
+        }
     }
 
-    return undefined;
+
+    return serverPath ? { serverPath, debugPath } : undefined;
 }
 
 function getConfiguredServerContext(): Maybe<ServerContext> {
     let conf = vsc.workspace.getConfiguration("CN");
     let serverPath: Maybe<string> = conf.get("serverPath");
     let cerbRuntime: Maybe<string> = conf.get("cerbRuntime");
+    let debugPath: Maybe<string> = conf.get("debugPath");
 
     // In practice, despite the type annotations, `conf.get` seems capable of
     // returning `null` values, so we need to check them
@@ -165,9 +234,12 @@ function getConfiguredServerContext(): Maybe<ServerContext> {
         serverPath !== "" &&
         cerbRuntime !== null &&
         cerbRuntime !== undefined &&
-        cerbRuntime !== ""
+        cerbRuntime !== "" && 
+        debugPath !== null &&
+        debugPath !== undefined &&
+        debugPath !== ""
     ) {
-        return { serverPath, cerbRuntime };
+        return { serverPath, cerbRuntime, debugPath };
     } else {
         return undefined;
     }
@@ -185,4 +257,9 @@ async function setConfiguredServerContext(serverContext: ServerContext) {
         serverContext.serverPath,
         vsc.ConfigurationTarget.Global
     );
+    await conf.update(
+        "debugPath",
+        serverContext.debugPath,
+        vsc.ConfigurationTarget.Global
+    );
 }
diff --git a/cn-dap/debugger/README.md b/cn-dap/debugger/README.md
@@ -0,0 +1,5 @@
+# Installation
+Pin Gillian
+```bash
+opam pin gillian [email protected]:GillianPlatform/Gillian.git#0c14d64 --with-version "0c14d64"
+```
diff --git a/cn-dap/debugger/cndap.opam b/cn-dap/debugger/cndap.opam
@@ -12,7 +12,7 @@ depends: [
   "cerberus-lib" {= "b9daa22"}
   "cn" {= "b9daa22"}
   "dap" {>= "1.0.6" & < "2.0.0"}
-  "gillian" {= "c6802c5"}
+  "gillian" {= "0c14d64"}
   "logs" {>= "0.7.0" & < "1.0.0"}
   "odoc" {with-doc}
 ]

diff --git a/cn-dap/debugger/dune-project b/cn-dap/debugger/dune-project
@@ -34,7 +34,7 @@
     (>= 1.0.6)
     (< 2.0.0)))
   (gillian
-   (= "c6802c5"))
+   (= "0c14d64"))
   (logs
    (and
     (>= 0.7.0)

diff --git a/cn-lsp/lib/server.ml b/cn-lsp/lib/server.ml
@@ -273,6 +273,14 @@ class lsp_server (env : LspCn.cerb_env) =
            return ()
          | Some (diag_uri, diag) ->
            self#publish_diagnostics_for notify_back diag_uri [ diag ])
+      | exception e ->
+        let backtrace = Backtrace.Exn.most_recent_for_exn e in
+        let backtrace_str = 
+          Option.map ~f:Backtrace.to_string backtrace
+          |> Option.value ~default:"<no backtrace>" in
+        Log.d (sprintf "Verification failed with exception: %s, backtrace: %s" (Exn.to_string e) backtrace_str);
+        return ()
+
 
     method clear_diagnostics_for
       (notify_back : Rpc.notify_back)