diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt index c873fc2c1c..4add1416a0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt @@ -333,6 +333,6 @@ class UIsExpr internal constructor( //region Utils val UBoolExpr.isFalse get() = this === ctx.falseExpr -val UBoolExpr.isTrue get() = !isFalse +val UBoolExpr.isTrue get() = this === ctx.trueExpr //endregion \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt b/usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt index dc9e595ff7..27a748af27 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt @@ -366,7 +366,7 @@ fun initializedAllocatedArrayRegion( content: Map>, guard: UBoolExpr ): UAllocatedArrayRegion { - val emptyRegionTree = emptyRegionTree, UArrayIndexRegion>() + val emptyRegionTree = emptyRegionTree>() val entries = content.entries.associate { (key, value) -> val region = indexRegion(key) diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt b/usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt index 6933c31951..602cea4643 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt @@ -77,7 +77,7 @@ interface UMemoryUpdates : Sequence> { /** * Accepts the [visitor]. Implementations should call [UMemoryUpdatesVisitor.visitInitialValue] firstly, then call - * [UMemoryUpdatesVisitor.visitUpdateNode] in the chronological order + * [UMemoryUpdatesVisitor.visitUpdate] in the chronological order * (from the oldest to the newest) with accumulated [Result]. * * Uses [lookupCache] to shortcut the traversal. The actual key is determined by the @@ -183,6 +183,11 @@ class UFlatUpdates private constructor( val mappedNode = node.update.map(keyMapper, composer) val mappedNext = node.next.map(keyMapper, composer) + // Doesn't apply the node, if its guard maps to `false` + if (mappedNode.guard.isFalse) { + return mappedNext + } + // If nothing changed, return this updates if (mappedNode === node.update && mappedNext === node.next) { return this @@ -250,7 +255,7 @@ class UFlatUpdates private constructor( //region Tree memory updates data class UTreeUpdates, Sort : USort>( - private val updates: RegionTree, Reg>, + private val updates: RegionTree>, private val keyToRegion: (Key) -> Reg, private val keyRangeToRegion: (Key, Key) -> Reg, private val symbolicEq: (Key, Key) -> UBoolExpr, @@ -259,7 +264,7 @@ data class UTreeUpdates, Sort : USort>( ) : UMemoryUpdates { override fun read(key: Key): UTreeUpdates { val reg = keyToRegion(key) - val updates = updates.localize(reg) + val updates = updates.localize(reg) { it.includesSymbolically(key).isFalse } if (updates === this.updates) { return this } @@ -272,7 +277,7 @@ data class UTreeUpdates, Sort : USort>( val newUpdates = updates.write( keyToRegion(key), update, - keyFilter = { it.isIncludedByUpdateConcretely(update) } + valueFilter = { it.isIncludedByUpdateConcretely(update) } ) return this.copy(updates = newUpdates) @@ -290,7 +295,7 @@ data class UTreeUpdates, Sort : USort>( val newUpdates = updates.write( region, update, - keyFilter = { it.isIncludedByUpdateConcretely(update) } + valueFilter = { it.isIncludedByUpdateConcretely(update) } ) return this.copy(updates = newUpdates) @@ -306,7 +311,7 @@ data class UTreeUpdates, Sort : USort>( val updatesSuffix = mutableListOf?>() // reconstructed region tree, including all updates unsatisfying `predicate(update.value(key))` in the same order - var splitUpdates = emptyRegionTree, Reg>() + var splitUpdates = emptyRegionTree>() // add an update to result tree fun applyUpdate(update: UUpdateNode) { @@ -314,7 +319,7 @@ data class UTreeUpdates, Sort : USort>( is UPinpointUpdateNode -> keyToRegion(update.key) is URangedUpdateNode<*, *, Key, Sort> -> keyRangeToRegion(update.fromKey, update.toKey) } - splitUpdates = splitUpdates.write(region, update, keyFilter = { it.isIncludedByUpdateConcretely(update) }) + splitUpdates = splitUpdates.write(region, update, valueFilter = { it.isIncludedByUpdateConcretely(update) }) } // traverse all updates one by one from the oldest one @@ -366,31 +371,35 @@ data class UTreeUpdates, Sort : USort>( var mappedNodeFound = false // Traverse [updates] using its iterator and fold them into a new updates tree with new mapped nodes - val initialEmptyTree = emptyRegionTree, Reg>() + val initialEmptyTree = emptyRegionTree>() val mappedUpdates = updates.fold(initialEmptyTree) { mappedUpdatesTree, updateNodeWithRegion -> val (updateNode, oldRegion) = updateNodeWithRegion // Map current node val mappedUpdateNode = updateNode.map(keyMapper, composer) + // Save information about whether something changed in the current node or not if (mappedUpdateNode !== updateNode) { mappedNodeFound = true } + // Doesn't apply the node, if its guard maps to `false` + if (mappedUpdateNode.guard.isFalse) { + return@fold mappedUpdatesTree + } + // Note that following code should be executed after checking for reference equality of a mapped node. // Otherwise, it is possible that for a tree with several impossible writes // it will be returned as a result, instead of an empty one. // Extract a new region by the mapped node - val newRegion = when (updateNode) { + val newRegion = when (mappedUpdateNode) { is UPinpointUpdateNode -> { - mappedUpdateNode as UPinpointUpdateNode val currentRegion = keyToRegion(mappedUpdateNode.key) oldRegion.intersect(currentRegion) } is URangedUpdateNode<*, *, Key, Sort> -> { - mappedUpdateNode as URangedUpdateNode<*, *, Key, Sort> val currentRegion = keyRangeToRegion(mappedUpdateNode.fromKey, mappedUpdateNode.toKey) oldRegion.intersect(currentRegion) } @@ -512,7 +521,7 @@ data class UTreeUpdates, Sort : USort>( * * *``` */ - private fun leftMostFold(updates: RegionTree, *>): Result { + private fun leftMostFold(updates: RegionTree<*, UUpdateNode>): Result { var result = cache[updates] if (result != null) { @@ -531,7 +540,7 @@ data class UTreeUpdates, Sort : USort>( private fun notLeftMostFold( accumulator: Result, - iterator: Iterator, Pair, RegionTree, *>>>>, + iterator: Iterator, Pair, RegionTree<*, UUpdateNode>>>>, ): Result { var accumulated = accumulator while (iterator.hasNext()) { diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt index 2903b3e947..57e68bd602 100644 --- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt @@ -315,11 +315,11 @@ internal class CompositionTest { @Test fun testComposeSeveralTimes() = with(ctx) { - val fstAddress = mockk() - val fstIndex = mockk() + val fstAddress = mkRegisterReading(0, addressSort) + val fstIndex = mkRegisterReading(1, sizeSort) - val sndAddress = mockk() - val sndIndex = mockk() + val sndAddress = mkRegisterReading(2, addressSort) + val sndIndex = mkRegisterReading(3, sizeSort) val arrayType: KClass> = Array::class // Create an empty region diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt index da25d9d3ca..0972dd3f18 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt @@ -3,8 +3,10 @@ package org.usvm.memory import io.ksmt.utils.mkConst import io.mockk.every import io.mockk.mockk +import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test +import org.usvm.Type import org.usvm.UBv32Sort import org.usvm.UComponents import org.usvm.UContext @@ -71,14 +73,36 @@ class MemoryRegionTests { ).write(address, 1.toBv(), guard) .write(address, 2.toBv(), anotherGuard) - assertTrue(treeUpdates.toList().size == 2) + assertEquals(2, treeUpdates.toList().size) val anotherTreeUpdates = treeUpdates .write(address, 3.toBv(), anotherGuard) .write(address, 4.toBv(), guard) - assertTrue(anotherTreeUpdates.toList().size == 2) + assertEquals(3, anotherTreeUpdates.toList().size) } } + @Test + fun testKeyFiltering() = with(ctx) { + val idx1 = mkRegisterReading(0, sizeSort) + val idx2 = mkRegisterReading(1, sizeSort) + + val memoryRegion = emptyAllocatedArrayRegion(mockk(), 0, sizeSort) + .write(idx1, mkBv(0), trueExpr) + .write(idx2, mkBv(1), trueExpr) + + val updatesBefore = memoryRegion.updates.toList() + assertEquals(2, updatesBefore.size) + assertTrue(updatesBefore.first().includesConcretely(idx1, trueExpr)) + assertTrue(updatesBefore.last().includesConcretely(idx2, trueExpr)) + + val memoryRegionAfter = memoryRegion.write(idx2, mkBv(2), trueExpr) + + val updatesAfter = memoryRegionAfter.updates.toList() + assertEquals(2, updatesAfter.size) + assertTrue(updatesAfter.first().includesConcretely(idx1, trueExpr)) + assertTrue(updatesAfter.last().includesConcretely(idx2, trueExpr)) + } + } \ No newline at end of file diff --git a/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt index 4661f97d72..abfae4b7cd 100644 --- a/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt @@ -3,6 +3,7 @@ package org.usvm.model import io.mockk.every import io.mockk.mockk import kotlinx.collections.immutable.persistentMapOf +import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test import org.usvm.* @@ -169,4 +170,49 @@ class ModelCompositionTest { val expr = composer.compose(reading) assertSame(composedRef0, expr) } + + @Test + fun testComposeAllocatedArrayWithFalseOverwrite() = with(ctx) { + val heapEvaluator = UHeapEagerModel( + concreteNull, + mapOf(), + mapOf(), + mapOf(), + ) + + val index0 = 0.toBv() + val index1 = 1.toBv() + + val defaultValue = bv32Sort.sampleUValue() + val nonDefaultValue0 = 17.toBv() + val nonDefaultValue1 = 42.toBv() + + val stackModel = URegistersStackEagerModel(concreteNull, mapOf(0 to trueExpr, 1 to falseExpr)) + val trueGuard = mkRegisterReading(0, boolSort) + val falseGuard = mkRegisterReading(1, boolSort) + + val composer = UComposer(this, stackModel, heapEvaluator, mockk(), mockk()) + + val emptyRegion = emptyAllocatedArrayRegion(mockk(), 1, bv32Sort) + + run { + val region = emptyRegion + .write(index0, nonDefaultValue0, trueGuard) + .write(index0, nonDefaultValue1, falseGuard) + val reading = region.read(index0) + + val expr = composer.compose(reading) + assertEquals(nonDefaultValue0, expr) + } + + run { + val region = emptyRegion + .write(index1, nonDefaultValue0, trueGuard) + .write(index0, nonDefaultValue1, falseGuard) + val reading = region.read(index0) + + val expr = composer.compose(reading) + assertEquals(defaultValue, expr) + } + } } \ No newline at end of file diff --git a/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt b/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt index 6ce5b889db..61e18bbeba 100644 --- a/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt +++ b/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt @@ -5,28 +5,39 @@ import kotlinx.collections.immutable.persistentMapOf import kotlinx.collections.immutable.toPersistentMap /** - * Region tree is a data structure storing collection of keys by abstract regions. + * Region tree is a data structure storing collection of values by abstract regions. You can think, that + * [RegionTree] is actually a persistent event-storage (event == [Value]) with + * support of grouped reading and writing, where events live in specific regions. + * * It maintains the following two invariants: * * (1) all sibling regions are pairwise disjoint; * * (2) all child regions are included into parent region. + * + * @param Reg a region of writing or reading + * @param Value a value to write or read */ -class RegionTree( - val entries: PersistentMap>> -) : Iterable> where Reg : Region { +class RegionTree( + val entries: PersistentMap>>, +) : Iterable> where Reg : Region { @Suppress("MemberVisibilityCanBePrivate") val isEmpty: Boolean get() = entries.isEmpty() /** * Splits the region tree into two trees: completely covered by the [region] and disjoint with it. * - * [keyFilter] is an arbitrary predicate suitable to filter out nodes from the results of the function. + * [valueFilter] is an arbitrary predicate suitable to filter out values from the results of the function. * Examples: - * * `{ it != 10 }` removes all the nodes with `key` equal to 10 + * * `{ it != 10 }` removes nodes with `value` equal to 10 * * `{ false }` doesn't remove anything + * + * **NB**: it doesn't filter out all the values satisfying [valueFilter], only those, that were touched during + * recursive split. + * + * @see localize */ private fun splitRecursively( region: Reg, - keyFilter: (Key) -> Boolean + valueFilter: (Value) -> Boolean, ): RecursiveSplitResult { if (isEmpty) { return RecursiveSplitResult(completelyCoveredRegionTree = this, disjointRegionTree = this) @@ -37,13 +48,20 @@ class RegionTree( // If we have precisely such region in the tree, then all its siblings are disjoint by invariant (1). // So just return a `Pair(node storing the region, rest of its siblings)` if (entry != null) { - val key = entry.first + val value = entry.first // IMPORTANT: usage of linked versions of maps is mandatory here, since - // it is required for correct order of keys returned by `iterator.next()` method - val inside = if (keyFilter(key)) persistentMapOf() else persistentMapOf(region to entry) + // it is required for correct order of values returned by `iterator.next()` method + val completelyCoveredRegionTree = if (!valueFilter(value)) { + val inside = persistentMapOf(region to entry) + if (entries.size == 1) { + this + } else { + RegionTree(inside) + } + } else { + entry.second + } val outside = entries.remove(region) - - val completelyCoveredRegionTree = RegionTree(inside) val disjointRegionTree = RegionTree(outside) return RecursiveSplitResult(completelyCoveredRegionTree, disjointRegionTree) @@ -55,42 +73,50 @@ class RegionTree( // (3) partially intersected with the [region]. // IMPORTANT: usage of linked versions of maps is mandatory here, since - // it is required for correct order of keys returned by `iterator.next()` method + // it is required for correct order of values returned by `iterator.next()` method // We have to support the following order: assume that we had entries [e0, e1, e2, e3, e4] // and a write operation into a region R that is a subregion of `e1` and `e3`, and covers e2 completely. // The correct order of the result is: // included = [R ∩ e1, e2, R ∩ e3], disjoint = [e0, e1\R, e3\R, e4] // That allows us to move recently updates region to the right side of the `entries` map and // leave the oldest ones in the left part of it. - val included = mutableMapOf>>() - val disjoint = mutableMapOf>>() - - entries.entries.forEach { (nodeRegion, keyWithRegionTree) -> - if (keyFilter(keyWithRegionTree.first)) { - // If we want to filter a region associated with the [key], - // we can simply do not add it to the `included` map result - return@forEach + val included = mutableMapOf>>() + val disjoint = mutableMapOf>>() + + fun MutableMap>>.addWithFilter( + nodeRegion: Reg, + valueWithRegionTree: Pair>, + valueFilter: (Value) -> Boolean, + ) { + val (value, childRegionTree) = valueWithRegionTree + if (valueFilter(value)) { + putAll(childRegionTree.entries) } else { - when (region.compare(nodeRegion)) { - RegionComparisonResult.INCLUDES -> included += nodeRegion to keyWithRegionTree - RegionComparisonResult.DISJOINT -> disjoint += nodeRegion to keyWithRegionTree - // For nodes with intersection, repeat process recursively. - RegionComparisonResult.INTERSECTS -> { - val (key, childRegionTree) = keyWithRegionTree - val (splitIncluded, splitDisjoint) = childRegionTree.splitRecursively(region, keyFilter) - - val includedReg = nodeRegion.intersect(region) - val disjointReg = nodeRegion.subtract(region) - - included[includedReg] = key to splitIncluded - disjoint[disjointReg] = key to splitDisjoint - } + put(nodeRegion, valueWithRegionTree) + } + } + + entries.entries.forEach { (nodeRegion, valueWithRegionTree) -> + when (region.compare(nodeRegion)) { + RegionComparisonResult.INCLUDES -> included.addWithFilter(nodeRegion, valueWithRegionTree, valueFilter) + + RegionComparisonResult.DISJOINT -> disjoint.addWithFilter(nodeRegion, valueWithRegionTree, valueFilter) + // For nodes with intersection, repeat process recursively. + RegionComparisonResult.INTERSECTS -> { + val (value, childRegionTree) = valueWithRegionTree + val (splitIncluded, splitDisjoint) = childRegionTree.splitRecursively(region, valueFilter) + + val includedReg = nodeRegion.intersect(region) + val disjointReg = nodeRegion.subtract(region) + + included.addWithFilter(includedReg, value to splitIncluded, valueFilter) + disjoint.addWithFilter(disjointReg, value to splitDisjoint, valueFilter) } } } // IMPORTANT: usage of linked versions of maps is mandatory here, since - // it is required for correct order of keys returned by `iterator.next()` method + // it is required for correct order of values returned by `iterator.next()` method val includedRegionTree = CompletelyCoveredRegionTree(included.toPersistentMap()) val disjointRegionTree = DisjointRegionTree(disjoint.toPersistentMap()) @@ -99,42 +125,67 @@ class RegionTree( /** * Returns a subtree completely included into the [region]. + * + * [valueFilter] is a predicate suitable to filter out particular nodes if their `value` satisfies it. + * Examples: + * * `{ false }` doesn't filter anything + * * `{ it != value }` writes into a tree and restrict for it to contain non-unique values. + * Suitable for deduplication. + * + * **NB**: it doesn't filter out all the values satisfying [valueFilter], only those, that were touched during + * recursive split. Consider this example: + * ``` + * r := some region + * tree := {r -> 1} + * {r -> 2} + * {r -> 3} + * tree.localize(r) { it % 2 == 1) = + * // first will be filtered out + * {r -> 2} + * {r -> 3} // this one won't be filtered out, though it satisfies `valueFilter` + * + * ``` */ - fun localize(region: Reg): RegionTree = - splitRecursively(region, keyFilter = { false }).completelyCoveredRegionTree + fun localize(region: Reg, valueFilter: (Value) -> Boolean = { false }): RegionTree = + splitRecursively(region, valueFilter).completelyCoveredRegionTree /** - * Places a Pair([region], [key]) into the tree, preserving its invariants. + * Places a Pair([region], [value]) into the tree, preserving its invariants. * - * [keyFilter] is a predicate suitable to filter out particular nodes if their `key` satisfies it. + * [valueFilter] is a predicate suitable to filter out particular nodes if their `value` satisfies it. * Examples: * * `{ false }` doesn't filter anything - * * `{ it != key }` writes into a tree and restrict for it to contain non-unique keys. + * * `{ it != value }` writes into a tree and restrict for it to contain non-unique values. * Suitable for deduplication. + * + * **NB**: it doesn't filter out all the values satisfying [valueFilter], only those, that were touched during + * recursive split. + * + * @see localize */ - fun write(region: Reg, key: Key, keyFilter: (Key) -> Boolean = { false }): RegionTree { - val (included, disjoint) = splitRecursively(region, keyFilter) + fun write(region: Reg, value: Value, valueFilter: (Value) -> Boolean = { false }): RegionTree { + val (included, disjoint) = splitRecursively(region, valueFilter) // A new node for a tree we construct accordingly to the (2) invariant. - val value = key to included + val node = value to included // Construct entries accordingly to the (1) invariant. - val disjointEntries = disjoint.entries.put(region, value) + val disjointEntries = disjoint.entries.put(region, node) return RegionTree(disjointEntries) } private fun checkInvariantRecursively(parentRegion: Reg?): Boolean { // Invariant (2): all child regions are included into parent region - val secondInvariant = parentRegion == null || entries.entries.all { (key, _) -> - parentRegion.compare(key) == RegionComparisonResult.INCLUDES + val secondInvariant = parentRegion == null || entries.entries.all { (reg, _) -> + parentRegion.compare(reg) == RegionComparisonResult.INCLUDES } val checkInvariantRecursively = { entries.entries.all { (entryKey, value) -> // Invariant (1): all sibling regions are pairwise disjoint val firstInvariant = entries.entries.all { other -> - val otherKey = other.key - otherKey === entryKey || entryKey.compare(otherKey) == RegionComparisonResult.DISJOINT + val otherReg = other.key + otherReg === entryKey || entryKey.compare(otherReg) == RegionComparisonResult.DISJOINT } firstInvariant && value.second.checkInvariantRecursively(entryKey) @@ -155,7 +206,7 @@ class RegionTree( * Note that elements from the same level will be processed in order from the * oldest entry to the most recently updated one. */ - override fun iterator(): Iterator> = TheLeftestTopSortIterator(entries.iterator()) + override fun iterator(): Iterator> = TheLeftestTopSortIterator(entries.iterator()) override fun toString(): String = if (isEmpty) "emptyTree" else toString(balance = 0) @@ -163,7 +214,7 @@ class RegionTree( entries.entries.joinToString(separator = System.lineSeparator()) { val subtree = it.value.second val region = it.key - val key = it.value.first + val value = it.value.first val indent = "\t".repeat(balance) val subtreeString = if (subtree.isEmpty) { @@ -172,7 +223,7 @@ class RegionTree( subtree.toString(balance + 1) } - indent + "$region -> $key:${System.lineSeparator()}$subtreeString" + indent + "$region -> $value:${System.lineSeparator()}$subtreeString" } /** @@ -180,14 +231,14 @@ class RegionTree( * the last element is the deepest one in the branch we explore. */ private inner class TheLeftestTopSortIterator private constructor( - private val entriesIterators: MutableList>, - ) : Iterator> { + private val entriesIterators: MutableList>, + ) : Iterator> { // A stack of elements we should emit after we process all their children. // We cannot use for it corresponding iterators since every value from an // iterator can be retrieved only once, but we already got it when we discovered the previous layer. - private val nodes: MutableList> = mutableListOf() + private val nodes: MutableList> = mutableListOf() - constructor(iterator: RegionTreeEntryIterator) : this(mutableListOf(iterator)) + constructor(iterator: RegionTreeEntryIterator) : this(mutableListOf(iterator)) override fun hasNext(): Boolean { while (entriesIterators.isNotEmpty()) { @@ -206,7 +257,7 @@ class RegionTree( return false } - override fun next(): Pair { + override fun next(): Pair { while (entriesIterators.isNotEmpty()) { val currentIterator = entriesIterators.last() @@ -219,8 +270,8 @@ class RegionTree( // Take the next element on the current layer val entry = currentIterator.next() - val keyWithRegionTree = entry.value - val regionTree = keyWithRegionTree.second + val valueWithRegionTree = entry.value + val regionTree = valueWithRegionTree.second // If it is a leaf, it is the answer, return it if (regionTree.isEmpty) { @@ -238,17 +289,17 @@ class RegionTree( } private inner class RecursiveSplitResult( - val completelyCoveredRegionTree: CompletelyCoveredRegionTree, - val disjointRegionTree: DisjointRegionTree + val completelyCoveredRegionTree: CompletelyCoveredRegionTree, + val disjointRegionTree: DisjointRegionTree, ) { - operator fun component1(): RegionTree = completelyCoveredRegionTree - operator fun component2(): RegionTree = disjointRegionTree + operator fun component1(): RegionTree = completelyCoveredRegionTree + operator fun component2(): RegionTree = disjointRegionTree } } -private typealias DisjointRegionTree = RegionTree -private typealias CompletelyCoveredRegionTree = RegionTree -private typealias RegionTreeMapEntry = Map.Entry>> -private typealias RegionTreeEntryIterator = Iterator> +private typealias DisjointRegionTree = RegionTree +private typealias CompletelyCoveredRegionTree = RegionTree +private typealias RegionTreeMapEntry = Map.Entry>> +private typealias RegionTreeEntryIterator = Iterator> -fun > emptyRegionTree() = RegionTree(persistentMapOf()) +fun , Value> emptyRegionTree() = RegionTree(persistentMapOf()) diff --git a/usvm-util/src/test/kotlin/org/usvm/test/RegionTreeIteratorTest.kt b/usvm-util/src/test/kotlin/org/usvm/test/RegionTreeIteratorTest.kt index f4873d8216..a98bd7586f 100644 --- a/usvm-util/src/test/kotlin/org/usvm/test/RegionTreeIteratorTest.kt +++ b/usvm-util/src/test/kotlin/org/usvm/test/RegionTreeIteratorTest.kt @@ -12,7 +12,7 @@ class RegionTreeIteratorTest { @Test fun testSimpleRecursiveIterator() { val region = SetRegion.ofSet(0, 1, 2, 3, 4, 5) - val tree = emptyRegionTree>() + val tree = emptyRegionTree, Int>() .write(region, 10) // {0..5} -> 10 .write(SetRegion.singleton(3), 5) // {0..2, 4, 5} -> 10, {3} -> (5, {3} -> 10) @@ -34,7 +34,7 @@ class RegionTreeIteratorTest { fun testRecursiveIteratorWritingsInTheSameRegion() { val region = SetRegion.singleton(1) val writes = List(5) { it } - val tree = writes.fold(emptyRegionTree>()) { acc, i -> + val tree = writes.fold(emptyRegionTree, Int>()) { acc, i -> acc.write(region, i) } @@ -90,7 +90,7 @@ class RegionTreeIteratorTest { @Test fun test() { - val tree = emptyRegionTree>() + val tree = emptyRegionTree, Int>() .write(SetRegion.ofSet(1, 2), 10) // {1, 2} -> 10 .write(SetRegion.singleton(1), 1) // {2} -> 10, {1} -> (1, {1} -> 10) .write(SetRegion.singleton(2), 2) // {1} -> (1, {1} -> 10), {2} -> (2, {2} -> 10) @@ -136,7 +136,7 @@ class RegionTreeIteratorTest { {3} -> 1: emptyTree */ - private fun constructComplicatedTree(): RegionTree> { + private fun constructComplicatedTree(): RegionTree, Int> { val initialRegion = SetRegion.ofSet(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10) val firstRegion = SetRegion.ofSet(2, 3, 4) val secondRegion = SetRegion.ofSet(3, 4, 5) @@ -147,7 +147,7 @@ class RegionTreeIteratorTest { val secondPoint = SetRegion.singleton(2) val thirdPoint = SetRegion.singleton(3) - return emptyRegionTree>() + return emptyRegionTree, Int>() .write(initialRegion, 1) .write(firstRegion, 2) .write(secondRegion, 3) diff --git a/usvm-util/src/test/kotlin/org/usvm/test/RegionTreeTests.kt b/usvm-util/src/test/kotlin/org/usvm/test/RegionTreeTests.kt index 589cdd2e3c..94657a6128 100644 --- a/usvm-util/src/test/kotlin/org/usvm/test/RegionTreeTests.kt +++ b/usvm-util/src/test/kotlin/org/usvm/test/RegionTreeTests.kt @@ -95,7 +95,7 @@ internal class RegionsTest { val seg2 = SetRegion.singleton(2) val seg3 = SetRegion.singleton(3) // Test writing - val tree0 = emptyRegionTree>() + val tree0 = emptyRegionTree, Int>() val tree1 = tree0.write(seg0_10, 0) val tree2 = tree1.write(seg2_4, 1) val tree3 = tree2.write(seg3_5, 2)