Fix type constraints (#79)

UnitTestBot · Oct 24, 2023 · fcf9606 · fcf9606
1 parent af95d68
commit fcf9606
Show file tree

Hide file tree

Showing 7 changed files with 59 additions and 20 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
@@ -381,7 +381,7 @@ class UTypeConstraints<Type>(
                 val typeRegion = getTypeRegion(symbolicRef)
 
                 if (typeRegion.addSupertype(supertype).isEmpty) {
-                    symbolicRef.ctx.falseExpr
+                    symbolicRef.uctx.mkEq(symbolicRef, symbolicRef.uctx.nullRef)
                 } else {
                     symbolicRef.uctx.mkIsSubtypeExpr(symbolicRef, supertype)
                 }

diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt
@@ -56,17 +56,8 @@ class UTypeRegion<Type>(
             return contradiction()
         }
 
-        val multipleInheritanceIsNotAllowed = !typeSystem.isMultipleInheritanceAllowedFor(supertype)
-
-        if (multipleInheritanceIsNotAllowed) {
-            // We've already checked it </: supertype
-            val incomparableSupertypeWithoutMultipleInheritanceAllowedExists = supertypes.any {
-                !typeSystem.isMultipleInheritanceAllowedFor(it) && !typeSystem.isSupertype(it, supertype)
-            }
-
-            if (incomparableSupertypeWithoutMultipleInheritanceAllowedExists) {
-                return contradiction()
-            }
+        if (!typeSystem.hasCommonSubtype(supertype, supertypes)) {
+            return contradiction()
         }
 
         val newSubtypes = if (typeSystem.isFinal(supertype)) {

diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeSystem.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeSystem.kt
@@ -12,9 +12,11 @@ interface UTypeSystem<Type> {
     fun isSupertype(supertype: Type, type: Type): Boolean
 
     /**
-     * @return true if [type] can be supertype for some type together with some incomparable type u.
+     * @return true if [types] and [type] can be supertypes for some type together.
+     * It is guaranteed that [type] is not a supertype for any type from [types]
+     * and that [types] have common subtype.
      */
-    fun isMultipleInheritanceAllowedFor(type: Type): Boolean
+    fun hasCommonSubtype(type: Type, types: Collection<Type>): Boolean
 
     /**
      * @return true if there is no type u distinct from [type] and subtyping [type].

diff --git a/usvm-core/src/test/kotlin/org/usvm/types/single/SingleTypeSystem.kt b/usvm-core/src/test/kotlin/org/usvm/types/single/SingleTypeSystem.kt
@@ -9,7 +9,7 @@ object SingleTypeSystem : UTypeSystem<SingleTypeSystem.SingleType> {
 
     override fun isSupertype(supertype: SingleType, type: SingleType): Boolean = true
 
-    override fun isMultipleInheritanceAllowedFor(type: SingleType): Boolean = false
+    override fun hasCommonSubtype(type: SingleType, types: Collection<SingleType>): Boolean = types.isEmpty()
 
     override fun isFinal(type: SingleType): Boolean = true
 

diff --git a/usvm-core/src/test/kotlin/org/usvm/types/system/TestTypeSystem.kt b/usvm-core/src/test/kotlin/org/usvm/types/system/TestTypeSystem.kt
@@ -52,8 +52,12 @@ class TestTypeSystem : UTypeSystem<TestType> {
             .any { isSupertype(supertype, it) }
     }
 
-    override fun isMultipleInheritanceAllowedFor(type: TestType): Boolean {
-        return type.isMultipleInheritanceAllowed
+    override fun hasCommonSubtype(type: TestType, types: Collection<TestType>): Boolean {
+        if (type.isMultipleInheritanceAllowed) return true
+        return types.all {
+            // It is guaranteed that it </: [type]
+            it.isMultipleInheritanceAllowed || isSupertype(it, type)
+        }
     }
 
     override fun isFinal(type: TestType): Boolean {

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt
@@ -23,11 +23,52 @@ class JcTypeSystem(
     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(supertype.jcClass.toType()))
+                (supertype is JcTypeVariable && type.isAssignable(cp.objectType) && supertype.bounds.all { type.isAssignable(it) })
 
-    override fun isMultipleInheritanceAllowedFor(type: JcType): Boolean =
+    private fun isInterface(type: JcType): Boolean =
         (type as? JcClassType)?.jcClass?.isInterface ?: false
 
+    override fun hasCommonSubtype(type: JcType, types: Collection<JcType>): Boolean {
+        when {
+            type is JcPrimitiveType -> {
+                return types.isEmpty()
+            }
+
+            isInterface(type) -> {
+                return types.none { it is JcArrayType || it is JcPrimitiveType }
+            }
+
+            type is JcClassType -> {
+                return types.all {
+                    // It is guaranteed that it </: [type]
+                    isInterface(it) || isSupertype(it, type)
+                }
+            }
+
+            type is JcArrayType -> {
+                val elementTypes = types.mapNotNull {
+                    when {
+                        it is JcArrayType -> it.elementType
+                        it == cp.objectType -> null
+                        else -> return false
+                    }
+                }
+                return hasCommonSubtype(type.elementType, elementTypes)
+            }
+
+            type is JcTypeVariable -> {
+                val bounds = type.bounds
+                return if (bounds.isEmpty()) {
+                    types.none { it is JcPrimitiveType }
+                } else {
+                    bounds.all { hasCommonSubtype(it, types) }
+                }
+            }
+
+            else -> error("Unexpected type: $type")
+        }
+    }
+
     override fun isFinal(type: JcType): Boolean =
         (type as? JcClassType)?.isFinal ?: false
 

diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleTypeSystem.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleTypeSystem.kt
@@ -11,7 +11,8 @@ class SampleTypeSystem : UTypeSystem<SampleType> {
 
     override fun isFinal(type: SampleType): Boolean = true
 
-    override fun isMultipleInheritanceAllowedFor(type: SampleType): Boolean = false
+    override fun hasCommonSubtype(type: SampleType, types: Collection<SampleType>): Boolean = types.isEmpty()
+
     override fun isInstantiable(type: SampleType): Boolean = true
 
     override fun findSubtypes(type: SampleType): Sequence<SampleType> = emptySequence()