Improve various machine features

.github/workflows/ci.yml

@@ -55,7 +55,7 @@ jobs:
         uses: gradle/actions/setup-gradle@v4
 
       - name: Run JVM tests
-        run: ./gradlew :usvm-jvm:check :usvm-jvm-dataflow:check :usvm-jvm-instrumentation:check
+        run: ./gradlew :usvm-jvm:check :usvm-jvm:usvm-jvm-api:check :usvm-jvm:usvm-jvm-test-api:check :usvm-jvm:usvm-jvm-util:check :usvm-jvm-dataflow:check :usvm-jvm-instrumentation:check
 
       - name: Upload Gradle reports
         if: (!cancelled())

build.gradle.kts

@@ -14,6 +14,9 @@ tasks.register("validateProjectList") {
             project(":usvm-dataflow"),
             project(":usvm-sample-language"),
             project(":usvm-jvm"),
+            project(":usvm-jvm:usvm-jvm-api"),
+            project(":usvm-jvm:usvm-jvm-test-api"),
+            project (":usvm-jvm:usvm-jvm-util"),
             project(":usvm-jvm-dataflow"),
             project(":usvm-jvm-instrumentation"),
             project(":usvm-python"),

settings.gradle.kts

@@ -2,6 +2,9 @@ rootProject.name = "usvm"
 
 include("usvm-core")
 include("usvm-jvm")
+include("usvm-jvm:usvm-jvm-api")
+include("usvm-jvm:usvm-jvm-test-api")
+include("usvm-jvm:usvm-jvm-util")
 include("usvm-ts")
 include("usvm-util")
 include("usvm-jvm-instrumentation")

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

@@ -27,6 +27,8 @@ class UCallStack<Method, Statement> private constructor(
 
     fun lastMethod(): Method = stack.last().method
 
+    fun penultimateMethod(): Method = stack[stack.lastIndex - 1].method
+
     fun push(method: Method, returnSite: Statement?) {
         stack.add(UCallStackFrame(method, returnSite))
     }

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

@@ -41,7 +41,16 @@
                     val state = pathSelector.peek()
                     observer.onStatePeeked(state)
 
-                    val (forkedStates, stateAlive) = interpreter.step(state)
+                    val (forkedStates, stateAlive) = try {
+                        interpreter.step(state)
+                    } catch (e: Throwable) {
+                        logger.error(e) { "Step failed" }
+                        observer.onState(state, forks = emptySequence())
+                        pathSelector.remove(state)
+                        observer.onStateTerminated(state, stateReachable = false)
+                        continue
+                    }
+
                     observer.onState(state, forkedStates)
 
                     val originalStateAlive = stateAlive && !isStateTerminated(state)
@@ -76,7 +85,8 @@
             }
 
             if (!pathSelector.isEmpty()) {
-                logger.debug { stopStrategy.stopReason() }
+                val stopReason = stopStrategy.stopReason()
+                logger.debug { stopReason }
             }
         }
     }

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

