Improve solver exceptions for BoundedChecker

build.gradle.kts

@@ -47,7 +47,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.28.1"
+    version = "6.28.2"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/impl/NullSolver.java

@@ -18,65 +18,121 @@
 import hu.bme.mit.theta.core.model.Valuation;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
-import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.SolverStatus;
+import hu.bme.mit.theta.solver.*;
+
 import java.util.Collection;
+import java.util.List;
 
-public final class NullSolver implements Solver {
+public final class NullSolver implements Solver, ItpSolver, UCSolver {
 
-    private NullSolver() {}
+    private final RuntimeException exception;
 
-    private static class LazyHolder {
+    private NullSolver(final RuntimeException exception) {
+        this.exception = exception;
+    }
 
-        static final NullSolver INSTANCE = new NullSolver();
+    private static class LazyHolder {
+        static final NullSolver INSTANCE =
+            new NullSolver(new UnsupportedOperationException());
     }
 
     public static NullSolver getInstance() {
         return LazyHolder.INSTANCE;
     }
 
+    public static NullSolver withException(final Throwable t) {
+        final RuntimeException ex =
+            (t instanceof RuntimeException)
+                ? (RuntimeException) t
+                : new RuntimeException(t);
+        return new NullSolver(ex);
+    }
+
+    private RuntimeException ex() {
+        return exception;
+    }
+
+    private <T> T fail() {
+        throw ex();
+    }
+
     @Override
     public void add(final Expr<BoolType> assertion) {
-        throw new UnsupportedOperationException();
+        throw ex();
     }
 
     @Override
     public SolverStatus check() {
-        throw new UnsupportedOperationException();
+        return fail();
     }
 
     @Override
     public void push() {
-        throw new UnsupportedOperationException();
+        throw ex();
     }
 
     @Override
     public void pop(final int n) {
-        throw new UnsupportedOperationException();
+        throw ex();
     }
 
     @Override
     public void reset() {
-        throw new UnsupportedOperationException();
+        throw ex();
     }
 
     @Override
     public SolverStatus getStatus() {
-        throw new UnsupportedOperationException();
+        return fail();
     }
 
     @Override
     public Valuation getModel() {
-        throw new UnsupportedOperationException();
+        return fail();
     }
 
     @Override
     public Collection<Expr<BoolType>> getAssertions() {
-        throw new UnsupportedOperationException();
+        return fail();
     }
 
     @Override
     public void close() throws Exception {
-        throw new UnsupportedOperationException();
+        throw ex();
+    }
+
+    @Override
+    public ItpPattern createTreePattern(ItpMarkerTree<? extends ItpMarker> root) {
+        return fail();
+    }
+
+    @Override
+    public ItpMarker createMarker() {
+        return fail();
+    }
+
+    @Override
+    public void add(ItpMarker marker, Expr<BoolType> assertion) {
+        throw ex();
+    }
+
+    @Override
+    public Interpolant getInterpolant(ItpPattern pattern) {
+        return fail();
+    }
+
+    @Override
+    public Collection<? extends ItpMarker> getMarkers() {
+        return fail();
+    }
+
+    @Override
+    public void track(Expr<BoolType> assertion) {
+        throw ex();
+    }
+
+    @Override
+    public Collection<Expr<BoolType>> getUnsatCore() {
+        return fail();
     }
-}
+}

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt

@@ -31,7 +31,19 @@ import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.analysis.unit.UnitPrec
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.frontend.ParseContext
+import hu.bme.mit.theta.core.model.Valuation
+import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.booltype.BoolType
+import hu.bme.mit.theta.solver.Interpolant
+import hu.bme.mit.theta.solver.ItpMarker
+import hu.bme.mit.theta.solver.ItpMarkerTree
+import hu.bme.mit.theta.solver.ItpPattern
+import hu.bme.mit.theta.solver.ItpSolver
+import hu.bme.mit.theta.solver.Solver
 import hu.bme.mit.theta.solver.SolverFactory
+import hu.bme.mit.theta.solver.SolverStatus
+import hu.bme.mit.theta.solver.UCSolver
+import hu.bme.mit.theta.solver.impl.NullSolver
 import hu.bme.mit.theta.xcfa.ErrorDetection
 import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
@@ -56,16 +68,16 @@ fun getBoundedChecker(
       monolithicExpr = monolithicExpr,
       bmcSolver =
         tryGetSolver(boundedConfig.bmcConfig.bmcSolver, boundedConfig.bmcConfig.validateBMCSolver)
-          ?.createSolver(),
+          .createSolver(),
       bmcEnabled = { !boundedConfig.bmcConfig.disable },
       lfPathOnly = { !boundedConfig.bmcConfig.nonLfPath },
       itpSolver =
         tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver)
-          ?.createItpSolver(),
+          .createItpSolver(),
       imcEnabled = { !boundedConfig.itpConfig.disable },
       indSolver =
         tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver)
-          ?.createSolver(),
+          .createSolver(),
       kindEnabled = { !boundedConfig.indConfig.disable },
       logger = logger,
       needProof = true,
@@ -103,7 +115,7 @@ internal fun getPipelineChecker(
   if (cegar) {
     passes.add(
       PredicateAbstractionMEPass(
-        createFwBinItpCheckerFactory(tryGetSolver(cegarSolver, cegarSolverValidate)!!)
+        createFwBinItpCheckerFactory(tryGetSolver(cegarSolver, cegarSolverValidate))
       )
     )
   }
@@ -122,10 +134,16 @@ internal fun getPipelineChecker(
   )
 }
 
-private fun tryGetSolver(name: String, validate: Boolean): SolverFactory? {
+private fun tryGetSolver(name: String, validate: Boolean): SolverFactory {
   return try {
     getSolver(name, validate)
-  } catch (_: Throwable) {
-    null
+  } catch (e: Throwable) {
+    object : SolverFactory {
+      private val stub = NullSolver.withException(e)
+      override fun createSolver() = stub
+      override fun createUCSolver() = stub
+      override fun createItpSolver() = stub
+    }
   }
 }
+