fix set iterator

UnitTestBot · Aug 28, 2024 · 0afeba3 · 0afeba3
1 parent 6d98a69
commit 0afeba3
Show file tree

Hide file tree

Showing 10 changed files with 25 additions and 23 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt
@@ -22,7 +22,7 @@ interface UMocker<Method> : UMockEvaluator {
         sort: Sort,
         ownership: MutabilityOwnership,
     ): UMockSymbol<Sort>
-    val trackedLiterals: Collection<TrackedLiteral>
+    val trackedLiterals: Sequence<TrackedLiteral>
 
     fun <Sort : USort> createMockSymbol(
         trackedLiteral: TrackedLiteral?,
@@ -56,8 +56,8 @@ class UIndexedMocker<Method>(
 
     override fun <Sort : USort> eval(symbol: UMockSymbol<Sort>): UExpr<Sort> = symbol
 
-    override val trackedLiterals: Collection<TrackedLiteral>
-        get() = trackedSymbols.keys().asSequence().toList()
+    override val trackedLiterals: Sequence<TrackedLiteral>
+        get() = trackedSymbols.keys
 
     /**
      * Creates a mock symbol. If [trackedLiteral] is not null, created expression

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegion.kt
@@ -366,7 +366,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         write: (R, DstKeyId, UExpr<ValueSort>, UBoolExpr) -> R
     ) = mergeAllocatedKeys(
         initial,
-        inputMapWithAllocatedKeys.keys().asSequence().toList(),
+        inputMapWithAllocatedKeys.keys,
         guard,
         keySet,
         srcMapRef,
@@ -386,7 +386,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         write: (R, DstKeyId, UExpr<ValueSort>, UBoolExpr) -> R
     ) = mergeAllocatedKeys(
         initial,
-        allocatedMapWithAllocatedKeys.keys().asSequence().filter { it.mapAddress == srcMapRef.address }.toList(),
+        allocatedMapWithAllocatedKeys.keys.filter { it.mapAddress == srcMapRef.address },
         guard,
         keySet,
         srcMapRef,
@@ -398,7 +398,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
 
     private inline fun <R, SrcKeyId, DstKeyId> mergeAllocatedKeys(
         initial: R,
-        keys: Iterable<SrcKeyId>,
+        keys: Sequence<SrcKeyId>,
         guard: UBoolExpr,
         keySet: URefSetRegion<MapType>,
         srcMapRef: UHeapRef,

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt
@@ -32,7 +32,7 @@ abstract class USetModelRegion<SetType, ElementSort : USort, Reg : Region<Reg>>(
         check(inputSet.constValue.isFalse) { "Set model is not complete" }
 
         val result = UPrimitiveSetEntries<SetType, ElementSort, Reg>()
-        inputSet.values.keys().forEach {
+        inputSet.values.keys.forEach {
             if (it.first == setRef) {
                 result.add(USetEntryLValue(elementSort, setRef, it.second, setType, elementInfo))
             }

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt
@@ -29,7 +29,7 @@ abstract class URefSetModelRegion<SetType>(
         check(inputSet.constValue.isFalse) { "Set model is not complete" }
 
         val result = URefSetEntries<SetType>()
-        inputSet.values.keys().forEach {
+        inputSet.values.keys.forEach {
             if (it.first == setRef) {
                 result.add(URefSetEntryLValue(setRef, it.second, regionId.setType))
             }

diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt
@@ -347,7 +347,7 @@ internal class URefSetMemoryRegion<SetType>(
         write: (R, DstKeyId, UBoolExpr, UBoolExpr) -> R
     ) = unionAllocatedElements(
         initial,
-        inputSetWithAllocatedElements.keys().asSequence().toList(),
+        inputSetWithAllocatedElements.keys,
         guard,
         read,
         { mkDstKeyId(it.elementAddress) },
@@ -363,7 +363,7 @@ internal class URefSetMemoryRegion<SetType>(
         write: (R, DstKeyId, UBoolExpr, UBoolExpr) -> R
     ) = unionAllocatedElements(
         initial,
-        allocatedSetWithAllocatedElements.keys().asSequence().filter { it.setAddress == srcAddress }.toList(),
+        allocatedSetWithAllocatedElements.keys.filter { it.setAddress == srcAddress },
         guard,
         read,
         { mkDstKeyId(it.elementAddress) },
@@ -372,7 +372,7 @@ internal class URefSetMemoryRegion<SetType>(
 
     private inline fun <R, SrcKeyId, DstKeyId> unionAllocatedElements(
         initial: R,
-        keys: Iterable<SrcKeyId>,
+        keys: Sequence<SrcKeyId>,
         guard: UBoolExpr,
         read: (SrcKeyId) -> UBoolExpr,
         mkDstKeyId: (SrcKeyId) -> DstKeyId,
@@ -391,7 +391,7 @@ internal class URefSetMemoryRegion<SetType>(
             initial = URefSetEntries(),
             initialGuard = ref.uctx.trueExpr,
             blockOnConcrete = { entries, (concreteRef, _) ->
-                allocatedSetWithAllocatedElements.keys().forEach { entry ->
+                allocatedSetWithAllocatedElements.keys.forEach { entry ->
                     if (entry.setAddress == concreteRef.address) {
                         val elem = ref.uctx.mkConcreteHeapRef(entry.elementAddress)
                         entries.add(URefSetEntryLValue(concreteRef, elem, setType))
@@ -413,7 +413,7 @@ internal class URefSetMemoryRegion<SetType>(
                 entries
             },
             blockOnSymbolic = { entries, (symbolicRef, _) ->
-                inputSetWithAllocatedElements.keys().forEach { entry ->
+                inputSetWithAllocatedElements.keys.forEach { entry ->
                     val elem = ref.uctx.mkConcreteHeapRef(entry.elementAddress)
                     entries.add(URefSetEntryLValue(symbolicRef, elem, setType))
                 }

diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
@@ -187,8 +187,8 @@ class UMemory<Type, Method>(
         otherOwnership: MutabilityOwnership,
         mergedOwnership: MutabilityOwnership,
     ): UMemory<Type, Method>? {
-        val ids = regions.keys().asSequence().toList()
-        val otherIds = other.regions.keys().asSequence().toList()
+        val ids = regions.keys.toList()
+        val otherIds = other.regions.keys.toList()
         if (ids != otherIds) {
             return null
         }

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt
@@ -80,11 +80,11 @@ internal class JcStaticFieldsMemoryRegion<Sort : USort>(
     fun mutatePrimitiveStaticFieldValuesToSymbolic(enclosingClass: JcClassOrInterface, ownership: MutabilityOwnership) {
         val staticFields = fieldValuesByClass[enclosingClass] ?: return
 
-        val staticsToRemove = staticFields
-            .keys()
-            .filter { fieldShouldBeSymbolic(it) }
+        val staticsToRemove = staticFields.keys.filter { fieldShouldBeSymbolic(it) }
 
-        initialStatics = initialStatics.addAll(staticsToRemove)
+        for (static in staticsToRemove) {
+            initialStatics = initialStatics.add(static)
+        }
 
         // Remove concrete fields from the region
         val updatedStaticFields = staticsToRemove.fold(staticFields) { acc, field ->

diff --git a/...l/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt b/...l/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt
@@ -873,7 +873,7 @@ class TrieNode<K, V>(
         }
     }
 
-    fun keys() = UPersistentHashMapKeysIterator(this) as Iterator<K>
+    val keys: Sequence<K> get() = UPersistentHashMapKeysIterator(this).asSequence()
 
     fun isEmpty() = firstOrNull() == null
     fun isNotEmpty() = firstOrNull() != null

diff --git a/...l/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/TrieNode.kt b/...l/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/TrieNode.kt
@@ -542,7 +542,7 @@ class TrieNode<E>(
                     thisIsNode -> @Suppress("UNCHECKED_CAST") {
                         thisCell as TrieNode<E>
                         otherNodeCell as E
-                        val oldCounter = this.calculateSize()
+                        val oldCounter = mutableRemovesCount
                         val removed = thisCell.mutableRemove(
                                 otherNodeCell.hashCode(),
                                 otherNodeCell,
@@ -695,8 +695,8 @@ class TrieNode<E>(
         return this
     }
 
-    fun isEmpty() = singleOrNull() == null
-    fun isNotEmpty() = singleOrNull() != null
+    fun isEmpty() = firstOrNull() == null
+    fun isNotEmpty() = firstOrNull() != null
 
     fun remove(element: E, owner: MutabilityOwnership): TrieNode<E> =
         mutableRemove(element.hashCode(), element, 0, owner)

diff --git a/...org/usvm/collections/immutable/implementations/immutableSet/UPersistentHashSetIterator.kt b/...org/usvm/collections/immutable/implementations/immutableSet/UPersistentHashSetIterator.kt
@@ -56,10 +56,12 @@ internal open class UPersistentHashSetIterator<E>(node: TrieNode<E>) : Iterator<
     }
 
     override fun hasNext(): Boolean {
+        ensureNextElementIsReady()
         return hasNext
     }
 
     override fun next(): E {
+        ensureNextElementIsReady()
         if (!hasNext)
             throw NoSuchElementException()