Merge pull request #34 from goblint/analysis-abort

Use analysis abort in server mode
goblint · Jul 25, 2022 · 95adf7a · 95adf7a
2 parents 649681e + 861e47b
commit 95adf7a
Show file tree

Hide file tree

Showing 6 changed files with 97 additions and 56 deletions.
diff --git a/pom.xml b/pom.xml
@@ -28,6 +28,13 @@
             <version>1.12</version>
         </dependency>
 
+        <!-- zt-process-killer -->
+        <dependency>
+            <groupId>org.zeroturnaround</groupId>
+            <artifactId>zt-process-killer</artifactId>
+            <version>1.10</version>
+        </dependency>
+
         <!-- log4j -->
         <dependency>
             <groupId>org.apache.logging.log4j</groupId>

diff --git a/src/main/java/analysis/GoblintAnalysis.java b/src/main/java/analysis/GoblintAnalysis.java
@@ -1,35 +1,42 @@
 package analysis;
 
-import java.io.File;
-import java.io.FileFilter;
-import java.io.IOException;
-import java.net.MalformedURLException;
-import java.util.*;
-import java.util.concurrent.TimeoutException;
-
 import com.ibm.wala.classLoader.Module;
-
+import goblintclient.GoblintClient;
+import goblintclient.communication.AnalyzeResponse;
+import goblintclient.communication.MessagesResponse;
+import goblintclient.communication.Request;
+import goblintclient.messages.GoblintMessages;
+import goblintserver.GoblintServer;
+import gobpie.GobPieConfiguration;
+import gobpie.GobPieException;
+import gobpie.GobPieExceptionType;
 import magpiebridge.core.AnalysisConsumer;
-import magpiebridge.core.ServerAnalysis;
 import magpiebridge.core.MagpieServer;
-
+import magpiebridge.core.ServerAnalysis;
 import org.apache.commons.io.monitor.FileAlterationListenerAdaptor;
 import org.apache.commons.io.monitor.FileAlterationObserver;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
-
 import org.eclipse.lsp4j.MessageParams;
 import org.eclipse.lsp4j.MessageType;
-
 import org.zeroturnaround.exec.InvalidExitValueException;
 import org.zeroturnaround.exec.ProcessExecutor;
 import org.zeroturnaround.exec.ProcessResult;
+import org.zeroturnaround.process.UnixProcess;
 
