diff --git a/Readme.md b/Readme.md index 9a76a06..1eac0f3 100644 --- a/Readme.md +++ b/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`. diff --git a/adb_examples/goblint.json b/adb_examples/goblint.json new file mode 100644 index 0000000..598ad35 --- /dev/null +++ b/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 + } + } +} \ No newline at end of file diff --git a/adb_examples/gobpie.json b/adb_examples/gobpie.json new file mode 100644 index 0000000..0283899 --- /dev/null +++ b/adb_examples/gobpie.json @@ -0,0 +1,6 @@ +{ + "goblintConf" : "goblint.json", + "abstractDebugging": true, + "showCfg": true, + "incrementalAnalysis": false +} diff --git a/adb_examples/thesis_example.c b/adb_examples/thesis_example.c new file mode 100644 index 0000000..c629698 --- /dev/null +++ b/adb_examples/thesis_example.c @@ -0,0 +1,36 @@ +#include +#include +#include + +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); +} \ No newline at end of file diff --git a/adb_examples/variables_example.c b/adb_examples/variables_example.c new file mode 100644 index 0000000..b15d340 --- /dev/null +++ b/adb_examples/variables_example.c @@ -0,0 +1,16 @@ +#include + +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; +} \ No newline at end of file diff --git a/pom.xml b/pom.xml index c67042f..d3ddca5 100644 --- a/pom.xml +++ b/pom.xml @@ -4,9 +4,16 @@ 4.0.0 goblint gobpie - 0.0.3-SNAPSHOT + 0.0.4-SNAPSHOT + + + org.eclipse.lsp4j + org.eclipse.lsp4j.debug + 0.19.0 + + org.eclipse.lsp4j diff --git a/src/main/java/HTTPserver/GobPieHttpHandler.java b/src/main/java/HTTPserver/GobPieHttpHandler.java index 53b7505..f9ca8d6 100644 --- a/src/main/java/HTTPserver/GobPieHttpHandler.java +++ b/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 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 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 ""} 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("")) { + 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 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); } } diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 1da8eb5..e7075ac 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,15 +1,17 @@ import HTTPserver.GobPieHTTPServer; +import abstractdebugging.AbstractDebuggingServerLauncher; +import abstractdebugging.ResultsService; import analysis.GoblintAnalysis; import analysis.ShowCFGCommand; import api.GoblintService; import api.GoblintServiceLauncher; -import api.messages.Params; +import api.messages.params.Params; import goblintserver.GoblintServer; import gobpie.GobPieConfReader; import gobpie.GobPieConfiguration; import gobpie.GobPieException; +import magpiebridge.core.MagpieServer; import magpiebridge.core.ServerAnalysis; -import magpiebridge.core.ToolAnalysis; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.eclipse.lsp4j.MessageParams; @@ -21,28 +23,45 @@ public class Main { private static final String gobPieConfFileName = "gobpie.json"; + private static final Logger log = LogManager.getLogger(Main.class); - private static GoblintMagpieServer magpieServer; public static void main(String... args) { + GoblintMagpieServer magpieServer = createMagpieServer(); + try { - createMagpieServer(); - addAnalysis(); + // Read GobPie configuration file + GobPieConfReader gobPieConfReader = new GobPieConfReader(magpieServer, gobPieConfFileName); + GobPieConfiguration gobpieConfiguration = gobPieConfReader.readGobPieConfiguration(); + + // Start GoblintServer + GoblintServer goblintServer = startGoblintServer(magpieServer, gobpieConfiguration); + + // Connect GoblintService and read configuration + GoblintService goblintService = connectGoblintService(magpieServer, gobpieConfiguration, goblintServer); + + // Add analysis + addAnalysis(magpieServer, gobpieConfiguration, goblintServer, goblintService); + + // Launch magpieServer magpieServer.configurationDone(); log.info("MagpieBridge server launched."); + + if (args.length > 0 && gobpieConfiguration.enableAbstractDebugging()) { + // Launch abstract debugging server + String socketAddress = args[0]; + launchAbstractDebuggingServer(socketAddress, goblintService); + log.info("Abstract debugging server launched on: " + socketAddress); + } else { + log.info("Abstract debugging server disabled."); + } } catch (GobPieException e) { String message = e.getMessage(); - String terminalMessage = e.getCause() == null ? message : message + " Cause: " + e.getCause().getMessage(); - forwardErrorMessageToClient(message, terminalMessage); - switch (e.getType()) { - case GOBLINT_EXCEPTION: - break; - case GOBPIE_EXCEPTION: - break; - case GOBPIE_CONF_EXCEPTION: - break; - } + String terminalMessage; + if (e.getCause() == null) terminalMessage = message; + else terminalMessage = message + " Cause: " + e.getCause().getMessage(); + forwardErrorMessageToClient(magpieServer, message, terminalMessage); } } @@ -52,48 +71,47 @@ public static void main(String... args) { * Method for creating and launching MagpieBridge server. */ - private static void createMagpieServer() { + private static GoblintMagpieServer createMagpieServer() { // set up configuration for MagpieServer GoblintServerConfiguration serverConfig = new GoblintServerConfiguration(); serverConfig.setUseMagpieHTTPServer(false); //TODO: Track any relevant changes in https://github.com/MagpieBridge/MagpieBridge/issues/88 and update this accordingly. serverConfig.setLanguageExtensionHandler(new GoblintLanguageExtensionHandler(serverConfig.getLanguageExtensionHandler())); - magpieServer = new GoblintMagpieServer(serverConfig); + GoblintMagpieServer magpieServer = new GoblintMagpieServer(serverConfig); // launch MagpieServer // note that the server will not accept messages until configurationDone is called magpieServer.launchOnStdio(); + + return magpieServer; } /** - * Method for creating and adding Goblint analysis to MagpieBridge server. - *

- * Creates GoblintServer, GoblintClient and the GoblintAnalysis classes. + * Starts Goblint server. * - * @throws GobPieException if something goes wrong with creating any of the classes: - *

    - *
  • GoblintServer;
    • - *
  • GoblintClient.
    • - *
+ * @throws GobPieException if running the server start command fails */ - - private static void addAnalysis() { - // define language - String language = "c"; - - // read GobPie configuration file - GobPieConfReader gobPieConfReader = new GobPieConfReader(magpieServer, gobPieConfFileName); - GobPieConfiguration gobpieConfiguration = gobPieConfReader.readGobPieConfiguration(); - - // start GoblintServer + private static GoblintServer startGoblintServer(MagpieServer magpieServer, GobPieConfiguration gobpieConfiguration) { GoblintServer goblintServer = new GoblintServer(magpieServer, gobpieConfiguration); + if (log.isDebugEnabled()) { + log.debug("Goblint version info:\n" + goblintServer.checkGoblintVersion()); + } goblintServer.startGoblintServer(); - // launch GoblintService + return goblintServer; + } + + + /** + * Connects the Goblint service to the Goblint server and reads the Goblint configuration file. + * + * @throws GobPieException if connecting fails + */ + private static GoblintService connectGoblintService(MagpieServer magpieServer, GobPieConfiguration gobpieConfiguration, GoblintServer goblintServer) { GoblintServiceLauncher launcher = new GoblintServiceLauncher(); GoblintService goblintService = launcher.connect(goblintServer.getGoblintSocket()); - // read Goblint configurations + // Read Goblint configurations goblintService.read_config(new Params(new File(gobpieConfiguration.getGoblintConf()).getAbsolutePath())) .exceptionally(ex -> { String msg = "Goblint was unable to successfully read the configuration: " + ex.getMessage(); @@ -103,10 +121,23 @@ private static void addAnalysis() { }) .join(); + return goblintService; + } + + + /** + * Method for creating and adding Goblint analysis to MagpieBridge server. + *

+ * Creates the GoblintAnalysis classes. + */ + private static void addAnalysis(MagpieServer magpieServer, GobPieConfiguration gobpieConfiguration, + GoblintServer goblintServer, GoblintService goblintService) { + // define language + String language = "c"; + // add analysis to the MagpieServer ServerAnalysis serverAnalysis = new GoblintAnalysis(magpieServer, goblintServer, goblintService, gobpieConfiguration); - Either analysis = Either.forLeft(serverAnalysis); - magpieServer.addAnalysis(analysis, language); + magpieServer.addAnalysis(Either.forLeft(serverAnalysis), language); // add HTTP server for showing CFGs, only if the option is specified in the configuration if (gobpieConfiguration.showCfg()) { @@ -117,6 +148,18 @@ private static void addAnalysis() { } + /** + * Launch abstract debugging server + * + * @throws GobPieException if creating domain socket for server fails + */ + private static void launchAbstractDebuggingServer(String socketAddress, GoblintService goblintService) { + ResultsService resultsService = new ResultsService(goblintService); + AbstractDebuggingServerLauncher launcher = new AbstractDebuggingServerLauncher(resultsService); + launcher.launchOnDomainSocket(socketAddress); + } + + /** * Method for forwarding Error messages to MagpieServer. * @@ -124,7 +167,7 @@ private static void addAnalysis() { * @param terminalMessage The message shown in the terminal. */ - private static void forwardErrorMessageToClient(String popUpMessage, String terminalMessage) { + private static void forwardErrorMessageToClient(MagpieServer magpieServer, String popUpMessage, String terminalMessage) { magpieServer.forwardMessageToClient( new MessageParams(MessageType.Error, "Unable to start GobPie extension: " + popUpMessage + " Check the output terminal of GobPie extension for more information.") ); diff --git a/src/main/java/abstractdebugging/AbstractDebuggingServer.java b/src/main/java/abstractdebugging/AbstractDebuggingServer.java new file mode 100644 index 0000000..44da074 --- /dev/null +++ b/src/main/java/abstractdebugging/AbstractDebuggingServer.java @@ -0,0 +1,1391 @@ +package abstractdebugging; + +import api.messages.GoblintLocation; +import api.messages.GoblintVarinfo; +import api.messages.params.LookupParams; +import com.google.gson.JsonElement; +import com.google.gson.JsonObject; +import org.apache.commons.lang3.tuple.Pair; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import org.eclipse.lsp4j.debug.Thread; +import org.eclipse.lsp4j.debug.*; +import org.eclipse.lsp4j.debug.services.IDebugProtocolClient; +import org.eclipse.lsp4j.debug.services.IDebugProtocolServer; +import org.eclipse.lsp4j.jsonrpc.ResponseErrorException; +import org.eclipse.lsp4j.jsonrpc.messages.ResponseError; +import org.eclipse.lsp4j.jsonrpc.messages.ResponseErrorCode; + +import javax.annotation.Nullable; +import java.io.File; +import java.nio.file.Path; +import java.util.*; +import java.util.concurrent.CompletableFuture; +import java.util.function.Function; +import java.util.function.Predicate; +import java.util.stream.Collectors; +import java.util.stream.IntStream; +import java.util.stream.StreamSupport; + +/** + * Abstract debugging server. + * An instance of this corresponds to a single debugging session. + * Implements the core logic of abstract debugging with the lsp4j DAP interface. + * + * @author Juhan Oskar Hennoste + * @since 0.0.4 + */ +public class AbstractDebuggingServer implements IDebugProtocolServer { + + /** + * Step in target id-s are calculated as offset + index, where offset determines the specific operation and index is the index of the target edge. + * Offset is one of the *_OFFSET constants. All offsets are multiples of TARGET_BLOCK_SIZE. + * This allows the retrieval of the index simply by subtracting the offset, provided that the index is less than TARGET_BLOCK_SIZE. + */ + private static final int TARGET_BLOCK_SIZE = 1_000_000; + private static final int STEP_OVER_OFFSET = TARGET_BLOCK_SIZE; + private static final int STEP_IN_OFFSET = 2 * TARGET_BLOCK_SIZE; + private static final int STEP_BACK_OVER_OFFSET = 3 * TARGET_BLOCK_SIZE; + private static final int STEP_BACK_OUT_OFFSET = 4 * TARGET_BLOCK_SIZE; + + /** + * Multiplier for thread id in frame id. + * Frame id is calculated as threadId * FRAME_ID_THREAD_ID_MULTIPLIER + frameIndex. + */ + private static final int FRAME_ID_THREAD_ID_MULTIPLIER = 100_000; + + /** + * Set of built-in and standard library variables. They are generally hidden in variable views to reduce noise. + * List taken from is_std function in Goblint. + */ + private static final Set STD_VARIABLES = Set.of( + "__tzname", "__daylight", "__timezone", "tzname", "daylight", "timezone", // unix time.h + "getdate_err", // unix time.h, but somehow always in MacOS even without include + "stdin", "stdout", "stderr", // standard stdio.h + "optarg", "optind", "opterr", "optopt", // unix unistd.h + "__environ" // Linux Standard Base Core Specification + ); + + private final ResultsService resultsService; + + private final EventQueue eventQueue = new EventQueue(); + private IDebugProtocolClient client; + private CompletableFuture configurationDoneFuture = new CompletableFuture<>(); + + private final List breakpoints = new ArrayList<>(); + private int activeBreakpoint = -1; + private final Map threads = new LinkedHashMap<>(); + + private final Map nodeScopes = new HashMap<>(); + private final List storedVariables = new ArrayList<>(); + + private final Logger log = LogManager.getLogger(AbstractDebuggingServer.class); + + + public AbstractDebuggingServer(ResultsService resultsService) { + this.resultsService = resultsService; + } + + /** + * Sets the client used to send events back to the debug adapter client (usually an IDE). + */ + public void connectClient(IDebugProtocolClient client) { + if (this.client != null) { + throw new IllegalStateException("Client already connected"); + } + this.client = client; + } + + /** + * Gets event queue where sending DAP events will be queued. + */ + public EventQueue getEventQueue() { + return eventQueue; + } + + /** + * DAP request to initialize debugger and report supported capabilities. + * For the abstract debugger this is a no-op (except for returning supported capabilities). + */ + @Override + public CompletableFuture initialize(InitializeRequestArguments args) { + Capabilities capabilities = new Capabilities(); + capabilities.setSupportsConfigurationDoneRequest(true); + capabilities.setSupportsStepInTargetsRequest(true); + capabilities.setSupportsStepBack(true); + capabilities.setSupportsConditionalBreakpoints(true); + capabilities.setSupportsRestartFrame(true); + capabilities.setSupportsTerminateThreadsRequest(true); + return CompletableFuture.completedFuture(capabilities); + } + + /** + * DAP request to set breakpoints. + */ + @Override + public CompletableFuture setBreakpoints(SetBreakpointsArguments args) { + Path absoluteSourcePath = Path.of(args.getSource().getPath()).toAbsolutePath(); + String goblintSourcePath = resultsService.getGoblintTrackedFiles().stream() + .filter(f -> Path.of(f).toAbsolutePath().equals(absoluteSourcePath)) + .findFirst().orElse(null); + log.info("Setting breakpoints for " + args.getSource().getPath() + " (" + goblintSourcePath + ")"); + + List newBreakpointStatuses = new ArrayList<>(); + List newBreakpoints = new ArrayList<>(); + for (var breakpoint : args.getBreakpoints()) { + var breakpointStatus = new Breakpoint(); + newBreakpointStatuses.add(breakpointStatus); + + if (goblintSourcePath == null) { + breakpointStatus.setVerified(false); + breakpointStatus.setMessage("File not analyzed"); + continue; + } + + var targetLocation = new GoblintLocation(goblintSourcePath, breakpoint.getLine(), breakpoint.getColumn() == null ? 0 : breakpoint.getColumn()); + CFGNodeInfo cfgNode; + try { + cfgNode = resultsService.lookupCFGNode(targetLocation); + } catch (RequestFailedException e) { + breakpointStatus.setVerified(false); + breakpointStatus.setMessage("No statement found at location " + targetLocation); + continue; + } + breakpointStatus.setSource(args.getSource()); + breakpointStatus.setLine(cfgNode.location().getLine()); + breakpointStatus.setColumn(cfgNode.location().getColumn()); + + ConditionalExpression condition; + if (breakpoint.getCondition() == null) { + condition = null; + } else { + try { + condition = ConditionalExpression.fromString(breakpoint.getCondition(), true); + } catch (IllegalArgumentException e) { + breakpointStatus.setVerified(false); + breakpointStatus.setMessage(e.getMessage()); + continue; + } + } + + List targetNodes; + try { + targetNodes = findTargetNodes(cfgNode, condition); + } catch (IllegalArgumentException e) { + breakpointStatus.setVerified(false); + // VSCode seems to use code formatting rules for conditional breakpoint messages. + // The character ' causes VSCode to format any following text as a string, which looks strange and causes unwanted line breaks. + // As a workaround all ' characters are replaced with a different Unicode apostrophe. + // TODO: Find a way to fix this without manipulating the error message. + // Possibly this will need opening an issue in the VSCode issue tracker. + breakpointStatus.setMessage(e.getMessage().replace('\'', '’')); + continue; + } + + newBreakpoints.add(new BreakpointInfo(cfgNode, condition, targetNodes)); + if (targetNodes.isEmpty()) { + breakpointStatus.setVerified(false); + breakpointStatus.setMessage("Unreachable"); + } else { + breakpointStatus.setVerified(true); + } + } + + int startIndex; + for (startIndex = 0; startIndex < breakpoints.size(); startIndex++) { + if (breakpoints.get(startIndex).cfgNode().location().getFile().equals(goblintSourcePath)) { + break; + } + } + breakpoints.removeIf(b -> b.cfgNode().location().getFile().equals(goblintSourcePath)); + breakpoints.addAll(startIndex, newBreakpoints); + + var response = new SetBreakpointsResponse(); + response.setBreakpoints(newBreakpointStatuses.toArray(Breakpoint[]::new)); + return CompletableFuture.completedFuture(response); + } + + /** + * DAP request to set exception breakpoints. + * Note: This should not be called by the IDE given our reported capabilities, but VSCode calls it anyway. + * It is implemented as a no-op to avoid errors. + */ + @Override + public CompletableFuture setExceptionBreakpoints(SetExceptionBreakpointsArguments args) { + var response = new SetExceptionBreakpointsResponse(); + response.setBreakpoints(new Breakpoint[0]); + return CompletableFuture.completedFuture(response); + } + + /** + * Finds target nodes having the given CFG node and matching the conditional expression if provided. + * + * @throws IllegalArgumentException if evaluating the condition failed. + */ + private List findTargetNodes(CFGNodeInfo cfgNode, @Nullable ConditionalExpression condition) { + var candidateNodes = resultsService.lookupNodes(LookupParams.byCFGNodeId(cfgNode.cfgNodeId())); + if (condition == null) { + return candidateNodes; + } else { + return candidateNodes.stream() + .filter(n -> condition.evaluateCondition(n, resultsService)) + .toList(); + } + } + + /** + * Notifies the debugger that all initial configuration requests have been made. + * Launching waits for this to arrive before starting the debugger. + */ + @Override + public CompletableFuture configurationDone(ConfigurationDoneArguments args) { + log.info("Debug adapter configuration done"); + configurationDoneFuture.complete(null); + configurationDoneFuture = new CompletableFuture<>(); + return CompletableFuture.completedFuture(null); + } + + /** + * DAP request to attach to debugger. + * Note: Attach doesn't make sense for abstract debugging, but to avoid issues in case the client requests it anyway we just treat it as a launch request. + */ + @Override + public CompletableFuture attach(Map args) { + return launch(args); + } + + /** + * DAP request to launch debugger. + * Launches the abstract debugger and runs to first breakpoint. Waits for configuration before launching. + */ + @Override + public CompletableFuture launch(Map args) { + // Start configuration by notifying that client is initialized. + client.initialized(); + log.info("Debug adapter initialized, waiting for configuration"); + // Wait for configuration to complete, then launch. + return configurationDoneFuture + .thenRun(() -> { + log.info("Debug adapter launched"); + activeBreakpoint = -1; + runToNextBreakpoint(1); + }); + } + + /** + * Disconnects the debugger. For abstract debugging this is a no-op. + */ + @Override + public CompletableFuture disconnect(DisconnectArguments args) { + return CompletableFuture.completedFuture(null); + } + + /** + * Runs to next breakpoint. + * Note: Breakpoints are run in the order in which the client sent them, not in any content based ordering. + * In VS Code breakpoints appear to be sent in the order of their line numbers. + */ + @Override + public CompletableFuture continue_(ContinueArguments args) { + runToNextBreakpoint(1); + return CompletableFuture.completedFuture(new ContinueResponse()); + } + + /** + * Runs to previous breakpoint. + */ + @Override + public CompletableFuture reverseContinue(ReverseContinueArguments args) { + runToNextBreakpoint(-1); + return CompletableFuture.completedFuture(null); + } + + /** + * DAP request to pause a thread. Abstract debugger threads are always paused so this is a no-op. + */ + @Override + public CompletableFuture pause(PauseArguments args) { + return CompletableFuture.completedFuture(null); + } + + /** + * Restarts the given frame at the start of the function. In VS Code this can be accessed as an icon on the right side of the stack frame in the call stacks view. + */ + @Override + public CompletableFuture restartFrame(RestartFrameArguments args) { + int targetThreadId = getThreadId(args.getFrameId()); + int targetFrameIndex = getFrameIndex(args.getFrameId()); + try { + stepAllThreadsToMatchingFrame(targetThreadId, targetFrameIndex, true); + return CompletableFuture.completedFuture(null); + } catch (IllegalStepException e) { + return CompletableFuture.failedFuture(userFacingError("Cannot restart frame. " + e.getMessage())); + } + } + + /** + * Terminates (removes) a thread. In VS Code this can be accessed by right-clicking on a thread in the call stacks view. + */ + @Override + public CompletableFuture terminateThreads(TerminateThreadsArguments args) { + for (int threadId : args.getThreadIds()) { + threads.remove(threadId); + } + for (int threadId : args.getThreadIds()) { + var event = new ThreadEventArguments(); + event.setReason("exited"); + event.setThreadId(threadId); + client.thread(event); + } + return CompletableFuture.completedFuture(null); + } + + /** + * Returns list of valid targets for step in operation. (In VS Code this is used by step into targets). + */ + @Override + public CompletableFuture stepInTargets(StepInTargetsArguments args) { + ThreadState currentThread = threads.get(getThreadId(args.getFrameId())); + NodeInfo currentNode = currentThread.getCurrentFrame().getNode(); + + List targets = new ArrayList<>(); + if (currentNode != null) { + List forwardTargets = new ArrayList<>(); + + { + var entryEdges = currentNode.outgoingEntryEdges(); + for (int i = 0; i < entryEdges.size(); i++) { + var edge = entryEdges.get(i); + forwardTargets.add(target( + STEP_IN_OFFSET + i, + "Step in: " + (edge.createsNewThread() ? "thread " : "call ") + edge.function() + "(" + String.join(", ", edge.args()) + ")", + currentNode.location() + )); + } + } + + // Only show CFG edges as step in targets if there is no stepping over function calls and there is branching + if (currentNode.outgoingEntryEdges().isEmpty() && currentNode.outgoingCFGEdges().size() > 1) { + var cfgEdges = currentNode.outgoingCFGEdges(); + for (int i = 0; i < cfgEdges.size(); i++) { + var edge = cfgEdges.get(i); + var node = resultsService.lookupNode(edge.nodeId()); + forwardTargets.add(target( + STEP_OVER_OFFSET + i, + "Step: " + edge.statementDisplayString(), + node.location() + )); + } + } + + // Sort forward stepping targets by the order they appear in code + forwardTargets.sort(Comparator.comparing(StepInTarget::getLine).thenComparing(StepInTarget::getColumn)); + targets.addAll(forwardTargets); + + // Backward stepping entry targets are not sorted, to ensure their order matches the order of stack frames + if (currentThread.hasPreviousFrame() && currentThread.getPreviousFrame().isAmbiguousFrame()) { + var frames = currentThread.getFrames(); + for (int i = 1; i < frames.size(); i++) { + var node = frames.get(i).getNode(); + assert node != null; // Ambiguous frames can't be unavailable + targets.add(target( + STEP_BACK_OUT_OFFSET + i, + "Step back: " + node.function() + " " + node.nodeId(), + node.location() + )); + } + } + + List backwardTargets = new ArrayList<>(); + + if (currentNode.incomingCFGEdges().size() > 1) { + var cfgEdges = currentNode.incomingCFGEdges(); + for (int i = 0; i < cfgEdges.size(); i++) { + var edge = cfgEdges.get(i); + var node = resultsService.lookupNode(edge.nodeId()); + backwardTargets.add(target( + STEP_BACK_OVER_OFFSET + i, + "Step back: " + edge.statementDisplayString(), + node.location() + )); + } + } + + // Sort backward stepping CFG targets by the order they appear in code + backwardTargets.sort(Comparator.comparing(StepInTarget::getLine).thenComparing(StepInTarget::getColumn)); + targets.addAll(backwardTargets); + } + + var response = new StepInTargetsResponse(); + response.setTargets(targets.toArray(StepInTarget[]::new)); + return CompletableFuture.completedFuture(response); + } + + /** + * Helper method to create StepInTarget. + */ + private StepInTarget target(int id, String label, GoblintLocation location) { + var target = new StepInTarget(); + target.setId(id); + target.setLabel(label); + target.setLine(location.getLine()); + target.setColumn(location.getColumn()); + target.setEndLine(location.getEndLine()); + target.setEndColumn(location.getEndColumn()); + return target; + } + + /** + * DAP next operation. In VS Code this corresponds to step over. + */ + @Override + public CompletableFuture next(NextArguments args) { + var targetThread = threads.get(args.getThreadId()); + var currentNode = targetThread.getCurrentFrame().getNode(); + if (currentNode == null) { + return CompletableFuture.failedFuture(userFacingError("Cannot step over. Location is unavailable.")); + } else if (currentNode.outgoingCFGEdges().isEmpty()) { + if (currentNode.outgoingReturnEdges().isEmpty()) { + return CompletableFuture.failedFuture(userFacingError("Cannot step over. Reached last statement.")); + } + var stepOutArgs = new StepOutArguments(); + stepOutArgs.setThreadId(args.getThreadId()); + stepOutArgs.setSingleThread(args.getSingleThread()); + stepOutArgs.setGranularity(args.getGranularity()); + return stepOut(stepOutArgs); + } + for (var thread : threads.values()) { + NodeInfo node = thread.getCurrentFrame().getNode(); + if (node != null && node.outgoingCFGEdges().size() > 1 && !node.outgoingEntryEdges().isEmpty()) { + return CompletableFuture.failedFuture(userFacingError("Ambiguous path through function" + (thread == targetThread ? "" : " for " + thread.getName()) + + ". Step into function to choose the desired path.")); + } + } + if (currentNode.outgoingCFGEdges().size() > 1) { + return CompletableFuture.failedFuture(userFacingError("Branching control flow. Use step into target to choose the desired branch.")); + } + return stepOver(args.getThreadId(), 0); + } + + /** + * DAP step in operation. + * Allows explicit target selection by setting targetId. In VS Code this is the step into targets operation. + */ + @Override + public CompletableFuture stepIn(StepInArguments args) { + var currentNode = threads.get(args.getThreadId()).getCurrentFrame().getNode(); + if (currentNode == null) { + return CompletableFuture.failedFuture(userFacingError((args.getTargetId() == null ? "Cannot step in." : "Cannot step to target.") + " Location is unavailable.")); + } + + if (args.getTargetId() == null) { + // Normal step in operation + if (currentNode.outgoingEntryEdges().isEmpty()) { + var nextArgs = new NextArguments(); + nextArgs.setThreadId(args.getThreadId()); + nextArgs.setSingleThread(args.getSingleThread()); + nextArgs.setGranularity(args.getGranularity()); + return next(nextArgs); + } else if (currentNode.outgoingEntryEdges().size() > 1) { + return CompletableFuture.failedFuture(userFacingError("Ambiguous function call. Use step into target to choose the desired call")); + } + return stepIn(args.getThreadId(), 0); + } else { + // Step into targets operation + int targetId = args.getTargetId(); + if (targetId >= STEP_BACK_OUT_OFFSET) { + int targetIndex = targetId - STEP_BACK_OUT_OFFSET; + return stepBackOut(args.getThreadId(), targetIndex); + } else if (targetId >= STEP_BACK_OVER_OFFSET) { + int targetIndex = targetId - STEP_BACK_OVER_OFFSET; + return stepBackOver(args.getThreadId(), targetIndex); + } else if (targetId >= STEP_IN_OFFSET) { + int targetIndex = targetId - STEP_IN_OFFSET; + return stepIn(args.getThreadId(), targetIndex); + } else if (targetId >= STEP_OVER_OFFSET) { + int targetIndex = targetId - STEP_OVER_OFFSET; + return stepOver(args.getThreadId(), targetIndex); + } else { + return CompletableFuture.failedFuture(new IllegalStateException("Unknown step in target: " + targetId)); + } + } + } + + /** + * DAP step out operation. + */ + @Override + public CompletableFuture stepOut(StepOutArguments args) { + ThreadState targetThread = threads.get(args.getThreadId()); + if (targetThread.getCurrentFrame().getNode() == null) { + return CompletableFuture.failedFuture(userFacingError("Cannot step out. Location is unavailable.")); + } else if (!targetThread.hasPreviousFrame()) { + return CompletableFuture.failedFuture(userFacingError("Cannot step out. Reached top of call stack.")); + } else if (targetThread.getPreviousFrame().isAmbiguousFrame()) { + // Restart frame isn't equivalent to step out, it moves you to the start of the frame, which means you have to step to your target location manually. + // TODO: Find/create a better alternative for stepping out with ambiguous caller. + return CompletableFuture.failedFuture(userFacingError("Ambiguous caller frame. Use restart frame to choose the desired frame.")); + } + + NodeInfo targetCallNode = targetThread.getPreviousFrame().getNode(); + assert targetCallNode != null; + if (targetCallNode.outgoingCFGEdges().isEmpty()) { + return CompletableFuture.failedFuture(userFacingError("Cannot step out. Function never returns.")); + } + + return stepOut(args.getThreadId()); + } + + /** + * DAP step back operation. + */ + @Override + public CompletableFuture stepBack(StepBackArguments args) { + var targetThread = threads.get(args.getThreadId()); + var currentNode = targetThread.getCurrentFrame().getNode(); + if (currentNode == null) { + return CompletableFuture.failedFuture(userFacingError("Cannot step back. Location is unavailable.")); + } else if (currentNode.incomingCFGEdges().isEmpty()) { + // Reached start of function + if (!targetThread.hasPreviousFrame()) { + return CompletableFuture.failedFuture(userFacingError("Cannot step back. Reached start of program.")); + } else if (targetThread.getPreviousFrame().isAmbiguousFrame()) { + return CompletableFuture.failedFuture(userFacingError("Ambiguous previous frame. Use step into target to choose desired frame.")); + } + return stepBackOut(args.getThreadId(), 1); + } else if (currentNode.incomingCFGEdges().size() > 1) { + return CompletableFuture.failedFuture(userFacingError("Ambiguous previous location. Use step into target to choose desired location.")); + } + + return stepBackOver(args.getThreadId(), 0); + } + + // Concrete implementations of step operations. These are called from the respective requests as well as from stepIn if a corresponding target is requested. + + /** + * Implements step over for a specific target edge. + * + * @param targetIndex index of the target edge + */ + private CompletableFuture stepOver(int targetThreadId, int targetIndex) { + NodeInfo currentNode = threads.get(targetThreadId).getCurrentFrame().getNode(); + assert currentNode != null; + try { + var targetEdge = currentNode.outgoingCFGEdges().get(targetIndex); + stepAllThreadsOverMatchingEdge(targetThreadId, targetEdge, NodeInfo::outgoingCFGEdges); + return CompletableFuture.completedFuture(null); + } catch (IllegalStepException e) { + // Log error because if 'Step into target' menu is open then errors returned by this function are not shown in VSCode. + // TODO: Open issue about this in VSCode issue tracker. + log.error("Cannot step over. " + e.getMessage()); + return CompletableFuture.failedFuture(userFacingError("Cannot step over. " + e.getMessage())); + } + } + + /** + * Implements step in for a specific target edge. + * + * @param targetIndex index of the target edge + */ + private CompletableFuture stepIn(int targetThreadId, int targetIndex) { + NodeInfo currentNode = threads.get(targetThreadId).getCurrentFrame().getNode(); + assert currentNode != null; + try { + var targetEdge = currentNode.outgoingEntryEdges().get(targetIndex); + stepAllThreadsIntoMatchingEdge(targetThreadId, targetEdge, NodeInfo::outgoingEntryEdges); + return CompletableFuture.completedFuture(null); + } catch (IllegalStepException e) { + // Log error because if 'Step into target' menu is open then errors returned by this function are not shown in VSCode. + // TODO: Open issue about this in VSCode issue tracker. + log.error("Cannot step in. " + e.getMessage()); + return CompletableFuture.failedFuture(userFacingError("Cannot step in. " + e.getMessage())); + } + } + + /** + * Implements step out. Assumes that the target thread has already been checked and is known to be available and have a previous frame. + */ + private CompletableFuture stepOut(int targetThreadId) { + ThreadState targetThread = threads.get(targetThreadId); + NodeInfo targetCallNode = targetThread.getPreviousFrame().getNode(); + assert targetCallNode != null; + + Map targetNodes = new HashMap<>(); + for (var threadEntry : threads.entrySet()) { + int threadId = threadEntry.getKey(); + ThreadState thread = threadEntry.getValue(); + + // Skip all threads that have no known previous frame or whose previous frame has a different location compared to the target thread. + // Note that threads with an unavailable current or previous frame are kept. + if (!thread.hasPreviousFrame() || thread.getPreviousFrame().isAmbiguousFrame() + || (thread.getPreviousFrame().getNode() != null && !Objects.equals(thread.getPreviousFrame().getNode().cfgNodeId(), targetCallNode.cfgNodeId()))) { + continue; + } + + NodeInfo currentNode = thread.getCurrentFrame().getNode(); + NodeInfo targetNode; + if (currentNode == null) { + targetNode = null; + } else { + Predicate filter; + if (thread.getCurrentFrame().getLocalThreadIndex() != thread.getPreviousFrame().getLocalThreadIndex()) { + // If thread exit then control flow will not return to parent frame. No information to filter with so simply allow all possible nodes. + filter = _id -> true; + } else { + // If not thread exit then filter possible nodes after function call in parent frame to those that are also possible return targets of current frame. + Set returnNodeIds = findMatchingNodes(currentNode, NodeInfo::outgoingCFGEdges, e -> !e.outgoingReturnEdges().isEmpty()).stream() + .flatMap(n -> n.outgoingReturnEdges().stream()) + .map(EdgeInfo::nodeId) + .collect(Collectors.toSet()); + filter = returnNodeIds::contains; + } + + NodeInfo currentCallNode = thread.getPreviousFrame().getNode(); + List candidateTargetNodeIds = currentCallNode.outgoingCFGEdges().stream() + .map(EdgeInfo::nodeId) + .filter(filter) + .toList(); + + if (candidateTargetNodeIds.isEmpty()) { + targetNode = null; + } else if (candidateTargetNodeIds.size() == 1) { + targetNode = resultsService.lookupNode(candidateTargetNodeIds.get(0)); + } else { + return CompletableFuture.failedFuture(userFacingError("Ambiguous return path" + (thread == targetThread ? "" : " for " + thread.getName()) + + ". Step to return manually to choose the desired path.")); + } + } + + targetNodes.put(threadId, targetNode); + } + + // Remove all threads that have no target node (note that threads with an unavailable (null) target node are kept). + threads.keySet().removeIf(k -> !targetNodes.containsKey(k)); + // Remove topmost stack frame and step to target node + for (var threadEntry : threads.entrySet()) { + int threadId = threadEntry.getKey(); + ThreadState thread = threadEntry.getValue(); + + thread.popFrame(); + thread.getCurrentFrame().setNode(targetNodes.get(threadId)); + } + + onThreadsStopped("step", targetThreadId); + + return CompletableFuture.completedFuture(null); + } + + private CompletableFuture stepBackOver(int targetThreadId, int targetIndex) { + NodeInfo currentNode = threads.get(targetThreadId).getCurrentFrame().getNode(); + assert currentNode != null; + EdgeInfo targetEdge = currentNode.incomingCFGEdges().get(targetIndex); + try { + stepAllThreadsOverMatchingEdge(targetThreadId, targetEdge, NodeInfo::incomingCFGEdges); + return CompletableFuture.completedFuture(null); + } catch (IllegalStepException e) { + // Log error because if 'Step into target' menu is open then errors returned by this function are not shown in VSCode. + // TODO: Open issue about this in VSCode issue tracker. + log.error("Cannot step back. " + e.getMessage()); + return CompletableFuture.failedFuture(userFacingError("Cannot step back. " + e.getMessage())); + } + } + + private CompletableFuture stepBackOut(int targetThreadId, int targetIndex) { + try { + stepAllThreadsToMatchingFrame(targetThreadId, targetIndex, false); + return CompletableFuture.completedFuture(null); + } catch (IllegalStepException e) { + return CompletableFuture.failedFuture(userFacingError("Cannot step back. " + e.getMessage())); + } + } + + /** + * Runs to next breakpoint in given direction. + * + * @param direction 1 to run to next breakpoint, -1 to run to previous breakpoint. + */ + private void runToNextBreakpoint(int direction) { + // Note: We treat breaking on entry as the only breakpoint if no breakpoints are set. + // TODO: Changing breakpoints when the debugger is active can cause breakpoints to be skipped or visited twice. + while (activeBreakpoint + direction < Math.max(1, breakpoints.size()) && activeBreakpoint + direction >= 0) { + activeBreakpoint += direction; + + String stopReason; + GoblintLocation targetLocation; + List targetNodes; + if (breakpoints.size() == 0) { + stopReason = "entry"; + targetLocation = null; + targetNodes = resultsService.lookupNodes(LookupParams.entryPoint()); + } else { + var breakpoint = breakpoints.get(activeBreakpoint); + stopReason = "breakpoint"; + targetLocation = breakpoint.cfgNode().location(); + targetNodes = breakpoint.targetNodes(); + } + + if (!targetNodes.isEmpty()) { + setThreads( + targetNodes.stream() + .map(node -> new ThreadState("breakpoint " + node.nodeId(), assembleStackTrace(node))) + .toList() + ); + + onThreadsStopped(stopReason, threads.keySet().stream().findFirst().orElseThrow()); + + log.info("Stopped on breakpoint " + activeBreakpoint + " (" + targetLocation + ")"); + return; + } + + log.info("Skipped unreachable breakpoint " + activeBreakpoint + " (" + targetLocation + ")"); + } + + log.info("All breakpoints visited. Terminating debugger."); + var event = new TerminatedEventArguments(); + client.terminated(event); + } + + /** + * Steps all threads along an edge matching primaryTargetEdge. + * Edges are matched by ARG node. If no edge with matching ARG node is found then edges are matched by CFG node. + * If no edge with matching CFG node is found then thread becomes unavailable. + * + * @throws IllegalStepException if the target node is ambiguous ie there are multiple candidate edges that have the target CFG node. + */ + private void stepAllThreadsOverMatchingEdge(int primaryThreadId, EdgeInfo primaryTargetEdge, Function> getCandidateEdges) + throws IllegalStepException { + List> steps = new ArrayList<>(); + for (var thread : threads.values()) { + StackFrameState currentFrame = thread.getCurrentFrame(); + + NodeInfo targetNode; + if (currentFrame.getNode() != null) { + List candidateEdges = getCandidateEdges.apply(currentFrame.getNode()); + EdgeInfo targetEdge = findTargetEdge(primaryTargetEdge, candidateEdges, thread.getName()); + targetNode = targetEdge == null ? null : resultsService.lookupNode(targetEdge.nodeId()); + } else if (currentFrame.getLastReachableNode() != null && currentFrame.getLastReachableNode().cfgNodeId().equals(primaryTargetEdge.cfgNodeId())) { + targetNode = currentFrame.getLastReachableNode(); + } else { + continue; + } + + steps.add(Pair.of(thread, targetNode)); + } + + for (var step : steps) { + ThreadState thread = step.getLeft(); + NodeInfo targetNode = step.getRight(); + thread.getCurrentFrame().setNode(targetNode); + } + + onThreadsStopped("step", primaryThreadId); + } + + /** + * Steps all threads along an edge matching primaryTargetEdge and adds a new stack frame with the target node. + * Edges are matched by ARG node. If no edge with matching ARG node is found then edges are matched by CFG node. + * If no edge with matching CFG node is found then thread becomes unavailable. + * + * @throws IllegalStepException if the target node is ambiguous ie there are multiple candidate edges that have the target CFG node. + */ + private void stepAllThreadsIntoMatchingEdge(int primaryThreadId, EdgeInfo primaryTargetEdge, Function> getCandidateEdges) + throws IllegalStepException { + // Note: It is important that all threads, including threads with unavailable location, are stepped, because otherwise the number of added stack frames will get out of sync. + List> steps = new ArrayList<>(); + for (var thread : threads.values()) { + StackFrameState currentFrame = thread.getCurrentFrame(); + + EdgeInfo targetEdge; + if (currentFrame.getNode() != null) { + List candidateEdges = getCandidateEdges.apply(currentFrame.getNode()); + targetEdge = findTargetEdge(primaryTargetEdge, candidateEdges, thread.getName()); + } else { + targetEdge = null; + } + + steps.add(Pair.of(thread, targetEdge)); + } + + for (var step : steps) { + ThreadState thread = step.getLeft(); + EdgeInfo targetEdge = step.getRight(); + NodeInfo targetNode = resultsService.lookupNode(targetEdge.nodeId()); + boolean isNewThread = targetEdge instanceof FunctionCallEdgeInfo fce && fce.createsNewThread(); + thread.pushFrame(new StackFrameState(targetNode, false, thread.getCurrentFrame().getLocalThreadIndex() - (isNewThread ? 1 : 0))); + } + + onThreadsStopped("step", primaryThreadId); + } + + private EdgeInfo findTargetEdge(EdgeInfo primaryTargetEdge, List candidateEdges, String threadName) throws IllegalStepException { + // This is will throw if there are multiple distinct target edges with the same target CFG node. + // TODO: Somehow ensure this can never happen. + // Options: + // * Throw error (current approach) (problem: might make it impossible to step at all in some cases. it is difficult to provide meaningful error messages for all cases) + // * Split thread into multiple threads. (problem: complicates 'step back' and maintaining thread ordering) + // * Identify true source of branching and use it to disambiguate (problem: there might not be a source of branching in all cases. complicates stepping logic) + // * Make ambiguous threads unavailable (problem: complicates mental model of when threads become unavailable.) + + EdgeInfo targetEdgeByARGNode = candidateEdges.stream() + .filter(e -> e.nodeId().equals(primaryTargetEdge.nodeId())) + .findAny().orElse(null); + if (targetEdgeByARGNode != null) { + return targetEdgeByARGNode; + } + List targetEdgesByCFGNode = candidateEdges.stream() + .filter(e -> e.cfgNodeId().equals(primaryTargetEdge.cfgNodeId())) + .toList(); + if (targetEdgesByCFGNode.size() > 1) { + throw new IllegalStepException("Path is ambiguous for " + threadName + "."); + } + return targetEdgesByCFGNode.size() == 1 ? targetEdgesByCFGNode.get(0) : null; + } + + /** + * Moves all threads to a matching frame. Frame is matched by frame index (position counting from topmost frame) and CFG node. + * + * @param restart if true, moves to the start of the frame, otherwise preserves current position in frame + * @throws IllegalStepException if the primary thread target frame is unavailable or the target frame is ambiguous for some thread. + */ + private void stepAllThreadsToMatchingFrame(int primaryThreadId, int primaryTargetFrameIndex, boolean restart) throws IllegalStepException { + ThreadState targetThread = threads.get(primaryThreadId); + + int targetPosition = primaryTargetFrameIndex; + while (targetPosition > 0 && targetThread.getFrames().get(targetPosition - 1).isAmbiguousFrame()) { + targetPosition -= 1; + } + + StackFrameState targetFrame = targetThread.getFrames().get(primaryTargetFrameIndex); + if (targetFrame.getNode() == null) { + throw new IllegalStepException("Target frame is unavailable."); + } + String targetCFGId = targetFrame.getNode().cfgNodeId(); + + Map frameIndexes = new HashMap<>(); + for (var threadEntry : threads.entrySet()) { + Integer frameIndex; + if (threadEntry.getValue() == targetThread) { + frameIndex = primaryTargetFrameIndex; + } else { + try { + frameIndex = findFrameIndex(threadEntry.getValue().getFrames(), targetPosition, targetCFGId); + } catch (IllegalStateException e) { + throw new IllegalStepException("Ambiguous target frame for " + threadEntry.getValue().getName() + "."); + } + } + + if (frameIndex != null) { + frameIndexes.put(threadEntry.getKey(), frameIndex); + } + } + + threads.keySet().removeIf(t -> !frameIndexes.containsKey(t)); + for (var threadEntry : threads.entrySet()) { + int threadId = threadEntry.getKey(); + ThreadState thread = threadEntry.getValue(); + + int frameIndex = frameIndexes.get(threadId); + // Remove all frames on top of the target frame + thread.getFrames().subList(0, frameIndex).clear(); + if (thread.getCurrentFrame().isAmbiguousFrame()) { + // If the target frame is ambiguous then rebuild stack + List newStackTrace = assembleStackTrace(thread.getCurrentFrame().getNode()); + thread.getFrames().clear(); + thread.getFrames().addAll(newStackTrace); + } + if (restart) { + NodeInfo startNode = thread.getCurrentFrame().getNode() != null ? thread.getCurrentFrame().getNode() : thread.getCurrentFrame().getLastReachableNode(); + if (startNode != null) { + thread.getCurrentFrame().setNode(getEntryNode(startNode)); + } + } + } + + onThreadsStopped("step", primaryThreadId); + } + + /** + * Helper method for {@link #stepAllThreadsToMatchingFrame}. + *

+ * Finds the matching frame for the given call stack and returns its index. + * Returns null if there is no matching frame, either because the desired index is out of range or does not have the desired CFG node. + * Note that unavailable frames are considered matching, on the assumption that for them to become unavailable + * they must have had a matching CFG node with other threads at some point in the past. + */ + private Integer findFrameIndex(List frames, int targetPosition, String targetCFGNodeId) { + // When restarting the frame it might make more sense to compare entry nodes rather than current nodes, + // however, this can cause unexpected ambiguities when there are ambiguous frames with the same entry node but different current nodes. + // TODO: Make an explicit and reasoned decision on this. + if (frames.size() <= targetPosition) { + return null; + } + if (frames.get(targetPosition).isAmbiguousFrame()) { + Integer foundIndex = null; + for (int i = targetPosition; i < frames.size(); i++) { + var frame = frames.get(i); + assert frame.getNode() != null; // It should be impossible for ambiguous frames to be unavailable. + if (frame.getNode().cfgNodeId().equals(targetCFGNodeId)) { + if (foundIndex != null) { + throw new IllegalStateException("Ambiguous target frame"); + } + foundIndex = i; + } + } + return foundIndex; + } else { + var frame = frames.get(targetPosition); + // Preserve unavailable frames because otherwise threads could be spuriously lost + if (frame.getNode() == null || frame.getNode().cfgNodeId().equals(targetCFGNodeId)) { + return targetPosition; + } + return null; + } + } + + @Override + public CompletableFuture threads() { + var response = new ThreadsResponse(); + Thread[] responseThreads = threads.entrySet().stream() + .map(entry -> { + Thread thread = new Thread(); + thread.setId(entry.getKey()); + thread.setName(entry.getValue().getName()); + return thread; + }) + .toArray(Thread[]::new); + response.setThreads(responseThreads); + return CompletableFuture.completedFuture(response); + } + + /** + * Returns the stack trace for the given thread. + */ + @Override + public CompletableFuture stackTrace(StackTraceArguments args) { + var thread = threads.get(args.getThreadId()); + + final int currentThreadId = thread.getCurrentFrame().getLocalThreadIndex(); + StackFrame[] stackFrames = new StackFrame[thread.getFrames().size()]; + for (int i = 0; i < thread.getFrames().size(); i++) { + var frame = thread.getFrames().get(i); + + var stackFrame = new StackFrame(); + stackFrame.setId(getFrameId(args.getThreadId(), i)); + // TODO: Notation for ambiguous frames and parent threads could be clearer. + if (frame.getNode() != null) { + stackFrame.setName((frame.isAmbiguousFrame() ? "? " : "") + (frame.getLocalThreadIndex() != currentThreadId ? "^" : "") + frame.getNode().function() + " " + frame.getNode().nodeId()); + var location = frame.getNode().location(); + stackFrame.setLine(location.getLine()); + stackFrame.setColumn(location.getColumn()); + stackFrame.setEndLine(location.getEndLine()); + stackFrame.setEndColumn(location.getEndColumn()); + var source = new Source(); + source.setName(location.getFile()); + source.setPath(new File(location.getFile()).getAbsolutePath()); + stackFrame.setSource(source); + } else { + stackFrame.setName("No matching path"); + } + + stackFrames[i] = stackFrame; + } + + var response = new StackTraceResponse(); + response.setStackFrames(stackFrames); + return CompletableFuture.completedFuture(response); + } + + /** + * Returns variable scopes for the given stack frame. + */ + @Override + public CompletableFuture scopes(ScopesArguments args) { + var frame = getFrame(args.getFrameId()); + if (frame.getNode() == null) { + throw new IllegalStateException("Attempt to request variables for unavailable frame " + args.getFrameId()); + } + + Scope[] scopes = nodeScopes.computeIfAbsent(frame.getNode().nodeId(), nodeId -> { + NodeInfo currentNode = frame.getNode(); + + JsonObject state = resultsService.lookupState(currentNode.nodeId()); + JsonElement globalState = resultsService.lookupGlobalState(); + Map varinfos = resultsService.getVarinfos().stream() + .filter(v -> (v.getFunction() == null || v.getFunction().equals(currentNode.function())) && !"function".equals(v.getRole())) + .collect(Collectors.toMap(GoblintVarinfo::getName, v -> v)); + + List localVariables = new ArrayList<>(); + List globalVariables = new ArrayList<>(); + + if (state.has("threadflag")) { + globalVariables.add(domainValueToVariable("", "(analysis threading mode)", state.get("threadflag"))); + } + if (state.has("mutex")) { + globalVariables.add(domainValueToVariable("", "(set of unique locked mutexes)", state.get("mutex"))); + } + if (state.has("symb_locks")) { + globalVariables.add(domainValueToVariable("", "(set of locked mutexes tracked by symbolic references)", state.get("symb_locks"))); + } + + JsonObject domainValues = state.get("base").getAsJsonObject().get("value domain").getAsJsonObject(); + + // Add special values. + for (var entry : domainValues.entrySet()) { + if (varinfos.containsKey(entry.getKey()) || entry.getKey().startsWith("((alloc")) { + // Hide normal variables because they are added later. + // Hide allocations because they require manually matching identifiers to interpret. + continue; + } + // In most cases the only remaining value is RETURN. Consider it local. + // TODO: RETURN special value can end up in globals if there is also a global variable RETURN. This needs changes on the Goblint side to fix. + localVariables.add(domainValueToVariable("(" + entry.getKey() + ")", "(special value)", entry.getValue())); + } + + // Add variables. + for (var varinfo : varinfos.values()) { + if (varinfo.getOriginalName() == null || (varinfo.getFunction() == null && STD_VARIABLES.contains(varinfo.getOriginalName()))) { + // Hide synthetic variables because they are impossible to interpret without looking at the CFG. + // Hide global built-in and standard library variables because they are generally irrelevant and not used in the analysis. + continue; + } + + String name = varinfo.getName().equals(varinfo.getOriginalName()) + ? varinfo.getName() + : varinfo.getOriginalName() + " (" + varinfo.getName() + ")"; + JsonElement value = domainValues.get(varinfo.getName()); + if (value == null) { + if (varinfo.getFunction() != null) { + // Skip local variables that are not present in base domain, because this generally means we are on a special ARG node where local variables are not tracked. + continue; + } + // If domain does not contain variable value use Goblint to evaluate the value. + // This generally happens for global variables in multithreaded mode. + value = resultsService.evaluateExpression(currentNode.nodeId(), varinfo.getName()); + } + + List scope = varinfo.getFunction() == null ? globalVariables : localVariables; + + scope.add(domainValueToVariable(name, varinfo.getType(), value)); + } + + List rawVariables = new ArrayList<>(); + rawVariables.add(domainValueToVariable("(local-state)", "local state; result of arg/state request", state)); + rawVariables.add(domainValueToVariable("(global-state)", "global state; result of global-state request", globalState)); + + return new Scope[]{ + scope("Local", localVariables), + scope("Global", globalVariables), + scope("Raw", rawVariables) + }; + }); + + var response = new ScopesResponse(); + response.setScopes(scopes); + return CompletableFuture.completedFuture(response); + } + + /** + * Returns variables for the given variable reference (a variable reference is generally a variable scope or a complex variable). + */ + @Override + public CompletableFuture variables(VariablesArguments args) { + var response = new VariablesResponse(); + response.setVariables(getVariables(args.getVariablesReference())); + return CompletableFuture.completedFuture(response); + } + + /** + * Evaluates the given expression and returns the result. + */ + @Override + public CompletableFuture evaluate(EvaluateArguments args) { + var frame = getFrame(args.getFrameId()); + if (frame.getNode() == null) { + throw new IllegalStateException("Attempt to evaluate expression in unavailable frame " + args.getFrameId()); + } + + JsonElement result; + try { + if (ConditionalExpression.hasExplicitMode(args.getExpression())) { + // If explicit mode is set then defer to ConditionalExpression for evaluation. + result = ConditionalExpression.fromString(args.getExpression(), false) + .evaluateValue(frame.getNode(), resultsService); + } else { + // If explicit mode is not set evaluate as a C expression using Goblint. + result = resultsService.evaluateExpression(frame.getNode().nodeId(), args.getExpression()); + } + } catch (RequestFailedException | IllegalArgumentException e) { + return CompletableFuture.failedFuture(userFacingError(e.getMessage())); + } + + var response = new EvaluateResponse(); + var resultVariable = domainValueToVariable("", null, result); + response.setResult(resultVariable.getValue()); + response.setVariablesReference(resultVariable.getVariablesReference()); + return CompletableFuture.completedFuture(response); + } + + /** + * Converts a Goblint domain value into a DAP variable. + * Note: Variables may contain variable references. Variable references are only valid until the next step. + */ + private Variable domainValueToVariable(String name, @Nullable String type, JsonElement value) { + if (value.isJsonObject()) { + return compoundVariable( + name, + type, + false, + value.getAsJsonObject().entrySet().stream() + .map(f -> domainValueToVariable(f.getKey(), null, f.getValue())) + .toArray(Variable[]::new) + ); + } else if (value.isJsonArray()) { + var valueArray = value.getAsJsonArray(); + // Integer domains are generally represented as an array of 1-4 strings. + // We want to display that as a non-compound variable for compactness and readability. + // As a general heuristic, only arrays containing compound values or longer than 4 elements are displayed as compound variables. + boolean displayAsCompound; + if (valueArray.size() > 4) { + displayAsCompound = true; + } else { + displayAsCompound = false; + for (JsonElement jsonElement : valueArray) { + if (!jsonElement.isJsonPrimitive()) { + displayAsCompound = true; + break; + } + } + } + + if (displayAsCompound) { + return compoundVariable( + name, + type, + true, + IntStream.range(0, valueArray.size()) + .mapToObj(i -> domainValueToVariable(Integer.toString(i), null, valueArray.get(i))) + .toArray(Variable[]::new) + ); + } + } + return variable(name, type, domainValueToString(value)); + } + + /** + * Converts a Goblint domain value into a string. + */ + private static String domainValueToString(JsonElement value) { + if (value.isJsonPrimitive()) { + return value.getAsString(); + } else if (value.isJsonArray()) { + return "[" + StreamSupport.stream(value.getAsJsonArray().spliterator(), false) + .map(AbstractDebuggingServer::domainValueToString) + .collect(Collectors.joining(", ")) + "]"; + } else if (value.isJsonObject()) { + return "{" + value.getAsJsonObject().entrySet().stream() + .map(e -> e.getKey() + ": " + domainValueToString(e.getValue())) + .collect(Collectors.joining(", ")) + "}"; + } else { + throw new IllegalArgumentException("Unknown domain value type: " + value.getClass()); + } + } + + /** + * Convenience function to construct a DAP scope. + */ + private Scope scope(String name, List variables) { + Scope scope = new Scope(); + scope.setName(name); + scope.setVariablesReference(storeVariables(variables.toArray(Variable[]::new))); + return scope; + } + + /** + * Convenience function to construct a DAP compound variable. + * Note: The given fields are stored as variable references. Variable references are only valid until the next step. + */ + private Variable compoundVariable(String name, @Nullable String type, boolean isArray, Variable... fields) { + Variable variable = new Variable(); + variable.setName(name); + variable.setType(type); + variable.setValue(compoundVariablePreview(isArray, fields)); + if (fields.length > 0) { + variable.setVariablesReference(storeVariables(fields)); + } + return variable; + } + + /** + * Constructs a preview string for a compound variable. + */ + private static String compoundVariablePreview(boolean isArray, Variable... fields) { + if (fields.length == 0) { + return isArray ? "[]" : "{}"; + } + if (isArray) { + return "[" + fields[0].getValue() + (fields.length > 1 ? ", …" : "") + "]"; + } else { + return "{" + Arrays.stream(fields) + .map(f -> f.getName() + ": " + (f.getVariablesReference() == 0 ? f.getValue() : "…")) + .collect(Collectors.joining(", ")) + "}"; + } + } + + /** + * Convenience function to construct a DAP variable. + */ + private static Variable variable(String name, @Nullable String type, String value) { + Variable variable = new Variable(); + variable.setName(name); + variable.setType(type); + variable.setValue(value); + return variable; + } + + // Helper methods: + + /** + * Get stack frame by frame id. + */ + private StackFrameState getFrame(int frameId) { + int threadId = getThreadId(frameId); + int frameIndex = getFrameIndex(frameId); + return threads.get(threadId).getFrames().get(frameIndex); + } + + /** + * Construct stack frame id from thread id and frame index. + */ + private static int getFrameId(int threadId, int frameIndex) { + return threadId * FRAME_ID_THREAD_ID_MULTIPLIER + frameIndex; + } + + /** + * Extract thread id from frame id. + */ + private int getThreadId(int frameId) { + return frameId / FRAME_ID_THREAD_ID_MULTIPLIER; + } + + /** + * Extract frame index from frame id. + */ + private int getFrameIndex(int frameId) { + return frameId % FRAME_ID_THREAD_ID_MULTIPLIER; + } + + private void setThreads(List newThreads) { + threads.clear(); + for (int i = 0; i < newThreads.size(); i++) { + threads.put(i, newThreads.get(i)); + } + } + + private Variable[] getVariables(int variablesReference) { + return storedVariables.get(variablesReference - 1); + } + + private int storeVariables(Variable[] variables) { + storedVariables.add(variables); + return storedVariables.size(); + } + + /** + * Logic that should run every time after threads have stopped after a step or breakpoint. + * Notifies client that threads have stopped and clears caches that should be invalidated whenever thread state changes.) + */ + private void onThreadsStopped(String stopReason, int primaryThreadId) { + storedVariables.clear(); + nodeScopes.clear(); + + var event = new StoppedEventArguments(); + event.setReason(stopReason); + event.setThreadId(primaryThreadId); + event.setAllThreadsStopped(true); + eventQueue.queue(() -> client.stopped(event)); + } + + /** + * Logic to assemble a stack trace with the given start node as the topmost frame. + */ + private List assembleStackTrace(NodeInfo startNode) { + int curThreadId = 0; + List stackFrames = new ArrayList<>(); + stackFrames.add(new StackFrameState(startNode, false, curThreadId)); + NodeInfo entryNode; + do { + entryNode = getEntryNode(stackFrames.get(stackFrames.size() - 1).getNode()); + boolean ambiguous = entryNode.incomingEntryEdges().size() > 1; + for (var edge : entryNode.incomingEntryEdges()) { + if (edge.createsNewThread()) { + curThreadId += 1; + } + var node = resultsService.lookupNode(edge.nodeId()); + stackFrames.add(new StackFrameState(node, ambiguous, curThreadId)); + } + } while (entryNode.incomingEntryEdges().size() == 1); + return stackFrames; + } + + /** + * Finds the entry node for the function that contains the given ARG node. + * The entry node is the first node of a function call. + * The first node of a function call in the ARG should be a synthetic node added by the CIL and consequently should always be uniquely defined. + */ + private NodeInfo getEntryNode(NodeInfo node) { + NodeInfo entryNode = _getEntryNode(node, new HashSet<>()); + if (entryNode == null) { + throw new IllegalStateException("Failed to find entry node for node " + node.nodeId()); + } + return entryNode; + } + + private NodeInfo _getEntryNode(NodeInfo node, Set seenNodes) { + if (node.incomingCFGEdges().isEmpty()) { + return node; + } + if (seenNodes.contains(node.nodeId())) { + return null; + } + seenNodes.add(node.nodeId()); + for (var edge : node.incomingCFGEdges()) { + NodeInfo entryNode = _getEntryNode(resultsService.lookupNode(edge.nodeId()), seenNodes); + if (entryNode != null) { + return entryNode; + } + } + return null; + } + + /** + * Finds all nodes matching the given condition that are inside the subgraph accessible + * by repeatedly traversing edges returned by candidateEdges starting from the given node. + */ + private List findMatchingNodes(NodeInfo node, Function> candidateEdges, Predicate condition) { + List foundNodes = new ArrayList<>(); + _findMatchingNodes(node, candidateEdges, condition, new HashSet<>(), foundNodes); + return foundNodes; + } + + private void _findMatchingNodes(NodeInfo node, Function> candidateEdges, Predicate condition, + Set seenNodes, List foundNodes) { + if (seenNodes.contains(node.nodeId())) { + return; + } + seenNodes.add(node.nodeId()); + if (condition.test(node)) { + foundNodes.add(node); + } + for (var edge : candidateEdges.apply(node)) { + _findMatchingNodes(resultsService.lookupNode(edge.nodeId()), candidateEdges, condition, seenNodes, foundNodes); + } + } + + /** + * Returns an exception that will be shown in the IDE as the message with no modifications and no additional context. + */ + private ResponseErrorException userFacingError(String message) { + return new ResponseErrorException(new ResponseError(ResponseErrorCode.RequestFailed, message, null)); + } + +} diff --git a/src/main/java/abstractdebugging/AbstractDebuggingServerLauncher.java b/src/main/java/abstractdebugging/AbstractDebuggingServerLauncher.java new file mode 100644 index 0000000..df744c0 --- /dev/null +++ b/src/main/java/abstractdebugging/AbstractDebuggingServerLauncher.java @@ -0,0 +1,112 @@ +package abstractdebugging; + +import gobpie.GobPieException; +import gobpie.GobPieExceptionType; +import org.apache.commons.lang3.exception.ExceptionUtils; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import org.eclipse.lsp4j.debug.services.IDebugProtocolClient; +import org.eclipse.lsp4j.jsonrpc.Launcher; +import org.eclipse.lsp4j.jsonrpc.MessageConsumer; +import org.eclipse.lsp4j.jsonrpc.debug.DebugLauncher; +import org.newsclub.net.unix.AFUNIXServerSocket; +import org.newsclub.net.unix.AFUNIXSocket; +import org.newsclub.net.unix.AFUNIXSocketAddress; + +import java.io.File; +import java.io.IOException; +import java.io.PrintWriter; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; + +/** + * Launcher for abstract debugging server. + * Responsible for exposing the DAP-based abstract debugging server over a UNIX domain socket. + * + * @author Juhan Oskar Hennoste + * @since 0.0.4 + */ +public class AbstractDebuggingServerLauncher { + + private final ResultsService resultsService; + + private final ExecutorService executorService = Executors.newCachedThreadPool(runnable -> { + Thread thread = new Thread(runnable, "adb-server-worker"); + thread.setDaemon(true); + return thread; + }); + + private final Logger log = LogManager.getLogger(AbstractDebuggingServerLauncher.class); + + public AbstractDebuggingServerLauncher(ResultsService resultsService) { + this.resultsService = resultsService; + } + + /** + * Launch abstract debugging server on domain socket. + * For each new connection to the domain socket a new AbstractDebuggingServer instance will be created and initialized. + * + * @param socketAddress address for the domain socket to bind to. the socket file will be created and cleaned up automatically + * @throws GobPieException if creating domain socket fails + */ + public void launchOnDomainSocket(String socketAddress) { + // TODO: Maybe lsp4j has built-in support for listening on domain socket. If so then that should be used instead. + AFUNIXServerSocket serverSocket; + try { + serverSocket = AFUNIXServerSocket.bindOn(AFUNIXSocketAddress.of(new File(socketAddress)), true); + } catch (Throwable e) { + throw new GobPieException("Failed to create domain socket for abstract debugging server on " + socketAddress, e, GobPieExceptionType.GOBPIE_EXCEPTION); + } + Runtime.getRuntime().addShutdownHook(new Thread(() -> { + // Close server socket when JVM shuts down. This will delete the socket file if possible. + try { + serverSocket.close(); + } catch (IOException e) { + ExceptionUtils.rethrow(e); + } + })); + executorService.submit(() -> listenOnDomainSocket(serverSocket)); + } + + private void listenOnDomainSocket(AFUNIXServerSocket serverSocket) { + while (!Thread.currentThread().isInterrupted()) { + try { + AFUNIXSocket clientSocket = serverSocket.accept(); + log.info("Accepted new connection to abstract debugging server."); + + AbstractDebuggingServer abstractDebuggingServer = new AbstractDebuggingServer(resultsService); + Launcher launcher = new AbstractDebuggingLauncherBuilder() + .setEventQueue(abstractDebuggingServer.getEventQueue()) + .setLocalService(abstractDebuggingServer) + .setRemoteInterface(IDebugProtocolClient.class) + .setInput(clientSocket.getInputStream()) + .setOutput(clientSocket.getOutputStream()) + .setExecutorService(executorService) + .traceMessages(log.isDebugEnabled() ? new PrintWriter(System.err) : null) + .create(); + abstractDebuggingServer.connectClient(launcher.getRemoteProxy()); + launcher.startListening(); + } catch (Throwable e) { + log.error("Error accepting connection to abstract debugging server:", e); + } + } + } + + static class AbstractDebuggingLauncherBuilder extends DebugLauncher.Builder { + + private EventQueue eventQueue; + + public AbstractDebuggingLauncherBuilder setEventQueue(EventQueue eventQueue) { + this.eventQueue = eventQueue; + return this; + } + + @Override + protected MessageConsumer wrapMessageConsumer(MessageConsumer consumer) { + MessageConsumer wrappedConsumer = super.wrapMessageConsumer(consumer); + return new EventQueueMessageConsumer(wrappedConsumer, eventQueue); + } + + } + +} diff --git a/src/main/java/abstractdebugging/BreakpointInfo.java b/src/main/java/abstractdebugging/BreakpointInfo.java new file mode 100644 index 0000000..4f36a26 --- /dev/null +++ b/src/main/java/abstractdebugging/BreakpointInfo.java @@ -0,0 +1,15 @@ +package abstractdebugging; + +import javax.annotation.Nullable; +import java.util.List; + +/** + * @since 0.0.4 + */ + +public record BreakpointInfo( + CFGNodeInfo cfgNode, + @Nullable ConditionalExpression condition, + List targetNodes +) { +} diff --git a/src/main/java/abstractdebugging/CFGEdgeInfo.java b/src/main/java/abstractdebugging/CFGEdgeInfo.java new file mode 100644 index 0000000..df8e637 --- /dev/null +++ b/src/main/java/abstractdebugging/CFGEdgeInfo.java @@ -0,0 +1,21 @@ +package abstractdebugging; + +/** + * @since 0.0.4 + */ + +public class CFGEdgeInfo extends EdgeInfo { + + private final String statementDisplayString; + + public CFGEdgeInfo(String nodeId, String cfgNodeId, String contextId, String pathId, + String statementDisplayString) { + super(nodeId, cfgNodeId, contextId, pathId); + this.statementDisplayString = statementDisplayString; + } + + public final String statementDisplayString() { + return statementDisplayString; + } + +} diff --git a/src/main/java/abstractdebugging/CFGNodeInfo.java b/src/main/java/abstractdebugging/CFGNodeInfo.java new file mode 100644 index 0000000..bee166a --- /dev/null +++ b/src/main/java/abstractdebugging/CFGNodeInfo.java @@ -0,0 +1,13 @@ +package abstractdebugging; + +import api.messages.GoblintLocation; + +/** + * @since 0.0.4 + */ + +public record CFGNodeInfo( + String cfgNodeId, + GoblintLocation location +) { +} diff --git a/src/main/java/abstractdebugging/ConditionalExpression.java b/src/main/java/abstractdebugging/ConditionalExpression.java new file mode 100644 index 0000000..5a4db24 --- /dev/null +++ b/src/main/java/abstractdebugging/ConditionalExpression.java @@ -0,0 +1,85 @@ +package abstractdebugging; + +import com.google.gson.JsonElement; +import com.google.gson.JsonPrimitive; + +import java.util.Locale; + +/** + * @since 0.0.4 + */ + +public record ConditionalExpression(boolean must, String expression) { + + private static final String EXPLICIT_MODE_PREFIX = "\\"; + + /** + *

+ * Creates a ConditionalExpression by parsing a string. + * If useDefault is true then expressions without an explicit mode will default to mode may, otherwise an exception is thrown. + *

+ *

+ * An expression with explicit mode takes the form {@code \ }. + * An expression without explicit mode takes the form {@code }. + *

+ *

+ * The supported modes are: + *

  • may - true if the given C expression may evaluate to true
    • + *
  • must - true if the given C expression must evaluate to true
    • + *

    + * + * @throws IllegalArgumentException if parsing the expression fails. + * Note that evaluating the expression may also throw, so this method not throwing does not mean the expression is guaranteed to be valid. + */ + public static ConditionalExpression fromString(String conditionalExpression, boolean useDefault) { + String mode, expression; + if (hasExplicitMode(conditionalExpression)) { + String[] parts = conditionalExpression.split("\\s+", 2); + if (parts.length != 2) { + throw new IllegalArgumentException("Invalid expression: " + conditionalExpression); + } + mode = parts[0].substring(EXPLICIT_MODE_PREFIX.length()).toLowerCase(Locale.ROOT); + expression = parts[1]; + } else { + if (!useDefault) { + throw new IllegalArgumentException("Must specify mode explicitly"); + } + mode = "may"; + expression = conditionalExpression; + } + + return switch (mode) { + case "may" -> new ConditionalExpression(false, expression); + case "must" -> new ConditionalExpression(true, expression); + default -> throw new IllegalArgumentException("Unknown mode: " + mode); + }; + } + + public static boolean hasExplicitMode(String conditionalExpression) { + return conditionalExpression.startsWith(EXPLICIT_MODE_PREFIX); + } + + /** + * Evaluate expression as conditional at given node. + * + * @throws IllegalArgumentException if evaluating the condition failed. + */ + public boolean evaluateCondition(NodeInfo node, ResultsService resultsService) { + try { + var result = resultsService.evaluateIntegerExpression(node.nodeId(), "!!(" + expression + ")"); + return must ? result.mustBeBool(true) : result.mayBeBool(true); + } catch (RequestFailedException e) { + throw new IllegalArgumentException("Error evaluating condition: " + e.getMessage()); + } + } + + /** + * Evaluate expression as value at given node. + * + * @throws IllegalArgumentException if evaluating the condition failed. + */ + public JsonElement evaluateValue(NodeInfo node, ResultsService resultsService) { + return new JsonPrimitive(evaluateCondition(node, resultsService)); + } + +} diff --git a/src/main/java/abstractdebugging/EdgeInfo.java b/src/main/java/abstractdebugging/EdgeInfo.java new file mode 100644 index 0000000..ae10828 --- /dev/null +++ b/src/main/java/abstractdebugging/EdgeInfo.java @@ -0,0 +1,40 @@ +package abstractdebugging; + +/** + * @since 0.0.4 + */ + +public class EdgeInfo { + + private final String nodeId; + private final String cfgNodeId; + private final String contextId; + private final String pathId; + + // Target node location is returned by Goblint, but cannot be safely used here because we patch the location + // based on outgoing edges which are not available here. (see AbstractDebuggingServer.lookupNodes for more info) + + public EdgeInfo(String nodeId, String cfgNodeId, String contextId, String pathId) { + this.nodeId = nodeId; + this.cfgNodeId = cfgNodeId; + this.contextId = contextId; + this.pathId = pathId; + } + + public final String nodeId() { + return nodeId; + } + + public final String cfgNodeId() { + return cfgNodeId; + } + + public final String contextId() { + return contextId; + } + + public final String pathId() { + return pathId; + } + +} diff --git a/src/main/java/abstractdebugging/EventQueue.java b/src/main/java/abstractdebugging/EventQueue.java new file mode 100644 index 0000000..febda60 --- /dev/null +++ b/src/main/java/abstractdebugging/EventQueue.java @@ -0,0 +1,37 @@ +package abstractdebugging; + +import java.util.ArrayList; +import java.util.List; + +public class EventQueue { + + private final List queuedEvents = new ArrayList<>(); + private final Object lock = new Object(); + + /** + * Queues a new event which will be run after the next message is sent to the client. + * Note: Sending an event/notification also triggers running events. + * To avoid problems any queued events should be added to the queue after all non-queued events are sent. + */ + public void queue(Runnable runnable) { + synchronized (lock) { + queuedEvents.add(runnable); + } + } + + /** + * Runs all queued events. + * If a new event is queued during runAll then it will not be run during this call to runAll and will remain in the queue. + */ + public void runAll() { + List events; + synchronized (lock) { + events = new ArrayList<>(queuedEvents); + queuedEvents.clear(); + } + for (var event : events) { + event.run(); + } + } + +} diff --git a/src/main/java/abstractdebugging/EventQueueMessageConsumer.java b/src/main/java/abstractdebugging/EventQueueMessageConsumer.java new file mode 100644 index 0000000..ba83098 --- /dev/null +++ b/src/main/java/abstractdebugging/EventQueueMessageConsumer.java @@ -0,0 +1,36 @@ +package abstractdebugging; + +import org.eclipse.lsp4j.jsonrpc.JsonRpcException; +import org.eclipse.lsp4j.jsonrpc.MessageConsumer; +import org.eclipse.lsp4j.jsonrpc.MessageIssueException; +import org.eclipse.lsp4j.jsonrpc.messages.Message; + +/** + * A wrapping lsp4j MessageConsumer that allows queueing events that will run after a message is sent. + * This is a reasonably clean workaround for lsp4j issue #229. + * TODO: Try to upstream an implementation of event queueing to lsp4j? + * TODO: If lsp4j issue #229 ever gets resolved then replace this with the implemented solution. + * + * @author Juhan Oskar Hennoste + */ +public class EventQueueMessageConsumer implements MessageConsumer { + + private final MessageConsumer inner; + private final EventQueue eventQueue; + + public EventQueueMessageConsumer(MessageConsumer inner, EventQueue eventQueue) { + if (eventQueue == null) { + throw new IllegalArgumentException("eventQueue must not be null"); + } + this.inner = inner; + this.eventQueue = eventQueue; + } + + @Override + public void consume(Message message) throws MessageIssueException, JsonRpcException { + inner.consume(message); + eventQueue.runAll(); + } + +} + diff --git a/src/main/java/abstractdebugging/FunctionCallEdgeInfo.java b/src/main/java/abstractdebugging/FunctionCallEdgeInfo.java new file mode 100644 index 0000000..9b2e8fe --- /dev/null +++ b/src/main/java/abstractdebugging/FunctionCallEdgeInfo.java @@ -0,0 +1,35 @@ +package abstractdebugging; + +import java.util.List; + +/** + * @since 0.0.4 + */ + +public class FunctionCallEdgeInfo extends EdgeInfo { + + private final String function; + private final List args; + private final boolean createsNewThread; + + public FunctionCallEdgeInfo(String nodeId, String cfgNodeId, String contextId, String pathId, + String function, List args, boolean createsNewThread) { + super(nodeId, cfgNodeId, contextId, pathId); + this.function = function; + this.args = args; + this.createsNewThread = createsNewThread; + } + + public final String function() { + return function; + } + + public final List args() { + return args; + } + + public final boolean createsNewThread() { + return createsNewThread; + } + +} diff --git a/src/main/java/abstractdebugging/IllegalStepException.java b/src/main/java/abstractdebugging/IllegalStepException.java new file mode 100644 index 0000000..aaf1db6 --- /dev/null +++ b/src/main/java/abstractdebugging/IllegalStepException.java @@ -0,0 +1,15 @@ +package abstractdebugging; + +/** + * Thrown when the requested step is invalid. + * Usually this occurs because the target node is ambiguous for some thread. + * + * @since 0.0.4 + */ +public class IllegalStepException extends Exception { + + public IllegalStepException(String message) { + super(message); + } + +} diff --git a/src/main/java/abstractdebugging/NodeInfo.java b/src/main/java/abstractdebugging/NodeInfo.java new file mode 100644 index 0000000..3afe339 --- /dev/null +++ b/src/main/java/abstractdebugging/NodeInfo.java @@ -0,0 +1,48 @@ +package abstractdebugging; + +import api.messages.GoblintLocation; + +import java.util.ArrayList; +import java.util.List; + +/** + * Represents information about an ARG node. + * + * @param nodeId The ARG node id assigned by Goblint + * @param cfgNodeId The corresponding CFG node id assigned by Goblint + * @param contextId The corresponding context id assigned by Goblint + * @param pathId The corresponding path id assigned by Goblint + * @param location Location of node in source code + * @param function Name of function that contains this node + * @since 0.0.4 + */ +public record NodeInfo( + String nodeId, + String cfgNodeId, + String contextId, + String pathId, + GoblintLocation location, + String function, + + List incomingCFGEdges, + List incomingEntryEdges, + List incomingReturnEdges, + + List outgoingCFGEdges, + List outgoingEntryEdges, + List outgoingReturnEdges +) { + + public NodeInfo(String nodeId, String cfgNodeId, String contextId, String pathId, GoblintLocation location, String function) { + this(nodeId, cfgNodeId, contextId, pathId, location, function, + new ArrayList<>(), new ArrayList<>(), new ArrayList<>(), + new ArrayList<>(), new ArrayList<>(), new ArrayList<>()); + } + + public NodeInfo withLocation(GoblintLocation location) { + return new NodeInfo(nodeId(), cfgNodeId(), contextId(), pathId(), location, function(), + incomingCFGEdges(), incomingEntryEdges(), incomingReturnEdges(), + outgoingCFGEdges(), outgoingEntryEdges(), outgoingReturnEdges()); + } + +} diff --git a/src/main/java/abstractdebugging/RequestFailedException.java b/src/main/java/abstractdebugging/RequestFailedException.java new file mode 100644 index 0000000..b7a8ec5 --- /dev/null +++ b/src/main/java/abstractdebugging/RequestFailedException.java @@ -0,0 +1,17 @@ +package abstractdebugging; + +import api.GoblintService; + +/** + * Exception thrown by {@link AbstractDebuggingServer} {@link GoblintService} wrapper methods + * when a syntactically valid request to the Goblint server fails for a known/expected reason. + * + * @since 0.0.4 + */ +public class RequestFailedException extends RuntimeException { + + public RequestFailedException(String message) { + super(message); + } + +} diff --git a/src/main/java/abstractdebugging/ResultsService.java b/src/main/java/abstractdebugging/ResultsService.java new file mode 100644 index 0000000..3fa5d12 --- /dev/null +++ b/src/main/java/abstractdebugging/ResultsService.java @@ -0,0 +1,136 @@ +package abstractdebugging; + +import api.GoblintService; +import api.messages.*; +import api.messages.params.*; +import com.google.gson.JsonElement; +import com.google.gson.JsonObject; +import org.eclipse.lsp4j.jsonrpc.ResponseErrorException; +import org.eclipse.lsp4j.jsonrpc.messages.ResponseErrorCode; + +import java.util.Collection; +import java.util.List; +import java.util.concurrent.CompletionException; + +/** + * Synchronous convenience methods for working with GoblintService for abstract debugging. + * In the future this can be converted to an interface and mocked for testing purposes. + * + * @since 0.0.4 + */ +public class ResultsService { + + private final GoblintService goblintService; + + public ResultsService(GoblintService goblintService) { + this.goblintService = goblintService; + } + + public List lookupNodes(LookupParams params) { + return goblintService.arg_lookup(params) + .thenApply(result -> result.stream() + .map(lookupResult -> { + NodeInfo nodeInfo = lookupResult.toNodeInfo(); + if (!nodeInfo.outgoingReturnEdges().isEmpty() && nodeInfo.outgoingCFGEdges().isEmpty()) { + // Location of return nodes is generally the entire function. + // That looks strange, so we patch it to be only the end of the last line of the function. + // TODO: Maybe it would be better to adjust location when returning stack so the node info retains the original location + return nodeInfo.withLocation(new GoblintLocation( + nodeInfo.location().getFile(), + nodeInfo.location().getEndLine(), nodeInfo.location().getEndColumn(), + nodeInfo.location().getEndLine(), nodeInfo.location().getEndColumn() + )); + } else { + return nodeInfo; + } + }) + .toList()) + .join(); + } + + /** + * @throws RequestFailedException if the node was not found or multiple nodes were found. + */ + public NodeInfo lookupNode(String nodeId) { + var nodes = lookupNodes(LookupParams.byNodeId(nodeId)); + return switch (nodes.size()) { + case 0 -> throw new RequestFailedException("Node with id " + nodeId + " not found"); + case 1 -> nodes.get(0); + default -> throw new RequestFailedException("Multiple nodes with id " + nodeId + " found"); + }; + } + + /** + * Find a CFG node by its location. Any node that appears at this location or after it, is considered matching. + * + * @throws RequestFailedException if a matching node was not found. + */ + public CFGNodeInfo lookupCFGNode(GoblintLocation location) { + try { + return goblintService.cfg_lookup(CFGLookupParams.byLocation(location)).join().toCFGNodeInfo(); + } catch (CompletionException e) { + if (isRequestFailedError(e.getCause())) { + throw new RequestFailedException(e.getCause().getMessage()); + } + throw e; + } + } + + public JsonObject lookupState(String nodeId) { + return goblintService.arg_state(new ARGStateParams(nodeId)).join(); + } + + public JsonElement lookupGlobalState() { + return goblintService.global_state(GlobalStateParams.all()).join(); + } + + /** + * @throws RequestFailedException if evaluating the expression failed, generally because the expression is syntactically or semantically invalid. + */ + public EvalIntResult evaluateIntegerExpression(String nodeId, String expression) { + try { + return goblintService.arg_eval_int(new EvalIntQueryParams(nodeId, expression)).join(); + } catch (CompletionException e) { + // Promote request failure to public API error because it is usually caused by the user entering an invalid expression + // and the error message contains useful info about why the expression was invalid. + if (isRequestFailedError(e.getCause())) { + throw new RequestFailedException(e.getCause().getMessage()); + } + throw e; + } + } + + /** + * @throws RequestFailedException if evaluating the expression failed, generally because the expression is syntactically or semantically invalid. + */ + public JsonElement evaluateExpression(String nodeId, String expression) { + try { + return goblintService.arg_eval(new EvalQueryParams(nodeId, expression)).join(); + } catch (CompletionException e) { + // See note in evaluateIntegerExpression + if (isRequestFailedError(e.getCause())) { + throw new RequestFailedException(e.getCause().getMessage()); + } + throw e; + } + } + + public List getVarinfos() { + return goblintService.cil_varinfos().join(); + } + + /** + * Retrieves and returns a list of source files analyzed by Goblint. + */ + public List getGoblintTrackedFiles() { + return goblintService.files().join() + .values().stream() + .flatMap(Collection::stream) + .toList(); + } + + private static boolean isRequestFailedError(Throwable e) { + return e instanceof ResponseErrorException re && re.getResponseError().getCode() == ResponseErrorCode.RequestFailed.getValue(); + } + +} diff --git a/src/main/java/abstractdebugging/StackFrameState.java b/src/main/java/abstractdebugging/StackFrameState.java new file mode 100644 index 0000000..f739337 --- /dev/null +++ b/src/main/java/abstractdebugging/StackFrameState.java @@ -0,0 +1,63 @@ +package abstractdebugging; + +import javax.annotation.Nullable; + +/** + * @since 0.0.4 + */ + +public class StackFrameState { + + private NodeInfo node; + private NodeInfo lastReachableNode; + private final boolean ambiguousFrame; + private final int localThreadIndex; + + public StackFrameState(NodeInfo node, boolean ambiguousFrame, int localThreadIndex) { + this.node = node; + this.lastReachableNode = node; + this.ambiguousFrame = ambiguousFrame; + this.localThreadIndex = localThreadIndex; + } + + /** + * Current ARG node in this frame. + */ + @Nullable + public NodeInfo getNode() { + return node; + } + + /** + * Returns the last reachable (non-null) node that this frame has been on. + */ + @Nullable + public NodeInfo getLastReachableNode() { + return lastReachableNode; + } + + /** + * If frame is ambiguous. An ambiguous frame is a frame where multiple possible frames can exist in the same position in the call stack. + */ + public boolean isAmbiguousFrame() { + return ambiguousFrame; + } + + /** + * Local thread index. Two stack frames in the same stack with different local thread indexes belong to different program threads. + */ + public int getLocalThreadIndex() { + return localThreadIndex; + } + + /** + * Sets current node. Tracks last reachable (non-null) node. + */ + public void setNode(NodeInfo node) { + if (node != null) { + this.lastReachableNode = node; + } + this.node = node; + } + +} diff --git a/src/main/java/abstractdebugging/ThreadState.java b/src/main/java/abstractdebugging/ThreadState.java new file mode 100644 index 0000000..e956739 --- /dev/null +++ b/src/main/java/abstractdebugging/ThreadState.java @@ -0,0 +1,57 @@ +package abstractdebugging; + +import java.util.List; + +/** + * Represents the state of a debugging thread. + * The state consists of a name, which is assigned when the thread is created, and a list of call stack frames. + *

    + * A note about terminology: The topmost frame is the frame that was added by the latest function call and contains the current location of the thread. + * It is located at index 0 in the list of frames. + * + * @author Juhan Oskar Hennoste + * @since 0.0.4 + */ +public class ThreadState { + + private final String name; + private final List frames; + + public ThreadState(String name, List frames) { + this.name = name; + this.frames = frames; + } + + public String getName() { + return name; + } + + /** + * Get list of stack frames with the latest/topmost frame first. + * Note: Do not manipulate the returned list directly. Use {@link #pushFrame} and {@link #popFrame} instead. + */ + public List getFrames() { + return frames; + } + + public StackFrameState getCurrentFrame() { + return frames.get(0); + } + + public StackFrameState getPreviousFrame() { + return frames.get(1); + } + + public boolean hasPreviousFrame() { + return frames.size() > 1; + } + + public void pushFrame(StackFrameState frame) { + frames.add(0, frame); + } + + public void popFrame() { + frames.remove(0); + } + +} diff --git a/src/main/java/analysis/GoblintAnalysis.java b/src/main/java/analysis/GoblintAnalysis.java index 58548e4..c11cfaa 100644 --- a/src/main/java/analysis/GoblintAnalysis.java +++ b/src/main/java/analysis/GoblintAnalysis.java @@ -2,6 +2,8 @@ import api.GoblintService; import api.messages.*; +import api.messages.params.AnalyzeParams; +import api.messages.params.Params; import com.ibm.wala.classLoader.Module; import goblintserver.GoblintServer; import gobpie.GobPieConfiguration; @@ -32,7 +34,6 @@ import java.util.concurrent.CompletionException; import java.util.concurrent.Future; import java.util.concurrent.TimeoutException; -import java.util.stream.Collectors; import java.util.stream.Stream; /** @@ -209,27 +210,19 @@ else if (analysisResult.getStatus().contains("VerifyError")) throw new GobPieException("Analysis returned VerifyError.", GobPieExceptionType.GOBLINT_EXCEPTION); } - private CompletableFuture> convertAndCombineResults( - CompletableFuture> messagesCompletableFuture, - CompletableFuture> functionsCompletableFuture) { - return messagesCompletableFuture - .thenCombine(functionsCompletableFuture, (messages, functions) -> - Stream.concat( - convertMessagesFromJson(messages).stream(), - convertFunctionsFromJson(functions).stream() - ).collect(Collectors.toList())); - } - private CompletableFuture> getComposedAnalysisResults(GoblintAnalysisResult analysisResult) { didAnalysisNotSucceed(analysisResult); // Get warning messages - CompletableFuture> messagesCompletableFuture = goblintService.messages(); + CompletableFuture> messagesCompletableFuture = goblintService.messages() + .thenApply(this::convertMessagesFromJson); if (!gobpieConfiguration.showCfg()) { - return messagesCompletableFuture.thenApply(this::convertMessagesFromJson); + return messagesCompletableFuture; } // Get list of functions - CompletableFuture> functionsCompletableFuture = goblintService.functions(); - return convertAndCombineResults(messagesCompletableFuture, functionsCompletableFuture); + CompletableFuture> functionsCompletableFuture = goblintService.functions() + .thenApply(this::convertFunctionsFromJson); + return messagesCompletableFuture + .thenCombine(functionsCompletableFuture, (messages, functions) -> Stream.concat(messages.stream(), functions.stream()).toList()); } @@ -248,7 +241,7 @@ private Collection convertMessagesFromJson(List convertFunctionsFromJson(List response) { - return response.stream().map(GoblintFunctionsResult::convert).collect(Collectors.toList()); + return response.stream().map(GoblintFunctionsResult::convert).flatMap(List::stream).toList(); } diff --git a/src/main/java/analysis/GoblintCFGAnalysisResult.java b/src/main/java/analysis/GoblintCFGAnalysisResult.java index fb05d5d..d009896 100644 --- a/src/main/java/analysis/GoblintCFGAnalysisResult.java +++ b/src/main/java/analysis/GoblintCFGAnalysisResult.java @@ -1,6 +1,6 @@ package analysis; -import com.ibm.wala.cast.tree.CAstSourcePositionMap; +import com.ibm.wala.cast.tree.CAstSourcePositionMap.Position; import com.ibm.wala.util.collections.Pair; import magpiebridge.core.AnalysisResult; import magpiebridge.core.Kind; @@ -21,20 +21,20 @@ */ public class GoblintCFGAnalysisResult implements AnalysisResult { - private final CAstSourcePositionMap.Position pos; + private final Position pos; + private final String title; private final String funName; - private final String fileName; - private final Iterable> related = new ArrayList<>(); + private final Iterable> related = new ArrayList<>(); - public GoblintCFGAnalysisResult(CAstSourcePositionMap.Position pos, String funName, String fileName) { + public GoblintCFGAnalysisResult(Position pos, String title, String funName) { this.pos = pos; + this.title = title; this.funName = funName; - this.fileName = fileName; } @Override public Iterable command() { - Command command = new Command("show cfg", "showcfg", Collections.singletonList(funName)); + Command command = new Command(title, "showcfg", Collections.singletonList(funName)); return Collections.singleton(command); } @@ -49,12 +49,12 @@ public String toString(boolean useMarkdown) { } @Override - public CAstSourcePositionMap.Position position() { + public Position position() { return pos; } @Override - public Iterable> related() { + public Iterable> related() { return related; } @@ -64,7 +64,7 @@ public DiagnosticSeverity severity() { } @Override - public Pair repair() { + public Pair repair() { return null; } diff --git a/src/main/java/analysis/ShowCFGCommand.java b/src/main/java/analysis/ShowCFGCommand.java index dad1685..156a6f3 100644 --- a/src/main/java/analysis/ShowCFGCommand.java +++ b/src/main/java/analysis/ShowCFGCommand.java @@ -18,7 +18,6 @@ import java.io.IOException; import java.io.InputStreamReader; -import java.net.URISyntaxException; import java.nio.charset.StandardCharsets; public class ShowCFGCommand implements WorkspaceCommand { @@ -41,10 +40,11 @@ public void execute(ExecuteCommandParams params, MagpieServer server, LanguageCl funName = (String) uriJson; } showHTMLinClientOrBrowser(server, client, funName); - } catch (IOException | URISyntaxException e) { - MagpieServer.ExceptionLogger.log(e); + } catch (IOException e) { + // Note: Logging the exception using log.error("Error:", e) causes JSON-RPC communication with VS Code to break. + // This is caused by a warning printed to stdout by log4j. See https://github.com/apache/logging-log4j2/issues/1484 for more info. + log.error("Error running showcfg command:"); e.printStackTrace(); - log.error(e); } } @@ -55,11 +55,10 @@ public void execute(ExecuteCommandParams params, MagpieServer server, LanguageCl * @param server The MagpieServer * @param client The IDE/Editor * @param funName The name of the function to show the CFG for - * @throws IOException IO exception - * @throws URISyntaxException URI exception + * @throws IOException IO exception */ - public void showHTMLinClientOrBrowser(MagpieServer server, LanguageClient client, String funName) throws IOException, URISyntaxException { + public void showHTMLinClientOrBrowser(MagpieServer server, LanguageClient client, String funName) throws IOException { if (server.clientSupportShowHTML()) { if (client instanceof MagpieClient) { String json = "{\"funName\": \"" + funName + "\"}"; diff --git a/src/main/java/api/GoblintService.java b/src/main/java/api/GoblintService.java index 9a2c896..700d062 100644 --- a/src/main/java/api/GoblintService.java +++ b/src/main/java/api/GoblintService.java @@ -1,11 +1,13 @@ package api; -import HTTPserver.GobPieHttpHandler; import api.messages.*; +import api.messages.params.*; +import com.google.gson.JsonElement; import com.google.gson.JsonObject; import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; import java.util.List; +import java.util.Map; import java.util.concurrent.CompletableFuture; /** @@ -37,14 +39,47 @@ public interface GoblintService { @JsonRequest CompletableFuture> functions(); + @JsonRequest + CompletableFuture>> files(); + + @JsonRequest + CompletableFuture>> pre_files(); + // request: {"jsonrpc":"2.0","id":0,"method":"cfg", "params":{"fname":"main"}} // response: {"id":0,"jsonrpc":"2.0","result":{"cfg":"digraph cfg {\n\tnode [id=\"\\N\", ... }} - @JsonRequest - CompletableFuture cfg(Params params); + @JsonRequest("cfg") + CompletableFuture cfg_dot(Params params); + + @JsonRequest("cfg/lookup") + CompletableFuture cfg_lookup(CFGLookupParams params); // request: {"jsonrpc":"2.0","id":0,"method":"node_state","params":{"nid":"fun2783"}} - @JsonRequest - CompletableFuture> node_state(GobPieHttpHandler.NodeParams params); + @JsonRequest("node_state") + CompletableFuture> cfg_state(NodeParams params); + + @JsonRequest("arg/dot") + CompletableFuture arg_dot(); + + @JsonRequest("arg/lookup") + CompletableFuture> arg_lookup(LookupParams params); + + @JsonRequest("arg/state") + CompletableFuture arg_state(ARGStateParams params); + + @JsonRequest("arg/eval-int") + CompletableFuture arg_eval_int(EvalIntQueryParams params); + + @JsonRequest("arg/eval") + CompletableFuture arg_eval(EvalQueryParams params); + + @JsonRequest("cil/varinfos") + CompletableFuture> cil_varinfos(); + + @JsonRequest("richvarinfos") + CompletableFuture richvarinfos(); + + @JsonRequest("global-state") + CompletableFuture global_state(GlobalStateParams params); @JsonRequest CompletableFuture reset_config(); diff --git a/src/main/java/api/json/GoblintMessageJsonHandler.java b/src/main/java/api/json/GoblintMessageJsonHandler.java index bafc038..8a3e3ab 100644 --- a/src/main/java/api/json/GoblintMessageJsonHandler.java +++ b/src/main/java/api/json/GoblintMessageJsonHandler.java @@ -30,7 +30,7 @@ public GsonBuilder getDefaultGsonBuilder() { .registerTypeAdapterFactory(new TupleTypeAdapters.TwoTypeAdapterFactory()) .registerTypeAdapterFactory(new EnumTypeAdapter.Factory()) .registerTypeAdapterFactory(new GoblintMessageTypeAdapter.Factory(this)) - .registerTypeAdapter(GoblintMessagesResult.tag.class, new GoblintTagInterfaceAdapter()); + .registerTypeAdapter(GoblintMessagesResult.Tag.class, new GoblintTagInterfaceAdapter()); } } diff --git a/src/main/java/api/json/GoblintSocketMessageConsumer.java b/src/main/java/api/json/GoblintSocketMessageConsumer.java index d614536..a0bdee9 100644 --- a/src/main/java/api/json/GoblintSocketMessageConsumer.java +++ b/src/main/java/api/json/GoblintSocketMessageConsumer.java @@ -47,7 +47,7 @@ public void consume(Message message) { output.write(contentBytes); output.flush(); } - log.debug("Request written to socket."); + log.debug("WRITTEN: {}", content); } catch (IOException exception) { throw new JsonRpcException(exception); } diff --git a/src/main/java/api/json/GoblintSocketMessageProducer.java b/src/main/java/api/json/GoblintSocketMessageProducer.java index a4ce11d..e94860f 100644 --- a/src/main/java/api/json/GoblintSocketMessageProducer.java +++ b/src/main/java/api/json/GoblintSocketMessageProducer.java @@ -95,7 +95,7 @@ protected boolean handleMessage() throws IOException { try { String content = inputReader.readLine(); - log.debug("Response read from socket."); + log.debug("READ: {}", content); try { if (content != null) { Message message = jsonHandler.parseMessage(content); @@ -105,10 +105,14 @@ protected boolean handleMessage() throws IOException { } } catch (MessageIssueException exception) { // An issue was found while parsing or validating the message - if (issueHandler != null) + if (issueHandler != null) { issueHandler.handle(exception.getRpcMessage(), exception.getIssues()); - else + } else { fireError(exception); + for (var issue : exception.getIssues()) { + fireError(issue.getCause()); + } + } return false; } } catch (Exception exception) { diff --git a/src/main/java/api/messages/EvalIntResult.java b/src/main/java/api/messages/EvalIntResult.java new file mode 100644 index 0000000..dd09cbb --- /dev/null +++ b/src/main/java/api/messages/EvalIntResult.java @@ -0,0 +1,54 @@ +package api.messages; + +import com.google.gson.JsonElement; +import com.google.gson.annotations.SerializedName; + +import javax.annotation.Nullable; +import java.math.BigInteger; + +/** + * @since 0.0.4 + */ +public class EvalIntResult { + + private JsonElement raw; + + @SerializedName("int") + @Nullable + private BigInteger int_; + @Nullable + private Boolean bool; + + public JsonElement getRaw() { + return raw; + } + + @Nullable + public BigInteger getInt() { + return int_; + } + + @Nullable + public Boolean getBool() { + return bool; + } + + public boolean isTop() { + // TODO: Is this the only possible representation of top? + return raw.isJsonPrimitive() && "top".equals(raw.getAsString()); + } + + public boolean isBot() { + // TODO: Is this the only possible representation of bot? + return raw.isJsonPrimitive() && "bot".equals(raw.getAsString()); + } + + public boolean mayBeBool(boolean bool) { + return mustBeBool(bool) || (!isBot() && this.bool == null); + } + + public boolean mustBeBool(boolean bool) { + return this.bool != null && this.bool == bool; + } + +} diff --git a/src/main/java/api/messages/GoblintARGLookupResult.java b/src/main/java/api/messages/GoblintARGLookupResult.java new file mode 100644 index 0000000..ad2ffba --- /dev/null +++ b/src/main/java/api/messages/GoblintARGLookupResult.java @@ -0,0 +1,98 @@ +package api.messages; + +import abstractdebugging.CFGEdgeInfo; +import abstractdebugging.FunctionCallEdgeInfo; +import abstractdebugging.NodeInfo; +import com.google.gson.JsonElement; +import com.google.gson.JsonObject; +import com.google.gson.annotations.SerializedName; + +import java.util.List; + +/** + * @since 0.0.4 + */ + +public class GoblintARGLookupResult { + + private String node; + private String cfg_node; + private String context; + private String path; + private GoblintLocation location; + private String function; + + private List prev; + private List next; + + public static class Edge { + private Properties edge; + + private String node; + private String cfg_node; + private String context; + private String path; + private GoblintLocation location; + private String function; + + public static class Properties { + private JsonObject cfg; + private JsonObject inlined; + + @SerializedName("return") + private FunctionCall ret; + private FunctionCall entry; + private FunctionCall thread; + + public static class FunctionCall { + JsonElement function; + List args; + JsonElement lval; + } + } + } + + public NodeInfo toNodeInfo() { + NodeInfo nodeInfo = new NodeInfo(node, cfg_node, context, path, location, function); + mapEdges(prev, nodeInfo.incomingCFGEdges(), nodeInfo.incomingReturnEdges(), nodeInfo.incomingEntryEdges()); + mapEdges(next, nodeInfo.outgoingCFGEdges(), nodeInfo.outgoingReturnEdges(), nodeInfo.outgoingEntryEdges()); + return nodeInfo; + } + + private static void mapEdges(List edges, List cfgEdges, List returnEdges, List entryEdges) { + for (var edge : edges) { + if (edge.edge.cfg != null || edge.edge.inlined != null) { + var properties = edge.edge.cfg != null ? edge.edge.cfg : edge.edge.inlined; + CFGEdgeInfo edgeInfo = new CFGEdgeInfo(edge.node, edge.cfg_node, edge.context, edge.path, + properties.get("string").getAsString()); + cfgEdges.add(edgeInfo); + } else if (edge.edge.ret != null) { + var properties = edge.edge.ret; + FunctionCallEdgeInfo edgeInfo = new FunctionCallEdgeInfo(edge.node, edge.cfg_node, edge.context, edge.path, + toPrettyString(properties.function), properties.args.stream().map(GoblintARGLookupResult::toPrettyString).toList(), false); + returnEdges.add(edgeInfo); + } else if (edge.edge.entry != null) { + var properties = edge.edge.entry; + FunctionCallEdgeInfo edgeInfo = new FunctionCallEdgeInfo(edge.node, edge.cfg_node, edge.context, edge.path, + toPrettyString(properties.function), properties.args.stream().map(GoblintARGLookupResult::toPrettyString).toList(), false); + entryEdges.add(edgeInfo); + } else if (edge.edge.thread != null) { + var properties = edge.edge.thread; + FunctionCallEdgeInfo edgeInfo = new FunctionCallEdgeInfo(edge.node, edge.cfg_node, edge.context, edge.path, + toPrettyString(properties.function), properties.args.stream().map(GoblintARGLookupResult::toPrettyString).toList(), true); + entryEdges.add(edgeInfo); + } else { + throw new IllegalStateException("Unknown edge type: " + edge); + } + } + } + + private static String toPrettyString(JsonElement value) { + if (value.isJsonPrimitive()) { + return value.getAsString(); + } else { + return value.toString(); + } + } + +} diff --git a/src/main/java/api/messages/GoblintARGResult.java b/src/main/java/api/messages/GoblintARGResult.java new file mode 100644 index 0000000..ca9c8d3 --- /dev/null +++ b/src/main/java/api/messages/GoblintARGResult.java @@ -0,0 +1,18 @@ +package api.messages; + +/** + * The Class GoblintARGResult. + *

    + * Corresponding object to the Goblint cfg request response results in JSON. + * + * @author Juhan Oskar Hennoste + * @since 0.0.4 + */ + +public class GoblintARGResult { + private String arg; + + public String getArg() { + return arg; + } +} diff --git a/src/main/java/api/messages/GoblintCFGLookupResult.java b/src/main/java/api/messages/GoblintCFGLookupResult.java new file mode 100644 index 0000000..46c649b --- /dev/null +++ b/src/main/java/api/messages/GoblintCFGLookupResult.java @@ -0,0 +1,18 @@ +package api.messages; + +import abstractdebugging.CFGNodeInfo; + +/** + * @since 0.0.4 + */ + +public class GoblintCFGLookupResult { + + private String node; + private GoblintLocation location; + + public CFGNodeInfo toCFGNodeInfo() { + return new CFGNodeInfo(node, location); + } + +} diff --git a/src/main/java/api/messages/GoblintFunctionsResult.java b/src/main/java/api/messages/GoblintFunctionsResult.java index 4a0d41d..1c59cba 100644 --- a/src/main/java/api/messages/GoblintFunctionsResult.java +++ b/src/main/java/api/messages/GoblintFunctionsResult.java @@ -3,8 +3,7 @@ import analysis.GoblintCFGAnalysisResult; import magpiebridge.core.AnalysisResult; -import java.io.File; -import java.net.MalformedURLException; +import java.util.List; /** * The Class GoblintFunctionsResult. @@ -21,29 +20,19 @@ public class GoblintFunctionsResult { String type = getClass().getName(); private String funName; - private location location; - - static class location { - private String file; - private int line; - private int column; - private int endLine; - private int endColumn; - } + private GoblintLocation location; public String getType() { return type; } - public AnalysisResult convert() { - try { - return new GoblintCFGAnalysisResult( - new GoblintPosition(location.line, location.endLine, location.column, location.endColumn, new File(location.file).toURI().toURL()), - funName, - new File(location.file).getName() - ); - } catch (MalformedURLException e) { - throw new RuntimeException(e); + public List convert() { + var cfgResult = new GoblintCFGAnalysisResult(location.toPosition(), "show cfg", funName); + if (funName.equals("main")) { + AnalysisResult argResult = new GoblintCFGAnalysisResult(location.toPosition(), "show arg", ""); + return List.of(argResult, cfgResult); + } else { + return List.of(cfgResult); } } diff --git a/src/main/java/api/messages/GoblintLocation.java b/src/main/java/api/messages/GoblintLocation.java new file mode 100644 index 0000000..214dfbe --- /dev/null +++ b/src/main/java/api/messages/GoblintLocation.java @@ -0,0 +1,80 @@ +package api.messages; + +import com.google.gson.annotations.SerializedName; + +import java.io.File; +import java.net.MalformedURLException; + +/** + * Goblint CIL location. + * + * @author Juhan Oskar Hennoste + * @since 0.0.4 + */ +public class GoblintLocation { + + private String file; + private int line; + private int column; + private Integer endLine; + private Integer endColumn; + + // Byte offsets from start of file. + // This duplicates information from line and column fields, but needs to exist when using the location as a parameter. + @SerializedName("byte") + private int startByte = -1; + + public GoblintLocation(String file, int line, int column) { + this.file = file; + this.line = line; + this.column = column; + } + + public GoblintLocation(String file, int line, int column, int endLine, int endColumn) { + this.file = file; + this.line = line; + this.column = column; + this.endLine = endLine; + this.endColumn = endColumn; + } + + public String getFile() { + return file; + } + + public int getLine() { + return line; + } + + public int getColumn() { + return column; + } + + public Integer getEndLine() { + return endLine; + } + + public Integer getEndColumn() { + return endColumn; + } + + public GoblintPosition toPosition() { + try { + return new GoblintPosition( + this.line, + this.endLine, + this.column < 0 ? 0 : this.column - 1, + this.endColumn < 0 ? 10000 : this.endColumn - 1, + new File(this.file).toURI().toURL()); + } catch (MalformedURLException e) { + throw new RuntimeException(e); + } + } + + @Override + public String toString() { + return file + " " + + line + ":" + column + + (endLine == null && endColumn == null ? "" : "-" + endLine + ":" + endColumn); + } +} diff --git a/src/main/java/api/messages/GoblintMessagesResult.java b/src/main/java/api/messages/GoblintMessagesResult.java index 3f0530d..1c4bdec 100644 --- a/src/main/java/api/messages/GoblintMessagesResult.java +++ b/src/main/java/api/messages/GoblintMessagesResult.java @@ -1,8 +1,8 @@ package api.messages; import analysis.GoblintMessagesAnalysisResult; -import com.ibm.wala.util.collections.Pair; import com.ibm.wala.cast.tree.CAstSourcePositionMap.Position; +import com.ibm.wala.util.collections.Pair; import magpiebridge.core.AnalysisResult; import java.io.File; @@ -25,15 +25,15 @@ public class GoblintMessagesResult { private final String type = getClass().getName(); - private final List tags = new ArrayList<>(); + private final List tags = new ArrayList<>(); private String severity; - private multipiece multipiece; + private Multipiece multipiece; - public interface tag { + public interface Tag { String toString(); } - public static class Category implements tag { + public static class Category implements Tag { private final List Category = new ArrayList<>(); @Override @@ -42,7 +42,7 @@ public String toString() { } } - public static class CWE implements tag { + public static class CWE implements Tag { private Integer CWE; @Override @@ -51,23 +51,15 @@ public String toString() { } } - static class loc { - private String file; - private int line; - private int column; - private int endLine; - private int endColumn; - } - - static class multipiece { - private loc loc; + static class Multipiece { + private GoblintLocation loc; private String text; private String group_text; - private final List pieces = new ArrayList<>(); + private final List pieces = new ArrayList<>(); - static class pieces { + static class Piece { private String text; - private loc loc; + private GoblintLocation loc; } } @@ -125,31 +117,18 @@ public List convertNonExplode() { } } - public GoblintPosition locationToPosition(loc loc) { - try { - return new GoblintPosition( - loc.line, - loc.endLine, - loc.column < 0 ? 0 : loc.column - 1, - loc.endColumn < 0 ? 10000 : loc.endColumn - 1, - new File(loc.file).toURI().toURL()); - } catch (MalformedURLException e) { - throw new RuntimeException(e); - } - } - - public GoblintPosition getLocation(loc loc) { + public GoblintPosition getLocation(GoblintLocation loc) { try { return loc == null ? new GoblintPosition(1, 1, 1, new File("").toURI().toURL()) - : locationToPosition(loc); + : loc.toPosition(); } catch (MalformedURLException e) { throw new RuntimeException(e); } } - public GoblintPosition getRandomLocation(multipiece multipiece) { - for (GoblintMessagesResult.multipiece.pieces piece : multipiece.pieces) { + public GoblintPosition getRandomLocation(Multipiece multipiece) { + for (GoblintMessagesResult.Multipiece.Piece piece : multipiece.pieces) { if (piece.loc != null) return getLocation(piece.loc); } return getLocation(multipiece.loc); @@ -157,29 +136,29 @@ public GoblintPosition getRandomLocation(multipiece multipiece) { public GoblintMessagesAnalysisResult createGoblintAnalysisResult() { GoblintPosition pos = getLocation(multipiece.loc); - String msg = tags.stream().map(tag::toString).collect(Collectors.joining("")) + " " + multipiece.text; + String msg = tags.stream().map(Tag::toString).collect(Collectors.joining("")) + " " + multipiece.text; return new GoblintMessagesAnalysisResult(pos, msg, severity); } - public GoblintMessagesAnalysisResult createGoblintAnalysisResult(multipiece.pieces piece, boolean addGroupText) { + public GoblintMessagesAnalysisResult createGoblintAnalysisResult(Multipiece.Piece piece, boolean addGroupText) { GoblintPosition pos = getLocation(piece.loc); return new GoblintMessagesAnalysisResult( pos, addGroupText - ? tags.stream().map(tag::toString).collect(Collectors.joining("")) + " Group: " + multipiece.group_text + ? tags.stream().map(Tag::toString).collect(Collectors.joining("")) + " Group: " + multipiece.group_text : "", piece.text, severity); } - public GoblintMessagesAnalysisResult createGoblintAnalysisResult(multipiece multipiece, List> related) { + public GoblintMessagesAnalysisResult createGoblintAnalysisResult(Multipiece multipiece, List> related) { GoblintPosition pos = multipiece.loc != null ? getLocation(multipiece.loc) : getRandomLocation(multipiece); return new GoblintMessagesAnalysisResult( pos, - tags.stream().map(tag::toString).collect(Collectors.joining("")) + " " + this.multipiece.group_text, + tags.stream().map(Tag::toString).collect(Collectors.joining("")) + " " + this.multipiece.group_text, severity, related); } diff --git a/src/main/java/api/messages/GoblintVarinfo.java b/src/main/java/api/messages/GoblintVarinfo.java new file mode 100644 index 0000000..c427775 --- /dev/null +++ b/src/main/java/api/messages/GoblintVarinfo.java @@ -0,0 +1,49 @@ +package api.messages; + +import javax.annotation.Nullable; + +/** + * @since 0.0.4 + */ + +public class GoblintVarinfo { + + private long vid; + private String name; + private String original_name; + private String role; + private String function; + private String type; + private GoblintLocation location; + + public long getVid() { + return vid; + } + + public String getName() { + return name; + } + + @Nullable + public String getOriginalName() { + return original_name; + } + + public String getRole() { + return role; + } + + @Nullable + public String getFunction() { + return function; + } + + public String getType() { + return type; + } + + public GoblintLocation getLocation() { + return location; + } + +} diff --git a/src/main/java/api/messages/params/ARGStateParams.java b/src/main/java/api/messages/params/ARGStateParams.java new file mode 100644 index 0000000..a7589aa --- /dev/null +++ b/src/main/java/api/messages/params/ARGStateParams.java @@ -0,0 +1,15 @@ +package api.messages.params; + +/** + * @since 0.0.4 + */ + +public class ARGStateParams { + + private String node; + + public ARGStateParams(String node) { + this.node = node; + } + +} diff --git a/src/main/java/api/messages/AnalyzeParams.java b/src/main/java/api/messages/params/AnalyzeParams.java similarity index 79% rename from src/main/java/api/messages/AnalyzeParams.java rename to src/main/java/api/messages/params/AnalyzeParams.java index 897a15f..d197cd6 100644 --- a/src/main/java/api/messages/AnalyzeParams.java +++ b/src/main/java/api/messages/params/AnalyzeParams.java @@ -1,11 +1,11 @@ -package api.messages; - -public class AnalyzeParams { - - boolean reset; - - public AnalyzeParams(boolean reset) { - this.reset = reset; - } - -} +package api.messages.params; + +public class AnalyzeParams { + + boolean reset; + + public AnalyzeParams(boolean reset) { + this.reset = reset; + } + +} diff --git a/src/main/java/api/messages/params/CFGLookupParams.java b/src/main/java/api/messages/params/CFGLookupParams.java new file mode 100644 index 0000000..e9faa71 --- /dev/null +++ b/src/main/java/api/messages/params/CFGLookupParams.java @@ -0,0 +1,27 @@ +package api.messages.params; + +import api.messages.GoblintLocation; + +/** + * @since 0.0.4 + */ + +public class CFGLookupParams { + + private String node; + private GoblintLocation location; + + private CFGLookupParams(String node, GoblintLocation location) { + this.node = node; + this.location = location; + } + + public static CFGLookupParams byCFGNodeId(String cfgNodeId) { + return new CFGLookupParams(cfgNodeId, null); + } + + public static CFGLookupParams byLocation(GoblintLocation location) { + return new CFGLookupParams(null, location); + } + +} diff --git a/src/main/java/api/messages/params/EvalIntQueryParams.java b/src/main/java/api/messages/params/EvalIntQueryParams.java new file mode 100644 index 0000000..a95d142 --- /dev/null +++ b/src/main/java/api/messages/params/EvalIntQueryParams.java @@ -0,0 +1,17 @@ +package api.messages.params; + +/** + * @since 0.0.4 + */ + +public class EvalIntQueryParams { + + private String node; + private String exp; + + public EvalIntQueryParams(String node, String exp) { + this.node = node; + this.exp = exp; + } + +} diff --git a/src/main/java/api/messages/params/EvalQueryParams.java b/src/main/java/api/messages/params/EvalQueryParams.java new file mode 100644 index 0000000..f46c254 --- /dev/null +++ b/src/main/java/api/messages/params/EvalQueryParams.java @@ -0,0 +1,23 @@ +package api.messages.params; + +/** + * @since 0.0.4 + */ + +public class EvalQueryParams { + + private String node; + private String exp; + private Long vid; + + public EvalQueryParams(String node, String exp) { + this.node = node; + this.exp = exp; + } + + public EvalQueryParams(String node, Long vid) { + this.node = node; + this.vid = vid; + } + +} diff --git a/src/main/java/api/messages/params/GlobalStateParams.java b/src/main/java/api/messages/params/GlobalStateParams.java new file mode 100644 index 0000000..8e6e3bd --- /dev/null +++ b/src/main/java/api/messages/params/GlobalStateParams.java @@ -0,0 +1,29 @@ +package api.messages.params; + +/** + * @since 0.0.4 + */ + +public class GlobalStateParams { + + private Long vid; + private String node; + + private GlobalStateParams(Long vid, String node) { + this.vid = vid; + this.node = node; + } + + public static GlobalStateParams all() { + return new GlobalStateParams(null, null); + } + + public static GlobalStateParams byVid(Long vid) { + return new GlobalStateParams(vid, null); + } + + public static GlobalStateParams byCFGNodeId(String cfgNodeId) { + return new GlobalStateParams(null, cfgNodeId); + } + +} diff --git a/src/main/java/api/messages/params/LookupParams.java b/src/main/java/api/messages/params/LookupParams.java new file mode 100644 index 0000000..0d3d2c8 --- /dev/null +++ b/src/main/java/api/messages/params/LookupParams.java @@ -0,0 +1,37 @@ +package api.messages.params; + +import api.messages.GoblintLocation; + +/** + * @since 0.0.4 + */ + +public class LookupParams { + + private String node; + private String cfg_node; + private GoblintLocation location; + + private LookupParams(String node, String cfg_node, GoblintLocation location) { + this.node = node; + this.cfg_node = cfg_node; + this.location = location; + } + + public static LookupParams entryPoint() { + return new LookupParams(null, null, null); + } + + public static LookupParams byNodeId(String nodeId) { + return new LookupParams(nodeId, null, null); + } + + public static LookupParams byCFGNodeId(String cfgNodeId) { + return new LookupParams(null, cfgNodeId, null); + } + + public static LookupParams byLocation(GoblintLocation location) { + return new LookupParams(null, null, location); + } + +} diff --git a/src/main/java/api/messages/params/NodeParams.java b/src/main/java/api/messages/params/NodeParams.java new file mode 100644 index 0000000..e914071 --- /dev/null +++ b/src/main/java/api/messages/params/NodeParams.java @@ -0,0 +1,18 @@ +package api.messages.params; + +/** + * @since 0.0.4 + */ + +public class NodeParams { + + private String nid; + + public NodeParams() { + } + + public NodeParams(String nid) { + this.nid = nid; + } + +} diff --git a/src/main/java/api/messages/Params.java b/src/main/java/api/messages/params/Params.java similarity index 80% rename from src/main/java/api/messages/Params.java rename to src/main/java/api/messages/params/Params.java index ac270d5..62ccaf5 100644 --- a/src/main/java/api/messages/Params.java +++ b/src/main/java/api/messages/params/Params.java @@ -1,14 +1,14 @@ -package api.messages; - -public class Params { - - private String fname; - - public Params() { - } - - public Params(String fname) { - this.fname = fname; - } - -} +package api.messages.params; + +public class Params { + + private String fname; + + public Params() { + } + + public Params(String fname) { + this.fname = fname; + } + +} diff --git a/src/main/java/goblintserver/GoblintServer.java b/src/main/java/goblintserver/GoblintServer.java index c48f2e5..5d97703 100644 --- a/src/main/java/goblintserver/GoblintServer.java +++ b/src/main/java/goblintserver/GoblintServer.java @@ -3,6 +3,7 @@ import gobpie.GobPieConfiguration; import gobpie.GobPieException; import magpiebridge.core.MagpieServer; +import org.apache.commons.lang3.ArrayUtils; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.eclipse.lsp4j.MessageParams; @@ -12,6 +13,7 @@ import org.zeroturnaround.exec.StartedProcess; import org.zeroturnaround.exec.listener.ProcessListener; +import java.io.ByteArrayOutputStream; import java.io.File; import java.io.IOException; import java.util.Arrays; @@ -61,17 +63,27 @@ public String getGoblintSocket() { /** * Method for constructing the command to run Goblint server. * Files to analyse must be defined in goblint conf. - * - * @throws GobPieException when running Goblint failed. */ private String[] constructGoblintRunCommand() { - return new String[]{ + String[] command = new String[]{ configuration.getGoblintExecutable(), "--enable", "server.enabled", "--enable", "server.reparse", "--set", "server.mode", "unix", "--set", "server.unix-socket", new File(getGoblintSocket()).getAbsolutePath() }; + if (configuration.enableAbstractDebugging()) { + command = ArrayUtils.addAll(command, "--enable", "exp.arg"); + } + return command; + } + + + private String[] constructGoblintVersionCheckCommand() { + return new String[]{ + configuration.getGoblintExecutable(), + "--version" + }; } @@ -91,6 +103,33 @@ public void startGoblintServer() { } + /** + * Checks Goblint command reported version. + * + * @throws GobPieException when running Goblint fails. + */ + public String checkGoblintVersion() { + File dirPath = new File(System.getProperty("user.dir")); + String[] command = constructGoblintVersionCheckCommand(); + + ByteArrayOutputStream output = new ByteArrayOutputStream(); + + try { + log.debug("Waiting for command: " + Arrays.toString(command) + " to run..."); + new ProcessExecutor() + .directory(dirPath) + .command(command) + .redirectOutput(output) + .redirectError(output) + .execute(); + } catch (IOException | InterruptedException | TimeoutException e) { + throw new GobPieException("Checking version failed.", e, GOBLINT_EXCEPTION); + } + + return output.toString(); + } + + /** * Method for running a command. * @@ -98,7 +137,7 @@ public void startGoblintServer() { * @param command The command to run. * @return An object that represents a process that has started. It may or may not have finished. */ - private StartedProcess runCommand(File dirPath, String[] command) throws IOException, InterruptedException, InvalidExitValueException, TimeoutException { + private StartedProcess runCommand(File dirPath, String[] command) throws IOException, InterruptedException, TimeoutException { ProcessListener listener = new ProcessListener() { public void afterStop(Process process) { diff --git a/src/main/java/gobpie/GobPieConfiguration.java b/src/main/java/gobpie/GobPieConfiguration.java index 248de28..e314ad2 100644 --- a/src/main/java/gobpie/GobPieConfiguration.java +++ b/src/main/java/gobpie/GobPieConfiguration.java @@ -13,12 +13,14 @@ public class GobPieConfiguration { private final String goblintExecutable; private String goblintConf; private String[] preAnalyzeCommand; + private final boolean abstractDebugging; private final boolean showCfg; private final boolean explodeGroupWarnings; private final boolean incrementalAnalysis; private GobPieConfiguration() { goblintExecutable = "goblint"; + abstractDebugging = false; showCfg = false; explodeGroupWarnings = true; incrementalAnalysis = true; @@ -37,6 +39,10 @@ public String[] getPreAnalyzeCommand() { return this.preAnalyzeCommand; } + public boolean enableAbstractDebugging() { + return abstractDebugging; + } + public boolean showCfg() { return this.showCfg; } diff --git a/vscode/installGobPie.sh b/vscode/installGobPie.sh index 395ea38..8a6b87a 100755 --- a/vscode/installGobPie.sh +++ b/vscode/installGobPie.sh @@ -1,4 +1,4 @@ mvn clean -f "../../GobPie/pom.xml" mvn install -f "../../GobPie/pom.xml" echo y | vsce package -code --install-extension gobpie-0.0.3.vsix \ No newline at end of file +code --install-extension gobpie-0.0.4.vsix \ No newline at end of file diff --git a/vscode/install_and_test.sh b/vscode/install_and_test.sh index 2368749..cf9925a 100644 --- a/vscode/install_and_test.sh +++ b/vscode/install_and_test.sh @@ -1,5 +1,5 @@ # Load environment variables from .env export $(grep -v '^#' .env | xargs) -code --install-extension gobpie-0.0.3.vsix +code --install-extension gobpie-0.0.4.vsix code $GOBPIE_TEST_PROJECT diff --git a/vscode/package.json b/vscode/package.json index b9a3aab..f90c53d 100644 --- a/vscode/package.json +++ b/vscode/package.json @@ -4,7 +4,7 @@ "description": "The interactive Goblint analyzer extension", "author": "Karoliine Holter", "license": "MIT", - "version": "0.0.3", + "version": "0.0.4", "repository": { "type": "git", "url": "https://github.com/goblint/GobPie.git" @@ -18,7 +18,9 @@ "vscode": "^1.30.0" }, "activationEvents": [ - "onLanguage:c" + "onLanguage:c", + "onDebugResolve:c_adb", + "onDebugDynamicConfigurations:c_adb" ], "main": "./dist/extension", "contributes": { @@ -52,10 +54,47 @@ ".i" ] } + ], + "breakpoints": [ + { + "language": "c" + } + ], + "debuggers": [ + { + "type": "c_adb", + "languages": [ + "c" + ], + "label": "C (GobPie Abstract Debugger)", + "configurationAttributes": { + "launch": { + "properties": {} + } + }, + "initialConfigurations": [ + { + "type": "c_adb", + "request": "launch", + "name": "C (GobPie Abstract Debugger)" + } + ], + "configurationSnippets": [ + { + "label": "C (GobPie Abstract Debugger)", + "description": "Debug C using Gobpie Abstract Debugger", + "body": { + "type": "c_adb", + "request": "launch", + "name": "C (GobPie Abstract Debugger)" + } + } + ] + } ] }, "scripts": { - "vscode:prepublish": "shx cp ../target/gobpie-0.0.3-SNAPSHOT.jar gobpie-0.0.3-SNAPSHOT.jar && npm run package", + "vscode:prepublish": "shx cp ../target/gobpie-0.0.4-SNAPSHOT.jar gobpie-0.0.4-SNAPSHOT.jar && npm run package", "webpack": "webpack --mode development", "webpack-dev": "webpack --mode development --watch", "package": "webpack --mode production --devtool hidden-source-map", diff --git a/vscode/src/extension.ts b/vscode/src/extension.ts index 046f632..5765e2e 100644 --- a/vscode/src/extension.ts +++ b/vscode/src/extension.ts @@ -1,6 +1,14 @@ 'use strict'; import * as vscode from 'vscode'; -import {ExtensionContext, ViewColumn, window, workspace} from 'vscode'; +import { + CancellationToken, + DebugConfiguration, + ExtensionContext, Uri, + ViewColumn, + window, + workspace, + WorkspaceFolder +} from 'vscode'; import { ClientCapabilities, DocumentSelector, @@ -14,13 +22,17 @@ import { ServerOptions } from 'vscode-languageclient'; import {XMLHttpRequest} from 'xmlhttprequest-ts'; +import * as crypto from "crypto"; +import * as os from "os"; // Track currently webview panel let panel: vscode.WebviewPanel | undefined = undefined; export function activate(context: ExtensionContext) { - let script = 'java'; - let args = ['-jar', context.asAbsolutePath('gobpie-0.0.3-SNAPSHOT.jar')]; + const adbSocketPath = `${os.tmpdir()}/gobpie_adb_${crypto.randomBytes(6).toString('base64url')}.sock` + + const script = 'java'; + const args = ['-jar', context.asAbsolutePath('gobpie-0.0.4-SNAPSHOT.jar'), adbSocketPath]; // Use this for communicating on stdio let serverOptions: ServerOptions = { @@ -57,6 +69,10 @@ export function activate(context: ExtensionContext) { let lc: LanguageClient = new LanguageClient('GobPie', 'GobPie', serverOptions, clientOptions); lc.registerFeature(new MagpieBridgeSupport(lc)); lc.start(); + + context.subscriptions.push(vscode.debug.registerDebugAdapterDescriptorFactory('c_adb', new AbstractDebuggingAdapterDescriptorFactory(adbSocketPath))); + context.subscriptions.push(vscode.debug.registerDebugConfigurationProvider('c_adb', new AbstractDebuggingConfigurationResolver())); + context.subscriptions.push(vscode.debug.registerDebugConfigurationProvider('c_adb', new AbstractDebuggingConfigurationProvider(), vscode.DebugConfigurationProviderTriggerKind.Dynamic)); } @@ -81,7 +97,7 @@ export class MagpieBridgeSupport implements DynamicFeature { createWebView(content: string) { const columnToShowIn = ViewColumn.Beside; - + if (panel) { // If we already have a panel, show it in the target column panel.reveal(columnToShowIn); @@ -128,3 +144,48 @@ export class MagpieBridgeSupport implements DynamicFeature { } +class AbstractDebuggingAdapterDescriptorFactory implements vscode.DebugAdapterDescriptorFactory { + + constructor(private adbSocketPath: string) { + } + + async createDebugAdapterDescriptor(session: vscode.DebugSession, executable: vscode.DebugAdapterExecutable | undefined): Promise { + // TODO: Make sure that GobPie is actually guaranteed to run and create a socket in the workspace folder (in particular multiple workspaces might violate this assumption) + try { + await vscode.workspace.fs.stat(Uri.file(this.adbSocketPath)); + } catch (e) { + if (e.code == 'FileNotFound' || e.code == 'ENOENT') { + throw 'GobPie Abstract Debugger is not running. Ensure abstract debugging is enabled in gobpie.json and open a C file to start GobPie.' + } else { + throw e; + } + } + return new vscode.DebugAdapterNamedPipeServer(this.adbSocketPath); + } + +} + +class AbstractDebuggingConfigurationProvider implements vscode.DebugConfigurationProvider { + + provideDebugConfigurations(folder: WorkspaceFolder | undefined, token?: CancellationToken): DebugConfiguration[] { + return [{ + type: "c_adb", + request: "launch", + name: "C (GobPie Abstract Debugger)" + }]; + } + +} + +class AbstractDebuggingConfigurationResolver implements vscode.DebugConfigurationProvider { + + resolveDebugConfiguration(folder: WorkspaceFolder | undefined, debugConfiguration: DebugConfiguration, token?: CancellationToken): DebugConfiguration { + return { + type: "c_adb", + request: "launch", + name: "C (GobPie Abstract Debugger)", + ...debugConfiguration + }; + } + +}