Fixes for bugs found during approximations testing

buildSrc/build.gradle.kts

@@ -17,4 +17,4 @@ dependencies {
     implementation("org.jetbrains.kotlin:kotlin-gradle-plugin:$kotlinVersion")
     implementation("io.gitlab.arturbosch.detekt:detekt-gradle-plugin:$detektVersion")
     implementation("org.glavo:gjavah:$gjavahVersion")
-}
+}

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

@@ -1,22 +1,12 @@
 package org.usvm.api.collection
 
-import org.usvm.StepScope
-import org.usvm.UContext
-import org.usvm.UExpr
-import org.usvm.UHeapRef
-import org.usvm.USort
-import org.usvm.UState
+import org.usvm.*
 import org.usvm.api.memcpy
 import org.usvm.api.readArrayIndex
 import org.usvm.api.readArrayLength
 import org.usvm.api.writeArrayIndex
 import org.usvm.api.writeArrayLength
 import org.usvm.memory.mapWithStaticAsConcrete
-import org.usvm.mkSizeAddExpr
-import org.usvm.mkSizeExpr
-import org.usvm.mkSizeGeExpr
-import org.usvm.mkSizeSubExpr
-import org.usvm.sizeSort
 import org.usvm.utils.logAssertFailure
 
 object ListCollectionApi {
@@ -150,7 +140,12 @@ object ListCollectionApi {
         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 +154,7 @@ object ListCollectionApi {
         dstFrom: UExpr<USizeSort>,
         length: UExpr<USizeSort>,
     ) {
+        // Copying contents
         memory.memcpy(
             srcRef = srcRef,
             dstRef = dstRef,
@@ -168,5 +164,11 @@ object ListCollectionApi {
             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/collection/map/ref/URefMapRegion.kt

@@ -172,7 +172,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                     symbolicMapper = { symbolicKey ->
                         val id = allocatedMapWithInputKeyId(concreteRef.address)
                         getAllocatedMapWithInputKeys(id).read(symbolicKey)
-                    }
+                    }, ignoreNullRefs = false
                 )
             },
             symbolicMapper = { symbolicRef ->
@@ -183,7 +183,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                     },
                     symbolicMapper = { symbolicKey ->
                         getInputMapWithInputKeys().read(symbolicRef to symbolicKey)
-                    }
+                    }, ignoreNullRefs = false
                 )
             }
         )
@@ -214,8 +214,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                     val newMap = region.getAllocatedMapWithInputKeys(id)
                         .write(symbolicKeyRef, value, guard, ownership)
                     region.updateAllocatedMapWithInputKeys(id, newMap, ownership)
-                }
-            )
+                }, ignoreNullRefs = false)
         },
         blockOnSymbolic = { mapRegion, (symbolicMapRef, mapGuard) ->
             foldHeapRefWithStaticAsSymbolic(
@@ -232,9 +231,9 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                     val newMap = region.getInputMapWithInputKeys()
                         .write(symbolicMapRef to symbolicKeyRef, value, guard, ownership)
                     region.updateInputMapWithInputKeys(newMap)
-                }
+                }, ignoreNullRefs = false
             )
