Merge pull request #60 from FeldrinH/abstract-debugging

Abstract debugging

Readme.md

@@ -8,7 +8,7 @@ The Integration of the static analyzer [Goblint](https://github.com/goblint/anal
 
 1. Install [Goblint](https://github.com/goblint/analyzer#installing).
 2. Download [GobPie plugin](https://nightly.link/goblint/GobPie/workflows/build/master/gobpie-plugin.zip) and unzip the archive.
-3. Install the extension into VSCode with `code --install-extension gobpie-0.0.3.vsix`.
+3. Install the extension into VSCode with `code --install-extension gobpie-0.0.4.vsix`.
 
 When installing goblint locally (as recommended), **make sure that GobPie can find the correct version Goblint**.
 This can be done in two ways:
@@ -40,6 +40,7 @@ Example GobPie configuration file `gobpie.json`:
     "goblintConf": "goblint.json",
     "goblintExecutable": "/home/user/goblint/analyzer/goblint",
     "preAnalyzeCommand": ["cmake", "-DCMAKE_EXPORT_COMPILE_COMMANDS=ON", "-B", "build"],
+    "abstractDebugging": true,
     "showCfg": true,
     "incrementalAnalysis": false
 }
@@ -48,6 +49,7 @@ Example GobPie configuration file `gobpie.json`:
 * `goblintConf` - the relative path from the project root to the Goblint configuration file (required)
 * `goblintExecutable` - the absolute or relative path to the Goblint executable (optional, default `goblint`, meaning Goblint is expected to be on `PATH`)
 * `preAnalyzeCommand` - the command to run before analysing (e.g. command for building/updating the compilation database for some automation) (optional)
+* `abstractDebugging` - if [abstract debugging](#abstract-debugging) is enabled (this automatically enables ARG generation) (optional, default `false`)
 * `showCfg` - if the code actions for showing the function's CFGs are shown (optional, default `false`)
 * `incrementalAnalyisis` - if Goblint should use incremental analysis (disabling this may, in some cases, improve the stability of Goblint) (optional, default `true`)
 
@@ -66,6 +68,23 @@ Example values for `files`:
   * `["./01-assert.c"]` (single file for analysis without database)
   * `["./01-assert.c", "extra.c"]` (multiple files for analysis without database)
 
+## Abstract debugging
+
+GobPie includes a special debugger called an **abstract debugger**, that uses the results of Goblint's analysis to emulate a standard debugger, but operates on abstract states instead of an actual running program.
+
+Once GobPie is installed and configured (see previous two sections), the debugger can be started by simply selecting "C (GobPie Abstract Debugger)" from the Run and Debug panel in VS Code and starting the debugger as normal.  
+Note: Abstract debugging is disabled by default. It must be explicitly enabled in `gobpie.json` before starting GobPie.
+
+The debugger supports breakpoints, including conditional breakpoints, shows the call stack and values of variables, allows interactively evaluating expressions and setting watch expressions and supports most standard stepping operations.
+
+In general the abstract debugger works analogously to a normal debugger, but instead of stepping through a running program, it steps through the program ARG generated by Goblint during analysis.
+Values of variables and expressions are obtained from the Goblint base analysis and are represented using the base analysis abstract domain.
+The function call stack is constructed by traversing the ARG from the current node to the program entrypoint.
+In case of multiple possible call stacks all possible callers at the location where call stacks diverge are shown. To view the call stack of one possible caller the restart frame operation can be used to restart the frame of the desired caller, which moves the active location to the start of the selected caller's frame.
+
+When there are multiple possible ARG nodes at the location of a breakpoint then all possible ARG nodes are shown at the same time as threads.
+When a step is made in one thread, an equivalent step is made in all other threads. An equivalent step is one that leads to the same CFG node. This means that all threads are synchronized such that stepping to an ARG node in one thread ensures that all threads are at an ARG node with the same corresponding CFG node.
+
 ## Developing
 
 Make sure the following are installed: `JDK 17`, `mvn`, `npm`, `nodejs`, `@vscode/vsce`.

adb_examples/goblint.json

@@ -0,0 +1,14 @@
+{
+  "files": [
+    "thesis_example.c"
+  ],
+  "ana": {
+    "int": {
+      "interval": true,
+      "congruence": true,
+      "refinement": "fixpoint",
+      "interval_threshold_widening" : true,
+      "def_exc_widen_by_join" : true
+    }
+  }
+}

adb_examples/gobpie.json

@@ -0,0 +1,6 @@
+{
+    "goblintConf" : "goblint.json",
+    "abstractDebugging": true,
+    "showCfg": true,
+    "incrementalAnalysis": false
+}

adb_examples/thesis_example.c

@@ -0,0 +1,36 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <pthread.h>
+
+pthread_mutex_t lukk = PTHREAD_MUTEX_INITIALIZER;
+
+void f(int a) {
+    printf("%i", a);
+}
+
+void g(int b) {
+    if (b >= 50) {
+        f(b - 50);
+    } else {
+        f(b);
+        f(b + 12);
+    }
+}
+
+void h(int c) {
+    if (c == 0) {
+        pthread_mutex_lock(&lukk);
+    }
+    if (c > 0) {
+        printf("%i", c);
+    }
+    if (c == 0) {
+        pthread_mutex_unlock(&lukk);
+    }
+}
+
+int main() {
+    int i = rand() % 100;
+    g(i);
+    h(i);
+}

adb_examples/variables_example.c

@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+struct s {
+    int n;
+    int m[3];
+};
+
+int main() {
+    int a = rand() % 19;
+    int b = 79;
+    struct s c = {
+        7 * a + 5,
+        {b, b + 1, b + 2}
+    };
+    return 0;
+}

pom.xml

@@ -4,9 +4,16 @@
     <modelVersion>4.0.0</modelVersion>
     <groupId>goblint</groupId>
     <artifactId>gobpie</artifactId>
-    <version>0.0.3-SNAPSHOT</version>
+    <version>0.0.4-SNAPSHOT</version>
     <dependencies>
 
+        <!-- lsp4j DAP -->
+        <dependency>
+            <groupId>org.eclipse.lsp4j</groupId>
+            <artifactId>org.eclipse.lsp4j.debug</artifactId>
+            <version>0.19.0</version>
+        </dependency>
+
         <!-- lsp4j json rpc -->
         <dependency>
             <groupId>org.eclipse.lsp4j</groupId>

src/main/java/HTTPserver/GobPieHttpHandler.java

@@ -1,8 +1,8 @@
 package HTTPserver;
 
 import api.GoblintService;
-import api.messages.GoblintCFGResult;
-import api.messages.Params;
+import api.messages.params.NodeParams;
+import api.messages.params.Params;
 import com.google.gson.JsonObject;
 import com.google.gson.JsonParser;
 import com.sun.net.httpserver.HttpExchange;
@@ -36,6 +36,7 @@
 public class GobPieHttpHandler implements HttpHandler {
 
     private static final int HTTP_OK_STATUS = 200;
+    private static final int HTTP_INTERNAL_ERROR_STATUS = 500;
     private final String httpServerAddress;
     private final GoblintService goblintService;
 
@@ -66,38 +67,50 @@ public void handle(HttpExchange exchange) throws IOException {
         TemplateEngine templateEngine = createTemplateEngine("/templates/", ".html", TemplateMode.HTML);
         Context context = new Context();
 
-        if (exchange.getRequestMethod().equalsIgnoreCase("post")) {
-            response = switch (path) {
-                case "/cfg/" -> {
-                    String funName = readRequestBody(is).get("funName").getAsString();
-                    context.setVariable("cfgSvg", getCFG(funName));
-                    context.setVariable("url", httpServerAddress + "node/");
-                    context.setVariable("jsonTreeCss", httpServerAddress + "static/jsonTree.css/");
-                    context.setVariable("jsonTreeJs", httpServerAddress + "static/jsonTree.js/");
-                    log.info("Showing CFG for function: " + funName);
-                    yield templateEngine.process("base", context);
-                }
-                case "/node/" -> {
-                    String nodeId = readRequestBody(is).get("node").getAsString();
-                    List<JsonObject> states = getNodeStates(nodeId);
-                    log.info("Showing state info for node with ID: " + nodeId);
-                    yield states.get(0).toString();
-                }
-                default -> templateEngine.process("index", context);
-            };
-        } else {
-            response = switch (path) {
-                case "/static/jsonTree.css/" -> {
-                    templateEngine = createTemplateEngine("/json-viewer/", ".css", TemplateMode.CSS);
-                    yield templateEngine.process("jquery.json-viewer", context);
-                }
-                case "/static/jsonTree.js/" -> {
-                    templateEngine = createTemplateEngine("/json-viewer/", ".js", TemplateMode.JAVASCRIPT);
-                    yield templateEngine.process("jquery.json-viewer", context);
-                }
-                default -> templateEngine.process("index", context);
-            };
+        try {
+            if (exchange.getRequestMethod().equalsIgnoreCase("post")) {
+                response = switch (path) {
+                    case "/cfg/" -> {
+                        String funName = readRequestBody(is).get("funName").getAsString();
+                        context.setVariable("cfgSvg", getCFG(funName));
+                        context.setVariable("url", httpServerAddress + "node/");
+                        context.setVariable("jsonTreeCss", httpServerAddress + "static/jsonTree.css/");
+                        context.setVariable("jsonTreeJs", httpServerAddress + "static/jsonTree.js/");
+                        log.info("Showing CFG for function: " + funName);
+                        yield templateEngine.process("base", context);
+                    }
+                    case "/node/" -> {
+                        String nodeId = readRequestBody(is).get("node").getAsString();
+                        List<JsonObject> states = getNodeStates(nodeId);
+                        log.info("Showing state info for node with ID: " + nodeId);
+                        yield states.get(0).toString();
+                    }
+                    default -> templateEngine.process("index", context);
+                };
+            } else {
+                response = switch (path) {
+                    case "/static/jsonTree.css/" -> {
+                        templateEngine = createTemplateEngine("/json-viewer/", ".css", TemplateMode.CSS);
+                        yield templateEngine.process("jquery.json-viewer", context);
+                    }
+                    case "/static/jsonTree.js/" -> {
+                        templateEngine = createTemplateEngine("/json-viewer/", ".js", TemplateMode.JAVASCRIPT);
+                        yield templateEngine.process("jquery.json-viewer", context);
+                    }
+                    default -> templateEngine.process("index", context);
+                };
+            }
+        } catch (Exception e) {
+            log.error("Error generating HTTP response:");
+            e.printStackTrace();
+
+            String errorMessage = "ERROR:\n" + e.getMessage();
+            exchange.sendResponseHeaders(HTTP_INTERNAL_ERROR_STATUS, errorMessage.getBytes().length);
+            writeResponse(os, errorMessage);
+
+            return;
         }
+
         exchange.sendResponseHeaders(HTTP_OK_STATUS, response.getBytes().length);
         writeResponse(os, response);
     }
@@ -137,18 +150,23 @@ private TemplateEngine createTemplateEngine(String prefix, String suffix, Templa
      * Sends the request to get the CFG for the given function,
      * converts the CFG to a svg and returns it.
      *
-     * @param funName The function name for which the CFG was requested.
+     * @param funName The function name for which the CFG was requested. If function name is {@code "<arg>"} requests the ARG instead.
      * @return The CFG of the given function as a svg.
      * @throws GobPieException if the request and response ID do not match.
      */
     private String getCFG(String funName) {
         Params params = new Params(funName);
         try {
-            GoblintCFGResult cfgResponse = goblintService.cfg(params).get();
-            String cfg = cfgResponse.getCfg();
+            String cfg;
+            if (funName.equals("<arg>")) {
+                cfg = goblintService.arg_dot().get().getArg();
+            } else {
+                cfg = goblintService.cfg_dot(params).get().getCfg();
+            }
             return cfg2svg(cfg);
         } catch (ExecutionException | InterruptedException e) {
-            throw new GobPieException("Sending the request to or receiving result from the server failed.", e, GobPieExceptionType.GOBLINT_EXCEPTION);
+            Throwable cause = e instanceof ExecutionException ? e.getCause() : e;
+            throw new GobPieException("Requesting data from Goblint failed: " + cause.getMessage(), e, GobPieExceptionType.GOBLINT_EXCEPTION);
         }
     }
 
@@ -184,21 +202,10 @@ private String cfg2svg(String cfg) {
     private List<JsonObject> getNodeStates(String nodeId) {
         NodeParams params = new NodeParams(nodeId);
         try {
-            return goblintService.node_state(params).get();
+            return goblintService.cfg_state(params).get();
         } catch (ExecutionException | InterruptedException e) {
-            throw new GobPieException("Sending the request to or receiving result from the server failed.", e, GobPieExceptionType.GOBLINT_EXCEPTION);
-        }
-    }
-
-    public static class NodeParams {
-
-        private String nid;
-
-        public NodeParams() {
-        }
-
-        public NodeParams(String nid) {
-            this.nid = nid;
+            Throwable cause = e instanceof ExecutionException ? e.getCause() : e;
+            throw new GobPieException("Requesting data from Goblint failed: " + cause.getMessage(), e, GobPieExceptionType.GOBLINT_EXCEPTION);
         }
     }