@@ -94,34 +94,36 @@
         state: T,
         conditions: Iterable<UBoolExpr>,
     ): List<T?> {
-        var curState = state
-        val result = mutableListOf<T?>()
-        for (condition in conditions) {
-            val (trueModels, _, _) = splitModelsByCondition(curState.models, condition)
+        val guardedModels = mutableListOf<Pair<List<UModelBase<Type>>, UBoolExpr>?>()
 
-            val nextRoot = if (trueModels.isNotEmpty()) {
-                val root = curState.clone()
-                curState.models = trueModels
-                curState.pathConstraints += condition
+        for (condition in conditions) {
+            val (trueModels, _, _) = splitModelsByCondition(state.models, condition)
 
-                root
+            if (trueModels.isNotEmpty()) {
+                guardedModels += trueModels to condition
             } else {
-                val root = forkIfSat(
-                    curState,
+                forkOriginalStateIfSat(
+                    state,
                     newConstraintToOriginalState = condition,
-                    newConstraintToForkedState = condition.ctx.trueExpr,
-                    stateToCheck = OriginalState
+                    guardedModels
                 )
-
-                root
             }
-
-            if (nextRoot != null) {
-                result += curState
-                curState = nextRoot
-            } else {
+        }
+        val result = mutableListOf<T?>()
+        var curState = state
+        val lastNotNullIndex = guardedModels.indexOfLast { x -> x != null }
+        for (i in guardedModels.indices) {
+            val current = guardedModels[i]
+            if (current == null) {
                 result += null
+                continue
             }
+            val nextState = if (i == lastNotNullIndex) curState else curState.clone()
+            val (models, cond) = current
+            curState.models = models
+            curState.pathConstraints += cond
+            result += curState
+            curState = nextState
         }
 
         return result
@@ -190,6 +192,34 @@
             }
         }
     }
+
+    @Suppress("MoveVariableDeclarationIntoWhen")
+    private fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext<*>> forkOriginalStateIfSat(
+        state: T,
+        newConstraintToOriginalState: UBoolExpr,
+        guardedModels: MutableList<Pair<List<UModelBase<Type>>, UBoolExpr>?>
+    ) {
+        val constraintsToCheck = state.pathConstraints.clone()
+
+        constraintsToCheck += newConstraintToOriginalState
+        val solver = state.ctx.solver<Type>()
+        val satResult = solver.check(constraintsToCheck)
+
+        when (satResult) {
+            is UUnsatResult -> guardedModels += null
+
+            is USatResult -> {
+                // Note that we cannot extract common code here due to
+                // heavy plusAssign operator in path constraints.
+                // Therefore, it is better to reuse already constructed [constraintToCheck].
+                guardedModels += listOf(satResult.model) to newConstraintToOriginalState
+            }
+
+            is UUnknownResult -> {
+                guardedModels += null
+            }
+        }
+    }
 }
 
 object NoSolverStateForker : StateForker {

usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt

@@ -42,6 +42,37 @@ fun <Type> UState<Type, *, *, *, *, *>.objectTypeEquals(
     )
 }
 
+fun <Type> UState<Type, *, *, *, *, *>.objectTypeSubtype(
+    lhs: UHeapRef,
+    rhs: UHeapRef
+): UBoolExpr = with(lhs.uctx) {
+    mapTypeStream(
+        ref = lhs,
+        onNull = { trueExpr },
+        operation = { lhsRef, lhsTypes ->
+            mapTypeStream(
+                rhs,
+                onNull = { falseExpr },
+                operation = { rhsRef, rhsTypes ->
+                    mkSubtypeConstraint(lhsRef, lhsTypes, rhsRef, rhsTypes)
+                }
+            )
+        }
+    )
+}
+
+fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStreamNotNull(
+    ref: UHeapRef,
+    operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>?
+): UExpr<R>? = mapTypeStream(
+    ref = ref,
+    onNull = { error("unexpected null") },
+    operation = { expr, types ->
+        operation(expr, types) ?: return null
+    },
+    ignoreNullRefs = true
+)
+
 fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
     ref: UHeapRef,
     operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>?
@@ -78,12 +109,38 @@ private fun <Type> UState<Type, *, *, *, *, *>.mkTypeEqualsConstraint(
     makeSymbolicPrimitive(boolSort)
 }
 
+private fun <Type> UState<Type, *, *, *, *, *>.mkSubtypeConstraint(
+    lhs: UHeapRef,
+    lhsTypes: UTypeStream<Type>,
+    rhs: UHeapRef,
+    rhsTypes: UTypeStream<Type>,
+): UBoolExpr = with(lhs.uctx) {
+    val lhsType = lhsTypes.singleOrNull()
+    val rhsType = rhsTypes.singleOrNull()
+
+    if (lhsType != null) {
+        return if (lhsType == rhsType) {
+            trueExpr
+        } else {
+            memory.types.evalIsSupertype(rhs, lhsType)
+        }
+    }
+
+    if (rhsType != null) {
+        return memory.types.evalIsSubtype(lhs, rhsType)
+    }
+
+    // TODO: don't mock type equals
+    makeSymbolicPrimitive(boolSort)
+}
+
 private inline fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
     ref: UHeapRef,
     onNull: () -> UExpr<R>,
-    operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>
+    operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>,
+    ignoreNullRefs: Boolean = false,
 ): UExpr<R> = ref.mapWithStaticAsConcrete(
-    ignoreNullRefs = false,
+    ignoreNullRefs = ignoreNullRefs,
     concreteMapper = { concreteRef ->
         val types = memory.types.getTypeStream(concreteRef)
         operation(concreteRef, types)

usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt

@@ -23,8 +23,8 @@
 import org.usvm.types.UTypeStream
 import org.usvm.uctx
 import org.usvm.withSizeSort
-import org.usvm.collection.array.allocateArray as allocateArrayInternal
-import org.usvm.collection.array.allocateArrayInitialized as allocateArrayInitializedInternal
+import org.usvm.collection.array.initializeArrayLength as initializeArrayLengthInternal
+import org.usvm.collection.array.initializeArray as initializeArrayInternal
 
 fun <Type> UReadOnlyMemory<Type>.typeStreamOf(ref: UHeapRef): UTypeStream<Type> =
     types.getTypeStream(ref)
@@ -93,13 +93,20 @@
     memsetInternal(ref, type, sort, sizeSort, contents)
 }
 
-fun <ArrayType, USizeSort : USort> UWritableMemory<ArrayType>.allocateArray(
-    type: ArrayType, sizeSort: USizeSort, count: UExpr<USizeSort>,
-): UConcreteHeapRef = allocateArrayInternal(type, sizeSort, count)
+fun <ArrayType, USizeSort : USort> UWritableMemory<ArrayType>.initializeArrayLength(
+    arrayHeapRef: UConcreteHeapRef,
+    type: ArrayType,
+    sizeSort: USizeSort,
+    count: UExpr<USizeSort>,
+) = initializeArrayLengthInternal(arrayHeapRef, type, sizeSort, count)
 
-fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayType>.allocateArrayInitialized(
-    type: ArrayType, sort: Sort, sizeSort: USizeSort, contents: Sequence<UExpr<Sort>>
-): UConcreteHeapRef = allocateArrayInitializedInternal(type, sort, sizeSort, contents)
+fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayType>.initializeArray(
+    arrayHeapRef: UConcreteHeapRef,
+    type: ArrayType,
+    sort: Sort,
+    sizeSort: USizeSort,
+    contents: Sequence<UExpr<Sort>>
+) = initializeArrayInternal(arrayHeapRef, type, sort, sizeSort, contents)
 
 fun <SetType, ElemSort : USort, Reg : Region<Reg>> UWritableMemory<SetType>.setAddElement(
     ref: UHeapRef,

usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt

@@ -23,6 +23,31 @@ fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRef(
 ): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
     mockSymbolicRef { memory.types.evalTypeEquals(it, type) }
 
+fun <Type, Method, State> StepScope<State, Type, *, *>.makeNullableSymbolicRef(
+    type: Type
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { ctx.mkOr(memory.types.evalTypeEquals(it, type), ctx.mkEq(it, ctx.nullRef)) }
+
+fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRefSubtype(
+    type: Type
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { ctx.mkAnd(memory.types.evalIsSubtype(it, type), ctx.mkNot(ctx.mkEq(it, ctx.nullRef))) }
+
+fun <Type, Method, State> StepScope<State, Type, *, *>.makeNullableSymbolicRefSubtype(
+    type: Type
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { memory.types.evalIsSubtype(it, type) }
+
+fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRefSubtype(
+    representative: UHeapRef
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { ctx.mkAnd(objectTypeSubtype(it, representative), ctx.mkNot(ctx.mkEq(it, ctx.nullRef))) }
+
+fun <Type, Method, State> StepScope<State, Type, *, *>.makeNullableSymbolicRefSubtype(
+    representative: UHeapRef
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { objectTypeSubtype(it, representative) }
+
 fun <Type, Method, State> StepScope<State, Type, *, *>.makeSymbolicRefWithSameType(
     representative: UHeapRef
 ): UHeapRef? where State : UState<Type, Method, *, *, *, State> =

usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt

@@ -15,6 +15,7 @@
 import org.usvm.mkSizeAddExpr
 import org.usvm.mkSizeExpr
 import org.usvm.mkSizeGeExpr
+import org.usvm.mkSizeGtExpr
 import org.usvm.mkSizeSubExpr
 import org.usvm.sizeSort
 import org.usvm.utils.logAssertFailure
@@ -150,7 +151,12 @@
         memory.writeArrayLength(listRef, updatedSize, listType, sizeSort)
     }
 
-    fun <ListType, Sort : USort, USizeSort : USort> UState<ListType, *, *, *, *, *>.symbolicListCopyRange(
+    private fun <USizeSort : USort, Ctx: UContext<USizeSort>> Ctx.max(
+        first: UExpr<USizeSort>,
+        second: UExpr<USizeSort>
+    ): UExpr<USizeSort> = mkIte(mkSizeGtExpr(first, second), first, second)
+
+    fun <ListType, Sort : USort, USizeSort : USort, Ctx: UContext<USizeSort>> UState<ListType, *, *, Ctx, *, *>.symbolicListCopyRange(
         srcRef: UHeapRef,
         dstRef: UHeapRef,
         listType: ListType,
@@ -159,6 +165,7 @@
         dstFrom: UExpr<USizeSort>,
         length: UExpr<USizeSort>,
     ) {
+        // Copying contents
         memory.memcpy(
             srcRef = srcRef,
             dstRef = dstRef,
@@ -168,5 +175,11 @@
             fromDst = dstFrom,
             length = length
         )
+
+        // Modifying destination length
+        val dstLength = symbolicListSize(dstRef, listType)
+        val copyLength = ctx.mkSizeAddExpr(dstFrom, length)
+        val resultDstLength = ctx.max(dstLength, copyLength)
+        memory.writeArrayLength(dstRef, resultDstLength, listType, ctx.sizeSort)
     }
 }

usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt

@@ -161,13 +161,27 @@ object ObjectMapCollectionApi {
         val srcMapSize = symbolicObjectMapSize(srcRef, mapType)
         val dstMapSize = symbolicObjectMapSize(dstRef, mapType)
 
+        // todo: precise map size approximation?
+        // val sizeLowerBound = mkIte(mkBvSignedGreaterExpr(srcMapSize, dstMapSize), srcMapSize, dstMapSize)
+        val sizeUpperBound = mkSizeAddExpr(srcMapSize, dstMapSize)
+
+        var currentSize = sizeUpperBound
+        val allKeys = memory.refSetEntries(srcRef, mapType)
+        for (entry in allKeys.entries) {
+            val key = entry.setElement
+            val srcContains = symbolicObjectMapContains(srcRef, key, mapType)
+            val dstContains = symbolicObjectMapContains(dstRef, key, mapType)
+            when {
+                srcContains.isTrue && dstContains.isTrue ->
+                    currentSize = ctx.mkSizeSubExpr(currentSize, ctx.mkSizeExpr(1))
+                else -> continue
+            }
+        }
+
         val containsSetId = URefSetRegionId(mapType, sort.uctx.boolSort)
         memory.refMapMerge(srcRef, dstRef, mapType, sort, containsSetId, guard = trueExpr)
         memory.refSetUnion(srcRef, dstRef, mapType, guard = trueExpr)
 
-        // todo: precise map size approximation?
-        // val sizeLowerBound = mkIte(mkBvSignedGreaterExpr(srcMapSize, dstMapSize), srcMapSize, dstMapSize)
-        val sizeUpperBound = mkSizeAddExpr(srcMapSize, dstMapSize)
-        memory.write(UMapLengthLValue(dstRef, mapType, sizeSort), sizeUpperBound, guard = trueExpr)
+        memory.write(UMapLengthLValue(dstRef, mapType, sizeSort), currentSize, guard = trueExpr)
     }
 }

usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt

@@ -60,7 +60,7 @@ interface UArrayRegion<ArrayType, Sort : USort, USizeSort : USort> : UMemoryRegi
         address: UConcreteHeapAddress,
         arrayType: ArrayType,
         sort: Sort,
-        content: Map<UExpr<USizeSort>, UExpr<Sort>>,
+        content: List<UExpr<Sort>>,
         operationGuard: UBoolExpr,
         ownership: MutabilityOwnership,
     ): UArrayRegion<ArrayType, Sort, USizeSort>
@@ -192,7 +192,7 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
         address: UConcreteHeapAddress,
         arrayType: ArrayType,
         sort: Sort,
-        content: Map<UExpr<USizeSort>, UExpr<Sort>>,
+        content: List<UExpr<Sort>>,
         operationGuard: UBoolExpr,
         ownership: MutabilityOwnership,
     ): UArrayMemoryRegion<ArrayType, Sort, USizeSort> {