-        }
+        }, ignoreNullRefs = false
     )
 
     /**
@@ -354,7 +353,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
             val adapter = UInputToInputSymbolicRefMapMergeAdapter(srcSymbolic, dstSymbolic, srcKeys)
             val updatedDstCollection = dstInputKeysCollection.copyRange(srcInputKeysCollection, adapter, guard)
             updatedRegion.updateInputMapWithInputKeys(updatedDstCollection)
-        },
+        }, ignoreNullRefs = false
     )
 
     private inline fun <R, DstKeyId> mergeInputMapAllocatedKeys(

usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt

@@ -178,7 +178,8 @@ internal class URefSetMemoryRegion<SetType>(
                     { symbolicElem ->
                         val id = allocatedSetWithInputElementsId(concreteRef.address)
                         getAllocatedSetWithInputElements(id).read(symbolicElem)
-                    }
+                    },
+                    ignoreNullRefs = false
                 )
             },
             { symbolicRef ->
@@ -189,7 +190,8 @@ internal class URefSetMemoryRegion<SetType>(
                     },
                     { symbolicElem ->
                         inputSetWithInputElements().read(symbolicRef to symbolicElem)
-                    }
+                    },
+                    ignoreNullRefs = false
                 )
             }
         )
@@ -220,8 +222,7 @@ internal class URefSetMemoryRegion<SetType>(
                     val newMap = region.getAllocatedSetWithInputElements(id)
                         .write(symbolicElemRef, value, guard, ownership)
                     region.updateAllocatedSetWithInputElements(id, newMap, ownership)
-                }
-            )
+                }, ignoreNullRefs = false)
         },
         blockOnSymbolic = { setRegion, (symbolicSetRef, setGuard) ->
             foldHeapRefWithStaticAsSymbolic(
@@ -238,9 +239,9 @@ internal class URefSetMemoryRegion<SetType>(
                     val newMap = region.inputSetWithInputElements()
                         .write(symbolicSetRef to symbolicElemRef, value, guard, ownership)
                     region.updateInputSetWithInputElements(newMap)
-                }
+                }, ignoreNullRefs = false
             )
-        }
+        }, ignoreNullRefs = false
     )
 
     override fun union(
@@ -337,7 +338,7 @@ internal class URefSetMemoryRegion<SetType>(
             val adapter = UInputToInputSymbolicRefSetUnionAdapter(srcSymbolic, dstSymbolic, srcCollection)
             val updated = dstCollection.copyRange(srcCollection, adapter, guard)
             updatedRegion.updateInputSetWithInputElements(updated)
-        },
+        }, ignoreNullRefs = false
     )
 
     private inline fun <R, DstKeyId> unionInputSetAllocatedElements(
@@ -427,6 +428,6 @@ internal class URefSetMemoryRegion<SetType>(
                 entries.markAsInput()
 
                 entries
-            }
+            }, ignoreNullRefs = false
         )
 }

usvm-jvm/build.gradle.kts

@@ -116,7 +116,6 @@ tasks.withType<Test> {
     environment("usvm.jvm.test.samples.approximations", testSamplesWithApproximations.asPath)
 }
 
-
 tasks {
     register<Jar>("testJar") {
         group = "jar"

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

@@ -2,9 +2,7 @@ package org.usvm.machine
 
 import io.ksmt.utils.asExpr
 import io.ksmt.utils.uncheckedCast
-import org.jacodb.api.jvm.JcArrayType
-import org.jacodb.api.jvm.JcMethod
-import org.jacodb.api.jvm.JcType
+import org.jacodb.api.jvm.*
 import org.jacodb.api.jvm.ext.boolean
 import org.jacodb.api.jvm.ext.byte
 import org.jacodb.api.jvm.ext.char
@@ -26,10 +24,7 @@ import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UFpSort
 import org.usvm.UHeapRef
-import org.usvm.api.Engine
-import org.usvm.api.SymbolicIdentityMap
-import org.usvm.api.SymbolicList
-import org.usvm.api.SymbolicMap
+import org.usvm.api.*
 import org.usvm.api.collection.ListCollectionApi.ensureListSizeCorrect
 import org.usvm.api.collection.ListCollectionApi.mkSymbolicList
 import org.usvm.api.collection.ListCollectionApi.symbolicListCopyRange
@@ -47,12 +42,6 @@ import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapMergeInto
 import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapPut
 import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapRemove
 import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapSize
-import org.usvm.api.makeSymbolicPrimitive
-import org.usvm.api.makeSymbolicRef
-import org.usvm.api.makeSymbolicRefWithSameType
-import org.usvm.api.mapTypeStream
-import org.usvm.api.memcpy
-import org.usvm.api.objectTypeEquals
 import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.machine.interpreter.JcExprResolver
@@ -70,7 +59,6 @@ import kotlin.reflect.KFunction0
 import kotlin.reflect.KFunction1
 import kotlin.reflect.KFunction2
 import kotlin.reflect.jvm.javaMethod
-import org.usvm.api.makeNullableSymbolicRefWithSameType
 
 class JcMethodApproximationResolver(
     private val ctx: JcContext,
@@ -89,6 +77,12 @@ class JcMethodApproximationResolver(
     private val usvmApiSymbolicMap by lazy { ctx.cp.findClassOrNull<SymbolicMap<*, *>>() }
     private val usvmApiSymbolicIdentityMap by lazy { ctx.cp.findClassOrNull<SymbolicIdentityMap<*, *>>() }
 
+    @Suppress("RecursivePropertyAccessor")
+    private val JcClassType.allFields: List<JcTypedField>
+        get() = declaredFields + (superType?.allFields ?: emptyList())
+    val JcClassType.allInstanceFields: List<JcTypedField>
+        get() = allFields.filter { !it.isStatic }
+
     fun approximate(scope: JcStepScope, exprResolver: JcExprResolver, callJcInst: JcMethodCall): Boolean = try {
         this.currentScope = scope
         this.currentExprResolver = exprResolver
@@ -142,7 +136,7 @@ class JcMethodApproximationResolver(
         }
 
         if (method.name == "clone" && enclosingClass == ctx.cp.objectClass) {
-            if (approximateArrayClone(methodCall)) return true
+            if (approximateObjectClone(methodCall)) return true
         }
 
         return approximateEmptyNativeMethod(methodCall)
@@ -357,18 +351,41 @@ class JcMethodApproximationResolver(
         scope.forkMulti(arrayTypeConstraintsWithBlockOnStates)
     }
 
-    private fun approximateArrayClone(methodCall: JcMethodCall): Boolean {
+    private fun approximateObjectClone(methodCall: JcMethodCall): Boolean {
         val instance = methodCall.arguments.first().asExpr(ctx.addressSort)
-
-        val arrayType = scope.calcOnState {
-            memory.types.getTypeStream(instance).commonSuperType
+        val type = scope.calcOnState { memory.types.getTypeStream(instance).commonSuperType }
+        if (type is JcArrayType) {
+            exprResolver.resolveArrayClone(methodCall, instance, type)
+            return true
         }
-        if (arrayType !is JcArrayType) {
-            return false
+
+        if (methodCall is JcConcreteMethodCallInst) {
+            type as JcClassType
+            exprResolver.resolveObjectClone(methodCall, instance, type)
+            return true
         }
 
-        exprResolver.resolveArrayClone(methodCall, instance, arrayType)
-        return true
+        return false
+    }
+
+    private fun JcExprResolver.resolveObjectClone(
+        methodCall: JcMethodCall,
+        instance: UHeapRef,
+        type: JcClassType,
+    ) = with(ctx) {
+        scope.doWithState {
+            checkNullPointer(instance) ?: return@doWithState
+
+            val clonedRef = memory.allocHeapRef(type, useStaticAddress = useStaticAddressForAllocation())
+            for (field in type.allInstanceFields) {
+                val fieldSort = ctx.typeToSort(field.type)
+                val jcField = field.field
+                val fieldValue = memory.readField(instance, jcField, fieldSort)
+                memory.writeField(clonedRef, jcField, fieldSort, fieldValue, ctx.trueExpr)
+            }
+
+            skipMethodInvocationWithValue(methodCall, clonedRef)
+        }
     }
 
     private fun JcExprResolver.resolveArrayClone(

usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsDecoderTest.kt

@@ -148,7 +148,6 @@ class ApproximationsDecoderTest : ApproximationsTestRunner() {
     }
 
     @Test
-    @Disabled("Incorrect decoder")
     fun testArrayListDecoder() {
         checkProperties(
             ArrayList_DecoderTests::test_0,