Virtual calls

buildSrc/src/main/kotlin/Versions.kt

@@ -4,7 +4,7 @@ object Versions {
     const val ksmt = "0.5.6"
     const val collections = "0.3.5"
     const val coroutines = "1.6.4"
-    const val jcdb = "1.1.3"
+    const val jcdb = "1.2.0"
     const val mockk = "1.13.4"
     const val junitParams = "5.9.3"
     const val logback = "1.4.8"

settings.gradle.kts

@@ -4,4 +4,3 @@ include("usvm-core")
 include("usvm-jvm")
 include("usvm-util")
 include("usvm-sample-language")
-include("usvm-jvm")

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

@@ -23,8 +23,8 @@ class StepScope<T : UState<Type, Field, *, *>, Type, Field>(
 ) {
     private val forkedStates = mutableListOf<T>()
 
-    private val alive: Boolean get() = stepScopeState != DEAD
-    private val canProcessFurtherOnCurrentStep: Boolean get() = stepScopeState == CAN_BE_PROCESSED
+    private inline val alive: Boolean get() = stepScopeState != DEAD
+    private inline val canProcessFurtherOnCurrentStep: Boolean get() = stepScopeState == CAN_BE_PROCESSED
 
     /**
      * Determines whether we interact this scope on the current step.
@@ -42,24 +42,20 @@ class StepScope<T : UState<Type, Field, *, *>, Type, Field>(
      *
      * @return `null` if the underlying state is `null`.
      */
-    fun doWithState(block: T.() -> Unit): Unit? =
-        if (canProcessFurtherOnCurrentStep) {
-            originalState.block()
-        } else {
-            null
-        }
+    fun doWithState(block: T.() -> Unit) {
+        check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
+        return originalState.block()
+    }
 
     /**
      * Executes [block] on a state.
      *
      * @return `null` if the underlying state is `null`, otherwise returns result of calling [block].
      */
-    fun <R> calcOnState(block: T.() -> R): R? =
-        if (canProcessFurtherOnCurrentStep) {
-            originalState.block()
-        } else {
-            null
-        }
+    fun <R> calcOnState(block: T.() -> R): R {
+        check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
+        return originalState.block()
+    }
 
     /**
      * Forks on a [condition], performing [blockOnTrueState] on a state satisfying [condition] and
@@ -138,7 +134,7 @@ class StepScope<T : UState<Type, Field, *, *>, Type, Field>(
     ): Unit? {
         check(canProcessFurtherOnCurrentStep)
 
-        val (posState, _) = fork(originalState, constraint)
+        val (posState) = forkMulti(originalState, listOf(constraint))
 
         posState?.block()
 

usvm-core/src/main/kotlin/org/usvm/ps/BfsPathSelector.kt

@@ -10,7 +10,10 @@ class BfsPathSelector<State> : UPathSelector<State> {
     override fun peek() = queue.first()
 
     override fun update(state: State) {
-        // nothing to do
+        if (state === queue.first()) {
+            queue.removeFirst()
+            queue.addLast(state)
+        }
     }
 
     override fun add(states: Collection<State>) {
@@ -24,4 +27,4 @@ class BfsPathSelector<State> : UPathSelector<State> {
             else -> queue.remove(state)
         }
     }
-}
+}

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

@@ -79,12 +79,10 @@ class USupportTypeStream<Type> private constructor(
         )
 
     override fun take(n: Int): Set<Type> {
-        val set = cacheFromQueries.toMutableSet()
-        for (it in cachingSequence) {
-            if (set.size == n) {
-                break
-            }
-            set += it
+        val set = cacheFromQueries.take(n).toMutableSet()
+        val iterator = cachingSequence.iterator()
+        while (set.size < n && iterator.hasNext()) {
+            set += iterator.next()
         }
         return set
     }

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

@@ -24,6 +24,9 @@ class UTypeRegion<Type>(
 
     override val isEmpty: Boolean get() = typeStream.isEmpty
 
+    private val <Type> UTypeRegion<Type>.size: Int
+        get() = supertypes.size + notSupertypes.size + subtypes.size + notSubtypes.size
+
     /**
      * Excludes from this type region types which are not subtypes of [supertype].
      * If new type constraints contradict with already existing ones,
@@ -32,19 +35,30 @@ class UTypeRegion<Type>(
      * The default implementation checks for the following contradictions
      * (here X is type from this region and t is [supertype]):
      *  - X <: t && t <: u && X </: u, i.e. if [notSupertypes] contains supertype of [supertype]
+     *  - X <: t && u <: X && u </: t
      *  - X <: t && X <: u && u </: t && t </: u && t and u can't be multiply inherited
      *  - t is final && t </: X && X <: t
+     *
+     * Also, if u <: X && X <: t && u <: t, then X = u = t.
      */
     fun addSupertype(supertype: Type): UTypeRegion<Type> {
+        // X <: it && it <: supertype -> nothing changes
         if (isEmpty || supertypes.any { typeSystem.isSupertype(supertype, it) }) {
             return this
         }
 
-        if (notSubtypes.any { typeSystem.isSupertype(it, supertype) }) {
+        // X </: it && supertype <: it -> X </: supertype
+        if (notSupertypes.any { typeSystem.isSupertype(it, supertype) }) {
+            return contradiction()
+        }
+
+        // it <: X && it </: supertype -> X </: supertype
+        if (subtypes.any { !typeSystem.isSupertype(supertype, it) }) {
             return contradiction()
         }
 
         val multipleInheritanceIsNotAllowed = !typeSystem.isMultipleInheritanceAllowedFor(supertype)
+
         if (multipleInheritanceIsNotAllowed) {
             // We've already checked it </: supertype
             val incomparableSupertypeWithoutMultipleInheritanceAllowedExists = supertypes.any {
@@ -67,10 +81,15 @@ class UTypeRegion<Type>(
             subtypes
         }
 
+        // it <: X && supertype <: it -> X == supertype
+        if (newSubtypes.any { typeSystem.isSupertype(it, supertype) }) {
+            return checkSingleTypeRegion(supertype)
+        }
+
         val newSupertypes = supertypes.removeAll { typeSystem.isSupertype(it, supertype) }.add(supertype)
         val newTypeStream = typeStream.filterBySupertype(supertype)
 
-        return UTypeRegion(typeSystem, newTypeStream, supertypes = newSupertypes, subtypes = newSubtypes)
+        return clone(newTypeStream, supertypes = newSupertypes, subtypes = newSubtypes)
     }
 
     /**
@@ -94,7 +113,7 @@ class UTypeRegion<Type>(
         val newNotSupertypes = notSupertypes.removeAll { typeSystem.isSupertype(notSupertype, it) }.add(notSupertype)
         val newTypeStream = typeStream.filterByNotSupertype(notSupertype)
 
-        return UTypeRegion(typeSystem, newTypeStream, notSupertypes = newNotSupertypes)
+        return clone(newTypeStream, notSupertypes = newNotSupertypes)
     }
 
     /**
@@ -106,24 +125,34 @@ class UTypeRegion<Type>(
      * (here X is type from this region and t is [subtype]):
      *  - t <: X && u <: t && u </: X, i.e. if [notSubtypes] contains subtype of [subtype]
      *  - t <: X && X <: u && t </: u
+     *
+     *  Also, if t <: X && X <: u && u <: t, then X = u = t.
      */
     fun addSubtype(subtype: Type): UTypeRegion<Type> {
+        // it <: X && subtype <: it -> nothing changes
         if (isEmpty || subtypes.any { typeSystem.isSupertype(it, subtype) }) {
             return this
         }
 
+        // it </: X && it <: subtype -> subtype </: X
         if (notSubtypes.any { typeSystem.isSupertype(subtype, it) }) {
             return contradiction()
         }
 
+        // X <: it && subtype </: it -> subtype </: X
         if (supertypes.any { !typeSystem.isSupertype(it, subtype) }) {
             return contradiction()
         }
 
+        // X <: it && it <: subtype -> X <: subtype -> X == subtype
+        if (supertypes.any { typeSystem.isSupertype(subtype, it) }) {
+            return checkSingleTypeRegion(subtype)
+        }
+
         val newSubtypes = subtypes.removeAll { typeSystem.isSupertype(subtype, it) }.add(subtype)
         val newTypeStream = typeStream.filterBySubtype(subtype)
 
-        return UTypeRegion(typeSystem, newTypeStream, subtypes = newSubtypes)
+        return clone(newTypeStream, subtypes = newSubtypes)
     }
 
     /**
@@ -149,7 +178,7 @@ class UTypeRegion<Type>(
         val newNotSubtypes = notSubtypes.removeAll { typeSystem.isSupertype(it, notSubtype) }.add(notSubtype)
         val newTypeStream = typeStream.filterByNotSubtype(notSubtype)
 
-        return UTypeRegion(typeSystem, newTypeStream, notSubtypes = newNotSubtypes)
+        return clone(newTypeStream, notSubtypes = newNotSubtypes)
     }
 
     override fun intersect(other: UTypeRegion<Type>): UTypeRegion<Type> {
@@ -202,7 +231,43 @@ class UTypeRegion<Type>(
         return RegionComparisonResult.INTERSECTS
     }
 
-}
+    private fun checkSingleTypeRegion(type: Type): UTypeRegion<Type> {
+        if (!typeSystem.isInstantiable(type)) {
+            return contradiction()
+        }
 
-private val <Type> UTypeRegion<Type>.size: Int
-    get() = supertypes.size + subtypes.size + notSupertypes.size + notSubtypes.size
+        // X <: it && type </: it && X == type -> X <: X && X </: X
+        if (supertypes.any { !typeSystem.isSupertype(it, type) }) {
+            return contradiction()
+        }
+
+        // X </: it && type <: it && X == type -> X </: it && X <: it
+        if (notSupertypes.any { typeSystem.isSupertype(it, type) }) {
+            return contradiction()
+        }
+
+        // it <: X && it </: type && X == type -> it <: X && it </: X
+        if (subtypes.any { !typeSystem.isSupertype(type, it) }) {
+            return contradiction()
+        }
+
+        // it </: X && it <: type && X == type -> it </: X && it <: X
+        if (notSubtypes.any { typeSystem.isSupertype(type, it) }) {
+            return contradiction()
+        }
+
+        return clone(
+            USingleTypeStream(typeSystem, type),
+            supertypes = persistentSetOf(type),
+            subtypes = persistentSetOf(type)
+        )
+    }
+
+    private fun clone(
+        typeStream: UTypeStream<Type>,
+        supertypes: PersistentSet<Type> = this.supertypes,
+        notSupertypes: PersistentSet<Type> = this.notSupertypes,
+        subtypes: PersistentSet<Type> = this.subtypes,
+        notSubtypes: PersistentSet<Type> = this.notSubtypes,
+    ) = UTypeRegion(typeSystem, typeStream, supertypes, notSupertypes, subtypes, notSubtypes)
+}

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

@@ -9,6 +9,7 @@ import org.usvm.CoverageZone
 import org.usvm.PathSelectorCombinationStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
+import org.usvm.machine.interpreter.JcInterpreter
 import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.lastStmt

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

@@ -6,6 +6,7 @@ import org.jacodb.api.JcClasspath
 import org.jacodb.api.JcPrimitiveType
 import org.jacodb.api.JcRefType
 import org.jacodb.api.JcType
+import org.jacodb.api.JcTypeVariable
 import org.jacodb.api.ext.isAssignable
 import org.jacodb.api.ext.objectType
 import org.jacodb.api.ext.toType
@@ -20,7 +21,9 @@ class JcTypeSystem(
     private val hierarchy = HierarchyExtensionImpl(cp)
 
     override fun isSupertype(supertype: JcType, type: JcType): Boolean =
-        type.isAssignable(supertype)
+        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()))
 
     override fun isMultipleInheritanceAllowedFor(type: JcType): Boolean =
         (type as? JcClassType)?.jcClass?.isInterface ?: false