From 0afeba39f6dcdb1742a471ff0f2d19446026f35c Mon Sep 17 00:00:00 2001 From: Roman Pozharskiy Date: Wed, 28 Aug 2024 16:57:47 +0300 Subject: [PATCH] fix set iterator --- usvm-core/src/main/kotlin/org/usvm/Mocks.kt | 6 +++--- .../org/usvm/collection/map/ref/URefMapRegion.kt | 6 +++--- .../usvm/collection/set/primitive/USetModelRegion.kt | 2 +- .../org/usvm/collection/set/ref/URefSetModelRegion.kt | 2 +- .../org/usvm/collection/set/ref/URefSetRegion.kt | 10 +++++----- usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt | 4 ++-- .../interpreter/statics/JcStaticFieldsRegion.kt | 8 ++++---- .../immutable/implementations/immutableMap/TrieNode.kt | 2 +- .../immutable/implementations/immutableSet/TrieNode.kt | 6 +++--- .../immutableSet/UPersistentHashSetIterator.kt | 2 ++ 10 files changed, 25 insertions(+), 23 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt index 81110a690c..f2915f0f93 100644 --- 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 : UMockEvaluator { sort: Sort, ownership: MutabilityOwnership, ): UMockSymbol - val trackedLiterals: Collection + val trackedLiterals: Sequence fun createMockSymbol( trackedLiteral: TrackedLiteral?, @@ -56,8 +56,8 @@ class UIndexedMocker( override fun eval(symbol: UMockSymbol): UExpr = symbol - override val trackedLiterals: Collection - get() = trackedSymbols.keys().asSequence().toList() + override val trackedLiterals: Sequence + 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 index 4d8da873a6..2ea6a557ec 100644 --- 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( write: (R, DstKeyId, UExpr, UBoolExpr) -> R ) = mergeAllocatedKeys( initial, - inputMapWithAllocatedKeys.keys().asSequence().toList(), + inputMapWithAllocatedKeys.keys, guard, keySet, srcMapRef, @@ -386,7 +386,7 @@ internal class URefMapMemoryRegion( write: (R, DstKeyId, UExpr, 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( private inline fun mergeAllocatedKeys( initial: R, - keys: Iterable, + keys: Sequence, guard: UBoolExpr, keySet: URefSetRegion, 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 index 114a1b306b..36ac911376 100644 --- 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>( check(inputSet.constValue.isFalse) { "Set model is not complete" } val result = UPrimitiveSetEntries() - 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 index 71a14adf64..36c8df5ff9 100644 --- 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( check(inputSet.constValue.isFalse) { "Set model is not complete" } val result = URefSetEntries() - 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 index 58d47425ef..a11e3f2c50 100644 --- 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( 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( 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( private inline fun unionAllocatedElements( initial: R, - keys: Iterable, + keys: Sequence, guard: UBoolExpr, read: (SrcKeyId) -> UBoolExpr, mkDstKeyId: (SrcKeyId) -> DstKeyId, @@ -391,7 +391,7 @@ internal class URefSetMemoryRegion( 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( 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 index 687f4516d0..bc8ae87e7b 100644 --- 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( otherOwnership: MutabilityOwnership, mergedOwnership: MutabilityOwnership, ): UMemory? { - 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 index 5cbe8e21c4..9baf30432d 100644 --- 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( 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/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt index e987126ae1..9985dfd61e 100644 --- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt +++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt @@ -873,7 +873,7 @@ class TrieNode( } } - fun keys() = UPersistentHashMapKeysIterator(this) as Iterator + val keys: Sequence get() = UPersistentHashMapKeysIterator(this).asSequence() fun isEmpty() = firstOrNull() == null fun isNotEmpty() = firstOrNull() != null diff --git a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/TrieNode.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/TrieNode.kt index a1d4412e76..c8ae3a18a7 100644 --- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/TrieNode.kt +++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/TrieNode.kt @@ -542,7 +542,7 @@ class TrieNode( thisIsNode -> @Suppress("UNCHECKED_CAST") { thisCell as TrieNode otherNodeCell as E - val oldCounter = this.calculateSize() + val oldCounter = mutableRemovesCount val removed = thisCell.mutableRemove( otherNodeCell.hashCode(), otherNodeCell, @@ -695,8 +695,8 @@ class TrieNode( 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 = mutableRemove(element.hashCode(), element, 0, owner) diff --git a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/UPersistentHashSetIterator.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/UPersistentHashSetIterator.kt index f630375fdd..fb580f6920 100644 --- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/UPersistentHashSetIterator.kt +++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableSet/UPersistentHashSetIterator.kt @@ -56,10 +56,12 @@ internal open class UPersistentHashSetIterator(node: TrieNode) : Iterator< } override fun hasNext(): Boolean { + ensureNextElementIsReady() return hasNext } override fun next(): E { + ensureNextElementIsReady() if (!hasNext) throw NoSuchElementException()