A first attempt to implement element and array types connection

Author: sergeypospelov

usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt

@@ -30,14 +30,14 @@ interface UTypeEvaluator<Type> {
  * Manages allocated objects separately from input ones. Indeed, we know the type of an allocated object
  * precisely, thus we can evaluate the subtyping constraints for them concretely (modulo generic type variables).
  */
-class UTypeConstraints<Type>(
+open class UTypeConstraints<Type>(
     private val typeSystem: UTypeSystem<Type>,
     private val equalityConstraints: UEqualityConstraints,
-    private val concreteRefToType: MutableMap<UConcreteHeapAddress, Type> = mutableMapOf(),
+    protected val concreteRefToType: MutableMap<UConcreteHeapAddress, Type> = mutableMapOf(),
     symbolicRefToTypeRegion: MutableMap<USymbolicHeapRef, UTypeRegion<Type>> = mutableMapOf(),
 ) : UTypeEvaluator<Type> {
     init {
-        equalityConstraints.subscribe(::intersectConstraints)
+        equalityConstraints.subscribe(::intersectRegions)
     }
 
     val symbolicRefToTypeRegion get(): Map<USymbolicHeapRef, UTypeRegion<Type>> = _symbolicRefToTypeRegion
@@ -57,7 +57,7 @@ class UTypeConstraints<Type>(
         )
     }
 
-    private fun contradiction() {
+    protected fun contradiction() {
         isContradicting = true
     }
 
@@ -68,11 +68,13 @@ class UTypeConstraints<Type>(
         concreteRefToType[ref] = type
     }
 
-    private fun getRegion(symbolicRef: USymbolicHeapRef) =
-        _symbolicRefToTypeRegion[equalityConstraints.equalReferences.find(symbolicRef)] ?: topTypeRegion
+    fun getTypeRegion(symbolicRef: USymbolicHeapRef, useRepresentative: Boolean = false): UTypeRegion<Type> {
+        val representative = if (useRepresentative) equalityConstraints.equalReferences.find(symbolicRef) else symbolicRef
+        return _symbolicRefToTypeRegion[representative] ?: topTypeRegion
+    }
 
 
-    private fun setRegion(symbolicRef: USymbolicHeapRef, value: UTypeRegion<Type>) {
+    private fun setTypeRegion(symbolicRef: USymbolicHeapRef, value: UTypeRegion<Type>) {
         _symbolicRefToTypeRegion[equalityConstraints.equalReferences.find(symbolicRef)] = value
     }
 
@@ -96,23 +98,7 @@ class UTypeConstraints<Type>(
             }
 
             is USymbolicHeapRef -> {
-                val constraints = getRegion(ref)
-                val newConstraints = constraints.addSupertype(type)
-                if (newConstraints.isContradicting) {
-                    // the only left option here is to be equal to null
-                    equalityConstraints.makeEqual(ref, ref.uctx.nullRef)
-                } else {
-                    // Inferring new symbolic disequalities here
-                    for ((key, value) in _symbolicRefToTypeRegion.entries) {
-                        // TODO: cache intersections?
-                        if (key != ref && value.intersect(newConstraints).isEmpty) {
-                            // If we have two inputs of incomparable reference types, then they are either non equal,
-                            // or both nulls
-                            equalityConstraints.makeNonEqualOrBothNull(ref, key)
-                        }
-                    }
-                    setRegion(ref, newConstraints)
-                }
+                updateRegionCanBeEqualNull(ref) { it.addSupertype(type) }
             }
 
             else -> error("Provided heap ref must be either concrete or purely symbolic one, found $ref")
@@ -139,23 +125,7 @@ class UTypeConstraints<Type>(
             }
 
             is USymbolicHeapRef -> {
-                val constraints = getRegion(ref)
-                val newConstraints = constraints.excludeSupertype(type)
-                equalityConstraints.makeNonEqual(ref, ref.uctx.nullRef)
-                if (newConstraints.isContradicting || equalityConstraints.isContradicting) {
-                    // the [ref] can't be equal to null
-                    contradiction()
-                } else {
-                    // Inferring new symbolic disequalities here
-                    for ((key, value) in _symbolicRefToTypeRegion.entries) {
-                        // TODO: cache intersections?
-                        if (key != ref && value.intersect(newConstraints).isEmpty) {
-                            // If we have two inputs of incomparable reference types, then they are non equal
-                            equalityConstraints.makeNonEqual(ref, key)
-                        }
-                    }
-                    setRegion(ref, newConstraints)
-                }
+                updateRegionCannotBeEqualNull(ref) { it.excludeSupertype(type) }
             }
 
             else -> error("Provided heap ref must be either concrete or purely symbolic one, found $ref")
@@ -165,7 +135,7 @@ class UTypeConstraints<Type>(
     /**
      * @return a type stream corresponding to the [ref].
      */
-    internal fun readTypeStream(ref: UHeapRef): UTypeStream<Type> =
+    internal fun getTypeStream(ref: UHeapRef): UTypeStream<Type> =
         when (ref) {
             is UConcreteHeapRef -> {
                 val concreteType = concreteRefToType[ref.address]
@@ -180,15 +150,61 @@ class UTypeConstraints<Type>(
             is UNullRef -> error("Null ref should be handled explicitly earlier")
 
             is USymbolicHeapRef -> {
-                getRegion(ref).typeStream
+                getTypeRegion(ref).typeStream
             }
 
             else -> error("Unexpected ref: $ref")
         }
 
-    private fun intersectConstraints(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) {
-        val newRegion = getRegion(ref1).intersect(getRegion(ref2))
-        setRegion(ref1, newRegion)
+    private fun intersectRegions(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) {
+        val region = getTypeRegion(ref2)
+        updateRegionCanBeEqualNull(ref1, region::intersect)
+    }
+
+    protected fun updateRegionCannotBeEqualNull(
+        ref: USymbolicHeapRef,
+        regionMapper: (UTypeRegion<Type>) -> UTypeRegion<Type>,
+    ) {
+        val region = getTypeRegion(ref)
+        val newRegion = regionMapper(region)
+        if (newRegion == region) {
+            return
+        }
+        equalityConstraints.makeNonEqual(ref, ref.uctx.nullRef)
+        if (newRegion.isEmpty || equalityConstraints.isContradicting) {
+            contradiction()
+            return
+        }
+        for ((key, value) in _symbolicRefToTypeRegion.entries) {
+            // TODO: cache intersections?
+            if (key != ref && value.intersect(newRegion).isEmpty) {
+                // If we have two inputs of incomparable reference types, then they are non equal
+                equalityConstraints.makeNonEqual(ref, key)
+            }
+        }
+        setTypeRegion(ref, newRegion)
+    }
+
+    protected fun updateRegionCanBeEqualNull(
+        ref: USymbolicHeapRef,
+        regionMapper: (UTypeRegion<Type>) -> UTypeRegion<Type>,
+    ) {
+        val region = getTypeRegion(ref)
+        val newRegion = regionMapper(region)
+        if (newRegion == region) {
+            return
+        }
+        if (newRegion.isEmpty) {
+            equalityConstraints.makeEqual(ref, ref.uctx.nullRef)
+        }
+        for ((key, value) in _symbolicRefToTypeRegion.entries) {
+            // TODO: cache intersections?
+            if (key != ref && value.intersect(newRegion).isEmpty) {
+                // If we have two inputs of incomparable reference types, then they are non equal
+                equalityConstraints.makeNonEqualOrBothNull(ref, key)
+            }
+        }
+        setTypeRegion(ref, newRegion)
     }
 
     /**
@@ -209,9 +225,9 @@ class UTypeConstraints<Type>(
                     // accordingly to the [UIsExpr] specification, [nullRef] always satisfies the [type]
                     return@mapper symbolicRef.ctx.trueExpr
                 }
-                val typeRegion = getRegion(symbolicRef)
+                val typeRegion = getTypeRegion(symbolicRef)
 
-                if (typeRegion.addSupertype(type).isContradicting) {
+                if (typeRegion.addSupertype(type).isEmpty) {
                     symbolicRef.ctx.falseExpr
                 } else {
                     symbolicRef.uctx.mkIsExpr(symbolicRef, type)

usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt

@@ -26,7 +26,7 @@ infix fun <T> GuardedExpr<T>.withAlso(guard: UBoolExpr) = GuardedExpr(expr, guar
  * @param symbolicHeapRef an ite made of all [USymbolicHeapRef]s with its guard, the single [USymbolicHeapRef] if it's
  * the single [USymbolicHeapRef] in the base expression or `null` if there are no [USymbolicHeapRef]s at all.
  */
-internal data class SplitHeapRefs(
+data class SplitHeapRefs(
     val concreteHeapRefs: List<GuardedExpr<UConcreteHeapRef>>,
     val symbolicHeapRef: GuardedExpr<UHeapRef>?,
 )
@@ -43,7 +43,7 @@ internal data class SplitHeapRefs(
  * @param ignoreNullRefs if true, then null references will be ignored. It means that all leafs with nulls
  * considered unsatisfiable, so we assume their guards equal to false, and they won't be added to the result.
  */
-internal fun splitUHeapRef(
+fun splitUHeapRef(
     ref: UHeapRef,
     initialGuard: UBoolExpr = ref.ctx.trueExpr,
     ignoreNullRefs: Boolean = true,
@@ -75,7 +75,7 @@ internal fun splitUHeapRef(
  * @param ignoreNullRefs if true, then null references will be ignored. It means that all leafs with nulls
  * considered unsatisfiable, so we assume their guards equal to false.
  */
-internal inline fun withHeapRef(
+inline fun withHeapRef(
     ref: UHeapRef,
     initialGuard: UBoolExpr,
     crossinline blockOnConcrete: (GuardedExpr<UConcreteHeapRef>) -> Unit,
@@ -104,9 +104,9 @@ internal inline fun withHeapRef(
     }
 }
 
-private const val LEFT_CHILD = 0
-private const val RIGHT_CHILD = 1
-private const val DONE = 2
+const val LEFT_CHILD = 0
+const val RIGHT_CHILD = 1
+const val DONE = 2
 
 
 /**
@@ -118,7 +118,7 @@ private const val DONE = 2
  * considered unsatisfiable, so we assume their guards equal to false. If [ignoreNullRefs] is true and [this] is
  * [UNullRef], throws an [IllegalArgumentException].
  */
-internal inline fun <Sort : USort> UHeapRef.map(
+inline fun <Sort : USort> UHeapRef.map(
     crossinline concreteMapper: (UConcreteHeapRef) -> UExpr<Sort>,
     crossinline symbolicMapper: (USymbolicHeapRef) -> UExpr<Sort>,
     ignoreNullRefs: Boolean = true,

usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt

@@ -162,5 +162,5 @@ open class UMemoryBase<Field, Type, Method>(
         UMemoryBase(ctx, typeConstraints, stack.clone(), heap.toMutableHeap(), mocker)
 
     override fun typeStreamOf(ref: UHeapRef): UTypeStream<Type> =
-        types.readTypeStream(ref)
+        types.getTypeStream(ref)
 }

usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt

@@ -117,7 +117,7 @@ class ULazyHeapModel<Field, ArrayType>(
         // All the expressions in the model are interpreted, therefore, they must
         // have concrete addresses. Moreover, the model knows only about input values
         // which have addresses less or equal than INITIAL_INPUT_ADDRESS
-        require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS)
+        require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" }
 
         val resolvedRegion = resolvedInputFields[field]
         val regionId = UInputFieldId(field, sort, contextHeap = null)
@@ -142,7 +142,7 @@ class ULazyHeapModel<Field, ArrayType>(
         // All the expressions in the model are interpreted, therefore, they must
         // have concrete addresses. Moreover, the model knows only about input values
         // which have addresses less or equal than INITIAL_INPUT_ADDRESS
-        require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS)
+        require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" }
 
         val key = ref to index
 
@@ -164,7 +164,7 @@ class ULazyHeapModel<Field, ArrayType>(
         // All the expressions in the model are interpreted, therefore, they must
         // have concrete addresses. Moreover, the model knows only about input values
         // which have addresses less or equal than INITIAL_INPUT_ADDRESS
-        require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS)
+        require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" }
 
         val resolvedRegion = resolvedInputLengths[arrayType]
         val regionId = UInputArrayLengthId(arrayType, ref.uctx.sizeSort, contextHeap = null)

usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt

@@ -52,7 +52,7 @@ class USoftConstraintsProvider<Field, Type>(override val ctx: UContext) : UTrans
     fun provide(initialExpr: UExpr<*>): Set<UBoolExpr> =
         caches.getOrElse(initialExpr) {
             apply(initialExpr)
-            provide(initialExpr)
+            caches.getValue(initialExpr)
         }
 
     // region The most common methods
@@ -97,10 +97,9 @@ class USoftConstraintsProvider<Field, Type>(override val ctx: UContext) : UTrans
         expr: UConcreteHeapRef,
     ): UExpr<UAddressSort> = error("Illegal operation since UConcreteHeapRef must not be translated into a solver")
 
-    override fun transform(expr: UNullRef): UExpr<UAddressSort> = expr
+    override fun transform(expr: UNullRef): UExpr<UAddressSort> = transformExpr(expr)
 
-    override fun transform(expr: UIsExpr<Type>): UBoolExpr =
-        error("Illegal operation since UIsExpr should not be translated into a SMT solver")
+    override fun transform(expr: UIsExpr<Type>): UBoolExpr = transformExpr(expr)
 
     override fun transform(
         expr: UInputArrayLengthReading<Type>,

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

@@ -16,8 +16,6 @@ open class UTypeRegion<Type>(
     val subtypes: PersistentSet<Type> = persistentSetOf(),
     val notSubtypes: PersistentSet<Type> = persistentSetOf(),
 ) : Region<UTypeRegion<Type>> {
-    val isContradicting get() = typeStream.isEmpty
-
     /**
      * Returns region that represents empty set of types. Called when type
      * constraints contradict, for example if X <: Y and X </: Y.
@@ -37,7 +35,7 @@ open class UTypeRegion<Type>(
      *  - t is final && t </: X && X <: t
      */
     open fun addSupertype(supertype: Type): UTypeRegion<Type> {
-        if (isContradicting || supertypes.any { typeSystem.isSupertype(supertype, it) }) {
+        if (isEmpty || supertypes.any { typeSystem.isSupertype(supertype, it) }) {
             return this
         }
 
@@ -84,7 +82,7 @@ open class UTypeRegion<Type>(
      *  X <: u && u <: t && X </: t, i.e. if [supertypes] contains subtype of [notSupertype]
      */
     open fun excludeSupertype(notSupertype: Type): UTypeRegion<Type> {
-        if (isContradicting || notSupertypes.any { typeSystem.isSupertype(it, notSupertype) }) {
+        if (isEmpty || notSupertypes.any { typeSystem.isSupertype(it, notSupertype) }) {
             return this
         }
 
@@ -108,8 +106,8 @@ open class UTypeRegion<Type>(
      *  - t <: X && u <: t && u </: X, i.e. if [notSubtypes] contains subtype of [subtype]
      *  - t <: X && X <: u && t </: u
      */
-    protected open fun addSubtype(subtype: Type): UTypeRegion<Type> {
-        if (isContradicting || subtypes.any { typeSystem.isSupertype(it, subtype) }) {
+    open fun addSubtype(subtype: Type): UTypeRegion<Type> {
+        if (isEmpty || subtypes.any { typeSystem.isSupertype(it, subtype) }) {
             return this
         }
 
@@ -134,8 +132,8 @@ open class UTypeRegion<Type>(
      *  - u <: X && t <: u && t </: X, i.e. if [subtypes] contains supertype of [notSubtype]
      *  - t is final && t </: X && X <: t
      */
-    protected open fun excludeSubtype(notSubtype: Type): UTypeRegion<Type> {
-        if (isContradicting || notSubtypes.any { typeSystem.isSupertype(notSubtype, it) }) {
+    open fun excludeSubtype(notSubtype: Type): UTypeRegion<Type> {
+        if (isEmpty || notSubtypes.any { typeSystem.isSupertype(notSubtype, it) }) {
             return this
         }
 
@@ -153,9 +151,12 @@ open class UTypeRegion<Type>(
         return UTypeRegion(typeSystem, newTypeStream, notSubtypes = newNotSubtypes)
     }
 
-    override val isEmpty: Boolean = isContradicting
+    override val isEmpty: Boolean = typeStream.isEmpty
 
     override fun intersect(other: UTypeRegion<Type>): UTypeRegion<Type> {
+        if (this == other) {
+            return this
+        }
         // TODO: optimize things up by not re-allocating type regions after each operation
         val otherSize = other.size
         val thisSize = this.size
@@ -164,6 +165,9 @@ open class UTypeRegion<Type>(
         } else {
             this to other
         }
+        if (smallRegion.isEmpty) {
+            return smallRegion
+        }
 
         val result1 = smallRegion.supertypes.fold(largeRegion) { acc, t -> acc.addSupertype(t) }
         val result2 = smallRegion.notSupertypes.fold(result1) { acc, t -> acc.excludeSupertype(t) }
@@ -172,6 +176,9 @@ open class UTypeRegion<Type>(
     }
 
     override fun subtract(other: UTypeRegion<Type>): UTypeRegion<Type> {
+        if (isEmpty || other.isEmpty) {
+            return this
+        }
         if (other.notSupertypes.isNotEmpty() || other.notSubtypes.isEmpty() || other.supertypes.size + other.subtypes.size != 1) {
             TODO("For now, we are able to subtract only positive singleton type constraints")
         }

usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt

@@ -148,6 +148,29 @@ class TypeSolverTest {
         assertIs<UUnsatResult<UModelBase<Field, TestType>>>(resultWithEqConstraint)
     }
 
+    @Test
+    fun `Test symbolic ref -- different types 3 refs`(): Unit = with(ctx) {
+        val ref0 = ctx.mkRegisterReading(0, addressSort)
+        val ref1 = ctx.mkRegisterReading(1, addressSort)
+        val ref2 = ctx.mkRegisterReading(2, addressSort)
+
+        pc += mkIsExpr(ref0, interfaceAB)
+        pc += mkIsExpr(ref1, interfaceBC1)
+        pc += mkIsExpr(ref2, interfaceAC)
+        pc += mkHeapRefEq(ref0, nullRef).not()
+        pc += mkHeapRefEq(ref1, nullRef).not()
+        pc += mkHeapRefEq(ref2, nullRef).not()
+
+        val resultWithoutEqConstraint = solver.check(pc)
+        val model = assertIs<USatResult<UModelBase<Field, TestType>>>(resultWithoutEqConstraint).model
+        assertNotEquals(model.eval(ref0), model.eval(ref1))
+
+        pc += mkHeapRefEq(ref0, ref1)
+        pc += mkHeapRefEq(ref1, ref2)
+
+        assertTrue(pc.isFalse)
+    }
+
     @Test
     fun `Test symbolic ref -- different interface types but same base type`(): Unit = with(ctx) {
         val ref0 = ctx.mkRegisterReading(0, addressSort)