Add exceptions support

usvm-core/src/main/kotlin/org/usvm/TypeSystem.kt

@@ -16,4 +16,6 @@ interface UTypeSystem<Type> {
      * Returns true if there is no type u distinct from [t] and subtyping [t].
      */
     fun isFinal(t: Type): Boolean
+    fun isInstantiable(t: Type): Boolean
+    fun findSubtypes(t: Type): Sequence<Type>
 }

usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt

@@ -75,7 +75,8 @@ class JcTestResolver(
         val result = when (val res = state.methodResult) {
             is JcMethodResult.NoCall -> error("No result found")
             is JcMethodResult.Success -> with(afterMemory) { Result.success(resolveExpr(res.value, method.returnType)) }
-            is JcMethodResult.Exception -> Result.failure(resolveException(res.exception))
+            is JcMethodResult.UnprocessedException -> error("An unprocessed exception should never occur in the Resolver")
+            is JcMethodResult.Exception -> Result.failure(resolveException(res.exception, afterMemory))
         }
         val coverage = resolveCoverage(method, state)
 
@@ -88,9 +89,14 @@ class JcTestResolver(
         )
     }
 
-    private fun resolveException(exception: Exception): Throwable =
+    private fun resolveException(exception: Exception, afterMemory: MemoryScope): Throwable =
         when (exception) {
-            is WrappedException -> Reflection.allocateInstance(classLoader.loadClass(exception.name)) as Throwable
+            is WrappedException -> {
+                val address = exception.address
+                with(afterMemory) {
+                    resolveExpr(address, exception.type) as Throwable
+                }
+            }
             else -> exception
         }
 