-import goblintclient.*;
-import goblintclient.communication.*;
-import goblintclient.messages.*;
-import goblintserver.*;
-import gobpie.*;
+import java.io.File;
+import java.io.FileFilter;
+import java.io.IOException;
+import java.net.MalformedURLException;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.List;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+import java.util.concurrent.Future;
+import java.util.concurrent.TimeoutException;
+import java.util.concurrent.atomic.AtomicBoolean;
 
 
 public class GoblintAnalysis implements ServerAnalysis {
@@ -39,6 +46,10 @@ public class GoblintAnalysis implements ServerAnalysis {
     private final GoblintClient goblintClient;
     private final GobPieConfiguration gobpieConfiguration;
     private final FileAlterationObserver goblintConfObserver;
+    private final int SIGINT = 2;
+    private static Future<?> lastAnalysisTask;
+    private static final ExecutorService execService = Executors.newSingleThreadExecutor();
+    private final AtomicBoolean analysisRunning = new AtomicBoolean(false);
 
     private final Logger log = LogManager.getLogger(GoblintAnalysis.class);
 
@@ -73,18 +84,21 @@ public String source() {
 
     @Override
     public void analyze(Collection<? extends Module> files, AnalysisConsumer consumer, boolean rerun) {
-        if (rerun) {
-            if (consumer instanceof MagpieServer server) {
-
-                goblintConfObserver.checkAndNotify();
-                preAnalyse();
-
-                System.err.println("\n---------------------- Analysis started ----------------------");
-                Collection<GoblintAnalysisResult> response = reanalyse();
-                if (response != null) server.consume(new ArrayList<>(response), source());
-                System.err.println("--------------------- Analysis finished ----------------------\n");
-
+        if (consumer instanceof MagpieServer server) {
+            if (analysisRunning.get()) {
+                abortAnalysis();
             }
+            goblintConfObserver.checkAndNotify();
+            preAnalyse();
+            log.info("---------------------- Analysis started ----------------------");
+            Runnable analysisTask = () -> {
+                Collection<GoblintAnalysisResult> response = reanalyse();
+                if (response != null) {
+                    server.consume(new ArrayList<>(response), source());
+                    log.info("--------------------- Analysis finished ----------------------");
+                }
+            };
+            lastAnalysisTask = execService.submit(analysisTask);
         }
     }
 
@@ -111,10 +125,26 @@ private void preAnalyse() {
     }
 
 
+    private void abortAnalysis() {
+        if (lastAnalysisTask != null && !lastAnalysisTask.isDone()) {
+            Process goblintProcess = goblintServer.getGoblintRunProcess().getProcess();
+            int pid = Math.toIntExact(goblintProcess.pid());
+            UnixProcess unixProcess = new UnixProcess(pid);
+            try {
+                unixProcess.kill(SIGINT);
+                log.info("--------------- This analysis has been aborted -------------");
+            } catch (IOException e) {
+                log.error("Aborting analysis failed.");
+            }
+        }
+
+    }
+
+
     /**
      * Sends the request to Goblint server to reanalyse and reads the result.
      *
-     * @return returns true if the request was sucessful, false otherwise
+     * @return returns a collection of analysis results if the request was sucessful, null otherwise
      */
 
     private Collection<GoblintAnalysisResult> reanalyse() {
@@ -123,18 +153,21 @@ private Collection<GoblintAnalysisResult> reanalyse() {
         Request messagesRequest = new Request("messages");
 
         try {
+            analysisRunning.set(true);
             goblintClient.writeRequestToSocket(analyzeRequest);
             AnalyzeResponse analyzeResponse = goblintClient.readAnalyzeResponseFromSocket();
+            analysisRunning.set(false);
             if (!analyzeRequest.getId().equals(analyzeResponse.getId()))
                 throw new GobPieException("Response ID does not match request ID.", GobPieExceptionType.GOBLINT_EXCEPTION);
+            if (analyzeResponse.getResult().getStatus().contains("Aborted"))
+                return null;
             goblintClient.writeRequestToSocket(messagesRequest);
             MessagesResponse messagesResponse = goblintClient.readMessagesResponseFromSocket();
             if (!messagesRequest.getId().equals(messagesResponse.getId()))
                 throw new GobPieException("Response ID does not match request ID.", GobPieExceptionType.GOBLINT_EXCEPTION);
             return convertResultsFromJson(messagesResponse);
         } catch (IOException e) {
-            log.info("Sending the request to or receiving result from the server failed: " + e);
-            return null;
+            throw new GobPieException("Sending the request to or receiving result from the server failed.", e, GobPieExceptionType.GOBLINT_EXCEPTION);
         }
     }
 

diff --git a/src/main/java/goblintclient/GoblintClient.java b/src/main/java/goblintclient/GoblintClient.java
@@ -80,7 +80,7 @@ public void connectGoblintClient() {
     public void writeRequestToSocket(Request request) throws IOException {
         String requestString = new GsonBuilder().create().toJson(request) + "\n";
         outputStream.write(requestString.getBytes());
-        log.info("Request " + request.getId() + " written to socket.");
+        log.info("Request (" + request.getMethod() + ") " + request.getId() + " written to socket.");
     }
 
 
@@ -93,7 +93,7 @@ public void writeRequestToSocket(Request request) throws IOException {
     public AnalyzeResponse readAnalyzeResponseFromSocket() throws IOException {
         String response = inputReader.readLine();
         AnalyzeResponse analyzeResponse = new Gson().fromJson(response, AnalyzeResponse.class);
-        log.info("Response " + analyzeResponse.getId() + " read from socket.");
+        log.info("Response (analyze) " + analyzeResponse.getId() + " read from socket.");
         return analyzeResponse;
     }
 
@@ -111,7 +111,7 @@ public MessagesResponse readMessagesResponseFromSocket() throws IOException {
         builder.registerTypeAdapter(GoblintMessages.tag.class, new GoblintTagInterfaceAdapter());
         Gson gson = builder.create();
         MessagesResponse messagesResponse = gson.fromJson(response, MessagesResponse.class);
-        log.info("Response " + messagesResponse.getId() + " read from socket.");
+        log.info("Response (messages) " + messagesResponse.getId() + " read from socket.");
         return messagesResponse;
     }
 

diff --git a/src/main/java/goblintclient/communication/AnalyzeResponse.java b/src/main/java/goblintclient/communication/AnalyzeResponse.java
@@ -18,7 +18,7 @@ public class AnalyzeResponse extends Response {
 
     private result result;
 
-    static class result {
+    public static class result {
         private final List<String> status = new ArrayList<>();
 
         public List<String> getStatus() {

diff --git a/src/main/java/goblintserver/GoblintServer.java b/src/main/java/goblintserver/GoblintServer.java
@@ -51,6 +51,10 @@ public String getGoblintConf() {
         return goblintConf;
     }
 
+    public StartedProcess getGoblintRunProcess() {
+        return goblintRunProcess;
+    }
+
 
     /**
      * Method for constructing the command to run Goblint server.
@@ -144,7 +148,7 @@ public void afterStop(Process process) {
                     log.info("Goblint server has been killed.");
                 } else {
                     magpieServer.forwardMessageToClient(new MessageParams(MessageType.Error, "Goblint server exited due to an error. Please check the output terminal of GobPie extension for more information."));
-                    log.error("Goblint server exited due to an error. Please fix the issue reported above and restart the extension.");
+                    log.error("Goblint server exited due to an error (code: " + process.exitValue() + "). Please fix the issue reported above and restart the extension.");
                 }
             }
         };

diff --git a/vscode/src/extension.ts b/vscode/src/extension.ts
@@ -1,23 +1,20 @@
 'use strict';
-import * as net from 'net';
-import * as path from 'path';
-
-import {  workspace, window, ExtensionContext } from 'vscode';
-import { LanguageClient, LanguageClientOptions, ServerOptions, StreamInfo } from 'vscode-languageclient';
+import {ExtensionContext, workspace} from 'vscode';
+import {LanguageClient, LanguageClientOptions, ServerOptions} from 'vscode-languageclient';
 
 export function activate(context: ExtensionContext) {
     let script = 'java';
-    let args = ['-jar',context.asAbsolutePath('gobpie-0.0.2-SNAPSHOT.jar')];
-    
-    // Use this for communicating on stdio 
+    let args = ['-jar', context.asAbsolutePath('gobpie-0.0.2-SNAPSHOT.jar')];
+
+    // Use this for communicating on stdio
     let serverOptions: ServerOptions = {
-        run : { command: script, args: args },
-        debug: { command: script, args: args} ,
+        run: {command: script, args: args},
+        debug: {command: script, args: args},
     };
-    
-   /**
-    *   Use this for debugging 
-    *   let serverOptions = () => {
+
+    /**
+     *   Use this for debugging
+     *   let serverOptions = () => {
 		const socket = net.connect({ port: 5007 })
 		const result: StreamInfo = {
 			writer: socket,
@@ -27,21 +24,21 @@ export function activate(context: ExtensionContext) {
 			socket.on("connect", () => resolve(result))
 			socket.on("error", _ =>
 				window.showErrorMessage(
-					"Failed to connect to TaintBench language server. Make sure that the language server is running " +
+					"Failed to connect to the language server. Make sure that the language server is running " +
 					"-or- configure the extension to connect via standard IO."))
 		})
     }*/
-    
+
     let clientOptions: LanguageClientOptions = {
-        documentSelector: [{ scheme: 'file', language: 'c' }],
+        documentSelector: [{scheme: 'file', language: 'c'}],
         synchronize: {
             configurationSection: 'c',
-            fileEvents: [ workspace.createFileSystemWatcher('**/*.c') ]
+            fileEvents: [workspace.createFileSystemWatcher('**/*.c')]
         }
     };
-    
+
     // Create the language client and start the client.
-    let lc : LanguageClient = new LanguageClient('GobPie','GobPie', serverOptions, clientOptions);
+    let lc: LanguageClient = new LanguageClient('GobPie', 'GobPie', serverOptions, clientOptions);
     lc.start();
 }