From 5e44022c368781e8fb4379d80936cbb9c082e9e4 Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Thu, 31 Aug 2023 14:42:19 +0300 Subject: [PATCH] Simplify composition (#53) --------- Co-authored-by: Valentyn Sobol --- .../src/main/kotlin/org/usvm/Composition.kt | 18 +- .../org/usvm/collection/array/ArrayRegion.kt | 12 +- .../collection/array/ArrayRegionTranslator.kt | 26 +- .../collection/array/UArrayModelRegion.kt | 16 +- .../array/USymbolicArrayCopyAdapter.kt | 162 +++---- .../usvm/collection/array/USymbolicArrayId.kt | 107 ++--- .../array/USymbolicArrayIndexKeyInfo.kt | 4 + .../array/length/ArrayLengthRegion.kt | 25 +- .../length/ArrayLengthRegionTranslator.kt | 2 +- .../array/length/UArrayLengthModelRegion.kt | 16 +- .../array/length/USymbolicArrayLengthId.kt | 124 +---- .../collection/field/FieldRegionTranslator.kt | 2 +- .../org/usvm/collection/field/FieldsRegion.kt | 26 +- .../collection/field/UFieldsModelRegion.kt | 16 +- .../usvm/collection/field/USymbolicFieldId.kt | 120 +---- .../collection/map/USymbolicMapKeyInfo.kt | 34 +- .../map/USymbolicMapMergeAdapter.kt | 124 ++--- .../map/length/UMapLengthModelRegion.kt | 16 +- .../collection/map/length/UMapLengthRegion.kt | 27 +- .../map/length/UMapLengthRegionTranslator.kt | 10 +- .../map/length/USymbolicMapLengthId.kt | 115 +---- .../map/primitive/UMapModelRegion.kt | 16 +- .../collection/map/primitive/UMapRegion.kt | 14 +- .../map/primitive/UMapRegionTranslator.kt | 10 +- .../map/primitive/USymbolicMapId.kt | 142 +++--- .../map/ref/SymbolicRefMapRegionTranslator.kt | 10 +- .../collection/map/ref/URefMapModelRegion.kt | 16 +- .../usvm/collection/map/ref/URefMapRegion.kt | 49 +- .../collection/map/ref/USymbolicRefMapId.kt | 294 +++--------- .../org/usvm/collection/set/USymbolicSetId.kt | 63 +-- .../usvm/memory/SymbolicCollectionUpdates.kt | 150 +------ .../org/usvm/memory/USymbolicCollection.kt | 79 ++-- .../usvm/memory/USymbolicCollectionAdapter.kt | 55 +-- .../org/usvm/memory/USymbolicCollectionId.kt | 94 +--- .../usvm/memory/USymbolicCollectionKeyInfo.kt | 7 +- .../kotlin/org/usvm/memory/UpdateNodes.kt | 131 ++---- .../org/usvm/memory/key/UHeapRefKeyInfo.kt | 4 + .../org/usvm/memory/key/USingleKeyInfo.kt | 20 - .../org/usvm/memory/key/USizeExprKeyInfo.kt | 4 + .../kotlin/org/usvm/model/LazyModelDecoder.kt | 11 +- .../src/main/kotlin/org/usvm/model/Model.kt | 9 +- .../org/usvm/solver/RegionTranslator.kt | 2 +- .../test/kotlin/org/usvm/CompositionTest.kt | 74 ++- .../src/test/kotlin/org/usvm/TestUtil.kt | 5 + .../org/usvm/memory/MapCompositionTest.kt | 423 ------------------ .../org/usvm/memory/UpdatesIteratorTest.kt | 2 +- .../kotlin/org/usvm/solver/TranslationTest.kt | 2 +- .../main/kotlin/org/usvm/util/RegionTree.kt | 60 ++- 48 files changed, 776 insertions(+), 1972 deletions(-) delete mode 100644 usvm-core/src/main/kotlin/org/usvm/memory/key/USingleKeyInfo.kt delete mode 100644 usvm-core/src/test/kotlin/org/usvm/memory/MapCompositionTest.kt diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt index eb47cddd3c..6da46a2caf 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Composition.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Composition.kt @@ -11,7 +11,6 @@ import org.usvm.collection.map.ref.UAllocatedRefMapWithInputKeysReading import org.usvm.collection.map.ref.UInputRefMapWithAllocatedKeysReading import org.usvm.collection.map.ref.UInputRefMapWithInputKeysReading import org.usvm.memory.UReadOnlyMemory -import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionId import org.usvm.util.Region @@ -62,18 +61,8 @@ open class UComposer( expr: UCollectionReading, key: Key, ): UExpr = with(expr) { - val mappedCollectionId = collection.collectionId.map(this@UComposer) - val mappedKey = mappedCollectionId.keyMapper(this@UComposer)(key) - val decomposedKey = mappedCollectionId.rebindKey(mappedKey) - if (decomposedKey != null) { - @Suppress("UNCHECKED_CAST") - // I'm terribly sorry to do this cast, but it's impossible to do it type safe way :( - val mappedCollection = - collection.mapTo(this@UComposer, decomposedKey.collectionId) as USymbolicCollection<*, Any?, Sort> - return mappedCollection.read(decomposedKey.key) - } - val mappedCollection = collection.mapTo(this@UComposer, mappedCollectionId) - return mappedCollection.read(mappedKey) + val mappedKey = collection.collectionId.keyMapper(this@UComposer)(key) + return collection.read(mappedKey, this@UComposer) } override fun transform(expr: UInputArrayLengthReading): USizeExpr = @@ -115,3 +104,6 @@ open class UComposer( override fun transform(expr: UNullRef): UExpr = memory.nullRef() } + +@Suppress("NOTHING_TO_INLINE") +inline fun UComposer<*>?.compose(expr: UExpr) = this?.apply(expr) ?: expr \ No newline at end of file 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 index fc90c2cfae..e706b1f2bc 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt @@ -8,12 +8,12 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USizeExpr import org.usvm.USort -import org.usvm.memory.key.USizeExprKeyInfo import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId import org.usvm.memory.USymbolicCollection import org.usvm.memory.foldHeapRef +import org.usvm.memory.key.USizeExprKeyInfo import org.usvm.memory.map data class UArrayIndexLValue( @@ -70,8 +70,14 @@ internal class UArrayMemoryRegion( arrayType: ArrayType, sort: Sort, address: UConcreteHeapAddress - ): UAllocatedArray = allocatedArrays[address] - ?: UAllocatedArrayId(arrayType, sort, address).emptyRegion() + ): UAllocatedArray { + var collection = allocatedArrays[address] + if (collection == null) { + collection = UAllocatedArrayId(arrayType, sort, address).emptyRegion() + allocatedArrays = allocatedArrays.put(address, collection) + } + return collection + } private fun updateAllocatedArray(ref: UConcreteHeapAddress, updated: UAllocatedArray) = UArrayMemoryRegion(allocatedArrays.put(ref, updated), inputArray) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionTranslator.kt index 2296a85aa5..a03139a6d4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionTranslator.kt @@ -35,7 +35,7 @@ class UArrayRegionDecoder( private val allocatedRegions = mutableMapOf>() - private var inputRegion: UInputArrayRegionTranslator? = null + private var inputRegionTranslator: UInputArrayRegionTranslator? = null fun allocatedArrayRegionTranslator( collectionId: UAllocatedArrayId @@ -51,19 +51,19 @@ class UArrayRegionDecoder( fun inputArrayRegionTranslator( collectionId: UInputArrayId ): URegionTranslator, USymbolicArrayIndex, Sort> { - if (inputRegion == null) { + if (inputRegionTranslator == null) { check(collectionId.arrayType == regionId.arrayType && collectionId.sort == regionId.sort) { "Unexpected collection: $collectionId" } - inputRegion = UInputArrayRegionTranslator(collectionId, exprTranslator) + inputRegionTranslator = UInputArrayRegionTranslator(collectionId, exprTranslator) } - return inputRegion!! + return inputRegionTranslator!! } override fun decodeLazyRegion( model: KModel, mapping: Map - ) = UArrayLazyModelRegion(regionId, model, mapping, inputRegion) + ) = inputRegionTranslator?.let { UArrayLazyModelRegion(regionId, model, mapping, it) } } private class UAllocatedArrayRegionTranslator( @@ -145,11 +145,13 @@ private class UAllocatedArrayUpdatesTranslator( val key = mkFreshConst("k", previous.sort.domain) val keyMapper = sourceCollection.collectionId.keyMapper(exprTranslator) - val convertedKey = keyMapper(adapter.convert(key)) + val convertedKey = keyMapper(adapter.convert(key, composer = null)) - val isInside = update.includesSymbolically(key).translated // already includes guard + val isInside = update.includesSymbolically(key, composer = null).translated // already includes guard - val result = sourceCollection.collectionId.instantiate(sourceCollection, convertedKey).translated + val result = sourceCollection.collectionId.instantiate( + sourceCollection, convertedKey, composer = null + ).translated val ite = mkIte(isInside, result, previous.select(key)) return mkArrayLambda(key.decl, ite) @@ -187,11 +189,13 @@ private class UInputArrayUpdatesTranslator( val key2 = mkFreshConst("k2", previous.sort.domain1) val keyMapper = sourceCollection.collectionId.keyMapper(exprTranslator) - val convertedKey = keyMapper(adapter.convert(key1 to key2)) + val convertedKey = keyMapper(adapter.convert(key1 to key2, composer = null)) - val isInside = update.includesSymbolically(key1 to key2).translated // already includes guard + val isInside = update.includesSymbolically(key1 to key2, composer = null).translated // already includes guard - val result = sourceCollection.collectionId.instantiate(sourceCollection, convertedKey).translated + val result = sourceCollection.collectionId.instantiate( + sourceCollection, convertedKey, composer = null + ).translated val ite = mkIte(isInside, result, previous.select(key1, key2)) return mkArrayLambda(key1.decl, key2.decl, ite) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt index 7dd591af75..102b404971 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt @@ -12,13 +12,11 @@ import org.usvm.solver.UCollectionDecoder abstract class UArrayModelRegion( private val regionId: UArrayRegionId, ) : UReadOnlyMemoryRegion, Sort> { - val defaultValue by lazy { regionId.sort.sampleUValue() } - - abstract val inputArray: UReadOnlyMemoryRegion? + abstract val inputArray: UReadOnlyMemoryRegion override fun read(key: UArrayIndexLValue): UExpr { - val ref = modelEnsureConcreteInputRef(key.ref) ?: return defaultValue - return inputArray?.read(ref to key.index) ?: defaultValue + val ref = modelEnsureConcreteInputRef(key.ref) + return inputArray.read(ref to key.index) } } @@ -26,14 +24,14 @@ class UArrayLazyModelRegion( regionId: UArrayRegionId, private val model: KModel, private val addressesMapping: AddressesMapping, - private val inputArrayDecoder: UCollectionDecoder? + private val inputArrayDecoder: UCollectionDecoder ) : UArrayModelRegion(regionId) { - override val inputArray: UReadOnlyMemoryRegion? by lazy { - inputArrayDecoder?.decodeCollection(model, addressesMapping) + override val inputArray: UReadOnlyMemoryRegion by lazy { + inputArrayDecoder.decodeCollection(model, addressesMapping) } } class UArrayEagerModelRegion( regionId: UArrayRegionId, - override val inputArray: UReadOnlyMemoryRegion? + override val inputArray: UReadOnlyMemoryRegion ) : UArrayModelRegion(regionId) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayCopyAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayCopyAdapter.kt index f07f810eb0..021ac22ffe 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayCopyAdapter.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayCopyAdapter.kt @@ -6,8 +6,8 @@ import org.usvm.UComposer import org.usvm.UContext import org.usvm.UExpr import org.usvm.USizeExpr +import org.usvm.compose import org.usvm.memory.USymbolicCollection -import org.usvm.memory.KeyMapper import org.usvm.memory.USymbolicCollectionAdapter import org.usvm.memory.USymbolicCollectionId import org.usvm.memory.USymbolicCollectionKeyInfo @@ -33,8 +33,6 @@ abstract class USymbolicArrayCopyAdapter( private val keyInfo: USymbolicCollectionKeyInfo ) : USymbolicCollectionAdapter { - override val srcKey = srcFrom - abstract val ctx: UContext override fun > region(): Reg = @@ -43,7 +41,7 @@ abstract class USymbolicArrayCopyAdapter( /** * Converts source memory key into destination memory key */ - abstract override fun convert(key: DstKey): SrcKey + abstract override fun convert(key: DstKey, composer: UComposer<*>?): SrcKey protected fun convertIndex( idx: USizeExpr, @@ -56,7 +54,7 @@ abstract class USymbolicArrayCopyAdapter( override fun includesConcretely(key: DstKey): Boolean = keyInfo.cmpConcreteLe(dstFrom, key) && keyInfo.cmpConcreteLe(key, dstTo) - override fun includesSymbolically(key: DstKey): UBoolExpr { + override fun includesSymbolically(key: DstKey, composer: UComposer<*>?): UBoolExpr { val leftIsLefter = keyInfo.cmpSymbolicLe(ctx, dstFrom, key) val rightIsRighter = keyInfo.cmpSymbolicLe(ctx, key, dstTo) val ctx = leftIsLefter.ctx @@ -70,75 +68,13 @@ abstract class USymbolicArrayCopyAdapter( ): Boolean = update.includesConcretely(dstFrom, guard) && update.includesConcretely(dstTo, guard) - override fun mapDstKeys( - mappedSrcKey: MappedSrcKey, - srcCollectionId: USymbolicCollectionId<*, *, *>, - dstKeyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): USymbolicCollectionAdapter? { - val mappedDstFrom = dstKeyMapper(dstFrom) ?: return null - val mappedDstTo = dstKeyMapper(dstTo) ?: return null - - if (srcKey === mappedSrcKey && dstFrom === mappedDstFrom && dstTo === mappedDstTo) { - @Suppress("UNCHECKED_CAST") - // In this case [MappedSrcKey] == [SrcKey] and [MappedDstKey] == [DstKey], - // but type system cannot type check that. - return this as USymbolicCollectionAdapter - } - - return mapKeyType( - mappedSrcKey, - concrete = { allocatedSrcKey -> - mapKeyType( - mappedDstFrom, - concrete = { allocatedDstFrom -> - USymbolicArrayAllocatedToAllocatedCopyAdapter( - allocatedSrcKey, - allocatedDstFrom, - ensureConcreteKey(mappedDstTo), - mappedKeyInfo.uncheckedCast() - ) - }, - symbolic = { symbolicDstFrom -> - USymbolicArrayAllocatedToInputCopyAdapter( - allocatedSrcKey, - symbolicDstFrom, - ensureSymbolicKey(mappedDstTo), - mappedKeyInfo.uncheckedCast() - ) - } - ) - }, - symbolic = { symbolicSrcKey -> - mapKeyType( - mappedDstFrom, - concrete = { allocatedDstFrom -> - USymbolicArrayInputToAllocatedCopyAdapter( - symbolicSrcKey, - allocatedDstFrom, - ensureConcreteKey(mappedDstTo), - mappedKeyInfo.uncheckedCast() - ) - }, - symbolic = { symbolicDstFrom -> - USymbolicArrayInputToInputCopyAdapter( - symbolicSrcKey, - symbolicDstFrom, - ensureSymbolicKey(mappedDstTo), - mappedKeyInfo.uncheckedCast() - ) - } - ) - } - ).uncheckedCast() - } - abstract override fun applyTo( memory: UWritableMemory, srcCollectionId: USymbolicCollectionId, dstCollectionId: USymbolicCollectionId, - guard: UBoolExpr + guard: UBoolExpr, + srcKey: SrcKey, + composer: UComposer<*> ) private fun keyToString(key: Key) = @@ -148,8 +84,18 @@ abstract class USymbolicArrayCopyAdapter( symbolic = { "${it.first}.${it.second}" } ) - override fun toString(collection: USymbolicCollection<*, SrcKey, *>): String { - return "[${keyToString(dstFrom)}..${keyToString(dstTo)}] <- $collection[${convert(dstFrom)}..${convert(dstTo)}]" + override fun toString(collection: USymbolicCollection<*, SrcKey, *>): String = buildString { + append("[") + append(keyToString(dstFrom)) + append("..") + append(keyToString(dstTo)) + append("] <- ") + append(collection) + append("[") + append(convert(dstFrom, composer = null)) + append("..") + append(convert(dstTo, composer = null)) + append("]") } companion object { @@ -162,12 +108,6 @@ abstract class USymbolicArrayCopyAdapter( is Pair<*, *> -> symbolic(key.uncheckedCast()) else -> error("Unexpected key: $key") } - - private fun ensureSymbolicKey(key: Key): USymbolicArrayIndex = - mapKeyType(key, symbolic = { it }, concrete = { error("Key type mismatch: $key") }) - - private fun ensureConcreteKey(key: Key): USizeExpr = - mapKeyType(key, concrete = { it }, symbolic = { error("Key type mismatch: $key") }) } } @@ -180,14 +120,16 @@ class USymbolicArrayAllocatedToAllocatedCopyAdapter( override val ctx: UContext get() = srcFrom.uctx - override fun convert(key: USizeExpr): USizeExpr = - convertIndex(key, dstFrom, srcFrom) + override fun convert(key: USizeExpr, composer: UComposer<*>?): USizeExpr = + convertIndex(key, composer.compose(dstFrom), composer.compose(srcFrom)) override fun applyTo( memory: UWritableMemory, srcCollectionId: USymbolicCollectionId, dstCollectionId: USymbolicCollectionId, - guard: UBoolExpr + guard: UBoolExpr, + srcKey: USizeExpr, + composer: UComposer<*> ) = with(ctx) { check(dstCollectionId is UAllocatedArrayId<*, *>) { "Unexpected collection: $dstCollectionId" } check(srcCollectionId is UAllocatedArrayId<*, *>) { "Unexpected collection: $srcCollectionId" } @@ -197,9 +139,9 @@ class USymbolicArrayAllocatedToAllocatedCopyAdapter( dstRef = mkConcreteHeapRef(dstCollectionId.address), type = dstCollectionId.arrayType, elementSort = dstCollectionId.sort, - fromSrcIdx = srcFrom, - fromDstIdx = dstFrom, - toDstIdx = dstTo, + fromSrcIdx = composer.compose(srcFrom), + fromDstIdx = composer.compose(dstFrom), + toDstIdx = composer.compose(dstTo), guard = guard ) } @@ -215,26 +157,28 @@ class USymbolicArrayAllocatedToInputCopyAdapter( override val ctx: UContext get() = srcFrom.uctx - override fun convert(key: USymbolicArrayIndex): USizeExpr = - convertIndex(key.second, dstFrom.second, srcFrom) + override fun convert(key: USymbolicArrayIndex, composer: UComposer<*>?): USizeExpr = + convertIndex(key.second, composer.compose(dstFrom.second), composer.compose(srcFrom)) override fun applyTo( memory: UWritableMemory, srcCollectionId: USymbolicCollectionId, dstCollectionId: USymbolicCollectionId, - guard: UBoolExpr + guard: UBoolExpr, + srcKey: USizeExpr, + composer: UComposer<*> ) = with(ctx) { check(dstCollectionId is USymbolicArrayId<*, *, *, *>) { "Unexpected collection: $dstCollectionId" } check(srcCollectionId is UAllocatedArrayId<*, *>) { "Unexpected collection: $srcCollectionId" } memory.memcpy( srcRef = mkConcreteHeapRef(srcCollectionId.address), - dstRef = dstFrom.first, + dstRef = composer.compose(dstFrom.first), type = dstCollectionId.arrayType, elementSort = dstCollectionId.sort, - fromSrcIdx = srcFrom, - fromDstIdx = dstFrom.second, - toDstIdx = dstTo.second, + fromSrcIdx = composer.compose(srcFrom), + fromDstIdx = composer.compose(dstFrom.second), + toDstIdx = composer.compose(dstTo.second), guard = guard ) } @@ -249,26 +193,29 @@ class USymbolicArrayInputToAllocatedCopyAdapter( override val ctx: UContext get() = dstFrom.uctx - override fun convert(key: USizeExpr): USymbolicArrayIndex = - srcFrom.first to convertIndex(key, dstFrom, srcFrom.second) + override fun convert(key: USizeExpr, composer: UComposer<*>?): USymbolicArrayIndex = + composer.compose(srcFrom.first) to + convertIndex(key, composer.compose(dstFrom), composer.compose(srcFrom.second)) override fun applyTo( memory: UWritableMemory, srcCollectionId: USymbolicCollectionId, dstCollectionId: USymbolicCollectionId, - guard: UBoolExpr + guard: UBoolExpr, + srcKey: USymbolicArrayIndex, + composer: UComposer<*> ) = with(ctx) { check(dstCollectionId is UAllocatedArrayId<*, *>) { "Unexpected collection: $dstCollectionId" } check(srcCollectionId is USymbolicArrayId<*, *, *, *>) { "Unexpected collection: $srcCollectionId" } memory.memcpy( - srcRef = srcFrom.first, + srcRef = composer.compose(srcFrom.first), dstRef = mkConcreteHeapRef(dstCollectionId.address), type = dstCollectionId.arrayType, elementSort = dstCollectionId.sort, - fromSrcIdx = srcFrom.second, - fromDstIdx = dstFrom, - toDstIdx = dstTo, + fromSrcIdx = composer.compose(srcFrom.second), + fromDstIdx = composer.compose(dstFrom), + toDstIdx = composer.compose(dstTo), guard = guard ) } @@ -284,26 +231,29 @@ class USymbolicArrayInputToInputCopyAdapter( override val ctx: UContext get() = srcFrom.second.uctx - override fun convert(key: USymbolicArrayIndex): USymbolicArrayIndex = - srcFrom.first to convertIndex(key.second, dstFrom.second, srcFrom.second) + override fun convert(key: USymbolicArrayIndex, composer: UComposer<*>?): USymbolicArrayIndex = + composer.compose(srcFrom.first) to + convertIndex(key.second, composer.compose(dstFrom.second), composer.compose(srcFrom.second)) override fun applyTo( memory: UWritableMemory, srcCollectionId: USymbolicCollectionId, dstCollectionId: USymbolicCollectionId, - guard: UBoolExpr + guard: UBoolExpr, + srcKey: USymbolicArrayIndex, + composer: UComposer<*> ) = with(ctx) { check(dstCollectionId is USymbolicArrayId<*, *, *, *>) { "Unexpected collection: $dstCollectionId" } check(srcCollectionId is USymbolicArrayId<*, *, *, *>) { "Unexpected collection: $srcCollectionId" } memory.memcpy( - srcRef = srcFrom.first, - dstRef = dstFrom.first, + srcRef = composer.compose(srcFrom.first), + dstRef = composer.compose(dstFrom.first), type = dstCollectionId.arrayType, elementSort = dstCollectionId.sort, - fromSrcIdx = srcFrom.second, - fromDstIdx = dstFrom.second, - toDstIdx = dstTo.second, + fromSrcIdx = composer.compose(srcFrom.second), + fromDstIdx = composer.compose(dstFrom.second), + toDstIdx = composer.compose(dstTo.second), guard = guard ) } 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 index 011c469436..c16df85974 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt @@ -5,25 +5,22 @@ import kotlinx.collections.immutable.toPersistentMap import org.usvm.UBoolExpr import org.usvm.UComposer import org.usvm.UConcreteHeapAddress -import org.usvm.UConcreteHeapRef -import org.usvm.UContext import org.usvm.UExpr import org.usvm.USizeExpr import org.usvm.USort import org.usvm.UTransformer -import org.usvm.memory.USymbolicCollection -import org.usvm.memory.UTreeUpdates -import org.usvm.memory.key.USizeExprKeyInfo -import org.usvm.memory.key.USizeRegion -import org.usvm.memory.DecomposedKey +import org.usvm.compose import org.usvm.memory.KeyTransformer -import org.usvm.memory.ULValue import org.usvm.memory.UPinpointUpdateNode +import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.USymbolicCollectionIdWithContextMemory +import org.usvm.memory.UTreeUpdates import org.usvm.memory.UUpdateNode import org.usvm.memory.UWritableMemory +import org.usvm.memory.key.USizeExprKeyInfo +import org.usvm.memory.key.USizeRegion import org.usvm.sampleUValue +import org.usvm.uctx import org.usvm.util.RegionTree import org.usvm.util.emptyRegionTree @@ -41,43 +38,38 @@ class UAllocatedArrayId internal constructor( override val arrayType: ArrayType, override val sort: Sort, val address: UConcreteHeapAddress, - val idDefaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory>(contextMemory), - USymbolicArrayId> { - - val defaultValue: UExpr by lazy { idDefaultValue ?: sort.sampleUValue() } +) : USymbolicArrayId> { + val defaultValue: UExpr by lazy { sort.sampleUValue() } - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, USizeExpr, Sort>, - key: USizeExpr + key: USizeExpr, + composer: UComposer<*>? ): UExpr { if (collection.updates.isEmpty()) { - return defaultValue + return composer.compose(defaultValue) + } + + if (composer == null) { + return key.uctx.mkAllocatedArrayReading(collection, key) } - return mkAllocatedArrayReading(collection, key) + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(UArrayIndexLValue(sort, key.uctx.mkConcreteHeapRef(address), key, arrayType)) } - override fun UContext.mkLValue( - key: USizeExpr - ): ULValue<*, Sort> = UArrayIndexLValue(sort, mkConcreteHeapRef(address), key, arrayType) + override fun write(memory: UWritableMemory, key: USizeExpr, value: UExpr, guard: UBoolExpr) { + val lvalue = UArrayIndexLValue(sort, key.uctx.mkConcreteHeapRef(address), key, arrayType) + memory.write(lvalue, value, guard) + } override fun keyMapper( transformer: UTransformer, ): KeyTransformer = { transformer.apply(it) } - override fun map(composer: UComposer): UAllocatedArrayId { - val composedDefaultValue = composer.compose(defaultValue) - check(contextMemory == null) { "contextHeap is not null in composition" } - return UAllocatedArrayId(arrayType, sort, address, composedDefaultValue, composer.memory.toWritableMemory()) - } - override fun keyInfo() = USizeExprKeyInfo - override fun rebindKey(key: USizeExpr): DecomposedKey<*, Sort>? = - null - override fun emptyRegion(): USymbolicCollection, USizeExpr, Sort> { val updates = UTreeUpdates( updates = emptyRegionTree(), @@ -130,19 +122,31 @@ class UAllocatedArrayId internal constructor( class UInputArrayId internal constructor( override val arrayType: ArrayType, override val sort: Sort, - private val defaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory>(contextMemory), - USymbolicArrayId> { +) : USymbolicArrayId> { - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, USymbolicArrayIndex, Sort>, - key: USymbolicArrayIndex - ): UExpr = mkInputArrayReading(collection, key.first, key.second) + key: USymbolicArrayIndex, + composer: UComposer<*>? + ): UExpr { + if (composer == null) { + return sort.uctx.mkInputArrayReading(collection, key.first, key.second) + } + + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(UArrayIndexLValue(sort, key.first, key.second, arrayType)) + } - override fun UContext.mkLValue( - key: USymbolicArrayIndex - ): ULValue<*, Sort> = UArrayIndexLValue(sort, key.first, key.second, arrayType) + override fun write( + memory: UWritableMemory, + key: USymbolicArrayIndex, + value: UExpr, + guard: UBoolExpr + ) { + val lvalue = UArrayIndexLValue(sort, key.first, key.second, arrayType) + memory.write(lvalue, value, guard) + } override fun keyMapper( transformer: UTransformer, @@ -160,30 +164,9 @@ class UInputArrayId internal constructor( return USymbolicCollection(this, updates) } - override fun map(composer: UComposer): UInputArrayId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefault = composer.compose(sort.sampleUValue()) - return UInputArrayId(arrayType, sort, composedDefault, composer.memory.toWritableMemory()) - } - override fun keyInfo(): USymbolicArrayIndexKeyInfo = USymbolicArrayIndexKeyInfo - override fun rebindKey(key: USymbolicArrayIndex): DecomposedKey<*, Sort>? = - when (val heapRef = key.first) { - is UConcreteHeapRef -> DecomposedKey( - UAllocatedArrayId( - arrayType, - sort, - heapRef.address, - defaultValue, - contextMemory - ), key.second - ) - - else -> null - } - override fun toString(): String = "inputArray<$arrayType>" override fun equals(other: Any?): Boolean { diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayIndexKeyInfo.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayIndexKeyInfo.kt index e2f9aaa281..09764fbb50 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayIndexKeyInfo.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayIndexKeyInfo.kt @@ -1,6 +1,7 @@ package org.usvm.collection.array import org.usvm.UBoolExpr +import org.usvm.UComposer import org.usvm.UContext import org.usvm.UHeapRef import org.usvm.USizeExpr @@ -21,6 +22,9 @@ typealias USymbolicArrayIndexRegion = ProductRegion * Provides information about keys of input arrays. */ object USymbolicArrayIndexKeyInfo: USymbolicCollectionKeyInfo { + override fun mapKey(key: USymbolicArrayIndex, composer: UComposer<*>?): USymbolicArrayIndex = + UHeapRefKeyInfo.mapKey(key.first, composer) to USizeExprKeyInfo.mapKey(key.second, composer) + override fun eqSymbolic(ctx: UContext, key1: USymbolicArrayIndex, key2: USymbolicArrayIndex): UBoolExpr = with(ctx) { UHeapRefKeyInfo.eqSymbolic(ctx, key1.first, key2.first) and 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 index aff541302e..5442093aa2 100644 --- 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 @@ -3,6 +3,7 @@ package org.usvm.collection.array.length import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentMapOf import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapAddress import org.usvm.UHeapRef import org.usvm.USizeExpr import org.usvm.USizeSort @@ -13,6 +14,7 @@ import org.usvm.memory.USymbolicCollection import org.usvm.memory.foldHeapRef import org.usvm.memory.guardedWrite import org.usvm.memory.map +import org.usvm.sampleUValue import org.usvm.uctx data class UArrayLengthLValue(val ref: UHeapRef, val arrayType: ArrayType) : @@ -32,24 +34,22 @@ data class UArrayLengthsRegionId(override val sort: USizeSort, val ar UMemoryRegionId, USizeSort> { override fun emptyRegion(): UMemoryRegion, USizeSort> = - UArrayLengthsMemoryRegion() + UArrayLengthsMemoryRegion(sort, arrayType) } -typealias UAllocatedArrayLengths = PersistentMap, USizeExpr> typealias UInputArrayLengths = USymbolicCollection, UHeapRef, USizeSort> interface UArrayLengthsRegion : UMemoryRegion, USizeSort> internal class UArrayLengthsMemoryRegion( - private val allocatedLengths: UAllocatedArrayLengths = persistentMapOf(), + private val sort: USizeSort, + private val arrayType: ArrayType, + private val allocatedLengths: PersistentMap = persistentMapOf(), private var inputLengths: UInputArrayLengths? = null ) : UArrayLengthsRegion { - private fun readAllocated(id: UAllocatedArrayLengthId) = - allocatedLengths[id] ?: id.defaultValue - - private fun updateAllocated(updated: UAllocatedArrayLengths) = - UArrayLengthsMemoryRegion(updated, inputLengths) + private fun updateAllocated(updated: PersistentMap) = + UArrayLengthsMemoryRegion(sort, arrayType, updated, inputLengths) private fun getInputLength(ref: UArrayLengthLValue): UInputArrayLengths { if (inputLengths == null) @@ -58,11 +58,11 @@ internal class UArrayLengthsMemoryRegion( } private fun updatedInput(updated: UInputArrayLengths) = - UArrayLengthsMemoryRegion(allocatedLengths, updated) + UArrayLengthsMemoryRegion(sort, arrayType, allocatedLengths, updated) override fun read(key: UArrayLengthLValue): USizeExpr = key.ref.map( - { concreteRef -> readAllocated(UAllocatedArrayLengthId(key.arrayType, concreteRef.address, key.sort)) }, + { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() }, { symbolicRef -> getInputLength(key).read(symbolicRef) } ) @@ -75,9 +75,8 @@ internal class UArrayLengthsMemoryRegion( initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, innerGuard) -> - val id = UAllocatedArrayLengthId(key.arrayType, concreteRef.address, key.sort) - val newRegion = region.allocatedLengths.guardedWrite(id, value, innerGuard) { - id.defaultValue + val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard) { + sort.sampleUValue() } region.updateAllocated(newRegion) }, diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegionTranslator.kt index a0f86abd5d..b276a61d33 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegionTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegionTranslator.kt @@ -43,7 +43,7 @@ class UArrayLengthRegionDecoder( override fun decodeLazyRegion( model: KModel, mapping: Map - ) = UArrayLengthLazyModelRegion(regionId, model, mapping, inputArrayLengthTranslator) + ) = inputArrayLengthTranslator?.let { UArrayLengthLazyModelRegion(regionId, model, mapping, it) } } private class UInputArrayLengthRegionTranslator( diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt index c19bfaa4b7..33b6285425 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt @@ -13,13 +13,11 @@ import org.usvm.solver.UCollectionDecoder abstract class UArrayLengthModelRegion( private val regionId: UArrayLengthsRegionId, ) : UReadOnlyMemoryRegion, USizeSort> { - val defaultValue by lazy { regionId.sort.sampleUValue() } - - abstract val inputArrayLength: UReadOnlyMemoryRegion? + abstract val inputArrayLength: UReadOnlyMemoryRegion override fun read(key: UArrayLengthLValue): UExpr { - val ref = modelEnsureConcreteInputRef(key.ref) ?: return defaultValue - return inputArrayLength?.read(ref) ?: defaultValue + val ref = modelEnsureConcreteInputRef(key.ref) + return inputArrayLength.read(ref) } } @@ -27,14 +25,14 @@ class UArrayLengthLazyModelRegion( regionId: UArrayLengthsRegionId, private val model: KModel, private val addressesMapping: AddressesMapping, - private val inputArrayLengthDecoder: UCollectionDecoder? + private val inputArrayLengthDecoder: UCollectionDecoder, ) : UArrayLengthModelRegion(regionId) { - override val inputArrayLength: UReadOnlyMemoryRegion? by lazy { - inputArrayLengthDecoder?.decodeCollection(model, addressesMapping) + override val inputArrayLength: UReadOnlyMemoryRegion by lazy { + inputArrayLengthDecoder.decodeCollection(model, addressesMapping) } } class UArrayLengthEagerModelRegion( regionId: UArrayLengthsRegionId, - override val inputArrayLength: UReadOnlyMemoryRegion? + override val inputArrayLength: UReadOnlyMemoryRegion, ) : UArrayLengthModelRegion(regionId) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt index 56ac0f15e2..c5c116fde7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt @@ -1,139 +1,57 @@ package org.usvm.collection.array.length -import io.ksmt.cache.hash +import org.usvm.UBoolExpr import org.usvm.UComposer -import org.usvm.UConcreteHeapAddress -import org.usvm.UConcreteHeapRef -import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef -import org.usvm.USizeExpr import org.usvm.USizeSort import org.usvm.UTransformer -import org.usvm.memory.USymbolicCollection -import org.usvm.memory.key.UHeapRefKeyInfo -import org.usvm.memory.key.USingleKeyInfo -import org.usvm.memory.DecomposedKey import org.usvm.memory.KeyTransformer import org.usvm.memory.UFlatUpdates -import org.usvm.memory.ULValue +import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.USymbolicCollectionIdWithContextMemory -import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.memory.UWritableMemory -import org.usvm.sampleUValue +import org.usvm.memory.key.UHeapRefKeyInfo +import org.usvm.uctx interface USymbolicArrayLengthId> : USymbolicCollectionId { val arrayType: ArrayType } -/** - * An id for a collection storing the concretely allocated array length at heap address [address]. - */ -class UAllocatedArrayLengthId internal constructor( - override val arrayType: ArrayType, - val address: UConcreteHeapAddress, - override val sort: USizeSort, - val idDefaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null -) : USymbolicCollectionIdWithContextMemory>(contextMemory), - USymbolicArrayLengthId> { - - val defaultValue: USizeExpr by lazy { - idDefaultValue ?: sort.sampleUValue() - } - - override fun rebindKey(key: Unit): DecomposedKey<*, USizeSort>? = null - - override fun keyInfo(): USymbolicCollectionKeyInfo = USingleKeyInfo - - override fun toString(): String = "allocatedLength<$arrayType>($address)" - - override fun UContext.mkReading( - collection: USymbolicCollection, Unit, USizeSort>, - key: Unit - ): UExpr { - check(collection.updates.isEmpty()) { "Can't instantiate length reading from non-empty collection" } - return defaultValue - } - - override fun UContext.mkLValue( - key: Unit - ): ULValue<*, USizeSort> = UArrayLengthLValue(mkConcreteHeapRef(address), arrayType) - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UAllocatedArrayLengthId<*> - - if (arrayType != other.arrayType) return false - if (address != other.address) return false - if (sort != other.sort) return false - - return true - } - - override fun hashCode(): Int = hash(address, arrayType, sort) - - override fun keyMapper(transformer: UTransformer): KeyTransformer = - error("This should not be called") - - override fun map(composer: UComposer): UAllocatedArrayLengthId = - error("This should not be called") - - override fun emptyRegion(): USymbolicCollection, Unit, USizeSort> = - error("This should not be called") -} - /** * A collection id for a collection storing array lengths for arrays of a specific [arrayType]. */ class UInputArrayLengthId internal constructor( override val arrayType: ArrayType, override val sort: USizeSort, - private val defaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory>(contextMemory), - USymbolicArrayLengthId> { +) : USymbolicArrayLengthId> { - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, UHeapRef, USizeSort>, - key: UHeapRef - ): UExpr = mkInputArrayLengthReading(collection, key) + key: UHeapRef, + composer: UComposer<*>? + ): UExpr { + if (composer == null) { + return key.uctx.mkInputArrayLengthReading(collection, key) + } - override fun UContext.mkLValue( - key: UHeapRef - ): ULValue<*, USizeSort> = UArrayLengthLValue(key, arrayType) + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(UArrayLengthLValue(key, arrayType)) + } + + override fun write(memory: UWritableMemory, key: UHeapRef, value: UExpr, guard: UBoolExpr) { + val lvalue = UArrayLengthLValue(key, arrayType) + memory.write(lvalue, value, guard) + } override fun keyMapper( transformer: UTransformer, ): KeyTransformer = { transformer.apply(it) } - override fun map(composer: UComposer): UInputArrayLengthId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefaultValue = composer.compose(sort.sampleUValue()) - return UInputArrayLengthId(arrayType, sort, composedDefaultValue, composer.memory.toWritableMemory()) - } - override fun keyInfo() = UHeapRefKeyInfo - override fun rebindKey(key: UHeapRef): DecomposedKey<*, USizeSort>? = when (key) { - is UConcreteHeapRef -> DecomposedKey( - UAllocatedArrayLengthId( - arrayType, - key.address, - sort, - defaultValue, - contextMemory - ), - Unit - ) - - else -> null - } - override fun emptyRegion(): USymbolicCollection, UHeapRef, USizeSort> = USymbolicCollection(this, UFlatUpdates(keyInfo())) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldRegionTranslator.kt index 87b281364d..47d1beeaec 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldRegionTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldRegionTranslator.kt @@ -43,7 +43,7 @@ class UFieldRegionDecoder( override fun decodeLazyRegion( model: KModel, mapping: Map - ) = UFieldsLazyModelRegion(regionId, model, mapping, inputRegionTranslator) + ) = inputRegionTranslator?.let { UFieldsLazyModelRegion(regionId, model, mapping, it) } } private class UInputFieldRegionTranslator( 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 index 96809d2648..a5e24cc7e1 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt @@ -14,6 +14,7 @@ import org.usvm.memory.USymbolicCollection import org.usvm.memory.foldHeapRef import org.usvm.memory.guardedWrite import org.usvm.memory.map +import org.usvm.sampleUValue data class UFieldLValue(override val sort: Sort, val ref: UHeapRef, val field: Field) : ULValue, Sort> { @@ -28,26 +29,22 @@ data class UFieldsRegionId(val field: Field, override val s UMemoryRegionId, Sort> { override fun emptyRegion(): UMemoryRegion, Sort> = - UFieldsMemoryRegion() + UFieldsMemoryRegion(sort, field) } -typealias UAllocatedFields = PersistentMap, UExpr> typealias UInputFields = USymbolicCollection, UHeapRef, Sort> interface UFieldsRegion : UMemoryRegion, Sort> internal class UFieldsMemoryRegion( - private val allocatedFields: UAllocatedFields = persistentMapOf(), + private val sort: Sort, + private val field: Field, + private val allocatedFields: PersistentMap> = persistentMapOf(), private var inputFields: UInputFields? = null ) : UFieldsRegion { - private fun readAllocated(address: UConcreteHeapAddress, field: Field, sort: Sort): UExpr { - val id = UAllocatedFieldId(field, address, sort) - return allocatedFields[id] ?: id.defaultValue - } - - private fun updateAllocated(updated: UAllocatedFields) = - UFieldsMemoryRegion(updated, inputFields) + private fun updateAllocated(updated: PersistentMap>) = + UFieldsMemoryRegion(sort, field, updated, inputFields) private fun getInputFields(ref: UFieldLValue): UInputFields { if (inputFields == null) @@ -56,11 +53,11 @@ internal class UFieldsMemoryRegion( } private fun updateInput(updated: UInputFields) = - UFieldsMemoryRegion(allocatedFields, updated) + UFieldsMemoryRegion(sort, field, allocatedFields, updated) override fun read(key: UFieldLValue): UExpr = key.ref.map( - { concreteRef -> readAllocated(concreteRef.address, key.field, key.sort) }, + { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() }, { symbolicRef -> getInputFields(key).read(symbolicRef) } ) @@ -74,9 +71,8 @@ internal class UFieldsMemoryRegion( initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, innerGuard) -> - val concreteKey = UAllocatedFieldId(key.field, concreteRef.address, key.sort) - val newRegion = region.allocatedFields.guardedWrite(concreteKey, value, innerGuard) { - concreteKey.defaultValue + val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard) { + sort.sampleUValue() } region.updateAllocated(newRegion) }, diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt index 6c48f4e4fa..d9652484e9 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt @@ -13,13 +13,11 @@ import org.usvm.solver.UCollectionDecoder abstract class UFieldsModelRegion( private val regionId: UFieldsRegionId, ) : UReadOnlyMemoryRegion, Sort> { - val defaultValue by lazy { regionId.sort.sampleUValue() } - - abstract val inputFields: UReadOnlyMemoryRegion? + abstract val inputFields: UReadOnlyMemoryRegion override fun read(key: UFieldLValue): UExpr { - val ref = modelEnsureConcreteInputRef(key.ref) ?: return defaultValue - return inputFields?.read(ref) ?: defaultValue + val ref = modelEnsureConcreteInputRef(key.ref) + return inputFields.read(ref) } } @@ -27,14 +25,14 @@ class UFieldsLazyModelRegion( regionId: UFieldsRegionId, private val model: KModel, private val addressesMapping: AddressesMapping, - private val inputFieldsDecoder: UCollectionDecoder? + private val inputFieldsDecoder: UCollectionDecoder ) : UFieldsModelRegion(regionId) { - override val inputFields: UReadOnlyMemoryRegion? by lazy { - inputFieldsDecoder?.decodeCollection(model, addressesMapping) + override val inputFields: UReadOnlyMemoryRegion by lazy { + inputFieldsDecoder.decodeCollection(model, addressesMapping) } } class UFieldsEagerModelRegion( regionId: UFieldsRegionId, - override val inputFields: UReadOnlyMemoryRegion? + override val inputFields: UReadOnlyMemoryRegion ) : UFieldsModelRegion(regionId) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt index ab9624494b..4133cdb426 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt @@ -1,136 +1,58 @@ package org.usvm.collection.field import io.ksmt.cache.hash +import org.usvm.UBoolExpr import org.usvm.UComposer -import org.usvm.UConcreteHeapAddress -import org.usvm.UConcreteHeapRef -import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort import org.usvm.UTransformer -import org.usvm.memory.DecomposedKey import org.usvm.memory.KeyTransformer -import org.usvm.memory.ULValue -import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.USymbolicCollectionIdWithContextMemory -import org.usvm.memory.UWritableMemory import org.usvm.memory.UFlatUpdates import org.usvm.memory.USymbolicCollection +import org.usvm.memory.USymbolicCollectionId +import org.usvm.memory.UWritableMemory import org.usvm.memory.key.UHeapRefKeyInfo -import org.usvm.memory.key.USingleKeyInfo -import org.usvm.memory.USymbolicCollectionKeyInfo -import org.usvm.sampleUValue +import org.usvm.uctx interface USymbolicFieldId> : USymbolicCollectionId { val field: Field } -/** - * An id for a collection storing the concretely allocated [field] at heap address [address]. - */ -class UAllocatedFieldId internal constructor( - override val field: Field, - val address: UConcreteHeapAddress, - override val sort: Sort, - val idDefaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null -) : USymbolicCollectionIdWithContextMemory>(contextMemory), - USymbolicFieldId> { - val defaultValue: UExpr by lazy { idDefaultValue ?: sort.sampleUValue() } - - override fun rebindKey(key: Unit): DecomposedKey<*, Sort>? = null - - override fun toString(): String = "allocatedField<$field>($address)" - - override fun keyInfo(): USymbolicCollectionKeyInfo = USingleKeyInfo - - override fun UContext.mkReading( - collection: USymbolicCollection, Unit, Sort>, - key: Unit - ): UExpr { - check(collection.updates.isEmpty()) { "Can't instantiate allocated field reading from non-empty collection" } - return defaultValue - } - - override fun UContext.mkLValue( - key: Unit - ): ULValue<*, Sort> = UFieldLValue(sort, mkConcreteHeapRef(address), field) - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UAllocatedFieldId<*, *> - - if (field != other.field) return false - if (address != other.address) return false - if (sort != other.sort) return false - - return true - } - - override fun hashCode(): Int = hash(field, address, sort) - - override fun keyMapper(transformer: UTransformer): KeyTransformer = - error("This should not be called") - - override fun map(composer: UComposer): UAllocatedFieldId = - error("This should not be called") - - override fun emptyRegion(): USymbolicCollection, Unit, Sort> = - error("This should not be called") -} - /** * An id for a collection storing the specific [field]. */ class UInputFieldId internal constructor( override val field: Field, override val sort: Sort, - private val defaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory>(contextMemory), - USymbolicFieldId> { +) : USymbolicFieldId> { - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, UHeapRef, Sort>, - key: UHeapRef - ): UExpr = mkInputFieldReading(collection, key) + key: UHeapRef, + composer: UComposer<*>?, + ): UExpr { + if (composer == null) { + return key.uctx.mkInputFieldReading(collection, key) + } - override fun UContext.mkLValue( - key: UHeapRef - ): ULValue<*, Sort> = UFieldLValue(sort, key, field) + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(UFieldLValue(sort, key, field)) + } + + override fun write(memory: UWritableMemory, key: UHeapRef, value: UExpr, guard: UBoolExpr) { + val lvalue = UFieldLValue(sort, key, field) + memory.write(lvalue, value, guard) + } override fun keyMapper( transformer: UTransformer, ): KeyTransformer = { transformer.apply(it) } - override fun map(composer: UComposer): UInputFieldId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefaultValue = composer.compose(sort.sampleUValue()) - return UInputFieldId(field, sort, composedDefaultValue, composer.memory.toWritableMemory()) - } - override fun keyInfo() = UHeapRefKeyInfo - override fun rebindKey(key: UHeapRef): DecomposedKey<*, Sort>? = - when (key) { - is UConcreteHeapRef -> DecomposedKey( - UAllocatedFieldId( - field, - key.address, - sort, - defaultValue, - contextMemory - ), - Unit - ) - - else -> null - } - override fun emptyRegion(): USymbolicCollection, UHeapRef, Sort> = USymbolicCollection(this, UFlatUpdates(keyInfo())) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapKeyInfo.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapKeyInfo.kt index acbd2593e2..eb54a8cc1f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapKeyInfo.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapKeyInfo.kt @@ -1,6 +1,7 @@ package org.usvm.collection.map import org.usvm.UBoolExpr +import org.usvm.UComposer import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef @@ -17,23 +18,32 @@ typealias USymbolicMapKeyRegion = ProductRegion /** * Provides information about keys of symbolic maps. */ -data class USymbolicMapKeyInfo>( +data class USymbolicMapKeyInfo>( val keyInfo: USymbolicCollectionKeyInfo, KeyReg> -): USymbolicCollectionKeyInfo, USymbolicMapKeyRegion> { - override fun eqSymbolic(ctx: UContext, key1: USymbolicMapKey, key2: USymbolicMapKey): UBoolExpr = - with(ctx) { - UHeapRefKeyInfo.eqSymbolic(ctx, key1.first, key2.first) and - keyInfo.eqSymbolic(ctx, key1.second, key2.second) - } +) : USymbolicCollectionKeyInfo, USymbolicMapKeyRegion> { + override fun mapKey(key: USymbolicMapKey, composer: UComposer<*>?): USymbolicMapKey = + UHeapRefKeyInfo.mapKey(key.first, composer) to keyInfo.mapKey(key.second, composer) + + override fun eqSymbolic( + ctx: UContext, + key1: USymbolicMapKey, + key2: USymbolicMapKey + ): UBoolExpr = with(ctx) { + UHeapRefKeyInfo.eqSymbolic(ctx, key1.first, key2.first) and + keyInfo.eqSymbolic(ctx, key1.second, key2.second) + } override fun eqConcrete(key1: USymbolicMapKey, key2: USymbolicMapKey): Boolean = UHeapRefKeyInfo.eqConcrete(key1.first, key2.first) && keyInfo.eqConcrete(key1.second, key2.second) - override fun cmpSymbolicLe(ctx: UContext, key1: USymbolicMapKey, key2: USymbolicMapKey): UBoolExpr = - with(ctx) { - UHeapRefKeyInfo.eqSymbolic(ctx, key1.first, key2.first) and - keyInfo.cmpSymbolicLe(ctx, key1.second, key2.second) - } + override fun cmpSymbolicLe( + ctx: UContext, + key1: USymbolicMapKey, + key2: USymbolicMapKey + ): UBoolExpr = with(ctx) { + UHeapRefKeyInfo.eqSymbolic(ctx, key1.first, key2.first) and + keyInfo.cmpSymbolicLe(ctx, key1.second, key2.second) + } override fun cmpConcreteLe(key1: USymbolicMapKey, key2: USymbolicMapKey): Boolean = UHeapRefKeyInfo.eqConcrete(key1.first, key2.first) && keyInfo.cmpConcreteLe(key1.second, key2.second) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapMergeAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapMergeAdapter.kt index bef0814d39..8eb79304ef 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapMergeAdapter.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/USymbolicMapMergeAdapter.kt @@ -1,37 +1,34 @@ package org.usvm.collection.map -import io.ksmt.utils.uncheckedCast import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UComposer import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort -import org.usvm.memory.USymbolicCollection -import org.usvm.collection.map.primitive.USymbolicMapId import org.usvm.collection.set.USymbolicSetId +import org.usvm.compose import org.usvm.isTrue -import org.usvm.memory.KeyMapper +import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionAdapter import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.memory.UUpdateNode import org.usvm.memory.UWritableMemory import org.usvm.util.Region + abstract class USymbolicMapMergeAdapter( - val dstKey: DstKey, - override val srcKey: SrcKey, val setOfKeys: USymbolicCollection, SrcKey, UBoolSort>, ) : USymbolicCollectionAdapter { - abstract override fun convert(key: DstKey): SrcKey + abstract override fun convert(key: DstKey, composer: UComposer<*>?): SrcKey override fun includesConcretely(key: DstKey) = - includesSymbolically(key).isTrue + includesSymbolically(key, composer = null).isTrue // todo: composer=null? - override fun includesSymbolically(key: DstKey): UBoolExpr { - val srcKey = convert(key) - return setOfKeys.read(srcKey) // ??? + override fun includesSymbolically(key: DstKey, composer: UComposer<*>?): UBoolExpr { + val srcKey = convert(key, composer) + return setOfKeys.read(srcKey, composer) } override fun isIncludedByUpdateConcretely( @@ -39,70 +36,20 @@ abstract class USymbolicMapMergeAdapter( guard: UBoolExpr, ) = false - override fun mapDstKeys( - mappedSrcKey: MappedSrcKey, - srcCollectionId: USymbolicCollectionId<*, *, *>, - dstKeyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): USymbolicCollectionAdapter? { - check(srcCollectionId is USymbolicMapId<*, *, *, *, *>) { - "Unexpected collection: $srcCollectionId" - } - - val mappedDstKey = dstKeyMapper(dstKey) ?: return null - val mappedSetOfKeys = setOfKeys.mapTo(composer, srcCollectionId.keysSetId) - - if (mappedSrcKey == srcKey && mappedDstKey == dstKey && mappedSetOfKeys == setOfKeys) { - @Suppress("UNCHECKED_CAST") - return this as USymbolicCollectionAdapter - } - - return mapKeyType( - key = mappedSrcKey, - concrete = { concreteSrc -> - mapKeyType( - key = mappedDstKey, - concrete = { concreteDst -> - USymbolicMapAllocatedToAllocatedMergeAdapter( - concreteDst, concreteSrc, mappedSetOfKeys.uncheckedCast() - ) - }, - symbolic = { symbolicDst -> - USymbolicMapAllocatedToInputMergeAdapter( - symbolicDst, concreteSrc, mappedSetOfKeys.uncheckedCast() - ) - } - ) - }, - symbolic = { symbolicSrc -> - mapKeyType( - key = mappedDstKey, - concrete = { concreteDst -> - USymbolicMapInputToAllocatedMergeAdapter( - concreteDst, symbolicSrc, mappedSetOfKeys.uncheckedCast() - ) - }, - symbolic = { symbolicDst -> - USymbolicMapInputToInputMergeAdapter( - symbolicDst, symbolicSrc, mappedSetOfKeys.uncheckedCast() - ) - } - ) - } - ).uncheckedCast() - } - override fun toString(collection: USymbolicCollection<*, SrcKey, *>): String = "(merge $collection)" + override fun applyTo( memory: UWritableMemory, srcCollectionId: USymbolicCollectionId, dstCollectionId: USymbolicCollectionId, - guard: UBoolExpr + guard: UBoolExpr, + srcKey: SrcKey, + composer: UComposer<*> ) { - TODO("Not yet implemented") + setOfKeys.applyTo(memory, srcKey, composer) + TODO() } override fun > region(): Reg = @@ -110,55 +57,42 @@ abstract class USymbolicMapMergeAdapter( private fun > convertRegion(srcReg: Reg): Reg = srcReg // TODO: implement valid region conversion logic - - companion object { - private inline fun mapKeyType( - key: Key, - concrete: (UExpr) -> T, - symbolic: (USymbolicMapKey) -> T - ): T = when (key) { - is UExpr<*> -> concrete(key.uncheckedCast()) - is Pair<*, *> -> symbolic(key.uncheckedCast()) - else -> error("Unexpected key: $key") - } - } } class USymbolicMapAllocatedToAllocatedMergeAdapter( - dstKey: UExpr, srcKey: UExpr, setOfKeys: USymbolicCollection, *, *>, UExpr, UBoolSort> ) : USymbolicMapMergeAdapter, UExpr>( - dstKey, srcKey, setOfKeys + setOfKeys ) { - override fun convert(key: UExpr): UExpr = key + override fun convert(key: UExpr, composer: UComposer<*>?): UExpr = key } class USymbolicMapAllocatedToInputMergeAdapter( - dstKey: USymbolicMapKey, - srcKey: UExpr, + val dstRef: UHeapRef, setOfKeys: USymbolicCollection, *, *>, UExpr, UBoolSort> ) : USymbolicMapMergeAdapter, USymbolicMapKey>( - dstKey, srcKey, setOfKeys + setOfKeys ) { - override fun convert(key: USymbolicMapKey): UExpr = key.second + override fun convert(key: USymbolicMapKey, composer: UComposer<*>?): UExpr = key.second } class USymbolicMapInputToAllocatedMergeAdapter( - dstKey: UExpr, - srcKey: USymbolicMapKey, + val srcRef: UHeapRef, setOfKeys: USymbolicCollection, *, *>, USymbolicMapKey, UBoolSort> ) : USymbolicMapMergeAdapter, UExpr>( - dstKey, srcKey, setOfKeys + setOfKeys ) { - override fun convert(key: UExpr): USymbolicMapKey = srcKey.first to key + override fun convert(key: UExpr, composer: UComposer<*>?): USymbolicMapKey = + composer.compose(srcRef) to key } class USymbolicMapInputToInputMergeAdapter( - dstKey: USymbolicMapKey, - srcKey: USymbolicMapKey, + val srcRef: UHeapRef, + val dstRef: UHeapRef, setOfKeys: USymbolicCollection, *, *>, USymbolicMapKey, UBoolSort> ) : USymbolicMapMergeAdapter, USymbolicMapKey>( - dstKey, srcKey, setOfKeys + setOfKeys ) { - override fun convert(key: USymbolicMapKey): USymbolicMapKey = srcKey.first to key.second + override fun convert(key: USymbolicMapKey, composer: UComposer<*>?): USymbolicMapKey = + composer.compose(srcRef) to key.second } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt index 00fb584908..deeb82f64c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt @@ -13,13 +13,11 @@ import org.usvm.solver.UCollectionDecoder abstract class UMapLengthModelRegion( private val regionId: UMapLengthRegionId, ) : UReadOnlyMemoryRegion, USizeSort> { - val defaultValue by lazy { regionId.sort.sampleUValue() } - - abstract val inputMapLength: UReadOnlyMemoryRegion? + abstract val inputMapLength: UReadOnlyMemoryRegion override fun read(key: UMapLengthLValue): UExpr { - val ref = modelEnsureConcreteInputRef(key.ref) ?: return defaultValue - return inputMapLength?.read(ref) ?: defaultValue + val ref = modelEnsureConcreteInputRef(key.ref) + return inputMapLength.read(ref) } } @@ -27,14 +25,14 @@ class UMapLengthLazyModelRegion( regionId: UMapLengthRegionId, private val model: KModel, private val addressesMapping: AddressesMapping, - private val inputLengthDecoder: UCollectionDecoder? + private val inputLengthDecoder: UCollectionDecoder ) : UMapLengthModelRegion(regionId) { - override val inputMapLength: UReadOnlyMemoryRegion? by lazy { - inputLengthDecoder?.decodeCollection(model, addressesMapping) + override val inputMapLength: UReadOnlyMemoryRegion by lazy { + inputLengthDecoder.decodeCollection(model, addressesMapping) } } class UMapLengthEagerModelRegion( regionId: UMapLengthRegionId, - override val inputMapLength: UReadOnlyMemoryRegion? + override val inputMapLength: UReadOnlyMemoryRegion ) : UMapLengthModelRegion(regionId) 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 index cbb2c3bbb8..246675e281 100644 --- 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 @@ -3,6 +3,7 @@ package org.usvm.collection.map.length import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentMapOf import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapAddress import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USizeExpr @@ -11,9 +12,10 @@ import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId import org.usvm.memory.USymbolicCollection -import org.usvm.memory.guardedWrite import org.usvm.memory.foldHeapRef +import org.usvm.memory.guardedWrite import org.usvm.memory.map +import org.usvm.sampleUValue import org.usvm.uctx typealias UInputMapLengthCollection = USymbolicCollection, UHeapRef, USizeSort> @@ -35,24 +37,22 @@ data class UMapLengthRegionId(override val sort: USizeSort, val mapType UMemoryRegionId, USizeSort> { override fun emptyRegion(): UMemoryRegion, USizeSort> = - UMapLengthMemoryRegion() + UMapLengthMemoryRegion(sort, mapType) } -typealias UAllocatedMapLength = PersistentMap, USizeExpr> typealias UInputMapLength = USymbolicCollection, UHeapRef, USizeSort> interface UMapLengthRegion : UMemoryRegion, USizeSort> internal class UMapLengthMemoryRegion( - private val allocatedLengths: UAllocatedMapLength = persistentMapOf(), + private val sort: USizeSort, + private val mapType: MapType, + private val allocatedLengths: PersistentMap = persistentMapOf(), private var inputLengths: UInputMapLength? = null ) : UMapLengthRegion { - private fun readAllocated(id: UAllocatedMapLengthId) = - allocatedLengths[id] ?: id.defaultValue - - private fun updateAllocated(updated: UAllocatedMapLength) = - UMapLengthMemoryRegion(updated, inputLengths) + private fun updateAllocated(updated: PersistentMap) = + UMapLengthMemoryRegion(sort, mapType, updated, inputLengths) private fun getInputLength(ref: UMapLengthLValue): UInputMapLength { if (inputLengths == null) @@ -61,11 +61,11 @@ internal class UMapLengthMemoryRegion( } private fun updateInput(updated: UInputMapLength) = - UMapLengthMemoryRegion(allocatedLengths, updated) + UMapLengthMemoryRegion(sort, mapType, allocatedLengths, updated) override fun read(key: UMapLengthLValue): USizeExpr = key.ref.map( - { concreteRef -> readAllocated(UAllocatedMapLengthId(key.mapType, concreteRef.address, key.sort)) }, + { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() }, { symbolicRef -> getInputLength(key).read(symbolicRef) } ) @@ -78,9 +78,8 @@ internal class UMapLengthMemoryRegion( initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, innerGuard) -> - val id = UAllocatedMapLengthId(key.mapType, concreteRef.address, key.sort) - val newRegion = region.allocatedLengths.guardedWrite(id, value, innerGuard) { - id.defaultValue + val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard) { + sort.sampleUValue() } region.updateAllocated(newRegion) }, diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegionTranslator.kt index dc09291652..b7baf42936 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegionTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegionTranslator.kt @@ -26,24 +26,24 @@ class UMapLengthRegionDecoder( private val exprTranslator: UExprTranslator<*> ) : URegionDecoder, USizeSort> { - private var inputTranslator: UInputMapLengthRegionTranslator? = null + private var inputRegionTranslator: UInputMapLengthRegionTranslator? = null fun inputMapLengthRegionTranslator( collectionId: UInputMapLengthId ): URegionTranslator, UHeapRef, USizeSort> { - if (inputTranslator == null) { + if (inputRegionTranslator == null) { check(collectionId.mapType == regionId.mapType && collectionId.sort == regionId.sort) { "Unexpected collection: $collectionId" } - inputTranslator = UInputMapLengthRegionTranslator(collectionId, exprTranslator) + inputRegionTranslator = UInputMapLengthRegionTranslator(collectionId, exprTranslator) } - return inputTranslator!! + return inputRegionTranslator!! } override fun decodeLazyRegion( model: KModel, mapping: Map - ) = UMapLengthLazyModelRegion(regionId, model, mapping, inputTranslator) + ) = inputRegionTranslator?.let { UMapLengthLazyModelRegion(regionId, model, mapping, it) } } private class UInputMapLengthRegionTranslator( diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt index 2d13ae3dbe..3e6e196343 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt @@ -1,129 +1,54 @@ package org.usvm.collection.map.length -import io.ksmt.cache.hash +import org.usvm.UBoolExpr import org.usvm.UComposer -import org.usvm.UConcreteHeapAddress -import org.usvm.UConcreteHeapRef -import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef -import org.usvm.USizeExpr import org.usvm.USizeSort import org.usvm.UTransformer -import org.usvm.memory.DecomposedKey import org.usvm.memory.KeyTransformer -import org.usvm.memory.ULValue -import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.USymbolicCollectionIdWithContextMemory -import org.usvm.memory.UWritableMemory import org.usvm.memory.UFlatUpdates import org.usvm.memory.USymbolicCollection +import org.usvm.memory.USymbolicCollectionId +import org.usvm.memory.UWritableMemory import org.usvm.memory.key.UHeapRefKeyInfo -import org.usvm.memory.key.USingleKeyInfo -import org.usvm.memory.USymbolicCollectionKeyInfo -import org.usvm.sampleUValue +import org.usvm.uctx interface USymbolicMapLengthId> : USymbolicCollectionId { val mapType: MapType } -class UAllocatedMapLengthId internal constructor( +class UInputMapLengthId internal constructor( override val mapType: MapType, - val address: UConcreteHeapAddress, override val sort: USizeSort, - val idDefaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory>(contextMemory), - USymbolicMapLengthId> { - - val defaultValue: USizeExpr by lazy { idDefaultValue ?: sort.sampleUValue() } - - override fun rebindKey(key: Unit): DecomposedKey<*, USizeSort>? = null - - override fun keyInfo(): USymbolicCollectionKeyInfo = USingleKeyInfo - - override fun toString(): String = "allocatedLength<$mapType>($address)" +) : USymbolicMapLengthId> { - override fun UContext.mkReading( - collection: USymbolicCollection, Unit, USizeSort>, - key: Unit + override fun instantiate( + collection: USymbolicCollection, UHeapRef, USizeSort>, + key: UHeapRef, + composer: UComposer<*>? ): UExpr { - check(collection.updates.isEmpty()) { "Can't instantiate length reading from non-empty collection" } - return defaultValue - } - - override fun UContext.mkLValue( - key: Unit - ): ULValue<*, USizeSort> = UMapLengthLValue(mkConcreteHeapRef(address), mapType) - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UAllocatedMapLengthId<*> + if (composer == null) { + return sort.uctx.mkInputMapLengthReading(collection, key) + } - if (mapType != other.mapType) return false - if (address != other.address) return false - - return true + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(UMapLengthLValue(key, mapType)) } - override fun hashCode(): Int = hash(mapType, address) - - override fun emptyRegion(): USymbolicCollection, Unit, USizeSort> = - error("This should not be called") - - override fun keyMapper(transformer: UTransformer): KeyTransformer = - error("This should not be called") - - override fun map(composer: UComposer): UAllocatedMapLengthId = - error("This should not be called") -} - -class UInputMapLengthId internal constructor( - override val mapType: MapType, - override val sort: USizeSort, - private val defaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory>(contextMemory), - USymbolicMapLengthId> { - override fun UContext.mkReading( - collection: USymbolicCollection, UHeapRef, USizeSort>, - key: UHeapRef - ): UExpr = mkInputMapLengthReading(collection, key) - - override fun UContext.mkLValue( - key: UHeapRef - ): ULValue<*, USizeSort> = UMapLengthLValue(key, mapType) + override fun write(memory: UWritableMemory, key: UHeapRef, value: UExpr, guard: UBoolExpr) { + val lvalue = UMapLengthLValue(key, mapType) + memory.write(lvalue, value, guard) + } override fun keyMapper( transformer: UTransformer, ): KeyTransformer = { transformer.apply(it) } - override fun map(composer: UComposer): UInputMapLengthId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefaultValue = composer.compose(sort.sampleUValue()) - return UInputMapLengthId(mapType, sort, composedDefaultValue, composer.memory.toWritableMemory()) - } - override fun keyInfo() = UHeapRefKeyInfo - override fun rebindKey(key: UHeapRef): DecomposedKey<*, USizeSort>? = when (key) { - is UConcreteHeapRef -> DecomposedKey( - UAllocatedMapLengthId( - mapType, - key.address, - sort, - defaultValue, - contextMemory - ), - Unit - ) - - else -> null - } - override fun emptyRegion(): USymbolicCollection, UHeapRef, USizeSort> = USymbolicCollection(this, UFlatUpdates(keyInfo())) 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 index 72f16c4c7c..160a21300e 100644 --- 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 @@ -14,13 +14,11 @@ import org.usvm.util.Region abstract class UMapModelRegion>( private val regionId: UMapRegionId ) : UReadOnlyMemoryRegion, ValueSort> { - val defaultValue by lazy { regionId.sort.sampleUValue() } - - abstract val inputMap: UReadOnlyMemoryRegion, ValueSort>? + abstract val inputMap: UReadOnlyMemoryRegion, ValueSort> override fun read(key: UMapEntryLValue): UExpr { - val mapRef = modelEnsureConcreteInputRef(key.mapRef) ?: return defaultValue - return inputMap?.read(mapRef to key.mapKey) ?: defaultValue + val mapRef = modelEnsureConcreteInputRef(key.mapRef) + return inputMap.read(mapRef to key.mapKey) } } @@ -28,14 +26,14 @@ class UMapLazyModelRegion, private val model: KModel, private val addressesMapping: AddressesMapping, - private val inputMapDecoder: UCollectionDecoder, ValueSort>? + private val inputMapDecoder: UCollectionDecoder, ValueSort> ) : UMapModelRegion(regionId) { - override val inputMap: UReadOnlyMemoryRegion, ValueSort>? by lazy { - inputMapDecoder?.decodeCollection(model, addressesMapping) + override val inputMap: UReadOnlyMemoryRegion, ValueSort> by lazy { + inputMapDecoder.decodeCollection(model, addressesMapping) } } class UMapEagerModelRegion>( regionId: UMapRegionId, - override val inputMap: UReadOnlyMemoryRegion, ValueSort>? + override val inputMap: UReadOnlyMemoryRegion, ValueSort> ) : UMapModelRegion(regionId) 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 index ee531e306e..4af9285442 100644 --- 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 @@ -6,11 +6,11 @@ import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort -import org.usvm.memory.USymbolicCollection import org.usvm.collection.map.USymbolicMapKey import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId +import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.memory.foldHeapRef import org.usvm.memory.map @@ -66,8 +66,16 @@ internal class UMapMemoryRegion) = - allocatedMaps[id] ?: id.emptyRegion() + private fun getAllocatedMap( + id: UAllocatedMapId + ): UAllocatedMap { + var collection = allocatedMaps[id] + if (collection == null) { + collection = id.emptyRegion() + allocatedMaps = allocatedMaps.put(id, collection) + } + return collection + } private fun updateAllocatedMap( id: UAllocatedMapId, 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 index 2e08b054e7..57a358d266 100644 --- 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 @@ -34,7 +34,7 @@ class UMapRegionDecoder>() - private var inputRegion: UInputMapTranslator? = null + private var inputRegionTranslator: UInputMapTranslator? = null fun allocatedMapTranslator( collectionId: UAllocatedMapId @@ -54,7 +54,7 @@ class UMapRegionDecoder ): URegionTranslator, USymbolicMapKey, ValueSort> { - if (inputRegion == null) { + if (inputRegionTranslator == null) { check( collectionId.mapType == regionId.mapType && collectionId.keySort == regionId.keySort @@ -63,15 +63,15 @@ class UMapRegionDecoder - ) = UMapLazyModelRegion(regionId, model, mapping, inputRegion) + ) = inputRegionTranslator?.let { UMapLazyModelRegion(regionId, model, mapping, it) } } private class UAllocatedMapTranslator>( diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt index ed7fcf812f..08c6ad1070 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt @@ -2,29 +2,27 @@ package org.usvm.collection.map.primitive import io.ksmt.cache.hash import io.ksmt.expr.KExpr +import org.usvm.UBoolExpr import org.usvm.UComposer import org.usvm.UConcreteHeapAddress -import org.usvm.UConcreteHeapRef -import org.usvm.UContext import org.usvm.UExpr import org.usvm.USort import org.usvm.UTransformer +import org.usvm.collection.map.USymbolicMapKey +import org.usvm.collection.map.USymbolicMapKeyInfo +import org.usvm.collection.map.USymbolicMapKeyRegion import org.usvm.collection.set.UAllocatedSetId import org.usvm.collection.set.UInputSetId import org.usvm.collection.set.USymbolicSetId -import org.usvm.memory.USymbolicCollection -import org.usvm.memory.DecomposedKey +import org.usvm.compose import org.usvm.memory.KeyTransformer -import org.usvm.memory.ULValue +import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.USymbolicCollectionIdWithContextMemory -import org.usvm.memory.UWritableMemory -import org.usvm.memory.UTreeUpdates -import org.usvm.collection.map.USymbolicMapKey -import org.usvm.collection.map.USymbolicMapKeyInfo -import org.usvm.collection.map.USymbolicMapKeyRegion import org.usvm.memory.USymbolicCollectionKeyInfo +import org.usvm.memory.UTreeUpdates +import org.usvm.memory.UWritableMemory import org.usvm.sampleUValue +import org.usvm.uctx import org.usvm.util.Region import org.usvm.util.emptyRegionTree @@ -33,7 +31,8 @@ interface USymbolicMapId< Key, ValueSort : USort, out KeysSetId : USymbolicSetId, - out MapId : USymbolicMapId> + out MapId : USymbolicMapId, + > : USymbolicCollectionId { val keysSetId: KeysSetId val mapType: MapType @@ -45,54 +44,51 @@ class UAllocatedMapId, Reg>, val address: UConcreteHeapAddress, - val idDefaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory< - UExpr, ValueSort, UAllocatedMapId>(contextMemory), - USymbolicMapId, ValueSort, - UAllocatedSetId, Reg>, - UAllocatedMapId> { +) : USymbolicMapId, ValueSort, + UAllocatedSetId, Reg>, + UAllocatedMapId> { - val defaultValue: UExpr by lazy { idDefaultValue ?: valueSort.sampleUValue() } + val defaultValue: UExpr by lazy { valueSort.sampleUValue() } override val keysSetId: UAllocatedSetId, Reg> - get() = UAllocatedSetId(keyInfo, contextMemory) + get() = UAllocatedSetId(keyInfo) override val sort: ValueSort get() = valueSort - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, UExpr, ValueSort>, - key: UExpr + key: UExpr, + composer: UComposer<*>? ): UExpr { if (collection.updates.isEmpty()) { - return defaultValue + return composer.compose(defaultValue) } - return mkAllocatedMapReading(collection, key) + if (composer == null) { + return key.uctx.mkAllocatedMapReading(collection, key) + } + + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(UMapEntryLValue(keySort, sort, key.uctx.mkConcreteHeapRef(address), key, mapType, keyInfo)) } - override fun UContext.mkLValue( - key: UExpr - ): ULValue<*, ValueSort> = UMapEntryLValue(keySort, sort, mkConcreteHeapRef(address), key, mapType, keyInfo) + override fun write( + memory: UWritableMemory, + key: UExpr, + value: UExpr, + guard: UBoolExpr, + ) { + val lvalue = UMapEntryLValue(keySort, sort, key.uctx.mkConcreteHeapRef(address), key, mapType, keyInfo) + memory.write(lvalue, value, guard) + } override fun keyMapper( transformer: UTransformer, ): KeyTransformer> = { transformer.apply(it) } - override fun map( - composer: UComposer - ): UAllocatedMapId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefaultValue = composer.compose(defaultValue) - return UAllocatedMapId( - keySort, valueSort, mapType, keyInfo, address, composedDefaultValue, composer.memory.toWritableMemory() - ) - } - override fun keyInfo(): USymbolicCollectionKeyInfo, Reg> = keyInfo - override fun rebindKey(key: UExpr): DecomposedKey<*, ValueSort>? = null - override fun emptyRegion(): USymbolicCollection, UExpr, ValueSort> { val updates = UTreeUpdates, Reg, ValueSort>( updates = emptyRegionTree(), @@ -125,26 +121,37 @@ class UInputMapId val valueSort: ValueSort, override val mapType: MapType, val keyInfo: USymbolicCollectionKeyInfo, Reg>, - val defaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory< - USymbolicMapKey, ValueSort, UInputMapId>(contextMemory), - USymbolicMapId, ValueSort, - UInputSetId, USymbolicMapKeyRegion>, - UInputMapId> { +) : USymbolicMapId, ValueSort, + UInputSetId, USymbolicMapKeyRegion>, + UInputMapId> { override val keysSetId: UInputSetId, USymbolicMapKeyRegion> - get() = UInputSetId(keyInfo(), contextMemory) + get() = UInputSetId(keyInfo()) override val sort: ValueSort get() = valueSort - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, USymbolicMapKey, ValueSort>, - key: USymbolicMapKey - ): UExpr = mkInputMapReading(collection, key.first, key.second) + key: USymbolicMapKey, + composer: UComposer<*>? + ): UExpr { + if (composer == null) { + return sort.uctx.mkInputMapReading(collection, key.first, key.second) + } + + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(UMapEntryLValue(keySort, sort, key.first, key.second, mapType, keyInfo)) + } - override fun UContext.mkLValue( - key: USymbolicMapKey - ): ULValue<*, ValueSort> = UMapEntryLValue(keySort, sort, key.first, key.second, mapType, keyInfo) + override fun write( + memory: UWritableMemory, + key: USymbolicMapKey, + value: UExpr, + guard: UBoolExpr + ) { + val lvalue = UMapEntryLValue(keySort, sort, key.first, key.second, mapType, keyInfo) + memory.write(lvalue, value, guard) + } override fun keyMapper( transformer: UTransformer, @@ -162,35 +169,8 @@ class UInputMapId return USymbolicCollection(this, updates) } - override fun map( - composer: UComposer - ): UInputMapId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefaultValue = composer.compose(sort.sampleUValue()) - return UInputMapId( - keySort, valueSort, mapType, keyInfo, composedDefaultValue, composer.memory.toWritableMemory() - ) - } - override fun keyInfo(): USymbolicMapKeyInfo = USymbolicMapKeyInfo(keyInfo) - override fun rebindKey(key: USymbolicMapKey): DecomposedKey<*, ValueSort>? = - when (val heapRef = key.first) { - is UConcreteHeapRef -> DecomposedKey( - UAllocatedMapId( - keySort, - sort, - mapType, - keyInfo, - heapRef.address, - defaultValue, - contextMemory - ), key.second - ) - - else -> null - } - override fun toString(): String = "inputMap<$mapType>()" override fun equals(other: Any?): Boolean { diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/SymbolicRefMapRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/SymbolicRefMapRegionTranslator.kt index d078b090b3..cdc7730956 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/SymbolicRefMapRegionTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/SymbolicRefMapRegionTranslator.kt @@ -35,7 +35,7 @@ class URefMapRegionDecoder( private val inputWithAllocatedKeysRegions = mutableMapOf>() - private var inputRegion: UInputRefMapTranslator? = null + private var inputRegionTranslator: UInputRefMapTranslator? = null fun allocatedRefMapWithInputKeysTranslator( collectionId: UAllocatedRefMapWithInputKeysId @@ -62,20 +62,20 @@ class URefMapRegionDecoder( fun inputRefMapTranslator( collectionId: UInputRefMapWithInputKeysId ): URegionTranslator, USymbolicMapKey, ValueSort> { - if (inputRegion == null) { + if (inputRegionTranslator == null) { check(collectionId.mapType == regionId.mapType && collectionId.sort == regionId.sort) { "Unexpected collection: $collectionId" } - inputRegion = UInputRefMapTranslator(collectionId, exprTranslator) + inputRegionTranslator = UInputRefMapTranslator(collectionId, exprTranslator) } - return inputRegion!! + return inputRegionTranslator!! } override fun decodeLazyRegion( model: KModel, mapping: Map - ) = URefMapLazyModelRegion(regionId, model, mapping, inputRegion) + ) = inputRegionTranslator?.let { URefMapLazyModelRegion(regionId, model, mapping, it) } } private class UAllocatedRefMapWithInputKeysTranslator( diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapModelRegion.kt index d6470e704f..f655fc3595 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapModelRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapModelRegion.kt @@ -14,13 +14,11 @@ import org.usvm.solver.UCollectionDecoder abstract class URefMapModelRegion( private val regionId: URefMapRegionId ) : UReadOnlyMemoryRegion, ValueSort> { - val defaultValue by lazy { regionId.sort.sampleUValue() } - - abstract val inputMap: UReadOnlyMemoryRegion, ValueSort>? + abstract val inputMap: UReadOnlyMemoryRegion, ValueSort> override fun read(key: URefMapEntryLValue): UExpr { - val mapRef = modelEnsureConcreteInputRef(key.mapRef) ?: return defaultValue - return inputMap?.read(mapRef to key.mapKey) ?: defaultValue + val mapRef = modelEnsureConcreteInputRef(key.mapRef) + return inputMap.read(mapRef to key.mapKey) } } @@ -28,14 +26,14 @@ class URefMapLazyModelRegion( regionId: URefMapRegionId, private val model: KModel, private val addressesMapping: AddressesMapping, - private val inputMapDecoder: UCollectionDecoder, ValueSort>? + private val inputMapDecoder: UCollectionDecoder, ValueSort> ) : URefMapModelRegion(regionId) { - override val inputMap: UReadOnlyMemoryRegion, ValueSort>? by lazy { - inputMapDecoder?.decodeCollection(model, addressesMapping) + override val inputMap: UReadOnlyMemoryRegion, ValueSort> by lazy { + inputMapDecoder.decodeCollection(model, addressesMapping) } } class URefMapEagerModelRegion( regionId: URefMapRegionId, - override val inputMap: UReadOnlyMemoryRegion, ValueSort>? + override val inputMap: UReadOnlyMemoryRegion, ValueSort> ) : URefMapModelRegion(regionId) 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 8dcb412638..cf985e0cd4 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 @@ -4,6 +4,7 @@ import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentMapOf import org.usvm.UAddressSort import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapAddress import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort @@ -16,6 +17,7 @@ import org.usvm.memory.USymbolicCollection import org.usvm.memory.foldHeapRef import org.usvm.memory.guardedWrite import org.usvm.memory.map +import org.usvm.sampleUValue data class URefMapEntryLValue( override val sort: ValueSort, @@ -59,17 +61,22 @@ typealias UInputRefMapWithAllocatedKeys = typealias UInputRefMap = USymbolicCollection, USymbolicMapKey, ValueSort> +internal data class UAllocatedRefMapWithAllocatedKeyId( + val mapRef: UConcreteHeapAddress, + val keyRef: UConcreteHeapAddress +) + internal class URefMapMemoryRegion( private val valueSort: ValueSort, private val mapType: MapType, - private var allocatedMapWithAllocatedKeys: PersistentMap, UExpr> = persistentMapOf(), + private var allocatedMapWithAllocatedKeys: PersistentMap> = persistentMapOf(), private var inputMapWithAllocatedKeys: PersistentMap, UInputRefMapWithAllocatedKeys> = persistentMapOf(), private var allocatedMapWithInputKeys: PersistentMap, UAllocatedRefMapWithInputKeys> = persistentMapOf(), private var inputMapWithInputKeys: UInputRefMap? = null, ) : URefMapRegion { private fun updateAllocatedMapWithAllocatedKeys( - updated: PersistentMap, UExpr> + updated: PersistentMap> ) = URefMapMemoryRegion( valueSort, mapType, @@ -79,8 +86,16 @@ internal class URefMapMemoryRegion( inputMapWithInputKeys ) - private fun getInputMapWithAllocatedKeys(id: UInputRefMapWithAllocatedKeysId) = - inputMapWithAllocatedKeys[id] ?: id.emptyRegion() + private fun getInputMapWithAllocatedKeys( + id: UInputRefMapWithAllocatedKeysId + ): UInputRefMapWithAllocatedKeys { + var collection = inputMapWithAllocatedKeys[id] + if (collection == null) { + collection = id.emptyRegion() + inputMapWithAllocatedKeys = inputMapWithAllocatedKeys.put(id, collection) + } + return collection + } private fun updateInputMapWithAllocatedKeys( id: UInputRefMapWithAllocatedKeysId, @@ -94,8 +109,16 @@ internal class URefMapMemoryRegion( inputMapWithInputKeys ) - private fun getAllocatedMapWithInputKeys(id: UAllocatedRefMapWithInputKeysId) = - allocatedMapWithInputKeys[id] ?: id.emptyRegion() + private fun getAllocatedMapWithInputKeys( + id: UAllocatedRefMapWithInputKeysId + ): UAllocatedRefMapWithInputKeys { + var collection = allocatedMapWithInputKeys[id] + if (collection == null) { + collection = id.emptyRegion() + allocatedMapWithInputKeys = allocatedMapWithInputKeys.put(id, collection) + } + return collection + } private fun updateAllocatedMapWithInputKeys( id: UAllocatedRefMapWithInputKeysId, @@ -132,10 +155,8 @@ internal class URefMapMemoryRegion( { concreteRef -> key.mapKey.map( { concreteKey -> - val id = UAllocatedRefMapWithAllocatedKeysId( - valueSort, mapType, concreteRef.address, concreteKey.address - ) - allocatedMapWithAllocatedKeys[id] ?: id.defaultValue + val id = UAllocatedRefMapWithAllocatedKeyId(concreteRef.address, concreteKey.address) + allocatedMapWithAllocatedKeys[id] ?: valueSort.sampleUValue() }, { symbolicKey -> val id = UAllocatedRefMapWithInputKeysId( @@ -174,10 +195,10 @@ internal class URefMapMemoryRegion( initial = mapRegion, initialGuard = mapGuard, blockOnConcrete = { region, (concreteKeyRef, guard) -> - val id = UAllocatedRefMapWithAllocatedKeysId( - valueSort, mapType, concreteMapRef.address, concreteKeyRef.address - ) - val newMap = region.allocatedMapWithAllocatedKeys.guardedWrite(id, value, guard) { id.defaultValue } + val id = UAllocatedRefMapWithAllocatedKeyId(concreteMapRef.address, concreteKeyRef.address) + val newMap = region.allocatedMapWithAllocatedKeys.guardedWrite(id, value, guard) { + valueSort.sampleUValue() + } region.updateAllocatedMapWithAllocatedKeys(newMap) }, blockOnSymbolic = { region, (symbolicKeyRef, guard) -> diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt index 0fcfeedc48..7d51f9aa24 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt @@ -2,10 +2,9 @@ package org.usvm.collection.map.ref import io.ksmt.cache.hash import org.usvm.UAddressSort +import org.usvm.UBoolExpr import org.usvm.UComposer import org.usvm.UConcreteHeapAddress -import org.usvm.UConcreteHeapRef -import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort @@ -16,19 +15,17 @@ import org.usvm.collection.map.USymbolicMapKeyRegion import org.usvm.collection.set.UAllocatedSetId import org.usvm.collection.set.UInputSetId import org.usvm.collection.set.USymbolicSetId -import org.usvm.memory.DecomposedKey +import org.usvm.compose import org.usvm.memory.KeyTransformer -import org.usvm.memory.ULValue import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionId -import org.usvm.memory.USymbolicCollectionIdWithContextMemory import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.memory.UTreeUpdates import org.usvm.memory.UWritableMemory import org.usvm.memory.key.UHeapRefKeyInfo import org.usvm.memory.key.UHeapRefRegion -import org.usvm.memory.key.USingleKeyInfo import org.usvm.sampleUValue +import org.usvm.uctx import org.usvm.util.emptyRegionTree interface USymbolicRefMapId< @@ -36,122 +33,47 @@ interface USymbolicRefMapId< Key, ValueSort : USort, out KeysSetId : USymbolicSetId, - out MapId : USymbolicRefMapId> + out MapId : USymbolicRefMapId, + > : USymbolicCollectionId { val keysSetId: KeysSetId val mapType: MapType } -class UAllocatedRefMapWithAllocatedKeysId( - override val sort: ValueSort, - override val mapType: MapType, - val mapAddress: UConcreteHeapAddress, - val keyAddress: UConcreteHeapAddress, - val idDefaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null -) : USymbolicCollectionIdWithContextMemory< - Unit, ValueSort, UAllocatedRefMapWithAllocatedKeysId>(contextMemory), - USymbolicRefMapId> { - - val defaultValue: UExpr by lazy { idDefaultValue ?: sort.sampleUValue() } - - override fun rebindKey(key: Unit): DecomposedKey<*, ValueSort>? = null - - override fun toString(): String = "allocatedMap<$mapType>($mapAddress)[$keyAddress]" - - override fun keyInfo(): USymbolicCollectionKeyInfo = USingleKeyInfo - - override fun UContext.mkReading( - collection: USymbolicCollection, Unit, ValueSort>, - key: Unit - ): UExpr { - check(collection.updates.isEmpty()) { "Can't instantiate allocated map reading from non-empty collection" } - return defaultValue - } - - override fun UContext.mkLValue( - key: Unit - ): ULValue<*, ValueSort> = URefMapEntryLValue( - sort, mkConcreteHeapRef(mapAddress), mkConcreteHeapRef(keyAddress), mapType - ) - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as UAllocatedRefMapWithAllocatedKeysId<*, *> - - if (sort != other.sort) return false - if (mapType != other.mapType) return false - if (mapAddress != other.mapAddress) return false - if (keyAddress != other.keyAddress) return false - - return true - } - - override fun hashCode(): Int = hash(mapAddress, keyAddress, mapType, sort) - - override val keysSetId: Nothing - get() = TODO() - - override fun emptyRegion() = - error("This should not be called") - - override fun keyMapper(transformer: UTransformer): KeyTransformer = - error("This should not be called") - - override fun map( - composer: UComposer - ) = error("This should not be called") -} - class UAllocatedRefMapWithInputKeysId( override val sort: ValueSort, override val mapType: MapType, val mapAddress: UConcreteHeapAddress, - val idDefaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory< - UHeapRef, ValueSort, UAllocatedRefMapWithInputKeysId>(contextMemory), - USymbolicRefMapId, - UAllocatedRefMapWithInputKeysId> { - - val defaultValue: UExpr by lazy { idDefaultValue ?: sort.sampleUValue() } - - override fun rebindKey(key: UHeapRef): DecomposedKey<*, ValueSort>? = - when (key) { - is UConcreteHeapRef -> DecomposedKey( - UAllocatedRefMapWithAllocatedKeysId( - sort, - mapType, - mapAddress, - key.address, - idDefaultValue, - contextMemory - ), - Unit - ) +) : USymbolicRefMapId, + UAllocatedRefMapWithInputKeysId> { + val defaultValue: UExpr by lazy { sort.sampleUValue() } - else -> null - } - - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, UHeapRef, ValueSort>, - key: UHeapRef + key: UHeapRef, + composer: UComposer<*>? ): UExpr { if (collection.updates.isEmpty()) { - return defaultValue + return composer.compose(defaultValue) + } + + if (composer == null) { + return key.uctx.mkAllocatedRefMapWithInputKeysReading(collection, key) } - return mkAllocatedRefMapWithInputKeysReading(collection, key) + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(URefMapEntryLValue(sort, key.uctx.mkConcreteHeapRef(mapAddress), key, mapType)) } - override fun UContext.mkLValue(key: UHeapRef): ULValue<*, ValueSort> = - URefMapEntryLValue(sort, mkConcreteHeapRef(mapAddress), key, mapType) + override fun write(memory: UWritableMemory, key: UHeapRef, value: UExpr, guard: UBoolExpr) { + val lvalue = URefMapEntryLValue(sort, value.uctx.mkConcreteHeapRef(mapAddress), key, mapType) + memory.write(lvalue, value, guard) + } override val keysSetId: UAllocatedSetId - get() = UAllocatedSetId(UHeapRefKeyInfo, contextMemory) + get() = UAllocatedSetId(UHeapRefKeyInfo) override fun keyInfo(): USymbolicCollectionKeyInfo = UHeapRefKeyInfo @@ -159,16 +81,6 @@ class UAllocatedRefMapWithInputKeysId( transformer: UTransformer, ): KeyTransformer = { transformer.apply(it) } - override fun map( - composer: UComposer - ): UAllocatedRefMapWithInputKeysId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefaultValue = composer.compose(defaultValue) - return UAllocatedRefMapWithInputKeysId( - sort, mapType, mapAddress, composedDefaultValue, composer.memory.toWritableMemory() - ) - } - override fun emptyRegion(): USymbolicCollection, UHeapRef, ValueSort> { val updates = UTreeUpdates( updates = emptyRegionTree(), @@ -199,49 +111,36 @@ class UInputRefMapWithAllocatedKeysId( override val sort: ValueSort, override val mapType: MapType, val keyAddress: UConcreteHeapAddress, - val idDefaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory< - UHeapRef, ValueSort, UInputRefMapWithAllocatedKeysId>(contextMemory), - USymbolicRefMapId, - UInputRefMapWithAllocatedKeysId> { - - val defaultValue: UExpr by lazy { idDefaultValue ?: sort.sampleUValue() } - - override fun rebindKey(key: UHeapRef): DecomposedKey<*, ValueSort>? = - when (key) { - is UConcreteHeapRef -> DecomposedKey( - UAllocatedRefMapWithAllocatedKeysId( - sort, - mapType, - key.address, - keyAddress, - idDefaultValue, - contextMemory - ), - Unit - ) - - else -> null - } +) : USymbolicRefMapId, + UInputRefMapWithAllocatedKeysId> { + val defaultValue: UExpr by lazy { sort.sampleUValue() } - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, UHeapRef, ValueSort>, - key: UHeapRef + key: UHeapRef, + composer: UComposer<*>? ): UExpr { if (collection.updates.isEmpty()) { - return defaultValue + return composer.compose(defaultValue) } - return mkInputRefMapWithAllocatedKeysReading(collection, key) + if (composer == null) { + return key.uctx.mkInputRefMapWithAllocatedKeysReading(collection, key) + } + + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(URefMapEntryLValue(sort, key, key.uctx.mkConcreteHeapRef(keyAddress), mapType)) } - override fun UContext.mkLValue(key: UHeapRef): ULValue<*, ValueSort> = - URefMapEntryLValue(sort, key, mkConcreteHeapRef(keyAddress), mapType) + override fun write(memory: UWritableMemory, key: UHeapRef, value: UExpr, guard: UBoolExpr) { + val lvalue = URefMapEntryLValue(sort, key, key.uctx.mkConcreteHeapRef(keyAddress), mapType) + memory.write(lvalue, value, guard) + } override val keysSetId: UAllocatedSetId - get() = UAllocatedSetId(UHeapRefKeyInfo, contextMemory) + get() = UAllocatedSetId(UHeapRefKeyInfo) override fun keyInfo(): USymbolicCollectionKeyInfo = UHeapRefKeyInfo @@ -249,16 +148,6 @@ class UInputRefMapWithAllocatedKeysId( transformer: UTransformer, ): KeyTransformer = { transformer.apply(it) } - override fun map( - composer: UComposer - ): UInputRefMapWithAllocatedKeysId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefaultValue = composer.compose(defaultValue) - return UInputRefMapWithAllocatedKeysId( - sort, mapType, keyAddress, composedDefaultValue, composer.memory.toWritableMemory() - ) - } - override fun emptyRegion(): USymbolicCollection, UHeapRef, ValueSort> { val updates = UTreeUpdates( updates = emptyRegionTree(), @@ -288,73 +177,36 @@ class UInputRefMapWithAllocatedKeysId( class UInputRefMapWithInputKeysId( override val sort: ValueSort, override val mapType: MapType, - val defaultValue: UExpr? = null, - contextMemory: UWritableMemory<*>? = null, -) : USymbolicCollectionIdWithContextMemory< - USymbolicMapKey, ValueSort, UInputRefMapWithInputKeysId>(contextMemory), - USymbolicRefMapId, ValueSort, - UInputSetId, *>, - UInputRefMapWithInputKeysId> { - - override fun rebindKey(key: USymbolicMapKey): DecomposedKey<*, ValueSort>? { - val mapRef = key.first - val keyRef = key.second - - return when (mapRef) { - is UConcreteHeapRef -> when (keyRef) { - is UConcreteHeapRef -> DecomposedKey( - UAllocatedRefMapWithAllocatedKeysId( - sort, - mapType, - mapRef.address, - keyRef.address, - defaultValue, - contextMemory - ), - Unit - ) - - else -> DecomposedKey( - UAllocatedRefMapWithInputKeysId( - sort, - mapType, - mapRef.address, - defaultValue, - contextMemory - ), - keyRef - ) - } - - else -> when (keyRef) { - is UConcreteHeapRef -> DecomposedKey( - UInputRefMapWithAllocatedKeysId( - sort, - mapType, - keyRef.address, - defaultValue, - contextMemory - ), - mapRef - ) - - else -> null - } - } - } +) : USymbolicRefMapId, ValueSort, + UInputSetId, *>, + UInputRefMapWithInputKeysId> { - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, USymbolicMapKey, ValueSort>, - key: USymbolicMapKey + key: USymbolicMapKey, + composer: UComposer<*>? ): UExpr { - return mkInputRefMapWithInputKeysReading(collection, key.first, key.second) + if (composer == null) { + return sort.uctx.mkInputRefMapWithInputKeysReading(collection, key.first, key.second) + } + + val memory = composer.memory.toWritableMemory() + collection.applyTo(memory, key, composer) + return memory.read(URefMapEntryLValue(sort, key.first, key.second, mapType)) } - override fun UContext.mkLValue(key: USymbolicMapKey): ULValue<*, ValueSort> = - URefMapEntryLValue(sort, key.first, key.second, mapType) + override fun write( + memory: UWritableMemory, + key: USymbolicMapKey, + value: UExpr, + guard: UBoolExpr + ) { + val lvalue = URefMapEntryLValue(sort, key.first, key.second, mapType) + memory.write(lvalue, value, guard) + } override val keysSetId: UInputSetId, *> - get() = UInputSetId(keyInfo(), contextMemory) + get() = UInputSetId(keyInfo()) override fun keyInfo(): USymbolicCollectionKeyInfo, *> = USymbolicMapKeyInfo(UHeapRefKeyInfo) @@ -367,16 +219,6 @@ class UInputRefMapWithInputKeysId( if (ref === it.first && idx === it.second) it else ref to idx } - override fun map( - composer: UComposer - ): UInputRefMapWithInputKeysId { - check(contextMemory == null) { "contextMemory is not null in composition" } - val composedDefaultValue = composer.compose(sort.sampleUValue()) - return UInputRefMapWithInputKeysId( - sort, mapType, composedDefaultValue, composer.memory.toWritableMemory() - ) - } - override fun emptyRegion(): USymbolicCollection, USymbolicMapKey, ValueSort> { val updates = UTreeUpdates, USymbolicMapKeyRegion, ValueSort>( diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/USymbolicSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/USymbolicSetId.kt index 37276ac42b..9305ae6d0c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/USymbolicSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/USymbolicSetId.kt @@ -4,17 +4,14 @@ import io.ksmt.utils.uncheckedCast import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UComposer -import org.usvm.UContext import org.usvm.UExpr import org.usvm.UTransformer -import org.usvm.memory.USymbolicCollection -import org.usvm.memory.DecomposedKey import org.usvm.memory.KeyTransformer -import org.usvm.memory.ULValue import org.usvm.memory.UMemoryUpdatesVisitor import org.usvm.memory.UPinpointUpdateNode import org.usvm.memory.URangedUpdateNode -import org.usvm.memory.USymbolicCollectionIdWithContextMemory +import org.usvm.memory.USymbolicCollection +import org.usvm.memory.USymbolicCollectionId import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.memory.USymbolicCollectionUpdates import org.usvm.memory.UUpdateNode @@ -23,14 +20,10 @@ import org.usvm.util.Region import java.util.IdentityHashMap -abstract class USymbolicSetId, out SetId : USymbolicSetId>( - contextMemory: UWritableMemory<*>? -) : USymbolicCollectionIdWithContextMemory(contextMemory) { +abstract class USymbolicSetId, out SetId : USymbolicSetId> + : USymbolicCollectionId { fun defaultRegion(): Reg { - if (contextMemory == null) { - return baseRegion() - } // TODO: get corresponding collection from contextMemory, recursively eval its region TODO() } @@ -52,8 +45,7 @@ abstract class USymbolicSetId, out SetId : USymbolicS class UAllocatedSetId>( val elementInfo: USymbolicCollectionKeyInfo, - contextMemory: UWritableMemory<*>? -) : USymbolicSetId>(contextMemory) { +) : USymbolicSetId>() { override val sort: UBoolSort get() = TODO("Not yet implemented") @@ -61,19 +53,14 @@ class UAllocatedSetId>( override fun baseRegion(): Reg = elementInfo.bottomRegion() - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, Element, UBoolSort>, - key: Element + key: Element, + composer: UComposer<*>? ): UExpr { TODO("Not yet implemented") } - override fun UContext.mkLValue( - key: Element - ): ULValue<*, UBoolSort> { - TODO("Not yet implemented") - } - override fun write(memory: UWritableMemory, key: Element, value: UExpr, guard: UBoolExpr) { TODO("Not yet implemented") } @@ -82,9 +69,6 @@ class UAllocatedSetId>( TODO("Not yet implemented") } - override fun map(composer: UComposer): UAllocatedSetId { - TODO("Not yet implemented") - } override fun keyInfo(): USymbolicCollectionKeyInfo { TODO("Not yet implemented") @@ -94,34 +78,27 @@ class UAllocatedSetId>( TODO("Not yet implemented") } - override fun rebindKey(key: Element): DecomposedKey<*, UBoolSort>? { - TODO("Not yet implemented") - } + } class UInputSetId>( - val elementInfo: USymbolicCollectionKeyInfo, - contextMemory: UWritableMemory<*>? -) : USymbolicSetId>(contextMemory) { + val elementInfo: USymbolicCollectionKeyInfo +) : USymbolicSetId>() { override val sort: UBoolSort get() = TODO("Not yet implemented") - override fun baseRegion(): Reg = - elementInfo.topRegion() - - override fun UContext.mkReading( + override fun instantiate( collection: USymbolicCollection, Element, UBoolSort>, - key: Element + key: Element, + composer: UComposer<*>? ): UExpr { TODO("Not yet implemented") } - override fun UContext.mkLValue( - key: Element - ): ULValue<*, UBoolSort> { - TODO("Not yet implemented") - } + override fun baseRegion(): Reg = + elementInfo.topRegion() + override fun write(memory: UWritableMemory, key: Element, value: UExpr, guard: UBoolExpr) { TODO("Not yet implemented") @@ -131,17 +108,11 @@ class UInputSetId>( TODO("Not yet implemented") } - override fun map(composer: UComposer): UInputSetId { - TODO("Not yet implemented") - } override fun keyInfo(): USymbolicCollectionKeyInfo { TODO("Not yet implemented") } - override fun rebindKey(key: Element): DecomposedKey<*, UBoolSort>? { - TODO("Not yet implemented") - } override fun emptyRegion(): USymbolicCollection, Element, UBoolSort> { TODO("Not yet implemented") diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt b/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt index 81adafad91..5d5758db6a 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/SymbolicCollectionUpdates.kt @@ -14,9 +14,11 @@ import org.usvm.util.emptyRegionTree */ interface USymbolicCollectionUpdates : Sequence> { /** + * Reads from collection updates and composes relevant ones. May filter out irrelevant updates for the [key]. + * * @return Relevant updates for a given key. */ - fun read(key: Key): USymbolicCollectionUpdates + fun read(key: Key, composer: UComposer<*>?): USymbolicCollectionUpdates /** * @return Symbolic collection which is obtained from this one by overwriting the address [key] with value [value] @@ -44,19 +46,9 @@ interface USymbolicCollectionUpdates : Sequence) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, + composer: UComposer<*>?, ): USymbolicCollectionUpdates - /** - * Returns a mapped [USymbolicCollection] using [keyMapper] and [composer]. - * It is used in [UComposer] during memory composition. - * Throws away all updates for which [keyMapper] returns null. - */ - fun > filterMap( - keyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): USymbolicCollectionUpdates - /** * @return Updates which express copying the slice of [fromCollection] guarded with * condition [guard]. @@ -123,9 +115,9 @@ class UFlatUpdates private constructor( val next: UFlatUpdates, ) - override fun read(key: Key): UFlatUpdates = + override fun read(key: Key, composer: UComposer<*>?): UFlatUpdates = when { - node != null && node.update.includesSymbolically(key).isFalse -> node.next.read(key) + node != null && node.update.includesSymbolically(key, composer).isFalse -> node.next.read(key, composer) else -> this } @@ -162,10 +154,11 @@ class UFlatUpdates private constructor( predicate: (UExpr) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, + composer: UComposer<*>?, ): UFlatUpdates { node ?: return this - val splitNode = node.update.split(key, predicate, matchingWrites, guardBuilder) - val splitNext = node.next.split(key, predicate, matchingWrites, guardBuilder) + val splitNode = node.update.split(key, predicate, matchingWrites, guardBuilder, composer) + val splitNext = node.next.split(key, predicate, matchingWrites, guardBuilder, composer) if (splitNode == null) { return splitNext @@ -181,46 +174,6 @@ class UFlatUpdates private constructor( ) } - override fun > filterMap( - keyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): UFlatUpdates { - node ?: return if (keyInfo == mappedKeyInfo) { - @Suppress("UNCHECKED_CAST") - this as UFlatUpdates - } else { - UFlatUpdates(null, mappedKeyInfo) - } - - // Map the current node and the next values recursively - val mappedNode = node.update.map(keyMapper, composer, mappedKeyInfo) - val mappedNext = node.next.filterMap(keyMapper, composer, mappedKeyInfo) - if (mappedNode == null) { - return mappedNext - } - - // 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 && keyInfo == mappedKeyInfo) { - // In this case Key = MappedKey is guaranteed, but type system can't express this - @Suppress("UNCHECKED_CAST") - return (this as UFlatUpdates) - } - - // Otherwise, construct a new one using the mapped values - return UFlatUpdates( - UFlatUpdatesNode( - mappedNode, - mappedNext - ), mappedKeyInfo - ) - } - /** * Returns updates in the FIFO order: the iterator emits updates from the oldest updates to the most recent one. * It means that the `initialNode` from the [UFlatUpdatesIterator] will be returned as the last element. @@ -283,9 +236,9 @@ data class UTreeUpdates, Sort : USort>( private val updates: RegionTree>, private val keyInfo: USymbolicCollectionKeyInfo ) : USymbolicCollectionUpdates { - override fun read(key: Key): UTreeUpdates { + override fun read(key: Key, composer: UComposer<*>?): USymbolicCollectionUpdates { val reg = keyInfo.keyToRegion(key) - val updates = updates.localize(reg) { it.includesSymbolically(key).isFalse } + val updates = updates.localize(reg) { !it.includesSymbolically(key, composer).isFalse } if (updates === this.updates) { return this } @@ -299,11 +252,11 @@ data class UTreeUpdates, Sort : USort>( guard: UBoolExpr ): UTreeUpdates { val update = UPinpointUpdateNode(key, keyInfo, value, guard) + val reg = keyInfo.keyToRegion(key) val newUpdates = updates.write( - keyInfo.keyToRegion(key), - update, - valueFilter = { it.isIncludedByUpdateConcretely(update) } - ) + reg, + update + ) { !it.isIncludedByUpdateConcretely(update) } return this.copy(updates = newUpdates) } @@ -316,9 +269,8 @@ data class UTreeUpdates, Sort : USort>( val update = URangedUpdateNode(fromCollection, adapter, guard) val newUpdates = updates.write( adapter.region(), - update, - valueFilter = { it.isIncludedByUpdateConcretely(update) } - ) + update + ) { !it.isIncludedByUpdateConcretely(update) } return this.copy(updates = newUpdates) } @@ -328,6 +280,7 @@ data class UTreeUpdates, Sort : USort>( predicate: (UExpr) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, + composer: UComposer<*>?, ): UTreeUpdates { // reconstructed region tree, including all updates unsatisfying `predicate(update.value(key))` in the same order var splitRegionTree = emptyRegionTree>() @@ -338,8 +291,8 @@ data class UTreeUpdates, Sort : USort>( is UPinpointUpdateNode -> keyInfo.keyToRegion(update.key) is URangedUpdateNode<*, *, Key, Sort> -> update.adapter.region() } - splitRegionTree = - splitRegionTree.write(region, update, valueFilter = { it.isIncludedByUpdateConcretely(update) }) + splitRegionTree = splitRegionTree + .write(region, update) { !it.isIncludedByUpdateConcretely(update) } } @@ -347,7 +300,7 @@ data class UTreeUpdates, Sort : USort>( // here we split updates from the newest to the oldest val splitUpdates = toMutableList?>().apply { reverse() } for ((idx, update) in splitUpdates.withIndex()) { - val splitUpdate = update?.split(key, predicate, matchingWrites, guardBuilder) + val splitUpdate = update?.split(key, predicate, matchingWrites, guardBuilder, composer) hasChanged = hasChanged or (update !== splitUpdate) splitUpdates[idx] = splitUpdate } @@ -369,67 +322,6 @@ data class UTreeUpdates, Sort : USort>( return this.copy(updates = splitRegionTree) } - - override fun > filterMap( - keyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): UTreeUpdates { - var mappedNodeFound = false - - // Traverse [updates] using its iterator and fold them into a new updates tree with new mapped nodes - val initialEmptyTree = emptyRegionTree>() - val mappedUpdates = updates.fold(initialEmptyTree) { mappedUpdatesTree, updateNodeWithRegion -> - val (updateNode, _) = updateNodeWithRegion - // Map current node - val mappedUpdateNode = updateNode.map(keyMapper, composer, mappedKeyInfo) - - - // Save information about whether something changed in the current node or not - if (mappedUpdateNode !== updateNode) { - mappedNodeFound = true - } - - // Ignore nodes which don't go into [targetCollectionId] after mapping - if (mappedUpdateNode == null) { - 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 (mappedUpdateNode) { - is UPinpointUpdateNode -> { - mappedKeyInfo.keyToRegion(mappedUpdateNode.key) - } - - is URangedUpdateNode<*, *, *, Sort> -> { - mappedUpdateNode as URangedUpdateNode<*, *, MappedKey, Sort> - mappedUpdateNode.adapter.region() - } - } - - // Ignore nodes estimated with an empty region - if (newRegion.isEmpty) { - return@fold mappedUpdatesTree - } - - // Otherwise, write the mapped node by a new region with a corresponding - // key filter for deduplication - mappedUpdatesTree.write(newRegion, mappedUpdateNode) { it == mappedUpdateNode } - } - - // If at least one node was changed, return a new updates, otherwise return this - return if (mappedNodeFound || mappedKeyInfo != keyInfo) { - UTreeUpdates(updates = mappedUpdates, mappedKeyInfo) - } else { - @Suppress("UNCHECKED_CAST") - this as UTreeUpdates - } - } - /** * Returns updates in the FIFO order: the iterator emits updates from the oldest updates to the most recent one. * Note that if some key in the tree is presented in more than one node, it will be returned exactly ones. diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt index d5ba56f7ae..2ee76ca86b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt @@ -7,8 +7,9 @@ import org.usvm.UComposer import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort +import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.uctx -import kotlin.collections.ArrayList /** * A uniform unbounded slice of memory. Indexed by [Key], stores symbolic values. @@ -25,14 +26,15 @@ data class USymbolicCollection + updates: USymbolicCollectionUpdates, + composer: UComposer<*>? ): UExpr { val lastUpdatedElement = updates.lastUpdatedElementOrNull() if (lastUpdatedElement != null) { - if (lastUpdatedElement.includesConcretely(key, precondition = sort.ctx.trueExpr)) { + if (lastUpdatedElement.includesSymbolically(key, composer).isTrue) { // The last write has overwritten the key - return lastUpdatedElement.value(key) + return lastUpdatedElement.value(key, composer) } } @@ -42,17 +44,20 @@ data class USymbolicCollection { + /** + * Reads a [key] from this collection with on-the-fly composition, if the [composer] provided. + */ + fun read(key: Key, composer: UComposer<*>?): UExpr { if (sort == sort.uctx.addressSort) { // Here we split concrete heap addresses from symbolic ones to optimize further memory operations. - return splittingRead(key) { it is UConcreteHeapRef } + return splittingRead(key, composer) { it is UConcreteHeapRef } } - val updates = updates.read(key) - return read(key, updates) + val updates = updates.read(key, composer) + return read(key, updates, composer) } /** @@ -67,14 +72,15 @@ data class USymbolicCollection?, predicate: (UExpr) -> Boolean ): UExpr { val ctx = sort.ctx val guardBuilder = GuardBuilder(ctx.trueExpr) val matchingWrites = ArrayList>>() // works faster than linked list - val splittingUpdates = split(key, predicate, matchingWrites, guardBuilder).updates + val splittingUpdates = split(key, predicate, matchingWrites, guardBuilder, composer).updates - val reading = read(key, splittingUpdates) + val reading = read(key, splittingUpdates, composer) // TODO: maybe introduce special expression for such operations? val readingWithBubbledWrites = matchingWrites.foldRight(reading) { (expr, guard), acc -> @@ -133,8 +139,9 @@ data class USymbolicCollection) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, + composer: UComposer<*>?, ): USymbolicCollection { - val splitUpdates = updates.read(key).split(key, predicate, matchingWrites, guardBuilder) + val splitUpdates = updates.read(key, composer).split(key, predicate, matchingWrites, guardBuilder, composer) return if (splitUpdates === updates) { this @@ -144,35 +151,29 @@ data class USymbolicCollection mapTo( - composer: UComposer, - targetCollectionId: USymbolicCollectionId - ): USymbolicCollection, MappedKey, Sort> { - val mapper = collectionId.keyFilterMapper(composer, targetCollectionId) - // Map the updates and the collectionId - val mappedUpdates = updates.filterMap(mapper, composer, targetCollectionId.keyInfo()) - - if (mappedUpdates === updates && targetCollectionId === collectionId) { - @Suppress("UNCHECKED_CAST") - return this as USymbolicCollection, MappedKey, Sort> - } + fun applyTo(memory: UWritableMemory, key: Key, composer: UComposer<*>) { + // Apply each update on the copy + for (update in updates) { + val guard = composer.compose(update.guard) - return USymbolicCollection(targetCollectionId, mappedUpdates) - } + if (guard.isFalse || update.includesSymbolically(key, composer).isFalse) { + continue + } - fun applyTo(memory: UWritableMemory) { - // Apply each update on the copy - updates.forEach { - when (it) { - is UPinpointUpdateNode -> collectionId.write(memory, it.key, it.value, it.guard) - is URangedUpdateNode<*, *, Key, Sort> -> it.applyTo(memory, collectionId) + when (update) { + is UPinpointUpdateNode -> collectionId.write( + memory, + update.keyInfo.mapKey(update.key, composer), + composer.compose(update.value), + guard + ) + + is URangedUpdateNode<*, *, Key, Sort> -> { + update.applyTo(memory, collectionId, key, composer) + } } } } @@ -191,6 +192,8 @@ data class USymbolicCollection = read(key, composer = null) + override fun toString(): String = buildString { append('<') diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionAdapter.kt index 1aa21fe7d1..7c656a176c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionAdapter.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionAdapter.kt @@ -2,7 +2,6 @@ package org.usvm.memory import org.usvm.UBoolExpr import org.usvm.UComposer -import org.usvm.USort import org.usvm.util.Region /** @@ -12,12 +11,7 @@ interface USymbolicCollectionAdapter { /** * Converts destination memory key into source memory key */ - fun convert(key: DstKey): SrcKey - - /** - * Key that defines adapted collection id (used to find id after mapping). - */ - val srcKey: SrcKey + fun convert(key: DstKey, composer: UComposer<*>?): SrcKey /** * Returns region covered by the adapted collection. @@ -26,59 +20,20 @@ interface USymbolicCollectionAdapter { fun includesConcretely(key: DstKey): Boolean - fun includesSymbolically(key: DstKey): UBoolExpr + fun includesSymbolically(key: DstKey, composer: UComposer<*>?): UBoolExpr fun isIncludedByUpdateConcretely( update: UUpdateNode, guard: UBoolExpr, ): Boolean - /** - * Maps this adapter by substituting all symbolic values using composer. - * The type of adapter might change in both [SrcKey] and [DstKey]. - * Type of [SrcKey] changes if [collectionId] rebinds [srcKey]. - * Type of [DstKey] changes to [MappedDstKey] by [dstKeyMapper]. - * @return - * - Null if destination keys are filtered out by [dstKeyMapper] - * - Pair(adapter, targetId), where adapter is a mapped version of this one, targetId is a - * new collection id for the mapped source collection we adapt. - */ - fun map( - dstKeyMapper: KeyMapper, - composer: UComposer, - collectionId: USymbolicCollectionId, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): Pair, USymbolicCollectionId<*, Sort, *>>? { - val mappedSrcKey = collectionId.keyMapper(composer)(srcKey) - val decomposedSrcKey = collectionId.rebindKey(mappedSrcKey) - if (decomposedSrcKey != null) { - val mappedAdapter = - mapDstKeys(decomposedSrcKey.key, decomposedSrcKey.collectionId, dstKeyMapper, composer, mappedKeyInfo) - ?: return null - return mappedAdapter to decomposedSrcKey.collectionId - } - - val mappedAdapter = mapDstKeys(mappedSrcKey, collectionId, dstKeyMapper, composer, mappedKeyInfo) ?: return null - return mappedAdapter to collectionId - } - - /** - * Returns new adapter with destination keys were successfully mapped by [dstKeyMapper]. - * If [dstKeyMapper] returns null for at least one key, returns null. - */ - fun mapDstKeys( - mappedSrcKey: MappedSrcKey, - srcCollectionId: USymbolicCollectionId<*, *, *>, - dstKeyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): USymbolicCollectionAdapter? - fun applyTo( memory: UWritableMemory, srcCollectionId: USymbolicCollectionId, dstCollectionId: USymbolicCollectionId, - guard: UBoolExpr + guard: UBoolExpr, + srcKey: SrcKey, + composer: UComposer<*> ) fun toString(collection: USymbolicCollection<*, SrcKey, *>): String diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionId.kt b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionId.kt index 9410c6f4ba..9f6ca0a7b0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionId.kt @@ -2,16 +2,11 @@ package org.usvm.memory import org.usvm.UBoolExpr import org.usvm.UComposer -import org.usvm.UContext import org.usvm.UExpr import org.usvm.USort import org.usvm.UTransformer -import org.usvm.uctx typealias KeyTransformer = (Key) -> Key -typealias KeyMapper = (Key) -> MappedKey? - -data class DecomposedKey(val collectionId: USymbolicCollectionId, val key: Key) /** * Represents any possible type of symbolic collections that can be used in symbolic memory. @@ -22,7 +17,11 @@ interface USymbolicCollectionId, key: Key): UExpr + fun instantiate( + collection: USymbolicCollection<@UnsafeVariance CollectionId, Key, Sort>, + key: Key, + composer: UComposer<*>?, + ): UExpr fun write( memory: UWritableMemory, @@ -36,57 +35,6 @@ interface USymbolicCollectionId keyMapper(transformer: UTransformer): KeyTransformer - /** - * Maps keys that belong to this collection to the collection with [expectedId] - * using [transformer]. - * Filters out keys that don't belong to the collection with [expectedId] after mapping. - * */ - fun keyFilterMapper( - transformer: UTransformer, - expectedId: USymbolicCollectionId - ): KeyMapper { - val mapper = keyMapper(transformer) - return filter@{ currentKey -> - val transformedKey = mapper(currentKey) - val decomposedKey = rebindKey(transformedKey) - - @Suppress("UNCHECKED_CAST") - return@filter when { - // transformedKey belongs to the symbolic collection with expectedId. - decomposedKey == null -> transformedKey - - /** - * Transformed key has been rebound to the collection with expectedId. - * For example, the expectedId is UAllocatedFieldId with address 0x1 - * and transformedKey has been rebound to the collection with the same id. - * */ - decomposedKey.collectionId == expectedId -> decomposedKey.key - - /** - * Transformed key has been rebound to the collection with id different from expectedId. - * For example, the expectedId is UAllocatedFieldId with address 0x1 - * and transformedKey has been rebound to the UAllocatedFieldId with address 0x2. - * Therefore, the key definitely doesn't belong to the - * collection with expectedId and can be filtered out. - * */ - else -> null - } as MappedKey? - } - } - - /** - * Maps the collection using [composer]. - * It is used in [UComposer] for composition operation. - */ - fun map(composer: UComposer): CollectionId - - /** - * Checks that [key] still belongs to the symbolic collection with this id. If yes, then returns null. - * If [key] belongs to some new memory region, returns lvalue for this new region. - * The implementation might assume that [key] is obtained by [keyMapper] from some key of symbolic collection with this id. - */ - fun rebindKey(key: Key): DecomposedKey<*, Sort>? - /** * Returns information about the key of this collection. * TODO: pass here context in the form of path constraints here. @@ -94,34 +42,4 @@ interface USymbolicCollectionId fun emptyRegion(): USymbolicCollection -} - -abstract class USymbolicCollectionIdWithContextMemory< - Key, Sort : USort, - out CollectionId : USymbolicCollectionId>( - val contextMemory: UWritableMemory<*>?, -) : USymbolicCollectionId { - - override fun instantiate( - collection: USymbolicCollection<@UnsafeVariance CollectionId, Key, Sort>, - key: Key - ): UExpr = if (contextMemory == null) { - sort.uctx.mkReading(collection, key) - } else { - collection.applyTo(contextMemory) - val lValue = sort.uctx.mkLValue(key) - contextMemory.read(lValue) - } - - abstract fun UContext.mkReading( - collection: USymbolicCollection<@UnsafeVariance CollectionId, Key, Sort>, - key: Key - ): UExpr - - abstract fun UContext.mkLValue(key: Key): ULValue<*, Sort> - - override fun write(memory: UWritableMemory, key: Key, value: UExpr, guard: UBoolExpr) { - val lValue = guard.uctx.mkLValue(key) - memory.write(lValue, value, guard) - } -} +} \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionKeyInfo.kt b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionKeyInfo.kt index 0831c9b076..90024d5f63 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionKeyInfo.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionKeyInfo.kt @@ -1,13 +1,18 @@ package org.usvm.memory import org.usvm.UBoolExpr +import org.usvm.UComposer import org.usvm.UContext +import org.usvm.UTransformer import org.usvm.util.Region /** * Provides information about entities used as keys of symbolic collections. */ -interface USymbolicCollectionKeyInfo> { +interface USymbolicCollectionKeyInfo> { + + fun mapKey(key: Key, composer: UComposer<*>?): Key + /** * Returns symbolic expression guaranteeing that [key1] is same as [key2]. */ diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt index 621f4807f3..5ea08424f5 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt @@ -4,6 +4,7 @@ import org.usvm.UBoolExpr import org.usvm.UComposer import org.usvm.UExpr import org.usvm.USort +import org.usvm.compose import org.usvm.isTrue import org.usvm.uctx @@ -31,7 +32,7 @@ sealed interface UUpdateNode { * If [includesConcretely] returns true, then this method is obligated to return [UTrue]. * Returned condition must imply [guard]. */ - fun includesSymbolically(key: Key): UBoolExpr + fun includesSymbolically(key: Key, composer: UComposer<*>?): UBoolExpr /** * Checks if the value in this [UUpdateNode] indexed by the [key] satisfies the [predicate]. If it does, @@ -49,28 +50,18 @@ sealed interface UUpdateNode { predicate: (UExpr) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, + composer: UComposer<*>?, ): UUpdateNode? /** * @return Value which has been written into the address [key] during this memory write operation. */ - fun value(key: Key): UExpr + fun value(key: Key, composer: UComposer<*>?): UExpr /** * Guard is a symbolic condition for this update. That is, this update is done only in states satisfying this guard. */ val guard: UBoolExpr - - /** - * Returns a mapped update node using [keyMapper] and [composer]. - * It is used in [UComposer] for composition. - * For some key, [keyMapper] might return null. Then, this function returns null as well. - */ - fun map( - keyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): UUpdateNode? } /** @@ -86,29 +77,34 @@ class UPinpointUpdateNode( this.key == key && (guard == guard.ctx.trueExpr || guard == precondition) // in fact, we can check less strict formulae: `precondition -> guard`, but it is too complex to compute. - override fun includesSymbolically(key: Key): UBoolExpr = - guard.ctx.mkAnd(keyInfo.eqSymbolic(guard.uctx, this.key, key), guard) + override fun includesSymbolically(key: Key, composer: UComposer<*>?): UBoolExpr = + guard.ctx.mkAnd( + keyInfo.eqSymbolic(guard.uctx, keyInfo.mapKey(this.key, composer), key), + composer.compose(guard) + ) override fun isIncludedByUpdateConcretely( update: UUpdateNode, ): Boolean = update.includesConcretely(key, guard) - override fun value(key: Key): UExpr = this.value + override fun value(key: Key, composer: UComposer<*>?): UExpr = composer.compose(value) override fun split( key: Key, predicate: (UExpr) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, + composer: UComposer<*>?, ): UUpdateNode? { val ctx = value.ctx - val nodeIncludesKey = includesSymbolically(key) // includes guard + val nodeIncludesKey = includesSymbolically(key, composer) // includes guard val nodeExcludesKey = ctx.mkNot(nodeIncludesKey) val guard = guardBuilder.guarded(nodeIncludesKey) - val res = if (predicate(value)) { - matchingWrites += value with guard + val transformedValue = composer.compose(value) + val res = if (predicate(transformedValue)) { + matchingWrites += transformedValue with guard null } else { this @@ -119,25 +115,6 @@ class UPinpointUpdateNode( return res } - override fun map( - keyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): UPinpointUpdateNode? { - val mappedKey = keyMapper(key) ?: return null - val mappedValue = composer.compose(value) - val mappedGuard = composer.compose(guard) - - // If nothing changed, return this value - if (mappedKey === key && mappedValue === value && mappedGuard === guard) { - @Suppress("UNCHECKED_CAST") - return this as UPinpointUpdateNode - } - - // Otherwise, construct a new one update node - return UPinpointUpdateNode(mappedKey, mappedKeyInfo, mappedValue, mappedGuard) - } - override fun equals(other: Any?): Boolean = other is UPinpointUpdateNode<*, *> && this.key == other.key && this.guard == other.guard @@ -162,28 +139,29 @@ class URangedUpdateNode?): UBoolExpr = + guard.ctx.mkAnd(adapter.includesSymbolically(key, composer), composer.compose(guard)) override fun isIncludedByUpdateConcretely( update: UUpdateNode, - ): Boolean = - adapter.isIncludedByUpdateConcretely(update, guard) + ): Boolean = adapter.isIncludedByUpdateConcretely(update, guard) - override fun value(key: DstKey): UExpr = sourceCollection.read(adapter.convert(key)) + override fun value(key: DstKey, composer: UComposer<*>?): UExpr = + sourceCollection.read(adapter.convert(key, composer), composer) override fun split( key: DstKey, predicate: (UExpr) -> Boolean, matchingWrites: MutableList>>, guardBuilder: GuardBuilder, + composer: UComposer<*>?, ): UUpdateNode { val ctx = guardBuilder.nonMatchingUpdatesGuard.ctx - val nodeIncludesKey = includesSymbolically(key) // contains guard + val nodeIncludesKey = includesSymbolically(key, composer) // contains guard val nodeExcludesKey = ctx.mkNot(nodeIncludesKey) val nextGuard = guardBuilder.guarded(nodeIncludesKey) val nextGuardBuilder = GuardBuilder(nextGuard) @@ -199,7 +177,7 @@ class URangedUpdateNode { k1, 0x1 } -> mkArrayConst(nullRef) * | * | copy from [this.region]{ 1..5 } - * | [this.keyConverter] = id + * | [this.adapter.convert] = id * | * [this.region]: { k2, 0x3 } -> mkArrayConst(nullRef) * ``` @@ -213,12 +191,12 @@ class URangedUpdateNode map( - keyMapper: KeyMapper, - composer: UComposer, - mappedKeyInfo: USymbolicCollectionKeyInfo - ): URangedUpdateNode<*, *, MappedDstKey, Sort>? { - val mappedCollectionId = sourceCollection.collectionId.map(composer) - val (mappedAdapter, targetCollectionId) = adapter.map(keyMapper, composer, mappedCollectionId, mappedKeyInfo) - ?: return null - val mappedGuard = composer.compose(guard) - - val mappedCollection = sourceCollection.mapTo(composer, targetCollectionId) - - // If nothing changed, return this - if (mappedCollection === sourceCollection - && mappedAdapter === adapter - && mappedGuard === guard - ) { - return this as URangedUpdateNode<*, *, MappedDstKey, Sort> - } - - // Otherwise, construct a new one updated node - return URangedUpdateNode( - // Type variables in this cast are incorrect, but who cares... - mappedCollection as USymbolicCollection, - mappedAdapter as USymbolicCollectionAdapter, - mappedGuard - ) - } - // Ignores update override fun equals(other: Any?): Boolean = other is URangedUpdateNode<*, *, *, *> && - this.adapter == other.adapter && - this.guard == other.guard + this.adapter == other.adapter && + this.guard == other.guard // Ignores update override fun hashCode(): Int = adapter.hashCode() * 31 + guard.hashCode() - fun applyTo(memory: UWritableMemory<*>, dstCollectionId: USymbolicCollectionId) { - sourceCollection.applyTo(memory) - adapter.applyTo(memory, sourceCollection.collectionId, dstCollectionId, guard) + /** + * Applies this update node to the [memory] with applying composition via [composer]. + */ + fun applyTo( + memory: UWritableMemory<*>, + dstCollectionId: USymbolicCollectionId, + key: DstKey, + composer: UComposer<*>, + ) { + val convertedKey = adapter.convert(key, composer) + sourceCollection.applyTo(memory, convertedKey, composer) + adapter.applyTo( + memory, + sourceCollection.collectionId, + dstCollectionId, + composer.compose(guard), + convertedKey, + composer + ) } override fun toString(): String = diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/key/UHeapRefKeyInfo.kt b/usvm-core/src/main/kotlin/org/usvm/memory/key/UHeapRefKeyInfo.kt index 9dd73f9767..62eb659d3e 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/key/UHeapRefKeyInfo.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/key/UHeapRefKeyInfo.kt @@ -1,10 +1,12 @@ package org.usvm.memory.key import org.usvm.UBoolExpr +import org.usvm.UComposer import org.usvm.UConcreteHeapAddress import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UHeapRef +import org.usvm.compose import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.util.SetRegion @@ -14,6 +16,8 @@ typealias UHeapRefRegion = SetRegion * Provides information about heap references used as symbolic collection keys. */ object UHeapRefKeyInfo : USymbolicCollectionKeyInfo { + override fun mapKey(key: UHeapRef, composer: UComposer<*>?): UHeapRef = composer.compose(key) + override fun eqSymbolic(ctx: UContext, key1: UHeapRef, key2: UHeapRef): UBoolExpr = ctx.mkHeapRefEq(key1, key2) diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/key/USingleKeyInfo.kt b/usvm-core/src/main/kotlin/org/usvm/memory/key/USingleKeyInfo.kt deleted file mode 100644 index 717b6cf343..0000000000 --- a/usvm-core/src/main/kotlin/org/usvm/memory/key/USingleKeyInfo.kt +++ /dev/null @@ -1,20 +0,0 @@ -package org.usvm.memory.key - -import org.usvm.UBoolExpr -import org.usvm.UContext -import org.usvm.memory.USymbolicCollectionKeyInfo -import org.usvm.util.TrivialRegion - -object USingleKeyInfo : USymbolicCollectionKeyInfo { - override fun eqSymbolic(ctx: UContext, key1: Unit, key2: Unit): UBoolExpr = ctx.trueExpr - override fun eqConcrete(key1: Unit, key2: Unit): Boolean = true - override fun cmpSymbolicLe(ctx: UContext, key1: Unit, key2: Unit): UBoolExpr = singleKeyError() - override fun cmpConcreteLe(key1: Unit, key2: Unit): Boolean = singleKeyError() - override fun keyToRegion(key: Unit): TrivialRegion = singleKeyError() - override fun keyRangeRegion(from: Unit, to: Unit): TrivialRegion = singleKeyError() - override fun topRegion(): TrivialRegion = singleKeyError() - override fun bottomRegion(): TrivialRegion = singleKeyError() - - private fun singleKeyError(): Nothing = - error("Unexpected operation on single key") -} \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/key/USizeExprKeyInfo.kt b/usvm-core/src/main/kotlin/org/usvm/memory/key/USizeExprKeyInfo.kt index 6dc990e208..93266ecfca 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/key/USizeExprKeyInfo.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/key/USizeExprKeyInfo.kt @@ -1,10 +1,12 @@ package org.usvm.memory.key import org.usvm.UBoolExpr +import org.usvm.UComposer import org.usvm.UConcreteSize import org.usvm.UContext import org.usvm.USizeExpr import org.usvm.USizeType +import org.usvm.compose import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.util.SetRegion @@ -15,6 +17,8 @@ typealias USizeRegion = SetRegion * Provides information about numeric values used as symbolic collection keys. */ object USizeExprKeyInfo : USymbolicCollectionKeyInfo { + override fun mapKey(key: USizeExpr, composer: UComposer<*>?): USizeExpr = composer.compose(key) + override fun eqSymbolic(ctx: UContext, key1: USizeExpr, key2: USizeExpr): UBoolExpr = ctx.mkEq(key1, key2) diff --git a/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt index daa22dd55c..172d3af848 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt @@ -11,6 +11,8 @@ import org.usvm.UContext import org.usvm.UExpr import org.usvm.solver.UExprTranslator import org.usvm.UMockEvaluator +import org.usvm.memory.UMemoryRegionId +import org.usvm.memory.UReadOnlyMemoryRegion interface UModelDecoder { fun decode(model: KModel): Model @@ -117,8 +119,13 @@ open class ULazyModelDecoder( private fun decodeHeap( model: KModel, addressesMapping: AddressesMapping, - ) = translator.regionIdToDecoder.mapValues { (_, decoder) -> - decoder.decodeLazyRegion(model, addressesMapping) + ): Map, UReadOnlyMemoryRegion<*, *>> { + val result = mutableMapOf, UReadOnlyMemoryRegion<*, *>>() + for ((regionId, decoder) in translator.regionIdToDecoder) { + val modelRegion = decoder.decodeLazyRegion(model, addressesMapping) ?: continue + result[regionId] = modelRegion + } + return result } private fun decodeMocker( diff --git a/usvm-core/src/main/kotlin/org/usvm/model/Model.kt b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt index c47fe04dd4..c72bd3f35d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/Model.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt @@ -85,13 +85,10 @@ open class UModelBase( } } -fun modelEnsureConcreteInputRef(ref: UHeapRef): UConcreteHeapRef? { +fun modelEnsureConcreteInputRef(ref: UHeapRef): UConcreteHeapRef { // All the expressions in the model are interpreted, therefore, they must // have concrete addresses. Moreover, the model knows only about input values // which have addresses less or equal than INITIAL_INPUT_ADDRESS - if (ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { - return ref - } - - return null + require(ref is UConcreteHeapRef && ref.address <= INITIAL_INPUT_ADDRESS) { "Unexpected ref: $ref" } + return ref } diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt index f6290093a6..92f4e53b9f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt @@ -27,7 +27,7 @@ interface URegionTranslator { - fun decodeLazyRegion(model: KModel, mapping: Map): UReadOnlyMemoryRegion + fun decodeLazyRegion(model: KModel, mapping: Map): UReadOnlyMemoryRegion? } interface UCollectionDecoder { diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt index 63322af8a8..e8d9019d74 100644 --- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt @@ -10,31 +10,34 @@ import io.ksmt.sort.KBv32Sort import io.mockk.every import io.mockk.mockk import io.mockk.spyk +import io.mockk.verify import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test import org.junit.jupiter.api.assertThrows import org.usvm.api.writeArrayIndex import org.usvm.api.writeArrayLength import org.usvm.api.writeField +import org.usvm.collection.array.UAllocatedArrayId +import org.usvm.collection.array.UAllocatedArrayReading +import org.usvm.collection.array.UInputArrayId +import org.usvm.collection.array.UInputArrayReading +import org.usvm.collection.array.USymbolicArrayIndex +import org.usvm.collection.array.USymbolicArrayIndexKeyInfo +import org.usvm.collection.array.USymbolicArrayInputToInputCopyAdapter +import org.usvm.collection.array.length.UInputArrayLengthId +import org.usvm.collection.field.UFieldLValue +import org.usvm.collection.field.UInputFieldId import org.usvm.constraints.UTypeEvaluator +import org.usvm.memory.UFlatUpdates import org.usvm.memory.UMemory import org.usvm.memory.UPinpointUpdateNode import org.usvm.memory.URangedUpdateNode import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.UReadOnlyRegistersStack -import org.usvm.memory.UUpdateNode -import org.usvm.memory.UFlatUpdates import org.usvm.memory.USymbolicCollection import org.usvm.memory.USymbolicCollectionUpdates -import org.usvm.collection.array.USymbolicArrayInputToInputCopyAdapter -import org.usvm.collection.array.UAllocatedArrayId -import org.usvm.collection.array.UAllocatedArrayReading -import org.usvm.collection.array.UInputArrayId -import org.usvm.collection.array.UInputArrayReading -import org.usvm.collection.array.length.UInputArrayLengthId -import org.usvm.collection.field.UInputFieldId -import org.usvm.collection.array.USymbolicArrayIndex -import org.usvm.collection.array.USymbolicArrayIndexKeyInfo +import org.usvm.memory.UUpdateNode +import org.usvm.memory.UWritableMemory import org.usvm.model.UModelBase import org.usvm.model.URegistersStackEagerModel import org.usvm.util.SetRegion @@ -227,6 +230,9 @@ internal class CompositionTest { val sndResultValue = 2.toBv() val keyInfo = object : TestKeyInfo> { + override fun mapKey(key: UHeapRef, composer: UComposer<*>?): UHeapRef = + composer.compose(key) + override fun eqSymbolic(ctx: UContext, key1: UHeapRef, key2: UHeapRef): UBoolExpr = key1 eq key2 } @@ -275,6 +281,9 @@ internal class CompositionTest { } val keyInfo = object : TestKeyInfo> { + override fun mapKey(key: USymbolicArrayIndex, composer: UComposer<*>?): USymbolicArrayIndex = + composer.compose(key.first) to composer.compose(key.second) + override fun cmpConcreteLe(key1: USymbolicArrayIndex, key2: USymbolicArrayIndex): Boolean = key1 == key2 override fun eqSymbolic(ctx: UContext, key1: USymbolicArrayIndex, key2: USymbolicArrayIndex): UBoolExpr = keyEqualityComparer(key1, key2) @@ -374,6 +383,7 @@ internal class CompositionTest { val sndSymbolicIndex = mockk() val keyInfo = object : TestKeyInfo> { + override fun mapKey(key: USizeExpr, composer: UComposer<*>?): USizeExpr = composer.compose(key) override fun eqSymbolic(ctx: UContext, key1: USizeExpr, key2: USizeExpr): UBoolExpr = key1 eq key2 } @@ -456,6 +466,7 @@ internal class CompositionTest { val bAddress = mockk() val keyInfo = object : TestKeyInfo> { + override fun mapKey(key: UHeapRef, composer: UComposer<*>?): UHeapRef = composer.compose(key) override fun eqSymbolic(ctx: UContext, key1: UHeapRef, key2: UHeapRef): UBoolExpr = (key1 == key2).expr } @@ -612,4 +623,45 @@ internal class CompositionTest { val expr = composer.compose(reading) assertSame(concreteNull, expr) } + + @Test + fun testUpdatesSimplification() = with(ctx) { + val composedMemory: UReadOnlyMemory = mockk() + + val field = mockk() + + val ref0 = mkRegisterReading(0, addressSort) + val ref1 = mkRegisterReading(1, addressSort) + val ref2 = mkRegisterReading(2, addressSort) + + val region = UInputFieldId(field, bv32Sort) + .emptyRegion() + .write(ref0, mkBv(0), trueExpr) + .write(ref1, mkBv(1), trueExpr) + + val reading = region.read(ref2) + + val composer = spyk(UComposer(this, composedMemory)) + + val writableMemory: UWritableMemory = mockk() + + every { composer.transform(ref0) } returns mkConcreteHeapRef(-1) + every { composer.transform(ref1) } returns ref1 + every { composer.transform(ref2) } returns ref2 + + every { composedMemory.toWritableMemory() } returns writableMemory + + every { + val lvalue = UFieldLValue(bv32Sort, ref1, field) + writableMemory.write(lvalue, mkBv(1), trueExpr) + } returns Unit + every { + val lvalue = UFieldLValue(bv32Sort, ref2, field) + writableMemory.read(lvalue) + } returns mkBv(42) + + val composedReading = composer.compose(reading) + assertEquals(mkBv(42), composedReading) + verify(exactly = 1) { writableMemory.write(any>(), any(), any())} + } } diff --git a/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt b/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt index 54936cbdd2..c3b80e65e0 100644 --- a/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt +++ b/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt @@ -38,6 +38,11 @@ internal class TestState( } interface TestKeyInfo> : USymbolicCollectionKeyInfo { + override fun mapKey(key: T, composer: UComposer<*>?): T { + if (composer == null) return key + return shouldNotBeCalled() + } + override fun keyToRegion(key: T): Reg = shouldNotBeCalled() override fun eqSymbolic(ctx: UContext, key1: T, key2: T): UBoolExpr = shouldNotBeCalled() override fun eqConcrete(key1: T, key2: T): Boolean = shouldNotBeCalled() diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/MapCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/MapCompositionTest.kt deleted file mode 100644 index 6742fe0517..0000000000 --- a/usvm-core/src/test/kotlin/org/usvm/memory/MapCompositionTest.kt +++ /dev/null @@ -1,423 +0,0 @@ -package org.usvm.memory - -import io.ksmt.expr.KExpr -import io.ksmt.utils.mkConst -import io.mockk.every -import io.mockk.mockk -import org.junit.jupiter.api.BeforeEach -import org.junit.jupiter.api.Disabled -import org.junit.jupiter.api.Test -import org.usvm.TestKeyInfo -import org.usvm.UAddressSort -import org.usvm.UBoolExpr -import org.usvm.UBv32Sort -import org.usvm.UComponents -import org.usvm.UComposer -import org.usvm.UConcreteHeapRef -import org.usvm.UContext -import org.usvm.UExpr -import org.usvm.UHeapRef -import org.usvm.USizeExpr -import org.usvm.USizeSort -import org.usvm.collection.array.USymbolicArrayAllocatedToAllocatedCopyAdapter -import org.usvm.collection.array.USymbolicArrayCopyAdapter -import org.usvm.collection.array.UAllocatedArrayId -import org.usvm.util.SetRegion -import org.usvm.util.emptyRegionTree -import kotlin.test.assertEquals -import kotlin.test.assertFalse -import kotlin.test.assertNotNull -import kotlin.test.assertNotSame -import kotlin.test.assertNull -import kotlin.test.assertSame -import kotlin.test.assertTrue - -class MapCompositionTest { - private lateinit var ctx: UContext - private lateinit var composer: UComposer - - @BeforeEach - fun initializeContext() { - val components: UComponents = mockk() - every { components.mkTypeSystem(any()) } returns mockk() - ctx = UContext(components) - composer = mockk() - } - - @Test - @Disabled("Non clear") - fun testWriteIntoEmptyTreeRegionAfterComposition() = with(ctx) { - val concreteAddr = UConcreteHeapRef(this, address = 1) - val symbolicAddr = addressSort.mkConst("addr") - val value = bv32Sort.mkConst("value") - - val keyInfo = object : TestKeyInfo> { - override fun keyToRegion(key: UHeapRef): SetRegion { - val singleRegion: SetRegion> = SetRegion.singleton(concreteAddr) - return if (key == symbolicAddr) { - // Z \ {1} - SetRegion.universe().subtract(singleRegion) - } else { - // {1} - singleRegion - } - } - } - - val updatesToCompose = UTreeUpdates, UBv32Sort>( - updates = emptyRegionTree(), - keyInfo = keyInfo - ).write(symbolicAddr, value, guard = trueExpr) - - val composer = mockk>() - - every { composer.compose(symbolicAddr) } returns concreteAddr - every { composer.compose(value) } returns 1.toBv() - every { composer.compose(mkTrue()) } returns mkTrue() - - val composedUpdates = updatesToCompose.filterMap(keyMapper = { composer.compose(it) }, composer, keyInfo) - - // Why should updates be empty after composition? - assertTrue(composedUpdates.isEmpty()) - } - - @Test - fun testWriteIntoIntersectionAfterComposition() { - with(ctx) { - val fstConcreteAddr = mkConcreteHeapRef(address = 1) - val sndConcreteAddr = mkConcreteHeapRef(address = 2) - val thirdConcreteAddr = mkConcreteHeapRef(address = 3) - - val symbolicAddr = addressSort.mkConst("addr") - - val value = bv32Sort.mkConst("value") - - val keyInfo = object : TestKeyInfo> { - override fun keyToRegion(key: UHeapRef): SetRegion { - return when (key) { - // Z \ {1, 2} - symbolicAddr -> { - SetRegion.universe().subtract(SetRegion.ofSet(fstConcreteAddr, sndConcreteAddr)) - } - // {1, 2, 3} - thirdConcreteAddr -> SetRegion.ofSet(fstConcreteAddr, sndConcreteAddr, thirdConcreteAddr) - else -> SetRegion.singleton(key) - } - } - } - - val updatesToCompose = UTreeUpdates, UBv32Sort>( - updates = emptyRegionTree(), - keyInfo - ).write(symbolicAddr, value, guard = trueExpr) - - val composer = mockk>() - - every { composer.compose(symbolicAddr) } returns thirdConcreteAddr - every { composer.compose(value) } returns 1.toBv() - every { composer.compose(mkTrue()) } returns mkTrue() - - // ComposedUpdates contains only one update in a region {3} - val composedUpdates = updatesToCompose.filterMap(keyMapper = { composer.compose(it) }, composer, keyInfo) - - assertFalse(composedUpdates.isEmpty()) - - // Write in the composedUpdates by a key with estimated region {3} - // If we'd have an initial region for the third address, it'd contain an update by region {1, 2, 3} - // Therefore, such writings cause updates splitting. Otherwise, it contains only one update. - val updatedKeyInfo = object : TestKeyInfo> { - override fun keyToRegion(key: UHeapRef): SetRegion = - SetRegion.singleton(thirdConcreteAddr) - } - - val updatedByTheSameRegion = composedUpdates - .copy(keyInfo = updatedKeyInfo) - .write(thirdConcreteAddr, 42.toBv(), guard = trueExpr) - - assertNotNull(updatedByTheSameRegion.singleOrNull()) - } - } - - @Test - fun testPinpointUpdateMapOperationWithoutCompositionEffect() = with(ctx) { - val key = addressSort.mkConst("key") as UExpr - val value = bv32Sort.mkConst("value") - val guard = boolSort.mkConst("guard") - - val keyInfo = object : TestKeyInfo> { - override fun eqSymbolic(ctx: UContext, key1: UHeapRef, key2: UHeapRef): UBoolExpr = key1 eq key2 - } - - val updateNode = UPinpointUpdateNode(key, keyInfo, value, guard) - - every { composer.compose(key) } returns key - every { composer.compose(value) } returns value - every { composer.compose(guard) } returns guard - - val mappedNode = updateNode.map({ k -> composer.compose(k) }, composer, keyInfo) - - assertSame(expected = updateNode, actual = mappedNode) - } - - @Test - fun testPinpointUpdateMapOperation() = with(ctx) { - val key = addressSort.mkConst("key") as UExpr - val value = bv32Sort.mkConst("value") - val guard = boolSort.mkConst("guard") - - val keyInfo = object : TestKeyInfo> { - override fun eqSymbolic(ctx: UContext, key1: UHeapRef, key2: UHeapRef): UBoolExpr = key1 eq key2 - } - - val updateNode = UPinpointUpdateNode(key, keyInfo, value, guard) - - val composedKey = addressSort.mkConst("interpretedKey") - - every { composer.compose(key) } returns composedKey - every { composer.compose(value) } returns 1.toBv() - every { composer.compose(guard) } returns mkTrue() - - val mappedNode = updateNode.map({ k -> composer.compose(k) }, composer, keyInfo) - - assertNotSame(illegal = updateNode, actual = mappedNode) - assertSame(expected = composedKey, actual = mappedNode?.key) - assertSame(expected = 1.toBv(), actual = mappedNode?.value) - assertSame(expected = mkTrue(), actual = mappedNode?.guard) - } - - @Test - fun testRangeUpdateNodeWithoutCompositionEffect() = with(ctx) { - val fromKey = sizeSort.mkConst("fromKey") as UExpr - val toKey = sizeSort.mkConst("toKey") as UExpr - val guard = boolSort.mkConst("guard") - - val keyInfo = object : TestKeyInfo> { - } - - val region = UAllocatedArrayId(Unit, bv32Sort, address = 1).emptyRegion() - val updateNode = URangedUpdateNode( - region, - USymbolicArrayAllocatedToAllocatedCopyAdapter(fromKey, fromKey, toKey, keyInfo), - guard - ) - - every { composer.compose(fromKey) } returns fromKey - every { composer.apply(fromKey) } returns fromKey - - every { composer.compose(toKey) } returns toKey - every { composer.apply(toKey) } returns toKey - - every { composer.compose(guard) } returns guard - - every { composer.compose(mkBv(0)) } returns mkBv(0) - every { composer.memory } returns UMemory(ctx, mockk()) - - val mappedUpdateNode = updateNode.map({ k -> composer.compose((k)) }, composer, keyInfo) - - // Region.contextMemory changed after composition - assertEquals(expected = updateNode, actual = mappedUpdateNode) - } - - @Test - fun testRangeUpdateNodeMapOperation() = with(ctx) { - val addr = mkConcreteHeapRef(0) - val fromKey = sizeSort.mkConst("fromKey") - val toKey = sizeSort.mkConst("toKey") - val guard = boolSort.mkConst("guard") - - val keyInfo = object : TestKeyInfo> { - } - - val region = UAllocatedArrayId(Unit, bv32Sort, addr.address).emptyRegion() - val updateNode = URangedUpdateNode( - region, - USymbolicArrayAllocatedToAllocatedCopyAdapter(fromKey, fromKey, toKey, keyInfo), - guard - ) - - val composedFromKey = sizeSort.mkConst("composedFromKey") - val composedToKey = sizeSort.mkConst("composedToKey") - val composedGuard = mkTrue() - - every { composer.compose(addr) } returns addr - - every { composer.compose(fromKey) } returns composedFromKey - every { composer.apply(fromKey) } returns composedFromKey - - every { composer.compose(toKey) } returns composedToKey - every { composer.apply(toKey) } returns composedToKey - - every { composer.compose(guard) } returns composedGuard - every { composer.compose(mkBv(0)) } returns mkBv(0) - every { composer.memory } returns UMemory(ctx, mockk()) - - val mappedUpdateNode = updateNode.map({ k -> composer.compose((k)) }, composer, keyInfo) - - assertNotSame(illegal = updateNode, actual = mappedUpdateNode) - assertSame( - expected = composedFromKey, - actual = (mappedUpdateNode?.adapter as? USymbolicArrayCopyAdapter<*, *>)?.dstFrom - ) - assertSame( - expected = composedToKey, - actual = (mappedUpdateNode?.adapter as? USymbolicArrayCopyAdapter<*, *>)?.dstTo - ) - assertSame(expected = composedGuard, actual = mappedUpdateNode?.guard) - - // Region.contextMemory changed after composition - assertEquals(expected = region, actual = mappedUpdateNode?.sourceCollection) - } - - @Test - fun testEmptyUpdatesMapOperation() { - val keyInfo = object : TestKeyInfo> { - } - - val emptyUpdates = UFlatUpdates, UBv32Sort>(keyInfo) - - val mappedUpdates = emptyUpdates.filterMap({ k -> composer.compose(k) }, composer, keyInfo) - - assertSame(expected = emptyUpdates, actual = mappedUpdates) - } - - @Test - fun testFlatUpdatesMapOperationWithoutEffect() = with(ctx) { - val fstKey = addressSort.mkConst("fstKey") - val fstValue = bv32Sort.mkConst("fstValue") - val sndKey = addressSort.mkConst("sndKey") - val sndValue = bv32Sort.mkConst("sndValue") - - val keyInfo = object : TestKeyInfo> { - } - - val flatUpdates = UFlatUpdates, UBv32Sort>(keyInfo) - .write(fstKey, fstValue, guard = trueExpr) - .write(sndKey, sndValue, guard = trueExpr) - - every { composer.compose(fstKey) } returns fstKey - every { composer.compose(sndKey) } returns sndKey - every { composer.compose(fstValue) } returns fstValue - every { composer.compose(sndValue) } returns sndValue - every { composer.compose(mkTrue()) } returns mkTrue() - - val mappedUpdates = flatUpdates.filterMap({ k -> composer.compose(k) }, composer, keyInfo) - - assertSame(expected = flatUpdates, actual = mappedUpdates) - } - - @Test - fun testFlatUpdatesMapOperation() = with(ctx) { - val fstKey = addressSort.mkConst("fstKey") - val fstValue = bv32Sort.mkConst("fstValue") - val sndKey = addressSort.mkConst("sndKey") - val sndValue = bv32Sort.mkConst("sndValue") - - val keyInfo = object : TestKeyInfo> { - } - - val flatUpdates = UFlatUpdates, UBv32Sort>(keyInfo) - .write(fstKey, fstValue, guard = trueExpr) - .write(sndKey, sndValue, guard = trueExpr) - - val composedFstKey = addressSort.mkConst("composedFstKey") - val composedSndKey = addressSort.mkConst("composedSndKey") - val composedFstValue = 1.toBv() - val composedSndValue = 2.toBv() - - every { composer.compose(fstKey) } returns composedFstKey - every { composer.compose(sndKey) } returns composedSndKey - every { composer.compose(fstValue) } returns composedFstValue - every { composer.compose(sndValue) } returns composedSndValue - every { composer.compose(mkTrue()) } returns mkTrue() - - val mappedUpdates = flatUpdates.filterMap({ k -> composer.compose(k) }, composer, keyInfo) - - assertNotSame(illegal = flatUpdates, actual = mappedUpdates) - - val node = mappedUpdates.node?.update as UPinpointUpdateNode<*, *> - val next = mappedUpdates.node.next as UFlatUpdates<*, *> - val nextNode = next.node?.update as UPinpointUpdateNode<*, *> - - assertSame(expected = composedSndKey, actual = node.key) - assertSame(expected = composedSndValue, actual = node.value) - assertSame(expected = composedFstKey, actual = nextNode.key) - assertSame(expected = composedFstValue, actual = nextNode.value) - assertNull(next.node.next.node) - } - - @Test - fun testTreeUpdatesMapOperationWithoutEffect() = with(ctx) { - val fstKey = addressSort.mkConst("fstKey") - val fstValue = bv32Sort.mkConst("fstValue") - val sndKey = addressSort.mkConst("sndKey") - val sndValue = bv32Sort.mkConst("sndValue") - - val keyInfo = object : TestKeyInfo> { - override fun keyToRegion(key: UHeapRef): SetRegion = SetRegion.singleton(key) - override fun keyRangeRegion(from: UHeapRef, to: UHeapRef): SetRegion = - SetRegion.ofSet(from, to) - } - - val treeUpdates = UTreeUpdates, SetRegion>, UBv32Sort>( - emptyRegionTree(), - keyInfo - ).write(fstKey, fstValue, guard = trueExpr) - .write(sndKey, sndValue, guard = trueExpr) - - every { composer.compose(fstKey) } returns fstKey - every { composer.compose(sndKey) } returns sndKey - every { composer.compose(fstValue) } returns fstValue - every { composer.compose(sndValue) } returns sndValue - every { composer.compose(mkTrue()) } returns mkTrue() - - val mappedUpdates = treeUpdates.filterMap({ k -> composer.compose(k) }, composer, keyInfo) - - assertSame(expected = treeUpdates, actual = mappedUpdates) - } - - @Test - fun testTreeUpdatesMapOperation() = with(ctx) { - val fstKey = addressSort.mkConst("fstKey") - val fstValue = bv32Sort.mkConst("fstValue") - val sndKey = addressSort.mkConst("sndKey") - val sndValue = bv32Sort.mkConst("sndValue") - - val keyInfo = object : TestKeyInfo> { - override fun keyToRegion(key: UHeapRef): SetRegion = SetRegion.universe() - override fun keyRangeRegion(from: UHeapRef, to: UHeapRef): SetRegion = SetRegion.universe() - } - - val treeUpdates = UTreeUpdates, SetRegion>, UBv32Sort>( - emptyRegionTree(), - keyInfo - ).write(fstKey, fstValue, guard = trueExpr) - .write(sndKey, sndValue, guard = trueExpr) - - val composedFstKey = addressSort.mkConst("composedFstKey") - val composedSndKey = addressSort.mkConst("composedSndKey") - val composedFstValue = 1.toBv() - val composedSndValue = 2.toBv() - - every { composer.compose(fstKey) } returns composedFstKey - every { composer.compose(sndKey) } returns composedSndKey - every { composer.compose(fstValue) } returns composedFstValue - every { composer.compose(sndValue) } returns composedSndValue - every { composer.compose(mkTrue()) } returns mkTrue() - - val mappedUpdates = treeUpdates.filterMap({ k -> composer.compose(k) }, composer, keyInfo) - - assertNotSame(illegal = treeUpdates, actual = mappedUpdates) - - val elements = mappedUpdates.toList() - - assert(elements.size == 2) - - val fstElement = elements.first() as UPinpointUpdateNode<*, *> - val sndElement = elements.last() as UPinpointUpdateNode<*, *> - - assertSame(expected = composedFstKey, actual = fstElement.key) - assertSame(expected = composedFstValue, actual = fstElement.value) - assertSame(expected = composedSndKey, actual = sndElement.key) - assertSame(expected = composedSndValue, actual = sndElement.value) - } -} diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/UpdatesIteratorTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/UpdatesIteratorTest.kt index a281ec045c..7636dd073f 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/UpdatesIteratorTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/UpdatesIteratorTest.kt @@ -89,7 +89,7 @@ class UpdatesIteratorTest { elements.zip(expectedValues).forEach { (pinpointUpdate, expectedKeyWithValue) -> val key = (pinpointUpdate as UPinpointUpdateNode).key - val value = pinpointUpdate.value(key) + val value = pinpointUpdate.value(key, composer = null) assertTrue { key == expectedKeyWithValue.first && value == expectedKeyWithValue.second } } diff --git a/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt b/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt index 8c042d525d..e6b8ac3baa 100644 --- a/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt @@ -191,7 +191,7 @@ class TranslationTest { val reading = concreteRegion.read(idx) - val key = region.collectionId.keyMapper(translator)(adapter.convert(translator.translate(idx))) + val key = region.collectionId.keyMapper(translator)(adapter.convert(translator.translate(idx), composer = null)) val innerReading = translator.translate(region.read(key)) val guard = 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 61e18bbeba..3610b4325d 100644 --- a/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt +++ b/usvm-util/src/main/kotlin/org/usvm/util/RegionTree.kt @@ -25,19 +25,15 @@ class RegionTree( /** * Splits the region tree into two trees: completely covered by the [region] and disjoint with it. * - * [valueFilter] is an arbitrary predicate suitable to filter out values from the results of the function. + * [filterPredicate] is a predicate suitable to filter out particular nodes if their `value` don't satisfy it. * Examples: - * * `{ 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. - * + * * `{ true }` doesn't filter anything + * * `{ it != value }` writes into a tree and restrict for it to contain non-unique values. * @see localize */ private fun splitRecursively( region: Reg, - valueFilter: (Value) -> Boolean, + filterPredicate: (Value) -> Boolean, ): RecursiveSplitResult { if (isEmpty) { return RecursiveSplitResult(completelyCoveredRegionTree = this, disjointRegionTree = this) @@ -51,7 +47,7 @@ class RegionTree( val value = entry.first // IMPORTANT: usage of linked versions of maps is mandatory here, since // it is required for correct order of values returned by `iterator.next()` method - val completelyCoveredRegionTree = if (!valueFilter(value)) { + val completelyCoveredRegionTree = if (filterPredicate(value)) { val inside = persistentMapOf(region to entry) if (entries.size == 1) { this @@ -59,7 +55,8 @@ class RegionTree( RegionTree(inside) } } else { - entry.second + // fixme: here we might have a deep recursion, maybe we should rewrite it + entry.second.splitRecursively(region, filterPredicate).completelyCoveredRegionTree } val outside = entries.remove(region) val disjointRegionTree = RegionTree(outside) @@ -86,31 +83,31 @@ class RegionTree( fun MutableMap>>.addWithFilter( nodeRegion: Reg, valueWithRegionTree: Pair>, - valueFilter: (Value) -> Boolean, + filterPredicate: (Value) -> Boolean, ) { val (value, childRegionTree) = valueWithRegionTree - if (valueFilter(value)) { - putAll(childRegionTree.entries) - } else { + if (filterPredicate(value)) { put(nodeRegion, valueWithRegionTree) + } else { + putAll(childRegionTree.entries) } } entries.entries.forEach { (nodeRegion, valueWithRegionTree) -> when (region.compare(nodeRegion)) { - RegionComparisonResult.INCLUDES -> included.addWithFilter(nodeRegion, valueWithRegionTree, valueFilter) + RegionComparisonResult.INCLUDES -> included.addWithFilter(nodeRegion, valueWithRegionTree, filterPredicate) - RegionComparisonResult.DISJOINT -> disjoint.addWithFilter(nodeRegion, valueWithRegionTree, valueFilter) + RegionComparisonResult.DISJOINT -> disjoint.addWithFilter(nodeRegion, valueWithRegionTree, filterPredicate) // For nodes with intersection, repeat process recursively. RegionComparisonResult.INTERSECTS -> { val (value, childRegionTree) = valueWithRegionTree - val (splitIncluded, splitDisjoint) = childRegionTree.splitRecursively(region, valueFilter) + val (splitIncluded, splitDisjoint) = childRegionTree.splitRecursively(region, filterPredicate) val includedReg = nodeRegion.intersect(region) val disjointReg = nodeRegion.subtract(region) - included.addWithFilter(includedReg, value to splitIncluded, valueFilter) - disjoint.addWithFilter(disjointReg, value to splitDisjoint, valueFilter) + included.addWithFilter(includedReg, value to splitIncluded, filterPredicate) + disjoint.addWithFilter(disjointReg, value to splitDisjoint, filterPredicate) } } } @@ -126,15 +123,12 @@ 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. + * [filterPredicate] is a predicate suitable to filter out particular nodes if their `value` don't satisfy it. * Examples: - * * `{ false }` doesn't filter anything + * * `{ true }` 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} @@ -142,29 +136,25 @@ class RegionTree( * 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` + * // third will be filtered out * * ``` */ - fun localize(region: Reg, valueFilter: (Value) -> Boolean = { false }): RegionTree = - splitRecursively(region, valueFilter).completelyCoveredRegionTree + fun localize(region: Reg, filterPredicate: (Value) -> Boolean = { true }): RegionTree = + splitRecursively(region, filterPredicate).completelyCoveredRegionTree /** * Places a Pair([region], [value]) into the tree, preserving its invariants. * - * [valueFilter] is a predicate suitable to filter out particular nodes if their `value` satisfies it. + * [filterPredicate] is a predicate suitable to filter out particular nodes if their `value` don't satisfy it. * Examples: - * * `{ false }` doesn't filter anything + * * `{ true }` 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. - * * @see localize */ - fun write(region: Reg, value: Value, valueFilter: (Value) -> Boolean = { false }): RegionTree { - val (included, disjoint) = splitRecursively(region, valueFilter) + fun write(region: Reg, value: Value, filterPredicate: (Value) -> Boolean = { true }): RegionTree { + val (included, disjoint) = splitRecursively(region, filterPredicate) // A new node for a tree we construct accordingly to the (2) invariant. val node = value to included