Enabled some usvm-jvm tests (#103)

usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt

@@ -90,6 +90,9 @@ class USupportTypeStream<Type> private constructor(
     override val isEmpty: Boolean
         get() = take(1).isEmpty()
 
+    override val commonSuperType: Type
+        get() = supportType
+
     companion object {
         fun <Type> from(typeSystem: UTypeSystem<Type>, type: Type): USupportTypeStream<Type> {
             val root = rootSequence(typeSystem, type).filter(typeSystem::isInstantiable)

usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt

@@ -48,6 +48,11 @@ interface UTypeStream<Type> {
     fun take(n: Int): Collection<Type>
 
     val isEmpty: Boolean
+
+    /**
+     * Stores a supertype that satisfies current type constraints and other satisfying types are inheritors of this type.
+     */
+    val commonSuperType: Type?
 }
 
 /**
@@ -66,6 +71,9 @@ object UEmptyTypeStream : UTypeStream<Nothing> {
 
     override val isEmpty: Boolean
         get() = true
+
+    override val commonSuperType: Nothing?
+        get() = null
 }
 
 @Suppress("UNCHECKED_CAST")
@@ -119,4 +127,7 @@ class USingleTypeStream<Type>(
 
     override val isEmpty: Boolean
         get() = false
+
+    override val commonSuperType: Type
+        get() = singleType
 }

usvm-jvm/build.gradle.kts

@@ -16,7 +16,7 @@ val `usvm-api` by sourceSets.creating {
 
 val approximations by configurations.creating
 val approximationsRepo = "com.github.UnitTestBot.java-stdlib-approximations"
-val approximationsVersion = "53ceeb23ea"
+val approximationsVersion = "fcfd10e495"
 
 dependencies {
     implementation(project(":usvm-core"))

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

@@ -0,0 +1,57 @@
+package org.usvm.api.util
+
+import org.jacodb.api.JcClassOrInterface
+import org.jacodb.api.JcRefType
+import org.jacodb.api.ext.allSuperHierarchySequence
+import org.jacodb.api.ext.toType
+import java.nio.ByteBuffer
+import java.security.CodeSource
+import java.security.SecureClassLoader
+
+/**
+ * Loads known classes using [ClassLoader.getSystemClassLoader], or defines them using bytecode from jacodb if they are unknown.
+ */
+object JcClassLoader : SecureClassLoader(ClassLoader.getSystemClassLoader()) {
+    fun loadClass(jcClass: JcClassOrInterface): Class<*> = defineClassRecursively(jcClass)
+
+    private fun defineClass(name: String, code: ByteArray): Class<*> {
+        return defineClass(name, ByteBuffer.wrap(code), null as CodeSource?)
+    }
+
+    private fun defineClassRecursively(jcClass: JcClassOrInterface): Class<*> =
+        defineClassRecursively(jcClass, hashSetOf())
+
+    private fun defineClassRecursively(
+        jcClass: JcClassOrInterface,
+        visited: MutableSet<JcClassOrInterface>
+    ): Class<*> {
+        visited += jcClass
+
+        return try {
+            // We cannot redefine a class that was already defined
+            loadClass(jcClass.name)
+        } catch (e: ClassNotFoundException) {
+            with(jcClass) {
+                // For unknown class we need to load all its supers, all classes mentioned in its ALL (not only declared)
+                // fields (as they are used in resolving), and then define the class itself using its bytecode from jacodb
+
+                val notVisitedSupers = allSuperHierarchySequence.filterNot { it in visited }
+                notVisitedSupers.forEach { defineClassRecursively(it, visited) }
+
+                val classType = toType()
+                val notVisitedRefFieldTypes = classType
+                    .fields
+                    .asSequence()
+                    .map { it.fieldType }
+                    .filterIsInstance<JcRefType>()
+                    .map { it.jcClass }
+                    .filterNot { it in visited }
+
+                notVisitedRefFieldTypes.forEach { defineClassRecursively(it, visited) }
+
+                return defineClass(name, bytecode())
+            }
+        }
+    }
+}
+

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

@@ -64,7 +64,7 @@ import org.usvm.types.firstOrNull
  * @param classLoader a class loader to load target classes.
  */
 class JcTestInterpreter(
-    private val classLoader: ClassLoader = ClassLoader.getSystemClassLoader(),
+    private val classLoader: ClassLoader = JcClassLoader,
 ): JcTestResolver {
     /**
      * Resolves a [JcTest] from a [method] from a [state].
@@ -122,7 +122,7 @@ class JcTestInterpreter(
         private val model: UModelBase<JcType>,
         private val memory: UReadOnlyMemory<JcType>,
         private val method: JcTypedMethod,
-        private val classLoader: ClassLoader = ClassLoader.getSystemClassLoader(),
+        private val classLoader: ClassLoader = JcClassLoader,
     ) {
         private val resolvedCache = mutableMapOf<UConcreteHeapAddress, Any?>()
 
@@ -350,7 +350,7 @@ class JcTestInterpreter(
 
                     else -> error("Unexpected type: $elementType")
                 }
-            } ?: classLoader.loadClass(type.jcClass.name)
+            } ?: classLoader.loadClass(type.jcClass)
 
         /**
          * If we resolve state after, [expr] is read from a state memory, so it requires concretization via [model].
@@ -365,4 +365,10 @@ class JcTestInterpreter(
         private fun JcRefType.getEnumAncestorOrNull(): JcClassOrInterface? =
             (sequenceOf(jcClass) + jcClass.allSuperHierarchySequence).firstOrNull { it.isEnum }
     }
-}
+}
+
+fun ClassLoader.loadClass(jcClass: JcClassOrInterface): Class<*> = if (this is JcClassLoader) {
+    loadClass(jcClass)
+} else {
+    loadClass(jcClass.name)
+}

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

@@ -62,7 +62,6 @@ import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.skipMethodInvocationWithValue
 import org.usvm.sizeSort
 import org.usvm.types.first
-import org.usvm.types.single
 import org.usvm.types.singleOrNull
 import org.usvm.util.allocHeapRef
 import org.usvm.util.write
@@ -353,12 +352,9 @@ class JcMethodApproximationResolver(
 
     private fun approximateArrayClone(methodCall: JcMethodCall): Boolean {
         val instance = methodCall.arguments.first().asExpr(ctx.addressSort)
-        if (instance !is UConcreteHeapRef) {
-            return false
-        }
 
         val arrayType = scope.calcOnState {
-            (memory.types.getTypeStream(instance).single())
+            memory.types.getTypeStream(instance).commonSuperType
         }
         if (arrayType !is JcArrayType) {
             return false
@@ -370,7 +366,7 @@ class JcMethodApproximationResolver(
 
     private fun JcExprResolver.resolveArrayClone(
         methodCall: JcMethodCall,
-        instance: UConcreteHeapRef,
+        instance: UHeapRef,
         arrayType: JcArrayType,
     ) = with(ctx) {
         scope.doWithState {

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

@@ -107,8 +107,9 @@ class JcContext(
         stringType.jcClass.toType().declaredFields.first { it.name == "value" }
     }
 
-    val stringCoderField: JcTypedField by lazy {
-        stringType.jcClass.toType().declaredFields.first { it.name == "coder" }
+    // The `coder` field is not presented in java 8, so return null if is missed
+    val stringCoderField: JcTypedField? by lazy {
+        stringType.jcClass.toType().declaredFields.firstOrNull { it.name == "coder" }
     }
 
     // Do not use JcTypedField here as its type is not required, however JcTypedField does not have required overridden `equals` method

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

@@ -11,6 +11,7 @@ import org.jacodb.api.JcMethod
 import org.jacodb.api.JcPrimitiveType
 import org.jacodb.api.JcRefType
 import org.jacodb.api.JcType
+import org.jacodb.api.JcTypeVariable
 import org.jacodb.api.JcTypedField
 import org.jacodb.api.JcTypedMethod
 import org.jacodb.api.PredefinedPrimitives
@@ -78,7 +79,6 @@ import org.jacodb.api.ext.enumValues
 import org.jacodb.api.ext.float
 import org.jacodb.api.ext.ifArrayGetElementType
 import org.jacodb.api.ext.int
-import org.jacodb.api.ext.isAssignable
 import org.jacodb.api.ext.isEnum
 import org.jacodb.api.ext.long
 import org.jacodb.api.ext.objectType
@@ -146,8 +146,9 @@ class JcExprResolver(
      * @return a symbolic expression, with the sort corresponding to the [type].
      */
     fun resolveJcExpr(expr: JcExpr, type: JcType = expr.type): UExpr<out USort>? {
-        val resolvedExpr = if (expr.type != type) {
-            resolveCast(expr, type)
+        val resolvedExpr = if (expr.type != type && type is JcPrimitiveType) {
+            // Only primitive casts may appear here because reference casts are handled with cast instruction
+            resolvePrimitiveCast(expr, type)
         } else {
             expr.accept(this)
         } ?: return null
@@ -311,7 +312,9 @@ class JcExprResolver(
     ): UExpr<out USort> = simpleValueResolver.visitJcClassConstant(value)
     // endregion
 
-    override fun visitJcCastExpr(expr: JcCastExpr): UExpr<out USort>? = resolveCast(expr.operand, expr.type)
+    override fun visitJcCastExpr(expr: JcCastExpr): UExpr<out USort>? =
+        // Note that primitive types may appear in JcCastExpr
+        resolveCast(expr.operand, expr.type)
 
     override fun visitJcInstanceOfExpr(expr: JcInstanceOfExpr): UExpr<out USort>? = with(ctx) {
         val ref = resolveJcExpr(expr.operand)?.asExpr(addressSort) ?: return null
@@ -334,7 +337,7 @@ class JcExprResolver(
     }
 
     override fun visitJcNewArrayExpr(expr: JcNewArrayExpr): UExpr<out USort>? = with(ctx) {
-        val size = resolveCast(expr.dimensions[0], ctx.cp.int)?.asExpr(bv32Sort) ?: return null
+        val size = resolvePrimitiveCast(expr.dimensions[0], ctx.cp.int)?.asExpr(bv32Sort) ?: return null
         // TODO: other dimensions ( > 1)
         checkNewArrayLength(size) ?: return null
 
@@ -724,7 +727,7 @@ class JcExprResolver(
 
         val arrayDescriptor = arrayDescriptorOf(array.type as JcArrayType)
 
-        val idx = resolveCast(index, ctx.cp.int)?.asExpr(bv32Sort) ?: return null
+        val idx = resolvePrimitiveCast(index, ctx.cp.int)?.asExpr(bv32Sort) ?: return null
         val lengthRef = UArrayLengthLValue(arrayRef, arrayDescriptor, sizeSort)
         val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
 
@@ -859,8 +862,13 @@ class JcExprResolver(
         typeBefore: JcRefType,
         type: JcRefType,
     ): UHeapRef? {
-        return if (!typeBefore.isAssignable(type)) {
+        check(type !is JcTypeVariable) {
+            "Unexpected type variable $type"
+        }
+
+        return if (!ctx.typeSystem<JcType>().isSupertype(type, typeBefore)) {
             val isExpr = scope.calcOnState { memory.types.evalIsSubtype(expr, type) }
+
             scope.fork(
                 isExpr,
                 blockOnFalseState = allocateException(ctx.classCastExceptionType)
@@ -871,6 +879,18 @@ class JcExprResolver(
         }
     }
 
+    private fun resolvePrimitiveCast(
+        expr: JcExpr,
+        type: JcPrimitiveType
+    ): UExpr<out USort>? = resolveAfterResolved(expr) {
+        val exprType = expr.type
+        check(exprType is JcPrimitiveType) {
+            "Trying cast not primitive type $exprType to primitive type $type"
+        }
+
+        resolvePrimitiveCast(it, exprType, type)
+    }
+
     private fun resolvePrimitiveCast(
         expr: UExpr<out USort>,
         typeBefore: JcPrimitiveType,
@@ -1032,7 +1052,6 @@ class JcSimpleValueResolver(
             // Equal string constants always have equal references
             val ref = resolveStringConstant(value.value)
             val stringValueLValue = UFieldLValue(addressSort, ref, stringValueField.field)
-            val stringCoderLValue = UFieldLValue(byteSort, ref, stringCoderField.field)
 
             // String.value type depends on the JVM version
             val charValues = when (stringValueField.fieldType.ifArrayGetElementType) {
@@ -1055,7 +1074,13 @@ class JcSimpleValueResolver(
 
             // String constants are immutable. Therefore, it is correct to overwrite value, coder and type.
             memory.write(stringValueLValue, charArrayRef)
-            memory.write(stringCoderLValue, mkBv(0, byteSort))
+
+            // Write coder only if it is presented (depends on the JVM version)
+            stringCoderField?.let {
+                val stringCoderLValue = UFieldLValue(byteSort, ref, it.field)
+                memory.write(stringCoderLValue, mkBv(0, byteSort))
+            }
+
             memory.types.allocate(ref.address, stringType)
 
             ref