tracking down some uncaught exceptions when interrupting Isabelle sol…

…vers manually
KeYProject · Sep 4, 2024 · c30fbc5 · c30fbc5
1 parent 861a3cd
commit c30fbc5
Show file tree

Hide file tree

Showing 6 changed files with 47 additions and 23 deletions.
diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncher.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleLauncher.java
@@ -109,5 +109,10 @@ public void addListener(IsabelleLauncherListener listener) {
     public void stopAll(IsabelleSolver.ReasonOfInterruption reasonOfInterruption) {
         shutdown();
         runningSolvers.forEach((solver) -> solver.interrupt(reasonOfInterruption));
+        solverQueue.forEach((solver) -> solver.interrupt(reasonOfInterruption));
+
+        runningSolvers.clear();
+        solverQueue.clear();
+        listener.launcherStopped(this, solverSet);
     }
 }
diff --git a/...slation/IsabelleLauncherListenerImpl.java → ...abelleLauncherProgressDialogMediator.java b/...slation/IsabelleLauncherListenerImpl.java → ...abelleLauncherProgressDialogMediator.java
@@ -12,7 +12,7 @@
 import java.util.Collection;
 import java.util.TimerTask;
 
-public class IsabelleLauncherListenerImpl implements IsabelleLauncherListener {
+public class IsabelleLauncherProgressDialogMediator implements IsabelleLauncherListener {
     private final Timer timer = new Timer();
     private int finishedCounter = 0;
 
@@ -127,25 +127,23 @@ private void unknownStopped(int x, int y) {
 
     private void setProgressText(int value) {
         JProgressBar bar = progressDialog.getProgressBar();
-        if (bar.getMaximum() == 1) {
             if (value == -1) {
                 bar.setString("Preparing...");
                 bar.setStringPainted(true);
-                return;
+            } else if (value == bar.getMaximum()){
+                bar.setString("Finished.");
+                bar.setStringPainted(true);
+            } else {
+                bar.setString("Processed " + value + " of " + bar.getMaximum() + " problems.");
+                bar.setStringPainted(true);
             }
-            bar.setString(value == 0 ? "Processing..." : "Finished.");
-            bar.setStringPainted(true);
-        } else {
-            bar.setString("Processed " + value + " of " + bar.getMaximum() + " problems.");
-            bar.setStringPainted(true);
-        }
     }
 
     protected void discardEvent(IsabelleLauncher launcher) {
 
     }
 
-    public IsabelleLauncherListenerImpl(IsabelleTranslationSettings settings) {
+    public IsabelleLauncherProgressDialogMediator(IsabelleTranslationSettings settings) {
 
     }
 

diff --git a/...isabelletranslation/src/main/java/key/isabelletranslation/IsabelleResourceController.java b/...isabelletranslation/src/main/java/key/isabelletranslation/IsabelleResourceController.java
@@ -49,13 +49,18 @@ public IsabelleResourceController(int numberOfInstances) {
 
     public void init() throws IOException {
         for (int i = 0; i < numberOfInstances; i++) {
-            idleInstances.add(createIsabelleResource());
+            IsabelleResource newResource = createIsabelleResource();
+            if (!isShutdown() && newResource != null) {
+                idleInstances.add(newResource);
+            }
         }
     }
 
     public IsabelleResource getIsabelleResource(IsabelleSolver requestingSolver) throws InterruptedException {
         waitingSolvers.add(requestingSolver);
-        return idleInstances.take();
+        IsabelleResource freeResource = idleInstances.take();
+        waitingSolvers.remove(requestingSolver);
+        return freeResource;
     }
 
     public void shutdownGracefully() {
@@ -73,6 +78,14 @@ public void shutdownGracefully() {
     public void returnResource(IsabelleSolver returningSolver, IsabelleResource resource) {
         assert resource != null;
 
+        if (isShutdown()) {
+            if (!resource.isDestroyed()) {
+                //TODO some kind of race condition happens here
+                resource.destroy();
+            }
+            return;
+        }
+
         if (resource.isDestroyed()) {
             try {
                 resource = createIsabelleResource();
@@ -81,12 +94,16 @@ public void returnResource(IsabelleSolver returningSolver, IsabelleResource reso
                 shutdownGracefully();
                 LOGGER.error(e.getMessage());
             }
+        } else {
+            resource.interrupt();
         }
-        resource.interrupt();
-        waitingSolvers.remove(returningSolver);
         idleInstances.offer(resource);
     }
 
+    public boolean isShutdown() {
+        return isShutdown;
+    }
+
     private IsabelleResource createIsabelleResource() throws IOException {
         Callable<IsabelleResource> creationTask = () -> {
             Isabelle isabelleInstance = startIsabelleInstance();
@@ -96,11 +113,15 @@ private IsabelleResource createIsabelleResource() throws IOException {
         try {
             return instanceCreatorService.submit(creationTask).get();
         } catch (InterruptedException e) {
+            shutdownGracefully();
             throw new RuntimeException(e);
         } catch (ExecutionException e) {
             if (e.getCause() instanceof IOException) {
                 throw (IOException) e.getCause();
             }
+            if (isShutdown()) {
+                return null;
+            }
             LOGGER.error("Error during Isabelle setup");
             throw new RuntimeException(e);
         } catch (RejectedExecutionException e) {
@@ -150,7 +171,7 @@ public boolean isDestroyed() {
             return instance.isDestroyed();
         }
 
-        public void destroy() {
+        void destroy() {
             instance.destroy();
         }
 

diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleSolverInstance.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/IsabelleSolverInstance.java
@@ -129,13 +129,13 @@ public void interrupt(ReasonOfInterruption reason) {
             thread.interrupt();
         }
         if (isabelleResource != null) {
-            shutdownAndReturnResource();
+            returnResource();
         }
     }
 
-    private void shutdownAndReturnResource() {
-        isabelleResource.interrupt();
+    private void returnResource() {
         resourceController.returnResource(this, isabelleResource);
+        isabelleResource = null;
     }
 
     private void setSolverState(SolverState solverState) {
@@ -316,7 +316,9 @@ fun go_run (state, thy) =
             this.result = result;
             notifyProcessTimeout();
         } catch (InterruptedException exception) {
-            interrupt(ReasonOfInterruption.Exception);
+            if (reasonOfInterruption == ReasonOfInterruption.NoInterruption) {
+                interrupt(ReasonOfInterruption.Exception);
+            }
             result = new SledgehammerResult(Option.apply(null));
             this.result = result;
             notifySledgehammerError(exception);

diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslateAllAction.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslateAllAction.java
@@ -59,7 +59,7 @@ private void generateTranslation() {
                 throw new RuntimeException(e);
             }
 
-            launcher.addListener(new IsabelleLauncherListenerImpl(settings));
+            launcher.addListener(new IsabelleLauncherProgressDialogMediator(settings));
             try {
                 launcher.try0ThenSledgehammerAllPooled(translations, 30, 1);
             } catch (IOException e) {

diff --git a/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslationAction.java b/keyext.isabelletranslation/src/main/java/key/isabelletranslation/TranslationAction.java
@@ -3,8 +3,6 @@
 import de.uka.ilkd.key.core.KeYMediator;
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.gui.actions.MainWindowAction;
-import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import de.uka.ilkd.key.smt.SMTRuleApp;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -58,7 +56,7 @@ private void generateTranslation() {
                     throw new RuntimeException(e);
                 }
 
-                launcher.addListener(new IsabelleLauncherListenerImpl(settings));
+                launcher.addListener(new IsabelleLauncherProgressDialogMediator(settings));
                 try {
                     launcher.try0ThenSledgehammerAllPooled(list, 30, 1);
                 } catch (IOException e) {