Support type variables in type regions (#104)

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

@@ -23,9 +23,15 @@ class JcTypeSystem(
     private val hierarchy = HierarchyExtensionImpl(cp)
 
     override fun isSupertype(supertype: JcType, type: JcType): Boolean =
-        type.isAssignable(supertype) ||
-                // It is possible when, for example, the returning type of a method is a type variable
-                (supertype is JcTypeVariable && type.isAssignable(cp.objectType) && supertype.bounds.all { type.isAssignable(it) })
+        when {
+            supertype == type -> true
+            supertype is JcTypeVariable ->
+                isSupertype(cp.objectType, type) && supertype.bounds.all { isSupertype(it, type) }
+
+            type is JcTypeVariable -> supertype == cp.objectType || type.bounds.any { isSupertype(supertype, it) }
+            else -> type.isAssignable(supertype)
+        }
+
 
     private fun isInterface(type: JcType): Boolean =
         (type as? JcClassType)?.jcClass?.isInterface ?: false

usvm-jvm/src/samples/java/org/usvm/samples/types/GenericWithUpperBound.java

@@ -0,0 +1,12 @@
+package org.usvm.samples.types;
+
+public class GenericWithUpperBound<C extends Comparable<C>> {
+    @SuppressWarnings({"DataFlowIssue"})
+    public int excludeComparable(C value) {
+        if (!(value instanceof Comparable<?>)) {
+            return 0;
+        }
+
+        return 1;
+    }
+}

usvm-jvm/src/test/kotlin/org/usvm/samples/types/GenericWithUpperBoundTest.kt

@@ -0,0 +1,19 @@
+package org.usvm.samples.types
+
+import org.junit.jupiter.api.Disabled
+import org.usvm.samples.JavaMethodTestRunner
+import org.usvm.test.util.checkers.eq
+import kotlin.test.Test
+
+internal class GenericWithUpperBoundTest : JavaMethodTestRunner() {
+    @Test
+    @Disabled("We do not support generics, so we may generate `GenericWithUpperBound<String>` here that leads to fail")
+    fun testExcludeComparable() {
+        checkDiscoveredProperties(
+            GenericWithUpperBound<Int>::excludeComparable,
+            eq(2),
+            { _, value, r -> value == null && r == 0 },
+            { _, value, r -> value != null && r == 1 },
+        )
+    }
+}