From 159e9fd76ec49bc57ed57dc139a81b2ae3083c91 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 7 Jun 2018 12:40:38 +0200 Subject: [PATCH] GUI: Handle StackOverflowErrors gracefully --- .../userinterface/GUIComputationThread.java | 33 +++++++++++++++---- .../model/computation/BuildModelThread.java | 2 +- .../computation/ComputeSteadyStateThread.java | 2 +- .../computation/ComputeTransientThread.java | 2 +- .../computation/ExportBuiltModelThread.java | 2 +- .../properties/GUIExperiment.java | 22 +++++++++++++ .../computation/ModelCheckThread.java | 5 +++ .../computation/SimulateModelCheckThread.java | 13 ++++++-- 8 files changed, 69 insertions(+), 12 deletions(-) diff --git a/prism/src/userinterface/GUIComputationThread.java b/prism/src/userinterface/GUIComputationThread.java index 4a5ecd57..535c9b81 100644 --- a/prism/src/userinterface/GUIComputationThread.java +++ b/prism/src/userinterface/GUIComputationThread.java @@ -26,6 +26,7 @@ package userinterface; +import common.StackTraceHelper; import prism.*; /** @@ -35,7 +36,10 @@ public class GUIComputationThread extends Thread { protected GUIPlugin plug; protected Prism prism; - + + /** Limit on number of lines for logging a stack trace */ + protected int STACK_TRACE_LIMIT = StackTraceHelper.DEFAULT_STACK_TRACE_LIMIT; + /** Creates a new instance of GUIComputationThread */ public GUIComputationThread(GUIPlugin plug) { @@ -50,16 +54,33 @@ public class GUIComputationThread extends Thread errorDialog(s); } - /** Report an error for an Exception (in log and popup dialog) */ - public void error(Exception e) - { + /** + * Report an error for an Exception/Error/Throwable (in log and popup dialog). + *
+ * In case of a serious error that is unlikely to be recovered from + * (i.e., an Error that is not a StackOverflowError), rethrow the error. + */ + public void error(Throwable e) { if (e instanceof jdd.JDD.CuddOutOfMemoryException) { error(e.getMessage()+".\nTry increasing the value of \"CUDD max. memory\" in the options and then restart PRISM"); } else if (e instanceof PrismException) { error(e.getMessage()); + } else if (e instanceof StackOverflowError) { + String hint = "\nTry increasing the value of the Java stack size (via the -javastack argument)"; + + // use message with stack trace for log + errorLog(e.toString() + "\n" + StackTraceHelper.asString(e, STACK_TRACE_LIMIT) + hint); + + // use short message, without stack trace, for dialog + errorDialog(e.toString() + hint); } else { error(e.toString()+"\nThis is an unexpected error, it might be a good idea to restart PRISM"); } + + // for a serious error, i.e., derived from Error, except stack overflow, rethrow the error + if (e instanceof Error && !(e instanceof StackOverflowError)) { + throw (Error)e; + } } /** Report an error (in log) */ @@ -68,8 +89,8 @@ public class GUIComputationThread extends Thread logln("\nError: " + s + "."); } - /** Report an Exception error (in log) */ - public void errorLog(Exception e) + /** Report an Exception/Throwable error (in log) */ + public void errorLog(Throwable e) { if (e instanceof PrismException || e instanceof jdd.JDD.CuddOutOfMemoryException) { logln("\nError: " + e.getMessage() + "."); diff --git a/prism/src/userinterface/model/computation/BuildModelThread.java b/prism/src/userinterface/model/computation/BuildModelThread.java index 6c1e4de6..e1ea8dfc 100644 --- a/prism/src/userinterface/model/computation/BuildModelThread.java +++ b/prism/src/userinterface/model/computation/BuildModelThread.java @@ -65,7 +65,7 @@ public class BuildModelThread extends GUIComputationThread // Do build try { prism.buildModel(); - } catch (Exception e) { + } catch (Throwable e) { error(e); SwingUtilities.invokeLater(new Runnable() { diff --git a/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java b/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java index 408e2202..793f30b7 100644 --- a/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java +++ b/prism/src/userinterface/model/computation/ComputeSteadyStateThread.java @@ -76,7 +76,7 @@ public class ComputeSteadyStateThread extends GUIComputationThread // Do Computation try { prism.doSteadyState(exportType, exportFile, null); - } catch (Exception e) { + } catch (Throwable e) { error(e); SwingUtilities.invokeLater(new Runnable() { diff --git a/prism/src/userinterface/model/computation/ComputeTransientThread.java b/prism/src/userinterface/model/computation/ComputeTransientThread.java index 1cfbe8f3..df67fa7a 100644 --- a/prism/src/userinterface/model/computation/ComputeTransientThread.java +++ b/prism/src/userinterface/model/computation/ComputeTransientThread.java @@ -78,7 +78,7 @@ public class ComputeTransientThread extends GUIComputationThread // Do Computation try { prism.doTransient(transientTime, exportType, exportFile, null); - } catch (Exception e) { + } catch (Throwable e) { error(e); SwingUtilities.invokeLater(new Runnable() { diff --git a/prism/src/userinterface/model/computation/ExportBuiltModelThread.java b/prism/src/userinterface/model/computation/ExportBuiltModelThread.java index a91a260a..6ddfa205 100644 --- a/prism/src/userinterface/model/computation/ExportBuiltModelThread.java +++ b/prism/src/userinterface/model/computation/ExportBuiltModelThread.java @@ -112,7 +112,7 @@ public class ExportBuiltModelThread extends GUIComputationThread } }); return; - } catch (Exception e2) { + } catch (Throwable e2) { error(e2); SwingUtilities.invokeAndWait(new Runnable() { diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index 4a78246d..126d90c0 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -35,6 +35,9 @@ import prism.*; import userinterface.*; import javax.swing.*; + +import common.StackTraceHelper; + import java.util.*; import userinterface.util.*; @@ -241,6 +244,13 @@ public class GUIExperiment setMultipleErrors(definedMFConstants, null, e); undefinedConstants.iterateModel(); continue; + } catch (StackOverflowError e) { + // in case of stack overflow, report it (in log only), + // store as PrismException in result, and go on to the next model + errorLog(e.toString() + "\n" + StackTraceHelper.asString(e, STACK_TRACE_LIMIT)); + setMultipleErrors(definedMFConstants, null, new PrismException("Stack overflow")); + undefinedConstants.iterateModel(); + continue; } // collect information for simulation if required @@ -295,6 +305,13 @@ public class GUIExperiment setMultipleErrors(definedMFConstants, null, e); undefinedConstants.iterateModel(); continue; + } catch (StackOverflowError e) { + // in case of stack overflow, report it (in log only), + // store as PrismException in result, and go on to the next model + errorLog(e.toString() + "\n" + StackTraceHelper.asString(e, STACK_TRACE_LIMIT)); + setMultipleErrors(definedMFConstants, null, new PrismException("Stack overflow")); + undefinedConstants.iterateModel(); + continue; } } else { // iterate through as many properties as necessary @@ -331,6 +348,11 @@ public class GUIExperiment // in case of error, report it (in log only), store exception as the result and proceed errorLog(e); res = new Result(e); + } catch (StackOverflowError e) { + // in case of stack overflow, report it (in log only), + // store as PrismException in result, and proceed + errorLog(e.toString() + "\n" + StackTraceHelper.asString(e, STACK_TRACE_LIMIT)); + res = new Result(new PrismException("Stack overflow")); } // store result of model checking SwingUtilities.invokeAndWait(new Runnable() diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index 047fc567..bf30a33c 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java @@ -107,6 +107,11 @@ public class ModelCheckThread extends GUIComputationThread } catch (Exception e) { result = new Result(e); error(e); + } catch (StackOverflowError e) { + // convert the StackOverflowError to a PrismException, as the result handling + // expects Exception instead of Error objects + result = new Result(new PrismException("Stack overflow")); + error(e); } ic.interrupt(); try { diff --git a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java index 078feda9..3a35e8c7 100644 --- a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java @@ -121,6 +121,11 @@ public class SimulateModelCheckThread extends GUIComputationThread // in the case of an error which affects all props, store/report it resultError = e; error(e); + } catch (StackOverflowError e) { + // in the case of an error which affects all props, store/report it + // convert to a PrismException for result + resultError = new PrismException("Stack overflow"); + error(e); } //after collecting the results stop all of the clock icons for (int i = 0; i < clkThreads.size(); i++) { @@ -164,9 +169,13 @@ public class SimulateModelCheckThread extends GUIComputationThread // do simulation result = prism.modelCheckSimulator(pf, pf.getProperty(i), definedPFConstants, initialState, maxPathLength, method); method.reset(); - } catch (PrismException e) { + } catch (Exception e) { result = new Result(e); - error(e.getMessage()); + error(e); + } catch (StackOverflowError e) { + // store as PrismException in result + result = new Result(new PrismException("Stack overflow")); + error(e); } ict.interrupt(); while (!ict.canContinue) {