Added better logging for failures

ftsrg · Nov 12, 2023 · 872236b · 872236b
1 parent 4585748
commit 872236b
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 11 deletions.
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExitCodes.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExitCodes.kt
@@ -45,36 +45,41 @@ private fun exitProcess(debug: Boolean, e: Throwable, code: Int): Nothing {
     } else exitProcess(code)
 }
 
+private fun Throwable.printCauseAndTrace(stacktrace: Boolean) {
+    if (stacktrace) printStackTrace()
+    val location = stackTrace.first { it.className.startsWith("hu.bme.mit.theta") }.toString()
+    System.err.println("Process failed! ($location, $this)")
+}
 
 fun <T> exitOnError(stacktrace: Boolean, debug: Boolean, body: () -> T): T {
     try {
         return body()
     } catch (e: SmtLibSolverException) {
-        if (stacktrace) e.printStackTrace();
+        e.printCauseAndTrace(stacktrace)
         exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code)
     } catch (e: SolverValidationException) {
-        if (stacktrace) e.printStackTrace();
+        e.printCauseAndTrace(stacktrace)
         exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code);
     } catch (e: Z3Exception) {
-        if (stacktrace) e.printStackTrace();
+        e.printCauseAndTrace(stacktrace)
         exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code);
     } catch (e: ClassCastException) {
-        if (stacktrace) e.printStackTrace();
+        e.printCauseAndTrace(stacktrace)
         if (e.message?.contains("com.microsoft.z3") == true)
             exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code);
         else
             exitProcess(debug, e, ExitCodes.GENERIC_ERROR.code);
     } catch (e: NotSolvableException) {
-        if (stacktrace) e.printStackTrace();
+        e.printCauseAndTrace(stacktrace)
         exitProcess(debug, e, ExitCodes.VERIFICATION_STUCK.code);
     } catch (e: OutOfMemoryError) {
-        if (stacktrace) e.printStackTrace();
+        e.printCauseAndTrace(stacktrace)
         exitProcess(debug, e, ExitCodes.OUT_OF_MEMORY.code);
     } catch (e: RuntimeException) {
-        if (stacktrace) e.printStackTrace();
+        e.printCauseAndTrace(stacktrace)
         exitProcess(debug, e, ExitCodes.SERVER_ERROR.code);
     } catch (e: Exception) {
-        if (stacktrace) e.printStackTrace();
+        e.printCauseAndTrace(stacktrace)
         exitProcess(debug, e, ExitCodes.GENERIC_ERROR.code);
     }
 }
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
@@ -294,8 +294,8 @@ class XcfaCli(private val args: Array<String>) {
                 "Loaded script engine (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
             stopwatch.reset().start()
 
-            kotlinEngine.context.setBindings(bindings,
-                100) // 100 seems to be a safe default, based on AbstractScriptEngine
+            // 100 seems to be a safe default, based on AbstractScriptEngine
+            kotlinEngine.context.setBindings(bindings, 100)
             val compiled = kotlinEngine.compile(FileReader(portfolioDescriptor))
             logger.write(Logger.Level.INFO, "Compiled portfolio (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n")
 
@@ -405,7 +405,8 @@ class XcfaCli(private val args: Array<String>) {
             }
         } catch (e: Exception) {
             if (stacktrace) e.printStackTrace()
-            logger.write(Logger.Level.RESULT, "Frontend failed!\n")
+            val location = e.stackTrace.filter { it.className.startsWith("hu.bme.mit.theta") }.first().toString()
+            logger.write(Logger.Level.RESULT, "Frontend failed! ($location, $e)\n")
             exitProcess(ExitCodes.FRONTEND_FAILED.code)
         }