linter warnings fixes

UnitTestBot · Jul 22, 2024 · 1079834 · 1079834
1 parent 1b433cb
commit 1079834
Show file tree

Hide file tree

Showing 71 changed files with 376 additions and 273 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt
@@ -2,8 +2,8 @@ package org.usvm
 
 import io.ksmt.utils.cast
 import kotlinx.collections.immutable.PersistentList
-import org.usvm.collections.immutable.persistentHashMapOf
 import kotlinx.collections.immutable.persistentListOf
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.merging.MergeGuard
@@ -77,7 +77,9 @@ class UIndexedMocker<Method>(
     }
 
     override fun clone(thisOwnership: MutabilityOwnership, cloneOwnership: MutabilityOwnership): UIndexedMocker<Method> =
-        UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols, cloneOwnership).also { ownership = thisOwnership }
+        UIndexedMocker(
+            methodMockClauses, trackedSymbols, untrackedSymbols, cloneOwnership
+        ).also { ownership = thisOwnership }
 
     /**
      * Check if this [UIndexedMocker] can be merged with [other] indexed mocker.
@@ -91,7 +93,7 @@ class UIndexedMocker<Method>(
         by: MergeGuard,
         thisOwnership: MutabilityOwnership,
         otherOwnership: MutabilityOwnership,
-        mergedOwnership: MutabilityOwnership
+        mergedOwnership: MutabilityOwnership,
     ): UIndexedMocker<Method>? {
         if (methodMockClauses !== other.methodMockClauses
             || trackedSymbols !== other.trackedSymbols

diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt
@@ -13,7 +13,7 @@ typealias StateId = UInt
 abstract class UState<Type, Method, Statement, Context, Target, State>(
     // TODO: add interpreter-specific information
     val ctx: Context,
-    initOwnership : MutabilityOwnership,
+    initOwnership: MutabilityOwnership,
     open val callStack: UCallStack<Method, Statement>,
     open val pathConstraints: UPathConstraints<Type>,
     open val memory: UMemory<Type, Method>,

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt
@@ -10,6 +10,8 @@ import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.UWritableMemory
 import org.usvm.collection.array.UArrayIndexLValue
 import org.usvm.collection.array.length.UArrayLengthLValue
+import org.usvm.collection.array.memcpy as memcpyInternal
+import org.usvm.collection.array.memset as memsetInternal
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.collection.set.primitive.USetEntryLValue
 import org.usvm.collection.set.ref.URefSetEntryLValue
@@ -21,8 +23,6 @@ import org.usvm.regions.Region
 import org.usvm.types.UTypeStream
 import org.usvm.uctx
 import org.usvm.withSizeSort
-import org.usvm.collection.array.memcpy as memcpyInternal
-import org.usvm.collection.array.memset as memsetInternal
 import org.usvm.collection.array.allocateArray as allocateArrayInternal
 import org.usvm.collection.array.allocateArrayInitialized as allocateArrayInitializedInternal
 
@@ -88,7 +88,7 @@ fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayType>.mems
     type: ArrayType,
     sort: Sort,
     sizeSort: USizeSort,
-    contents: Sequence<UExpr<Sort>>,
+    contents: Sequence<UExpr<Sort>>
 ) {
     memsetInternal(ref, type, sort, sizeSort, contents)
 }

diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt
@@ -158,7 +158,6 @@ object ListCollectionApi {
         srcFrom: UExpr<USizeSort>,
         dstFrom: UExpr<USizeSort>,
         length: UExpr<USizeSort>,
-
     ) {
         memory.memcpy(
             srcRef = srcRef,

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt
@@ -66,25 +66,28 @@ interface UArrayRegion<ArrayType, Sort : USort, USizeSort : USort> : UMemoryRegi
 
 internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
     private var allocatedArrays: UPersistentHashMap<UConcreteHeapAddress, UAllocatedArray<ArrayType, Sort, USizeSort>> = persistentHashMapOf(),
-    private var inputArray: UInputArray<ArrayType, Sort, USizeSort>? = null
+    private var inputArray: UInputArray<ArrayType, Sort, USizeSort>? = null,
 ) : UArrayRegion<ArrayType, Sort, USizeSort> {
 
     private fun getAllocatedArray(
         arrayType: ArrayType,
         sort: Sort,
         address: UConcreteHeapAddress,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ): UAllocatedArray<ArrayType, Sort, USizeSort> {
-        val (updatedArrays, collection) = 
-            allocatedArrays.getOrPut(address, UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address).emptyRegion(), ownership)
+        val (updatedArrays, collection) = allocatedArrays.getOrPut(
+            address,
+            UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address).emptyRegion(),
+            ownership
+        )
         allocatedArrays = updatedArrays
         return collection
     }
 
     private fun updateAllocatedArray(
         ref: UConcreteHeapAddress,
         updated: UAllocatedArray<ArrayType, Sort, USizeSort>,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ) = UArrayMemoryRegion(allocatedArrays.put(ref, updated, ownership), inputArray)
 
     private fun getInputArray(arrayType: ArrayType, sort: Sort): UInputArray<ArrayType, Sort, USizeSort> {
@@ -96,16 +99,21 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
     private fun updateInput(updated: UInputArray<ArrayType, Sort, USizeSort>) =
         UArrayMemoryRegion(allocatedArrays, updated)
 
-    override fun read(key: UArrayIndexLValue<ArrayType, Sort, USizeSort>, ownership: MutabilityOwnership): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
-        concreteMapper = { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address, ownership).read(key.index, ownership) },
-        symbolicMapper = { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index, ownership) }
-    )
+    override fun read(key: UArrayIndexLValue<ArrayType, Sort, USizeSort>, ownership: MutabilityOwnership): UExpr<Sort> =
+        key.ref.mapWithStaticAsSymbolic(
+            concreteMapper = { concreteRef ->
+                getAllocatedArray(key.arrayType, key.sort, concreteRef.address, ownership).read(key.index, ownership)
+            },
+            symbolicMapper = { symbolicRef ->
+                getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index, ownership)
+            }
+        )
 
     override fun write(
         key: UArrayIndexLValue<ArrayType, Sort, USizeSort>,
         value: UExpr<Sort>,
         guard: UBoolExpr,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ): UMemoryRegion<UArrayIndexLValue<ArrayType, Sort, USizeSort>, Sort> = foldHeapRefWithStaticAsSymbolic(
         key.ref,
         initial = this,
@@ -191,7 +199,7 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
         sort: Sort,
         content: Map<UExpr<USizeSort>, UExpr<Sort>>,
         operationGuard: UBoolExpr,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ): UArrayMemoryRegion<ArrayType, Sort, USizeSort> {
         val arrayId = UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address)
         val newCollection = arrayId.initializedArray(content, operationGuard)

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt
@@ -36,7 +36,7 @@ internal fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayT
     type: ArrayType,
     elementSort: Sort,
     sizeSort: USizeSort,
-    contents: Sequence<UExpr<Sort>>,
+    contents: Sequence<UExpr<Sort>>
 ): UConcreteHeapRef = elementSort.uctx.withSizeSort {
     val arrayValues = hashMapOf<UExpr<USizeSort>, UExpr<Sort>>()
     contents.forEachIndexed { idx, value -> arrayValues[mkSizeExpr(idx)] = value }
@@ -96,7 +96,7 @@ internal fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayT
         fromSrcIdx = mkSizeExpr(0),
         fromDstIdx = mkSizeExpr(0),
         toDstIdx = contentLength,
-        guard = trueExpr,
+        guard = trueExpr
     )
 
     write(UArrayLengthLValue(ref, type, sizeSort), contentLength, guard = trueExpr)

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt
@@ -42,7 +42,7 @@ class UAllocatedArrayId<ArrayType, Sort : USort, USizeSort : USort> internal con
     override fun instantiate(
         collection: USymbolicCollection<UAllocatedArrayId<ArrayType, Sort, USizeSort>, UExpr<USizeSort>, Sort>,
         key: UExpr<USizeSort>,
-        composer: UComposer<*, *>?,
+        composer: UComposer<*, *>?
     ): UExpr<Sort> {
         if (collection.updates.isEmpty()) {
             return composer.compose(defaultValue)
@@ -123,7 +123,7 @@ class UInputArrayId<ArrayType, Sort : USort, USizeSort : USort> internal constru
     override fun instantiate(
         collection: USymbolicCollection<UInputArrayId<ArrayType, Sort, USizeSort>, USymbolicArrayIndex<USizeSort>, Sort>,
         key: USymbolicArrayIndex<USizeSort>,
-        composer: UComposer<*, *>?,
+        composer: UComposer<*, *>?
     ): UExpr<Sort> {
         if (composer == null) {
             return sort.uctx.withSizeSort<USizeSort>().mkInputArrayReading(collection, key.first, key.second)

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt
@@ -63,13 +63,13 @@ internal class UArrayLengthsMemoryRegion<ArrayType, USizeSort : USort>(
         key.ref.mapWithStaticAsSymbolic(
             concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
             symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef, ownership) }
-    )
+        )
 
     override fun write(
         key: UArrayLengthLValue<ArrayType, USizeSort>,
         value: UExpr<USizeSort>,
         guard: UBoolExpr,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ) = foldHeapRefWithStaticAsSymbolic(
         key.ref,
         initial = this,

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt
@@ -56,16 +56,17 @@ internal class UFieldsMemoryRegion<Field, Sort : USort>(
     private fun updateInput(updated: UInputFields<Field, Sort>) =
         UFieldsMemoryRegion(sort, field, allocatedFields, updated)
 
-    override fun read(key: UFieldLValue<Field, Sort>, ownership: MutabilityOwnership): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
-        concreteMapper = { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
-        symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef, ownership) }
-    )
+    override fun read(key: UFieldLValue<Field, Sort>, ownership: MutabilityOwnership): UExpr<Sort> =
+        key.ref.mapWithStaticAsSymbolic(
+            concreteMapper = { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
+            symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef, ownership) }
+        )
 
     override fun write(
         key: UFieldLValue<Field, Sort>,
         value: UExpr<Sort>,
         guard: UBoolExpr,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ): UMemoryRegion<UFieldLValue<Field, Sort>, Sort> = foldHeapRefWithStaticAsSymbolic(
         key.ref,
         initial = this,

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegion.kt
@@ -64,13 +64,13 @@ internal class UMapLengthMemoryRegion<MapType, USizeSort : USort>(
         key.ref.mapWithStaticAsSymbolic(
             concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
             symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef, ownership) }
-    )
+        )
 
     override fun write(
         key: UMapLengthLValue<MapType, USizeSort>,
         value: UExpr<USizeSort>,
         guard: UBoolExpr,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.ref,
         initial = this,

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapModelRegion.kt
@@ -15,7 +15,10 @@ abstract class UMapModelRegion<MapType, KeySort : USort, ValueSort : USort, Reg
 ) : UReadOnlyMemoryRegion<UMapEntryLValue<MapType, KeySort, ValueSort, Reg>, ValueSort> {
     abstract val inputMap: UReadOnlyMemoryRegion<USymbolicMapKey<KeySort>, ValueSort>
 
-    override fun read(key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>, ownership: MutabilityOwnership): UExpr<ValueSort> {
+    override fun read(
+        key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>,
+        ownership: MutabilityOwnership,
+    ): UExpr<ValueSort> {
         val mapRef = modelEnsureConcreteInputRef(key.mapRef)
         return inputMap.read(mapRef to key.mapKey, ownership)
     }

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt
@@ -80,17 +80,17 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
 
     private fun getAllocatedMap(
         id: UAllocatedMapId<MapType, KeySort, ValueSort, Reg>,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ): UAllocatedMap<MapType, KeySort, ValueSort, Reg> {
-        val (updatesMaps, collection) =  allocatedMaps.getOrPut(id, id.emptyRegion(), ownership)
+        val (updatesMaps, collection) = allocatedMaps.getOrPut(id, id.emptyRegion(), ownership)
         allocatedMaps = updatesMaps
         return collection
     }
 
     private fun updateAllocatedMap(
         id: UAllocatedMapId<MapType, KeySort, ValueSort, Reg>,
         updatedMap: UAllocatedMap<MapType, KeySort, ValueSort, Reg>,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ) = UMapMemoryRegion(
         keySort,
         valueSort,
@@ -119,7 +119,7 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
 
     override fun read(
         key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ): UExpr<ValueSort> =
         key.mapRef.mapWithStaticAsSymbolic(
             concreteMapper = { concreteRef ->
@@ -133,7 +133,7 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
         key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>,
         value: UExpr<ValueSort>,
         guard: UBoolExpr,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.mapRef,
         initial = this,
@@ -157,7 +157,7 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
         mapType: MapType,
         srcKeySet: USetRegion<MapType, KeySort, *>,
         initialGuard: UBoolExpr,
-        ownership: MutabilityOwnership
+        ownership: MutabilityOwnership,
     ) = foldHeapRef2(
         ref0 = srcRef,
         ref1 = dstRef,

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt
@@ -6,7 +6,6 @@ import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.collection.set.primitive.USetRegion
 import org.usvm.collection.set.primitive.USetRegionId
-import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.USymbolicCollectionKeyInfo
 import org.usvm.memory.UWritableMemory
 import org.usvm.regions.Region

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionTranslator.kt
@@ -154,7 +154,7 @@ private class UInputMapUpdatesTranslator<KeySort : USort, ValueSort : USort>(
 ) : U2DUpdatesTranslator<UAddressSort, KeySort, ValueSort>(exprTranslator, initialValue) {
     override fun KContext.translateRangedUpdate(
         previous: KExpr<KArray2Sort<UAddressSort, KeySort, ValueSort>>,
-        update: URangedUpdateNode<*, *, USymbolicMapKey<KeySort>, ValueSort>,
+        update: URangedUpdateNode<*, *, USymbolicMapKey<KeySort>, ValueSort>
     ): KExpr<KArray2Sort<UAddressSort, KeySort, ValueSort>> {
         check(update.adapter is USymbolicMapMergeAdapter<*, *, USymbolicMapKey<KeySort>, *>) {
             "Unexpected adapter: ${update.adapter}"
@@ -165,7 +165,7 @@ private class UInputMapUpdatesTranslator<KeySort : USort, ValueSort : USort>(
             previous,
             update,
             update.sourceCollection as USymbolicCollection<USymbolicCollectionId<Any, ValueSort, *>, Any, ValueSort>,
-            update.adapter as USymbolicMapMergeAdapter<*, Any, USymbolicMapKey<KeySort>, *>,
+            update.adapter as USymbolicMapMergeAdapter<*, Any, USymbolicMapKey<KeySort>, *>
         )
     }
 

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt
@@ -63,7 +63,7 @@ class UAllocatedToAllocatedSymbolicMapMergeAdapter<MapType, KeySort : USort>(
         dstCollectionId: USymbolicCollectionId<UExpr<KeySort>, *, *>,
         guard: UBoolExpr,
         srcKey: UExpr<KeySort>,
-        composer: UComposer<*, *>
+        composer: UComposer<*, *>,
     ) {
         check(srcCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $srcCollectionId" }
         check(dstCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $dstCollectionId" }
@@ -114,7 +114,7 @@ class UAllocatedToInputSymbolicMapMergeAdapter<MapType, KeySort : USort>(
         dstCollectionId: USymbolicCollectionId<USymbolicMapKey<KeySort>, *, *>,
         guard: UBoolExpr,
         srcKey: UExpr<KeySort>,
-        composer: UComposer<*, *>
+        composer: UComposer<*, *>,
     ) {
         check(srcCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $srcCollectionId" }
         check(dstCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $dstCollectionId" }
@@ -166,7 +166,7 @@ class UInputToAllocatedSymbolicMapMergeAdapter<MapType, KeySort : USort>(
         dstCollectionId: USymbolicCollectionId<UExpr<KeySort>, *, *>,
         guard: UBoolExpr,
         srcKey: USymbolicMapKey<KeySort>,
-        composer: UComposer<*, *>
+        composer: UComposer<*, *>,
     ) {
         check(srcCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $srcCollectionId" }
         check(dstCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $dstCollectionId" }
@@ -219,7 +219,7 @@ class UInputToInputSymbolicMapMergeAdapter<MapType, KeySort : USort>(
         dstCollectionId: USymbolicCollectionId<USymbolicMapKey<KeySort>, *, *>,
         guard: UBoolExpr,
         srcKey: USymbolicMapKey<KeySort>,
-        composer: UComposer<*, *>
+        composer: UComposer<*, *>,
     ) {
         check(srcCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $srcCollectionId" }
         check(dstCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $dstCollectionId" }