@@ -217,6 +223,11 @@ class JcTestResolver(
             val instance = Reflection.allocateInstance(jClass)
             resolvedCache[idx] = instance
 
+            // TODO skips throwable construction for now
+            if (instance is Throwable) {
+                return instance
+            }
+
             val fields = type.jcClass.toType().declaredFields // TODO: now it skips inherited fields
             for (field in fields) {
                 val ref = UFieldLValue(ctx.typeToSort(field.fieldType), heapRef, field.field)

usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt

@@ -92,8 +92,8 @@ import org.usvm.machine.operator.mkNarrow
 import org.usvm.machine.operator.wideTo32BitsIfNeeded
 import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.addNewMethodCall
+import org.usvm.machine.state.createUnprocessedException
 import org.usvm.machine.state.lastStmt
-import org.usvm.machine.state.throwException
 
 /**
  * An expression resolver based on JacoDb 3-address code. A result of resolving is `null`, iff
@@ -451,7 +451,7 @@ class JcExprResolver(
             inside,
             blockOnFalseState = {
                 val exception = ArrayIndexOutOfBoundsException((models.first().eval(idx) as KBitVec32Value).intValue)
-                throwException(exception)
+                createUnprocessedException(exception)
             }
         )
     }
@@ -465,7 +465,7 @@ class JcExprResolver(
             blockOnFalseState = {
                 val ln = lastStmt.lineNumber
                 val exception = NegativeArraySizeException("[negative array size] $ln")
-                throwException(exception)
+                createUnprocessedException(exception)
             }
         )
     }
@@ -481,7 +481,7 @@ class JcExprResolver(
             blockOnFalseState = {
                 val ln = lastStmt.lineNumber
                 val exception = ArithmeticException("[division by zero] $ln")
-                throwException(exception)
+                createUnprocessedException(exception)
             }
         )
     }
@@ -493,7 +493,7 @@ class JcExprResolver(
             blockOnFalseState = {
                 val ln = lastStmt.lineNumber
                 val exception = NullPointerException("[null pointer dereference] $ln")
-                throwException(exception)
+                createUnprocessedException(exception)
             }
         )
     }

usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt

@@ -25,6 +25,7 @@ import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.WrappedException
 import org.usvm.machine.state.addEntryMethodCall
+import org.usvm.machine.state.createUnprocessedException
 import org.usvm.machine.state.lastStmt
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.returnValue
@@ -88,13 +89,71 @@ class JcInterpreter(
         return scope.stepResult()
     }
 
+    // TODO this section doesn't work as it should considering symbolic exceptions.
     private fun handleException(
         scope: JcStepScope,
         exception: Exception,
         lastStmt: JcInst,
     ) {
-        applicationGraph.successors(lastStmt) // TODO: check catchers for lastStmt
-        scope.calcOnState { throwException(exception) }
+        // TODO process WrapperExceptions here with their symbolic types
+        val exceptionTypeName = if (exception is WrappedException) {
+            exception.type.typeName
+        } else {
+            exception::class.java.name
+        }
+
+        // TODO replace it with type streams when they are ready
+        fun findAllSubtypes(type: JcType): List<JcType> {
+            val queue = mutableListOf(type)
+            val processedSubtypes = mutableSetOf<JcType>()
+            val result = mutableSetOf<JcType>()
+
+            while (queue.isNotEmpty()) {
+                val processingType = queue.removeLast()
+                result += processingType
+                processedSubtypes += processingType
+                ctx.typeSystem<JcType>().findSubtypes(processingType).forEach {
+                    if (it !in processedSubtypes) {
+                        queue += it
+                    }
+                }
+            }
+
+            return result.toList()
+        }
+
+        // TODO that's not true, we have to process a situation when a symbolic exception
+        //      can be handled in several catch sections
+        val catchInst = applicationGraph.successors(lastStmt)
+            .filterIsInstance<JcCatchInst>()
+            .firstOrNull { catchInst ->
+                val possibleTypesNames = catchInst
+                    .throwableTypes
+                    .flatMapTo(mutableSetOf()) { findAllSubtypes(it) }
+                    .map { it.typeName } // TODO use smth more efficient than strings for comparison
+
+                // TODO should be replaced with symbolic types intersection in the future
+                exceptionTypeName in possibleTypesNames
+            }
+
+        if (catchInst == null) {
+            scope.calcOnState { throwException(exception) }
+            return
+        }
+
+        scope.doWithState {
+            val lValue = exprResolverWithScope(scope).resolveLValue(catchInst.throwable) ?: return@doWithState
+            val exceptionResult = methodResult as JcMethodResult.Exception
+
+            // TODO shouldn't we process implicit exceptions here as well?
+            //      For now, it's impossible since they don't have addresses.
+            if (exceptionResult.exception is WrappedException) {
+                memory.write(lValue, (exceptionResult.exception).address)
+            }
+
+            methodResult = JcMethodResult.NoCall
+            newStmt(catchInst.nextStmt)
+        }
     }
 
     private fun visitAssignInst(scope: JcStepScope, stmt: JcAssignInst) {
@@ -157,8 +216,11 @@ class JcInterpreter(
     }
 
     private fun visitThrowStmt(scope: JcStepScope, stmt: JcThrowInst) {
+        val resolver = exprResolverWithScope(scope)
+        val address = resolver.resolveJcExpr(stmt.throwable)?.asExpr(ctx.addressSort) ?: return
+
         scope.calcOnState {
-            throwException(WrappedException(stmt.throwable.type.typeName))
+            createUnprocessedException(WrappedException(address, stmt.throwable.type))
         }
     }
 
@@ -180,7 +242,9 @@ class JcInterpreter(
                 } ?: return
             }
 
-            is JcMethodResult.Exception -> error("Exception should be handled earlier")
+            is JcMethodResult.UnprocessedException, is JcMethodResult.Exception -> {
+                error("Exception should be handled earlier")
+            }
         }
     }
 

usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt

@@ -5,13 +5,20 @@ import org.jacodb.api.JcMethod
 import org.jacodb.api.cfg.JcInst
 import org.jacodb.api.ext.methods
 import org.usvm.CoverageZone
-import org.usvm.UMachineOptions
 import org.usvm.PathSelectorCombinationStrategy
 import org.usvm.UMachine
+import org.usvm.UMachineOptions
 import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
+import org.usvm.machine.state.lastStmt
 import org.usvm.ps.createPathSelector
-import org.usvm.statistics.*
+import org.usvm.statistics.CompositeUMachineObserver
+import org.usvm.statistics.CoverageStatistics
+import org.usvm.statistics.CoveredNewStatesCollector
+import org.usvm.statistics.DistanceStatistics
+import org.usvm.statistics.PathsTreeStatistics
+import org.usvm.statistics.TransitiveCoverageZoneObserver
+import org.usvm.statistics.UMachineObserver
 import org.usvm.stopstrategies.createStopStrategy
 
 class JcMachine(
@@ -20,7 +27,7 @@ class JcMachine(
 ) : UMachine<JcState>() {
     private val applicationGraph = JcApplicationGraph(cp)
 
-    private val typeSystem = JcTypeSystem()
+    private val typeSystem = JcTypeSystem(cp)
     private val components = JcComponents(typeSystem, options.solverType)
     private val ctx = JcContext(cp, components)
 
@@ -99,7 +106,7 @@ class JcMachine(
     }
 
     private fun isStateTerminated(state: JcState): Boolean {
-        return state.callStack.isEmpty() || state.methodResult is JcMethodResult.Exception
+        return state.callStack.isEmpty()
     }
 
     override fun close() {

usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt

@@ -1,11 +1,17 @@
 package org.usvm.machine
 
 import org.jacodb.api.JcClassType
+import org.jacodb.api.JcClasspath
+import org.jacodb.api.JcRefType
 import org.jacodb.api.JcType
 import org.jacodb.api.ext.isAssignable
+import org.jacodb.api.ext.toType
+import org.jacodb.impl.features.HierarchyExtensionImpl
 import org.usvm.UTypeSystem
 
-class JcTypeSystem : UTypeSystem<JcType> {
+class JcTypeSystem(cp: JcClasspath) : UTypeSystem<JcType> {
+    private val hierarchy = HierarchyExtensionImpl(cp)
+
     override fun isSupertype(u: JcType, t: JcType): Boolean {
         return t.isAssignable(u)
     }
@@ -17,4 +23,14 @@ class JcTypeSystem : UTypeSystem<JcType> {
     override fun isFinal(t: JcType): Boolean {
         return (t as? JcClassType)?.isFinal ?: false
     }
-}
+
+    override fun isInstantiable(t: JcType): Boolean {
+        return t !is JcRefType || (!t.jcClass.isInterface && !t.jcClass.isAbstract)
+    }
+
+    // TODO: deal with generics
+    override fun findSubtypes(t: JcType): Sequence<JcType> =
+        hierarchy
+            .findSubClasses((t as JcRefType).jcClass, allHierarchy = false)
+            .map { it.toType() }
+}

usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcMethodResult.kt

@@ -1,6 +1,8 @@
 package org.usvm.machine.state
 
+import org.jacodb.api.JcType
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.USort
 
 /**
@@ -16,19 +18,23 @@ sealed interface JcMethodResult {
      * A method successfully returned a [value].
      */
     class Success(
-        val value: UExpr<out USort>
+        val value: UExpr<out USort>,
     ) : JcMethodResult
 
     /**
      * A method threw an [exception].
      */
-    class Exception(
-        val exception: kotlin.Exception
+    open class Exception(
+        val exception: kotlin.Exception,
     ) : JcMethodResult
 
+    class UnprocessedException(
+        exception: kotlin.Exception,
+    ) : Exception(exception)
 }
 
 // TODO: stub for symbolic exceptions
 class WrappedException(
-    val name: String
+    val address: UHeapRef,
+    val type: JcType,
 ) : kotlin.Exception()

usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt

@@ -27,6 +27,13 @@ fun JcState.returnValue(valueToReturn: UExpr<out USort>) {
     }
 }
 
+/**
+ * Create an unprocessed exception from the [exception] and assign it to the [JcState.methodResult].
+ */
+fun JcState.createUnprocessedException(exception: Exception) {
+    methodResult = JcMethodResult.UnprocessedException(exception)
+}
+
 fun JcState.throwException(exception: Exception) {
     // TODO: think about it later
     val returnSite = callStack.pop()

usvm-jvm/src/samples/java/org/usvm/samples/exceptions/ExceptionExamples.java

@@ -1,5 +1,7 @@
 package org.usvm.samples.exceptions;
 
+import java.nio.file.InvalidPathException;
+
 public class ExceptionExamples {
     public int initAnArray(int n) {
         try {
@@ -32,14 +34,14 @@ public int doNotCatchNested(int i) {
 
     private int checkAll(int i) {
         if (i < 0) {
-            throw new IllegalArgumentException("Negative");
+            throw new IllegalArgumentException();
         }
         return checkPositive(i);
     }
 
     private int checkPositive(int i) {
         if (i > 0) {
-            throw new NullPointerException("Positive");
+            throw new NullPointerException();
         }
         return 0;
     }
@@ -51,7 +53,7 @@ public int finallyThrowing(int i) {
         } catch (NullPointerException e) {
             throw e;
         } finally {
-            throw new IllegalStateException("finally");
+            throw new IllegalStateException();
         }
     }
 
@@ -99,7 +101,7 @@ public int catchExceptionAfterOtherPossibleException(int i) {
     }
 
     public IllegalArgumentException createException() {
-        return new IllegalArgumentException("Here we are: " + Math.sqrt(10));
+        return new IllegalArgumentException();
     }
 
     public int hangForSeconds(int seconds) throws InterruptedException {
@@ -119,8 +121,24 @@ private int callNestedWithThrow(int i) {
 
     private int nestedWithThrow(int i) {
         if (i < 0) {
-            throw new IllegalArgumentException("Negative");
+            throw new IllegalArgumentException();
         }
         return i;
     }
+
+    public int symbolicExceptionCheck(Exception e) {
+        try {
+            throw e;
+        } catch (NumberFormatException | InvalidPathException exception) {
+            if (e instanceof NumberFormatException) {
+                return 1;
+            }
+
+            return 2;
+        } catch (RuntimeException exception) {
+            return 3;
+        } catch (Exception exception) {
+            return 4;
+        }
+    }
 }