From 25d037ac4f030b817b8e87b44758c04e8cb8edd3 Mon Sep 17 00:00:00 2001 From: Roman Pozharskiy Date: Thu, 18 Jul 2024 12:24:33 +0300 Subject: [PATCH] add ownership in memory --- usvm-core/src/main/kotlin/org/usvm/Context.kt | 2 + usvm-core/src/main/kotlin/org/usvm/Mocks.kt | 31 +++-- usvm-core/src/main/kotlin/org/usvm/State.kt | 15 +- .../src/main/kotlin/org/usvm/StateForker.kt | 19 +-- .../src/main/kotlin/org/usvm/StepScope.kt | 2 + .../src/main/kotlin/org/usvm/api/MemoryApi.kt | 3 +- .../usvm/api/collection/ListCollectionApi.kt | 1 + .../org/usvm/collection/array/ArrayRegion.kt | 64 +++++---- .../usvm/collection/array/ArrayRegionApi.kt | 12 +- .../collection/array/UArrayModelRegion.kt | 5 +- .../usvm/collection/array/USymbolicArrayId.kt | 4 +- .../array/length/ArrayLengthRegion.kt | 23 ++-- .../array/length/UArrayLengthModelRegion.kt | 5 +- .../org/usvm/collection/field/FieldsRegion.kt | 20 +-- .../collection/field/UFieldsModelRegion.kt | 5 +- .../map/length/UMapLengthModelRegion.kt | 5 +- .../collection/map/length/UMapLengthRegion.kt | 23 ++-- .../map/primitive/UMapModelRegion.kt | 5 +- .../collection/map/primitive/UMapRegion.kt | 64 +++++---- .../collection/map/primitive/UMapRegionApi.kt | 5 +- .../map/primitive/UMapRegionTranslator.kt | 4 +- .../map/primitive/USymbolicMapMergeAdapter.kt | 8 +- .../collection/map/ref/URefMapModelRegion.kt | 5 +- .../usvm/collection/map/ref/URefMapRegion.kt | 130 ++++++++++-------- .../collection/map/ref/URefMapRegionApi.kt | 2 +- .../map/ref/URefMapRegionTranslator.kt | 2 +- .../collection/set/USetCollectionDecoder.kt | 10 +- .../set/primitive/USetModelRegion.kt | 9 +- .../collection/set/primitive/USetRegion.kt | 71 +++++----- .../collection/set/primitive/USetRegionApi.kt | 5 +- .../set/primitive/USymbolicSetUnionAdapter.kt | 2 +- .../collection/set/ref/URefSetModelRegion.kt | 9 +- .../usvm/collection/set/ref/URefSetRegion.kt | 121 ++++++++-------- .../collection/set/ref/URefSetRegionApi.kt | 5 +- .../usvm/constraints/EqualityConstraints.kt | 7 +- .../org/usvm/constraints/PathConstraints.kt | 4 +- .../usvm/constraints/UNumericConstraints.kt | 18 +-- .../src/main/kotlin/org/usvm/memory/Memory.kt | 54 ++++---- .../kotlin/org/usvm/memory/RegistersStack.kt | 5 +- .../org/usvm/memory/USymbolicCollection.kt | 14 +- .../kotlin/org/usvm/memory/UpdateNodes.kt | 4 +- .../main/kotlin/org/usvm/merging/Merging.kt | 1 - .../org/usvm/merging/MergingPathSelector.kt | 2 +- .../kotlin/org/usvm/model/LazyModelDecoder.kt | 3 +- .../src/main/kotlin/org/usvm/model/Model.kt | 2 + .../kotlin/org/usvm/model/ModelRegions.kt | 13 +- .../kotlin/org/usvm/model/UModelEvaluator.kt | 20 +-- .../kotlin/org/usvm/ps/PathSelectorFactory.kt | 2 +- .../org/usvm/solver/RegionTranslator.kt | 2 +- .../main/kotlin/org/usvm/utils/StateUtils.kt | 2 +- .../test/kotlin/org/usvm/CompositionTest.kt | 35 ++--- .../src/test/kotlin/org/usvm/TestUtil.kt | 2 +- .../collections/SymbolicCollectionTestBase.kt | 10 +- .../kotlin/org/usvm/memory/HeapMemCpyTest.kt | 2 +- .../kotlin/org/usvm/memory/HeapMemsetTest.kt | 2 +- .../kotlin/org/usvm/memory/HeapRefEqTest.kt | 7 +- .../org/usvm/memory/HeapRefSplittingTest.kt | 5 +- .../org/usvm/memory/MemoryRegionTest.kt | 15 +- .../kotlin/org/usvm/memory/SetEntriesTest.kt | 2 +- .../org/usvm/merging/MemoryMergingTest.kt | 15 +- .../org/usvm/model/ModelCompositionTest.kt | 51 +++---- .../org/usvm/model/ModelDecodingTest.kt | 4 +- .../org/usvm/solver/SoftConstraintsTest.kt | 6 +- .../kotlin/org/usvm/solver/TranslationTest.kt | 71 +++++----- .../kotlin/org/usvm/types/TypeSolverTest.kt | 13 +- .../kotlin/org/usvm/machine/JcTransformer.kt | 3 +- .../machine/interpreter/JcCallSiteRegion.kt | 16 ++- .../machine/interpreter/JcExprResolver.kt | 12 +- .../statics/JcStaticFieldsRegion.kt | 32 ++--- .../kotlin/org/usvm/machine/state/JcState.kt | 25 ++-- .../main/kotlin/org/usvm/machine/PyMachine.kt | 8 +- .../org/usvm/machine/PyPathConstraints.kt | 14 +- .../main/kotlin/org/usvm/machine/PyState.kt | 10 +- .../model/regions/WrappedArrayIndexRegion.kt | 5 +- .../model/regions/WrappedArrayLengthRegion.kt | 5 +- .../model/regions/WrappedRefMapRegion.kt | 5 +- .../model/regions/WrappedRefSetRegion.kt | 5 +- .../machine/model/regions/WrappedSetRegion.kt | 5 +- .../kotlin/org/usvm/machine/SampleState.kt | 14 +- .../algorithms/PersistentMultiMapBuilder.kt | 8 +- .../usvm/collections/immutable/extensions.kt | 2 + .../immutableMap/TrieIterator.kt | 3 + .../implementations/immutableMap/TrieNode.kt | 11 +- .../kotlin/org/usvm/regions/RegionTree.kt | 2 +- 84 files changed, 704 insertions(+), 570 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt index dfda6180df..61f40773aa 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Context.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt @@ -42,6 +42,7 @@ import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElements import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading import org.usvm.collection.set.ref.UInputRefSetWithInputElements import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UAddressCounter import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.splitUHeapRef @@ -66,6 +67,7 @@ open class UContext( components.mkComposer(this) as (UReadOnlyMemory<*>) -> UComposer<*, USizeSort> } + val defaultOwnership = MutabilityOwnership() val sizeExprs by lazy { components.mkSizeExprProvider(this) } val statesForkProvider by lazy { components.mkStatesForkProvider() } diff --git a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt index c689ba2725..1025dfc0b7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt @@ -2,11 +2,12 @@ package org.usvm import io.ksmt.utils.cast import kotlinx.collections.immutable.PersistentList -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf +import org.usvm.collections.immutable.persistentHashMapOf import kotlinx.collections.immutable.persistentListOf +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.merging.MergeGuard -import org.usvm.merging.UMergeable +import org.usvm.merging.UOwnedMergeable interface UMockEvaluator { fun eval(symbol: UMockSymbol): UExpr @@ -26,14 +27,15 @@ interface UMocker : UMockEvaluator { fun getTrackedExpression(trackedLiteral: TrackedLiteral): UExpr - fun clone(): UMocker + fun clone(ownership: MutabilityOwnership): UMocker } class UIndexedMocker( - private var methodMockClauses: PersistentMap>> = persistentHashMapOf(), - private var trackedSymbols: PersistentMap> = persistentHashMapOf(), + private var methodMockClauses: UPersistentHashMap>> = persistentHashMapOf(), + private var trackedSymbols: UPersistentHashMap> = persistentHashMapOf(), private var untrackedSymbols: PersistentList> = persistentListOf(), -) : UMocker, UMergeable, MergeGuard> { + internal var ownership: MutabilityOwnership, +) : UMocker, UOwnedMergeable, MergeGuard> { override fun call( method: Method, args: Sequence>, @@ -42,7 +44,7 @@ class UIndexedMocker( val currentClauses = methodMockClauses.getOrDefault(method, persistentListOf()) val index = currentClauses.size val const = sort.uctx.mkIndexedMethodReturnValue(method, index, sort) - methodMockClauses = methodMockClauses.put(method, currentClauses.add(const)) + methodMockClauses = methodMockClauses.put(method, currentClauses.add(const), ownership) return const } @@ -50,7 +52,7 @@ class UIndexedMocker( override fun eval(symbol: UMockSymbol): UExpr = symbol override val trackedLiterals: Collection - get() = trackedSymbols.keys + get() = trackedSymbols.keys() /** * Creates a mock symbol. If [trackedLiteral] is not null, created expression @@ -60,7 +62,7 @@ class UIndexedMocker( val const = sort.uctx.mkTrackedSymbol(sort) if (trackedLiteral != null) { - trackedSymbols = trackedSymbols.put(trackedLiteral, const) + trackedSymbols = trackedSymbols.put(trackedLiteral, const, ownership) } else { untrackedSymbols = untrackedSymbols.add(const) } @@ -71,10 +73,11 @@ class UIndexedMocker( override fun getTrackedExpression(trackedLiteral: TrackedLiteral): UExpr { if (trackedLiteral !in trackedSymbols) error("Access by unregistered track literal $trackedLiteral") - return trackedSymbols.getValue(trackedLiteral).cast() + return trackedSymbols[trackedLiteral]!!.cast() } - override fun clone(): UIndexedMocker = UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols) + override fun clone(ownership: MutabilityOwnership): UIndexedMocker = + UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols, ownership) /** * Check if this [UIndexedMocker] can be merged with [other] indexed mocker. @@ -83,14 +86,14 @@ class UIndexedMocker( * * @return the merged indexed mocker. */ - override fun mergeWith(other: UIndexedMocker, by: MergeGuard): UIndexedMocker? { + override fun mergeWith(other: UIndexedMocker, by: MergeGuard, ownership: MutabilityOwnership): UIndexedMocker? { if (methodMockClauses !== other.methodMockClauses || trackedSymbols !== other.trackedSymbols || untrackedSymbols !== other.untrackedSymbols ) { return null } - + this.ownership = ownership return this } } diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt index 5f920c6c10..4505a3add0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/State.kt +++ b/usvm-core/src/main/kotlin/org/usvm/State.kt @@ -4,7 +4,6 @@ import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.constraints.UPathConstraints import org.usvm.memory.UMemory import org.usvm.merging.UMergeable -import org.usvm.merging.UOwnedMergeable import org.usvm.model.UModelBase import org.usvm.targets.UTarget import org.usvm.targets.UTargetsSet @@ -14,7 +13,7 @@ typealias StateId = UInt abstract class UState( // TODO: add interpreter-specific information val ctx: Context, - private var ownership : MutabilityOwnership, + initOwnership : MutabilityOwnership, open val callStack: UCallStack, open val pathConstraints: UPathConstraints, open val memory: UMemory, @@ -26,7 +25,7 @@ abstract class UState( open var pathNode: PathNode, open var forkPoints: PathNode>, open val targets: UTargetsSet, -) : UOwnedMergeable +) : UMergeable where Context : UContext<*>, Target : UTarget, State : UState { @@ -35,19 +34,23 @@ abstract class UState( * TODO: Can be replaced with overridden hashCode */ val id: StateId = ctx.getNextStateId() + + open var ownership = initOwnership + protected set - fun changeOwnership(newOwnership: MutabilityOwnership) { + protected fun changeOwnership(newOwnership: MutabilityOwnership) { ownership = newOwnership pathConstraints.changeOwnership(ownership) + memory.changeOwnership(ownership) } /** * Creates new state structurally identical to this. * If [newConstraints] is null, clones [pathConstraints]. Otherwise, uses [newConstraints] in cloned state. */ - abstract fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints? = null): State + abstract fun clone(newConstraints: UPathConstraints? = null): State - override fun mergeWith(other: State, by: Unit, ownership: MutabilityOwnership): State? = null + override fun mergeWith(other: State, by: Unit): State? = null override fun equals(other: Any?): Boolean { if (this === other) return true diff --git a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt index 412d4cbe43..4656307739 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt @@ -52,8 +52,7 @@ object WithSolverStateForker : StateForker { trueModels.isNotEmpty() && falseModels.isNotEmpty() -> { val posState = state - posState.changeOwnership(MutabilityOwnership()) - val negState = state.clone(MutabilityOwnership()) + val negState = state.clone() posState.models = trueModels negState.models = falseModels @@ -101,11 +100,9 @@ object WithSolverStateForker : StateForker { val (trueModels, _, _) = splitModelsByCondition(curState.models, condition) val nextRoot = if (trueModels.isNotEmpty()) { - val newOwnership = MutabilityOwnership() - val root = curState.clone(newOwnership) + val root = curState.clone() curState.models = trueModels curState.pathConstraints += condition - curState.changeOwnership(MutabilityOwnership()) root } else { @@ -167,14 +164,12 @@ object WithSolverStateForker : StateForker { // heavy plusAssign operator in path constraints. // Therefore, it is better to reuse already constructed [constraintToCheck]. if (stateToCheck) { - state.changeOwnership(MutabilityOwnership()) - val forkedState = state.clone(newOwnership, constraintsToCheck) + val forkedState = state.clone(constraintsToCheck) state.pathConstraints += newConstraintToOriginalState forkedState.models = listOf(satResult.model) forkedState } else { - val forkedState = state.clone(newOwnership) - state.changeOwnership(MutabilityOwnership()) + val forkedState = state.clone() state.pathConstraints += newConstraintToOriginalState state.models = listOf(satResult.model) // TODO: implement path condition setter (don't forget to reset UMemoryBase:types!) @@ -204,13 +199,13 @@ object NoSolverStateForker : StateForker { clonedPathConstraints += condition val (posState, negState) = if (clonedPathConstraints.isFalse) { + // changing ownership is unnecessary state.pathConstraints += notCondition state.models = falseModels - state.changeOwnership(MutabilityOwnership()) null to state.takeIf { !it.pathConstraints.isFalse } } else { - val falseState = state.clone(newOwnership) + val falseState = state.clone() // TODO how to reuse "clonedPathConstraints" here? state.pathConstraints += condition @@ -242,7 +237,7 @@ object NoSolverStateForker : StateForker { continue } - val nextRoot = curState.clone(newOwnership) + val nextRoot = curState.clone() curState.models = trueModels // TODO how to reuse "clonedConstraints"? diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt index a80a1e0805..780635c3d3 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt @@ -43,6 +43,8 @@ class StepScope, Type, Statement, val isDead: Boolean get() = stepScopeState === DEAD + val ownership = originalState.ownership + /** * Executes [block] on a state. * diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt index 89f259894f..4740d86dd5 100644 --- a/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt @@ -6,7 +6,6 @@ import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort -import org.usvm.memory.UMemory import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.UWritableMemory import org.usvm.collection.array.UArrayIndexLValue @@ -89,7 +88,7 @@ fun UWritableMemory.mems type: ArrayType, sort: Sort, sizeSort: USizeSort, - contents: Sequence> + contents: Sequence>, ) { memsetInternal(ref, type, sort, sizeSort, contents) } diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt index 438955a882..65d77a8574 100644 --- a/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt @@ -158,6 +158,7 @@ object ListCollectionApi { srcFrom: UExpr, dstFrom: UExpr, length: UExpr, + ) { memory.memcpy( srcRef = srcRef, diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt index 4c7dc1b96b..e3e86f2859 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 @@ -1,12 +1,13 @@ package org.usvm.collection.array -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UBoolExpr import org.usvm.UConcreteHeapAddress import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -50,6 +51,7 @@ interface UArrayRegion : UMemoryRegi fromDstIdx: UExpr, toDstIdx: UExpr, operationGuard: UBoolExpr, + ownership: MutabilityOwnership, ): UArrayRegion fun initializeAllocatedArray( @@ -57,30 +59,33 @@ interface UArrayRegion : UMemoryRegi arrayType: ArrayType, sort: Sort, content: Map, UExpr>, - operationGuard: UBoolExpr + operationGuard: UBoolExpr, + ownership: MutabilityOwnership, ): UArrayRegion } internal class UArrayMemoryRegion( - private var allocatedArrays: PersistentMap> = persistentHashMapOf(), + private var allocatedArrays: UPersistentHashMap> = persistentHashMapOf(), private var inputArray: UInputArray? = null ) : UArrayRegion { private fun getAllocatedArray( arrayType: ArrayType, sort: Sort, - address: UConcreteHeapAddress + address: UConcreteHeapAddress, + ownership: MutabilityOwnership ): UAllocatedArray { - var collection = allocatedArrays[address] - if (collection == null) { - collection = UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address).emptyRegion() - allocatedArrays = allocatedArrays.put(address, collection) - } + val (updatedArrays, collection) = + allocatedArrays.getOrPut(address, UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address).emptyRegion(), ownership) + allocatedArrays = updatedArrays return collection } - private fun updateAllocatedArray(ref: UConcreteHeapAddress, updated: UAllocatedArray) = - UArrayMemoryRegion(allocatedArrays.put(ref, updated), inputArray) + private fun updateAllocatedArray( + ref: UConcreteHeapAddress, + updated: UAllocatedArray, + ownership: MutabilityOwnership + ) = UArrayMemoryRegion(allocatedArrays.put(ref, updated, ownership), inputArray) private fun getInputArray(arrayType: ArrayType, sort: Sort): UInputArray { if (inputArray == null) @@ -91,27 +96,28 @@ internal class UArrayMemoryRegion( private fun updateInput(updated: UInputArray) = UArrayMemoryRegion(allocatedArrays, updated) - override fun read(key: UArrayIndexLValue): UExpr = key.ref.mapWithStaticAsSymbolic( - concreteMapper = { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address).read(key.index) }, - symbolicMapper = { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index) } + override fun read(key: UArrayIndexLValue, ownership: MutabilityOwnership): UExpr = key.ref.mapWithStaticAsSymbolic( + concreteMapper = { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address, ownership).read(key.index, ownership) }, + symbolicMapper = { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index, ownership) } ) override fun write( key: UArrayIndexLValue, value: UExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership ): UMemoryRegion, Sort> = foldHeapRefWithStaticAsSymbolic( key.ref, initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, innerGuard) -> - val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address) - val newRegion = oldRegion.write(key.index, value, innerGuard) - region.updateAllocatedArray(concreteRef.address, newRegion) + val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address, ownership) + val newRegion = oldRegion.write(key.index, value, innerGuard, ownership) + region.updateAllocatedArray(concreteRef.address, newRegion, ownership) }, blockOnSymbolic = { region, (symbolicRef, innerGuard) -> val oldRegion = region.getInputArray(key.arrayType, key.sort) - val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard) + val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard, ownership) region.updateInput(newRegion) } ) @@ -125,23 +131,24 @@ internal class UArrayMemoryRegion( fromDstIdx: UExpr, toDstIdx: UExpr, operationGuard: UBoolExpr, + ownership: MutabilityOwnership, ) = foldHeapRef2( ref0 = srcRef, ref1 = dstRef, initial = this, initialGuard = operationGuard, blockOnConcrete0Concrete1 = { region, srcConcrete, dstConcrete, guard -> - val srcCollection = region.getAllocatedArray(type, elementSort, srcConcrete.address) - val dstCollection = region.getAllocatedArray(type, elementSort, dstConcrete.address) + val srcCollection = region.getAllocatedArray(type, elementSort, srcConcrete.address, ownership) + val dstCollection = region.getAllocatedArray(type, elementSort, dstConcrete.address, ownership) val adapter = USymbolicArrayAllocatedToAllocatedCopyAdapter( fromSrcIdx, fromDstIdx, toDstIdx, USizeExprKeyInfo() ) val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard) - region.updateAllocatedArray(dstConcrete.address, newDstCollection) + region.updateAllocatedArray(dstConcrete.address, newDstCollection, ownership) }, blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard -> - val srcCollection = region.getAllocatedArray(type, elementSort, srcConcrete.address) + val srcCollection = region.getAllocatedArray(type, elementSort, srcConcrete.address, ownership) val dstCollection = region.getInputArray(type, elementSort) val adapter = USymbolicArrayAllocatedToInputCopyAdapter( fromSrcIdx, @@ -154,7 +161,7 @@ internal class UArrayMemoryRegion( }, blockOnSymbolic0Concrete1 = { region, srcSymbolic, dstConcrete, guard -> val srcCollection = region.getInputArray(type, elementSort) - val dstCollection = region.getAllocatedArray(type, elementSort, dstConcrete.address) + val dstCollection = region.getAllocatedArray(type, elementSort, dstConcrete.address, ownership) val adapter = USymbolicArrayInputToAllocatedCopyAdapter( srcSymbolic to fromSrcIdx, fromDstIdx, @@ -162,7 +169,7 @@ internal class UArrayMemoryRegion( USizeExprKeyInfo() ) val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard) - region.updateAllocatedArray(dstConcrete.address, newDstCollection) + region.updateAllocatedArray(dstConcrete.address, newDstCollection, ownership) }, blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard -> val srcCollection = region.getInputArray(type, elementSort) @@ -183,10 +190,11 @@ internal class UArrayMemoryRegion( arrayType: ArrayType, sort: Sort, content: Map, UExpr>, - operationGuard: UBoolExpr + operationGuard: UBoolExpr, + ownership: MutabilityOwnership ): UArrayMemoryRegion { val arrayId = UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address) val newCollection = arrayId.initializedArray(content, operationGuard) - return UArrayMemoryRegion(allocatedArrays.put(address, newCollection), inputArray) + return UArrayMemoryRegion(allocatedArrays.put(address, newCollection, ownership), inputArray) } } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt index 8136f72a3f..c9bb414a03 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt @@ -6,7 +6,6 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort import org.usvm.collection.array.length.UArrayLengthLValue -import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UWritableMemory import org.usvm.mkSizeExpr import org.usvm.uctx @@ -29,7 +28,7 @@ internal fun UWritableMemory<*>.mem "memcpy is not applicable to $region" } - val newRegion = region.memcpy(srcRef, dstRef, type, elementSort, fromSrcIdx, fromDstIdx, toDstIdx, guard) + val newRegion = region.memcpy(srcRef, dstRef, type, elementSort, fromSrcIdx, fromDstIdx, toDstIdx, guard, ownership) setRegion(regionId, newRegion) } @@ -52,7 +51,14 @@ internal fun UWritableMemory( ) : UReadOnlyMemoryRegion, Sort> { abstract val inputArray: UReadOnlyMemoryRegion, Sort> - override fun read(key: UArrayIndexLValue): UExpr { + override fun read(key: UArrayIndexLValue, ownership: MutabilityOwnership): UExpr { val ref = modelEnsureConcreteInputRef(key.ref) - return inputArray.read(ref to key.index) + return inputArray.read(ref to key.index, ownership) } } 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 d621bca821..bc52685804 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 @@ -42,7 +42,7 @@ class UAllocatedArrayId internal con override fun instantiate( collection: USymbolicCollection, UExpr, Sort>, key: UExpr, - composer: UComposer<*, *>? + composer: UComposer<*, *>?, ): UExpr { if (collection.updates.isEmpty()) { return composer.compose(defaultValue) @@ -123,7 +123,7 @@ class UInputArrayId internal constru override fun instantiate( collection: USymbolicCollection, USymbolicArrayIndex, Sort>, key: USymbolicArrayIndex, - composer: UComposer<*, *>? + composer: UComposer<*, *>?, ): UExpr { if (composer == null) { return sort.uctx.withSizeSort().mkInputArrayReading(collection, key.first, key.second) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt index 693b237371..1234b8a464 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 @@ -1,12 +1,13 @@ package org.usvm.collection.array.length -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UBoolExpr import org.usvm.UConcreteHeapAddress import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -42,11 +43,11 @@ interface UArrayLengthsRegion : UMemoryRegion( private val sort: USizeSort, private val arrayType: ArrayType, - private val allocatedLengths: PersistentMap> = persistentHashMapOf(), + private val allocatedLengths: UPersistentHashMap> = persistentHashMapOf(), private var inputLengths: UInputArrayLengths? = null ) : UArrayLengthsRegion { - private fun updateAllocated(updated: PersistentMap>) = + private fun updateAllocated(updated: UPersistentHashMap>) = UArrayLengthsMemoryRegion(sort, arrayType, updated, inputLengths) private fun getInputLength(ref: UArrayLengthLValue): UInputArrayLengths { @@ -58,28 +59,30 @@ internal class UArrayLengthsMemoryRegion( private fun updatedInput(updated: UInputArrayLengths) = UArrayLengthsMemoryRegion(sort, arrayType, allocatedLengths, updated) - override fun read(key: UArrayLengthLValue): UExpr = key.ref.mapWithStaticAsSymbolic( - concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() }, - symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef) } + override fun read(key: UArrayLengthLValue, ownership: MutabilityOwnership): UExpr = + key.ref.mapWithStaticAsSymbolic( + concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() }, + symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef, ownership) } ) override fun write( key: UArrayLengthLValue, value: UExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership ) = foldHeapRefWithStaticAsSymbolic( key.ref, initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, innerGuard) -> - val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard) { + val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard, ownership) { sort.sampleUValue() } region.updateAllocated(newRegion) }, blockOnSymbolic = { region, (symbolicRef, innerGuard) -> val oldRegion = region.getInputLength(key) - val newRegion = oldRegion.write(symbolicRef, value, innerGuard) + val newRegion = oldRegion.write(symbolicRef, value, innerGuard, ownership) region.updatedInput(newRegion) } ) 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 625520868b..2d330e66a7 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 @@ -3,6 +3,7 @@ package org.usvm.collection.array.length import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelEvaluator import org.usvm.model.modelEnsureConcreteInputRef @@ -13,9 +14,9 @@ abstract class UArrayLengthModelRegion( ) : UReadOnlyMemoryRegion, USizeSort> { abstract val inputArrayLength: UReadOnlyMemoryRegion - override fun read(key: UArrayLengthLValue): UExpr { + override fun read(key: UArrayLengthLValue, ownership: MutabilityOwnership): UExpr { val ref = modelEnsureConcreteInputRef(key.ref) - return inputArrayLength.read(ref) + return inputArrayLength.read(ref, ownership) } } 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 400496f117..381b9e40f3 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 @@ -1,12 +1,13 @@ package org.usvm.collection.field -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UBoolExpr import org.usvm.UConcreteHeapAddress import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -39,11 +40,11 @@ interface UFieldsRegion : UMemoryRegion( private val sort: Sort, private val field: Field, - private val allocatedFields: PersistentMap> = persistentHashMapOf(), + private val allocatedFields: UPersistentHashMap> = persistentHashMapOf(), private var inputFields: UInputFields? = null ) : UFieldsRegion { - private fun updateAllocated(updated: PersistentMap>) = + private fun updateAllocated(updated: UPersistentHashMap>) = UFieldsMemoryRegion(sort, field, updated, inputFields) private fun getInputFields(ref: UFieldLValue): UInputFields { @@ -55,28 +56,29 @@ internal class UFieldsMemoryRegion( private fun updateInput(updated: UInputFields) = UFieldsMemoryRegion(sort, field, allocatedFields, updated) - override fun read(key: UFieldLValue): UExpr = key.ref.mapWithStaticAsSymbolic( + override fun read(key: UFieldLValue, ownership: MutabilityOwnership): UExpr = key.ref.mapWithStaticAsSymbolic( concreteMapper = { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() }, - symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef) } + symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef, ownership) } ) override fun write( key: UFieldLValue, value: UExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership ): UMemoryRegion, Sort> = foldHeapRefWithStaticAsSymbolic( key.ref, initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, innerGuard) -> - val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard) { + val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard, ownership) { sort.sampleUValue() } region.updateAllocated(newRegion) }, blockOnSymbolic = { region, (symbolicRef, innerGuard) -> val oldRegion = region.getInputFields(key) - val newRegion = oldRegion.write(symbolicRef, value, innerGuard) + val newRegion = oldRegion.write(symbolicRef, value, innerGuard, ownership) region.updateInput(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 a4b6aab5a2..052b32e47c 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 @@ -3,6 +3,7 @@ package org.usvm.collection.field import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelEvaluator import org.usvm.model.modelEnsureConcreteInputRef @@ -13,9 +14,9 @@ abstract class UFieldsModelRegion( ) : UReadOnlyMemoryRegion, Sort> { abstract val inputFields: UReadOnlyMemoryRegion - override fun read(key: UFieldLValue): UExpr { + override fun read(key: UFieldLValue, ownership: MutabilityOwnership): UExpr { val ref = modelEnsureConcreteInputRef(key.ref) - return inputFields.read(ref) + return inputFields.read(ref, ownership) } } 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 81a280919b..3bd90a17e9 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 @@ -3,6 +3,7 @@ package org.usvm.collection.map.length import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelEvaluator import org.usvm.model.modelEnsureConcreteInputRef @@ -13,9 +14,9 @@ abstract class UMapLengthModelRegion( ) : UReadOnlyMemoryRegion, USizeSort> { abstract val inputMapLength: UReadOnlyMemoryRegion - override fun read(key: UMapLengthLValue): UExpr { + override fun read(key: UMapLengthLValue, ownership: MutabilityOwnership): UExpr { val ref = modelEnsureConcreteInputRef(key.ref) - return inputMapLength.read(ref) + return inputMapLength.read(ref, ownership) } } 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 0ceacf1974..4ef9ae06f9 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 @@ -1,12 +1,13 @@ package org.usvm.collection.map.length -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UBoolExpr import org.usvm.UConcreteHeapAddress import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -43,11 +44,11 @@ interface UMapLengthRegion : UMemoryRegion( private val sort: USizeSort, private val mapType: MapType, - private val allocatedLengths: PersistentMap> = persistentHashMapOf(), + private val allocatedLengths: UPersistentHashMap> = persistentHashMapOf(), private var inputLengths: UInputMapLength? = null ) : UMapLengthRegion { - private fun updateAllocated(updated: PersistentMap>) = + private fun updateAllocated(updated: UPersistentHashMap>) = UMapLengthMemoryRegion(sort, mapType, updated, inputLengths) private fun getInputLength(ref: UMapLengthLValue): UInputMapLength { @@ -59,28 +60,30 @@ internal class UMapLengthMemoryRegion( private fun updateInput(updated: UInputMapLength) = UMapLengthMemoryRegion(sort, mapType, allocatedLengths, updated) - override fun read(key: UMapLengthLValue): UExpr = key.ref.mapWithStaticAsSymbolic( - concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() }, - symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef) } + override fun read(key: UMapLengthLValue, ownership: MutabilityOwnership): UExpr = + key.ref.mapWithStaticAsSymbolic( + concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() }, + symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef, ownership) } ) override fun write( key: UMapLengthLValue, value: UExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership ) = foldHeapRefWithStaticAsSymbolic( ref = key.ref, initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, innerGuard) -> - val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard) { + val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard, ownership) { sort.sampleUValue() } region.updateAllocated(newRegion) }, blockOnSymbolic = { region, (symbolicRef, innerGuard) -> val oldRegion = region.getInputLength(key) - val newRegion = oldRegion.write(symbolicRef, value, innerGuard) + val newRegion = oldRegion.write(symbolicRef, value, innerGuard, ownership) region.updateInput(newRegion) } ) 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 14021f29c1..ff10f56048 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 @@ -3,6 +3,7 @@ package org.usvm.collection.map.primitive import org.usvm.UExpr import org.usvm.USort import org.usvm.collection.map.USymbolicMapKey +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelEvaluator import org.usvm.model.modelEnsureConcreteInputRef @@ -14,9 +15,9 @@ abstract class UMapModelRegion, ValueSort> { abstract val inputMap: UReadOnlyMemoryRegion, ValueSort> - override fun read(key: UMapEntryLValue): UExpr { + override fun read(key: UMapEntryLValue, ownership: MutabilityOwnership): UExpr { val mapRef = modelEnsureConcreteInputRef(key.mapRef) - return inputMap.read(mapRef to key.mapKey) + return inputMap.read(mapRef to key.mapKey, ownership) } } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt index 44a1707ddd..bcf85ca99c 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 @@ -1,13 +1,14 @@ package org.usvm.collection.map.primitive -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort import org.usvm.collection.map.USymbolicMapKey import org.usvm.collection.set.primitive.USetRegion +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -58,7 +59,8 @@ interface UMapRegion, - initialGuard: UBoolExpr + initialGuard: UBoolExpr, + ownership: MutabilityOwnership, ): UMapRegion } @@ -67,7 +69,7 @@ internal class UMapMemoryRegion, Reg>, - private var allocatedMaps: PersistentMap, UAllocatedMap> = persistentHashMapOf(), + private var allocatedMaps: UPersistentHashMap, UAllocatedMap> = persistentHashMapOf(), private var inputMap: UInputMap? = null, ) : UMapRegion { init { @@ -77,25 +79,24 @@ internal class UMapMemoryRegion + id: UAllocatedMapId, + ownership: MutabilityOwnership ): UAllocatedMap { - var collection = allocatedMaps[id] - if (collection == null) { - collection = id.emptyRegion() - allocatedMaps = allocatedMaps.put(id, collection) - } + val (updatesMaps, collection) = allocatedMaps.getOrPut(id, id.emptyRegion(), ownership) + allocatedMaps = updatesMaps return collection } private fun updateAllocatedMap( id: UAllocatedMapId, - updatedMap: UAllocatedMap + updatedMap: UAllocatedMap, + ownership: MutabilityOwnership ) = UMapMemoryRegion( keySort, valueSort, mapType, keyInfo, - allocatedMaps.put(id, updatedMap), + allocatedMaps.put(id, updatedMap, ownership), inputMap ) @@ -116,32 +117,36 @@ internal class UMapMemoryRegion): UExpr = + override fun read( + key: UMapEntryLValue, + ownership: MutabilityOwnership + ): UExpr = key.mapRef.mapWithStaticAsSymbolic( concreteMapper = { concreteRef -> val id = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, concreteRef.address) - getAllocatedMap(id).read(key.mapKey) + getAllocatedMap(id, ownership).read(key.mapKey, ownership) }, - symbolicMapper = { symbolicRef -> getInputMap().read(symbolicRef to key.mapKey) } + symbolicMapper = { symbolicRef -> getInputMap().read(symbolicRef to key.mapKey, ownership) } ) override fun write( key: UMapEntryLValue, value: UExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership ) = foldHeapRefWithStaticAsSymbolic( ref = key.mapRef, initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, guard) -> val id = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, concreteRef.address) - val map = region.getAllocatedMap(id) - val newMap = map.write(key.mapKey, value, guard) - region.updateAllocatedMap(id, newMap) + val map = region.getAllocatedMap(id, ownership) + val newMap = map.write(key.mapKey, value, guard, ownership) + region.updateAllocatedMap(id, newMap, ownership) }, blockOnSymbolic = { region, (symbolicRef, guard) -> val map = region.getInputMap() - val newMap = map.write(symbolicRef to key.mapKey, value, guard) + val newMap = map.write(symbolicRef to key.mapKey, value, guard, ownership) region.updateInputMap(newMap) } ) @@ -151,7 +156,8 @@ internal class UMapMemoryRegion, - initialGuard: UBoolExpr + initialGuard: UBoolExpr, + ownership: MutabilityOwnership ) = foldHeapRef2( ref0 = srcRef, ref1 = dstRef, @@ -159,20 +165,20 @@ internal class UMapMemoryRegion val srcId = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, srcConcrete.address) - val srcCollection = region.getAllocatedMap(srcId) - val srcKeys = srcKeySet.allocatedSetElements(srcConcrete.address) + val srcCollection = region.getAllocatedMap(srcId, ownership) + val srcKeys = srcKeySet.allocatedSetElements(srcConcrete.address, ownership) val dstId = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, dstConcrete.address) - val dstCollection = region.getAllocatedMap(dstId) + val dstCollection = region.getAllocatedMap(dstId, ownership) val adapter = UAllocatedToAllocatedSymbolicMapMergeAdapter(srcKeys) val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard) - region.updateAllocatedMap(dstId, newDstCollection) + region.updateAllocatedMap(dstId, newDstCollection, ownership) }, blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard -> val srcId = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, srcConcrete.address) - val srcCollection = region.getAllocatedMap(srcId) - val srcKeys = srcKeySet.allocatedSetElements(srcConcrete.address) + val srcCollection = region.getAllocatedMap(srcId, ownership) + val srcKeys = srcKeySet.allocatedSetElements(srcConcrete.address, ownership) val dstCollection = getInputMap() val adapter = UAllocatedToInputSymbolicMapMergeAdapter(dstSymbolic, srcKeys) @@ -184,11 +190,11 @@ internal class UMapMemoryRegion val srcCollection = region.getInputMap() diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt index 4d6b2adc84..68762b3330 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt @@ -6,6 +6,7 @@ import org.usvm.UHeapRef import org.usvm.USort import org.usvm.collection.set.primitive.USetRegion import org.usvm.collection.set.primitive.USetRegionId +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.memory.UWritableMemory import org.usvm.regions.Region @@ -18,7 +19,7 @@ internal fun > UW sort: ValueSort, keyInfo: USymbolicCollectionKeyInfo, Reg>, keySet: USetRegionId, - guard: UBoolExpr + guard: UBoolExpr, ) { val regionId = UMapRegionId(keySort, sort, mapType, keyInfo) val region = getRegion(regionId) @@ -32,6 +33,6 @@ internal fun > UW "mapMerge is not applicable to set $region" } - val newRegion = region.merge(srcRef, dstRef, mapType, keySetRegion, guard) + val newRegion = region.merge(srcRef, dstRef, mapType, keySetRegion, guard, ownership) setRegion(regionId, newRegion) } 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 17f6458518..c420db92fa 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 @@ -154,7 +154,7 @@ private class UInputMapUpdatesTranslator( ) : U2DUpdatesTranslator(exprTranslator, initialValue) { override fun KContext.translateRangedUpdate( previous: KExpr>, - update: URangedUpdateNode<*, *, USymbolicMapKey, ValueSort> + update: URangedUpdateNode<*, *, USymbolicMapKey, ValueSort>, ): KExpr> { check(update.adapter is USymbolicMapMergeAdapter<*, *, USymbolicMapKey, *>) { "Unexpected adapter: ${update.adapter}" @@ -165,7 +165,7 @@ private class UInputMapUpdatesTranslator( previous, update, update.sourceCollection as USymbolicCollection, Any, ValueSort>, - update.adapter as USymbolicMapMergeAdapter<*, Any, USymbolicMapKey, *> + update.adapter as USymbolicMapMergeAdapter<*, Any, USymbolicMapKey, *>, ) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt index 6c94e61d88..2ae4440fbf 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt @@ -63,7 +63,7 @@ class UAllocatedToAllocatedSymbolicMapMergeAdapter( dstCollectionId: USymbolicCollectionId, *, *>, guard: UBoolExpr, srcKey: UExpr, - composer: UComposer<*, *>, + composer: UComposer<*, *> ) { check(srcCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $srcCollectionId" } check(dstCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $dstCollectionId" } @@ -114,7 +114,7 @@ class UAllocatedToInputSymbolicMapMergeAdapter( dstCollectionId: USymbolicCollectionId, *, *>, guard: UBoolExpr, srcKey: UExpr, - composer: UComposer<*, *>, + composer: UComposer<*, *> ) { check(srcCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $srcCollectionId" } check(dstCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $dstCollectionId" } @@ -166,7 +166,7 @@ class UInputToAllocatedSymbolicMapMergeAdapter( dstCollectionId: USymbolicCollectionId, *, *>, guard: UBoolExpr, srcKey: USymbolicMapKey, - composer: UComposer<*, *>, + composer: UComposer<*, *> ) { check(srcCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $srcCollectionId" } check(dstCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $dstCollectionId" } @@ -219,7 +219,7 @@ class UInputToInputSymbolicMapMergeAdapter( dstCollectionId: USymbolicCollectionId, *, *>, guard: UBoolExpr, srcKey: USymbolicMapKey, - composer: UComposer<*, *>, + composer: UComposer<*, *> ) { check(srcCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $srcCollectionId" } check(dstCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $dstCollectionId" } 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 126aa229ba..a5aef9aa2a 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 @@ -4,6 +4,7 @@ import org.usvm.UAddressSort import org.usvm.UExpr import org.usvm.USort import org.usvm.collection.map.USymbolicMapKey +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelEvaluator import org.usvm.model.modelEnsureConcreteInputRef @@ -14,9 +15,9 @@ abstract class URefMapModelRegion( ) : UReadOnlyMemoryRegion, ValueSort> { abstract val inputMap: UReadOnlyMemoryRegion, ValueSort> - override fun read(key: URefMapEntryLValue): UExpr { + override fun read(key: URefMapEntryLValue, ownership: MutabilityOwnership): UExpr { val mapRef = modelEnsureConcreteInputRef(key.mapRef) - return inputMap.read(mapRef to key.mapKey) + return inputMap.read(mapRef to key.mapKey, ownership) } } 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 a842d980d1..ea16b54c22 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 @@ -1,7 +1,5 @@ package org.usvm.collection.map.ref -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UConcreteHeapAddress @@ -12,6 +10,9 @@ import org.usvm.USort import org.usvm.collection.map.USymbolicMapKey import org.usvm.collection.set.ref.URefSetEntryLValue import org.usvm.collection.set.ref.URefSetRegion +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -52,7 +53,8 @@ interface URefMapRegion mapType: MapType, sort: ValueSort, keySet: URefSetRegion, - operationGuard: UBoolExpr + operationGuard: UBoolExpr, + ownership: MutabilityOwnership ): URefMapRegion } @@ -73,14 +75,14 @@ internal data class UAllocatedRefMapWithAllocatedKeysId( internal class URefMapMemoryRegion( private val valueSort: ValueSort, private val mapType: MapType, - private var allocatedMapWithAllocatedKeys: PersistentMap> = persistentHashMapOf(), - private var inputMapWithAllocatedKeys: PersistentMap, UInputRefMapWithAllocatedKeys> = persistentHashMapOf(), - private var allocatedMapWithInputKeys: PersistentMap, UAllocatedRefMapWithInputKeys> = persistentHashMapOf(), + private var allocatedMapWithAllocatedKeys: UPersistentHashMap> = persistentHashMapOf(), + private var inputMapWithAllocatedKeys: UPersistentHashMap, UInputRefMapWithAllocatedKeys> = persistentHashMapOf(), + private var allocatedMapWithInputKeys: UPersistentHashMap, UAllocatedRefMapWithInputKeys> = persistentHashMapOf(), private var inputMapWithInputKeys: UInputRefMap? = null, ) : URefMapRegion { private fun updateAllocatedMapWithAllocatedKeys( - updated: PersistentMap> + updated: UPersistentHashMap> ) = URefMapMemoryRegion( valueSort, mapType, @@ -94,24 +96,23 @@ internal class URefMapMemoryRegion( UInputRefMapWithAllocatedKeysId(valueSort, mapType, keyAddress) private fun getInputMapWithAllocatedKeys( - id: UInputRefMapWithAllocatedKeysId + id: UInputRefMapWithAllocatedKeysId, + ownership: MutabilityOwnership ): UInputRefMapWithAllocatedKeys { - var collection = inputMapWithAllocatedKeys[id] - if (collection == null) { - collection = id.emptyRegion() - inputMapWithAllocatedKeys = inputMapWithAllocatedKeys.put(id, collection) - } + val (updatedMap, collection) = inputMapWithAllocatedKeys.getOrPut(id, id.emptyRegion(), ownership) + inputMapWithAllocatedKeys = updatedMap return collection } private fun updateInputMapWithAllocatedKeys( id: UInputRefMapWithAllocatedKeysId, - updatedMap: UInputRefMapWithAllocatedKeys + updatedMap: UInputRefMapWithAllocatedKeys, + ownership: MutabilityOwnership ) = URefMapMemoryRegion( valueSort, mapType, allocatedMapWithAllocatedKeys, - inputMapWithAllocatedKeys.put(id, updatedMap), + inputMapWithAllocatedKeys.put(id, updatedMap, ownership), allocatedMapWithInputKeys, inputMapWithInputKeys ) @@ -120,25 +121,24 @@ internal class URefMapMemoryRegion( UAllocatedRefMapWithInputKeysId(valueSort, mapType, mapAddress) private fun getAllocatedMapWithInputKeys( - id: UAllocatedRefMapWithInputKeysId + id: UAllocatedRefMapWithInputKeysId, + ownership: MutabilityOwnership ): UAllocatedRefMapWithInputKeys { - var collection = allocatedMapWithInputKeys[id] - if (collection == null) { - collection = id.emptyRegion() - allocatedMapWithInputKeys = allocatedMapWithInputKeys.put(id, collection) - } + val (updatedMap, collection) = allocatedMapWithInputKeys.getOrPut(id, id.emptyRegion(), ownership) + allocatedMapWithInputKeys = updatedMap return collection } private fun updateAllocatedMapWithInputKeys( id: UAllocatedRefMapWithInputKeysId, - updatedMap: UAllocatedRefMapWithInputKeys + updatedMap: UAllocatedRefMapWithInputKeys, + ownership: MutabilityOwnership ) = URefMapMemoryRegion( valueSort, mapType, allocatedMapWithAllocatedKeys, inputMapWithAllocatedKeys, - allocatedMapWithInputKeys.put(id, updatedMap), + allocatedMapWithInputKeys.put(id, updatedMap, ownership), inputMapWithInputKeys ) @@ -160,7 +160,7 @@ internal class URefMapMemoryRegion( updatedMap ) - override fun read(key: URefMapEntryLValue): UExpr = + override fun read(key: URefMapEntryLValue, ownership: MutabilityOwnership): UExpr = key.mapRef.mapWithStaticAsSymbolic( concreteMapper = { concreteRef -> key.mapKey.mapWithStaticAsSymbolic( @@ -170,7 +170,7 @@ internal class URefMapMemoryRegion( }, symbolicMapper = { symbolicKey -> val id = allocatedMapWithInputKeyId(concreteRef.address) - getAllocatedMapWithInputKeys(id).read(symbolicKey) + getAllocatedMapWithInputKeys(id, ownership).read(symbolicKey, ownership) } ) }, @@ -178,10 +178,10 @@ internal class URefMapMemoryRegion( key.mapKey.mapWithStaticAsSymbolic( concreteMapper = { concreteKey -> val id = inputMapWithAllocatedKeyId(concreteKey.address) - getInputMapWithAllocatedKeys(id).read(symbolicRef) + getInputMapWithAllocatedKeys(id, ownership).read(symbolicRef, ownership) }, symbolicMapper = { symbolicKey -> - getInputMapWithInputKeys().read(symbolicRef to symbolicKey) + getInputMapWithInputKeys().read(symbolicRef to symbolicKey, ownership) } ) } @@ -190,7 +190,8 @@ internal class URefMapMemoryRegion( override fun write( key: URefMapEntryLValue, value: UExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership, ) = foldHeapRefWithStaticAsSymbolic( ref = key.mapRef, initial = this, @@ -202,16 +203,16 @@ internal class URefMapMemoryRegion( initialGuard = mapGuard, blockOnConcrete = { region, (concreteKeyRef, guard) -> val id = UAllocatedRefMapWithAllocatedKeysId(concreteMapRef.address, concreteKeyRef.address) - val newMap = region.allocatedMapWithAllocatedKeys.guardedWrite(id, value, guard) { + val newMap = region.allocatedMapWithAllocatedKeys.guardedWrite(id, value, guard, ownership) { valueSort.sampleUValue() } region.updateAllocatedMapWithAllocatedKeys(newMap) }, blockOnSymbolic = { region, (symbolicKeyRef, guard) -> val id = allocatedMapWithInputKeyId(concreteMapRef.address) - val newMap = region.getAllocatedMapWithInputKeys(id) - .write(symbolicKeyRef, value, guard) - region.updateAllocatedMapWithInputKeys(id, newMap) + val newMap = region.getAllocatedMapWithInputKeys(id, ownership) + .write(symbolicKeyRef, value, guard, ownership) + region.updateAllocatedMapWithInputKeys(id, newMap, ownership) } ) }, @@ -222,13 +223,13 @@ internal class URefMapMemoryRegion( initialGuard = mapGuard, blockOnConcrete = { region, (concreteKeyRef, guard) -> val id = inputMapWithAllocatedKeyId(concreteKeyRef.address) - val newMap = region.getInputMapWithAllocatedKeys(id) - .write(symbolicMapRef, value, guard) - region.updateInputMapWithAllocatedKeys(id, newMap) + val newMap = region.getInputMapWithAllocatedKeys(id, ownership) + .write(symbolicMapRef, value, guard, ownership) + region.updateInputMapWithAllocatedKeys(id, newMap, ownership) }, blockOnSymbolic = { region, (symbolicKeyRef, guard) -> val newMap = region.getInputMapWithInputKeys() - .write(symbolicMapRef to symbolicKeyRef, value, guard) + .write(symbolicMapRef to symbolicKeyRef, value, guard, ownership) region.updateInputMapWithInputKeys(newMap) } ) @@ -255,7 +256,8 @@ internal class URefMapMemoryRegion( mapType: MapType, sort: ValueSort, keySet: URefSetRegion, - operationGuard: UBoolExpr + operationGuard: UBoolExpr, + ownership: MutabilityOwnership ) = foldHeapRef2( ref0 = srcRef, ref1 = dstRef, @@ -268,41 +270,42 @@ internal class URefMapMemoryRegion( srcMapRef = srcConcrete, guard = guard, keySet = keySet, + ownership = ownership, read = { initialAllocatedMapState[it] ?: valueSort.sampleUValue() }, mkDstKeyId = { UAllocatedRefMapWithAllocatedKeysId(dstConcrete.address, it) }, write = { result, dstKeyId, value, g -> - result.guardedWrite(dstKeyId, value, g) { valueSort.sampleUValue() } + result.guardedWrite(dstKeyId, value, g, ownership) { valueSort.sampleUValue() } } ) val updatedRegion = region.updateAllocatedMapWithAllocatedKeys(updatedAllocatedMap) - val srcKeys = keySet.allocatedSetWithInputElements(srcConcrete.address) + val srcKeys = keySet.allocatedSetWithInputElements(srcConcrete.address, ownership) val srcInputKeysId = updatedRegion.allocatedMapWithInputKeyId(srcConcrete.address) - val srcInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(srcInputKeysId) + val srcInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(srcInputKeysId, ownership) val dstInputKeysId = updatedRegion.allocatedMapWithInputKeyId(dstConcrete.address) - val dstInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(dstInputKeysId) + val dstInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(dstInputKeysId, ownership) val adapter = UAllocatedToAllocatedSymbolicRefMapMergeAdapter(srcKeys) val updatedDstCollection = dstInputKeysCollection.copyRange(srcInputKeysCollection, adapter, guard) - updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection) + updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection, ownership) }, blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard -> val initialAllocatedMapState = region.allocatedMapWithAllocatedKeys val updatedRegion = region.mergeAllocatedMapAllocatedKeys( - initial = region, srcMapRef = srcConcrete, guard = guard, keySet = keySet, + initial = region, srcMapRef = srcConcrete, guard = guard, keySet = keySet, ownership = ownership, read = { initialAllocatedMapState[it] ?: valueSort.sampleUValue() }, mkDstKeyId = { inputMapWithAllocatedKeyId(it) }, write = { result, dstKeyId, value, g -> - val newMap = result.getInputMapWithAllocatedKeys(dstKeyId) - .write(dstSymbolic, value, g) - result.updateInputMapWithAllocatedKeys(dstKeyId, newMap) + val newMap = result.getInputMapWithAllocatedKeys(dstKeyId, ownership) + .write(dstSymbolic, value, g, ownership) + result.updateInputMapWithAllocatedKeys(dstKeyId, newMap, ownership) } ) - val srcKeys = keySet.allocatedSetWithInputElements(srcConcrete.address) + val srcKeys = keySet.allocatedSetWithInputElements(srcConcrete.address, ownership) val srcInputKeysId = updatedRegion.allocatedMapWithInputKeyId(srcConcrete.address) - val srcInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(srcInputKeysId) + val srcInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(srcInputKeysId, ownership) val dstInputKeysCollection = updatedRegion.getInputMapWithInputKeys() @@ -313,11 +316,11 @@ internal class URefMapMemoryRegion( blockOnSymbolic0Concrete1 = { region, srcSymbolic, dstConcrete, guard -> val updatedAllocatedMap = region.mergeInputMapAllocatedKeys( initial = region.allocatedMapWithAllocatedKeys, - srcMapRef = srcSymbolic, guard = guard, keySet = keySet, - read = { region.getInputMapWithAllocatedKeys(it).read(srcSymbolic) }, + srcMapRef = srcSymbolic, guard = guard, keySet = keySet, ownership = ownership, + read = { region.getInputMapWithAllocatedKeys(it, ownership).read(srcSymbolic, ownership) }, mkDstKeyId = { UAllocatedRefMapWithAllocatedKeysId(dstConcrete.address, it) }, write = { result, dstKeyId, value, g -> - result.guardedWrite(dstKeyId, value, g) { sort.sampleUValue() } + result.guardedWrite(dstKeyId, value, g, ownership) { sort.sampleUValue() } } ) val updatedRegion = region.updateAllocatedMapWithAllocatedKeys(updatedAllocatedMap) @@ -326,21 +329,21 @@ internal class URefMapMemoryRegion( val srcInputKeysCollection = updatedRegion.getInputMapWithInputKeys() val dstInputKeysId = updatedRegion.allocatedMapWithInputKeyId(dstConcrete.address) - val dstInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(dstInputKeysId) + val dstInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(dstInputKeysId, ownership) val adapter = UInputToAllocatedSymbolicRefMapMergeAdapter(srcSymbolic, srcKeys) val updatedDstCollection = dstInputKeysCollection.copyRange(srcInputKeysCollection, adapter, guard) - updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection) + updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection, ownership) }, blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard -> val updatedRegion = region.mergeInputMapAllocatedKeys( - initial = region, srcMapRef = srcSymbolic, guard = guard, keySet = keySet, - read = { region.getInputMapWithAllocatedKeys(it).read(srcSymbolic) }, + initial = region, srcMapRef = srcSymbolic, guard = guard, keySet = keySet, ownership = ownership, + read = { region.getInputMapWithAllocatedKeys(it, ownership).read(srcSymbolic, ownership) }, mkDstKeyId = { inputMapWithAllocatedKeyId(it) }, write = { result, dstKeyId, value, g -> - val newMap = result.getInputMapWithAllocatedKeys(dstKeyId) - .write(dstSymbolic, value, g) - result.updateInputMapWithAllocatedKeys(dstKeyId, newMap) + val newMap = result.getInputMapWithAllocatedKeys(dstKeyId, ownership) + .write(dstSymbolic, value, g, ownership) + result.updateInputMapWithAllocatedKeys(dstKeyId, newMap, ownership) } ) val srcKeys = keySet.inputSetWithInputElements() @@ -359,15 +362,17 @@ internal class URefMapMemoryRegion( srcMapRef: UHeapRef, guard: UBoolExpr, keySet: URefSetRegion, + ownership: MutabilityOwnership, read: (UInputRefMapWithAllocatedKeysId) -> UExpr, mkDstKeyId: (UConcreteHeapAddress) -> DstKeyId, write: (R, DstKeyId, UExpr, UBoolExpr) -> R ) = mergeAllocatedKeys( initial, - inputMapWithAllocatedKeys.keys, + inputMapWithAllocatedKeys.keys(), guard, keySet, srcMapRef, + ownership, { it.keyAddress }, read, mkDstKeyId, @@ -379,15 +384,17 @@ internal class URefMapMemoryRegion( srcMapRef: UConcreteHeapRef, guard: UBoolExpr, keySet: URefSetRegion, + ownership: MutabilityOwnership, read: (UAllocatedRefMapWithAllocatedKeysId) -> UExpr, mkDstKeyId: (UConcreteHeapAddress) -> DstKeyId, write: (R, DstKeyId, UExpr, UBoolExpr) -> R ) = mergeAllocatedKeys( initial, - allocatedMapWithAllocatedKeys.keys.filter { it.mapAddress == srcMapRef.address }, + allocatedMapWithAllocatedKeys.keys().filter { it.mapAddress == srcMapRef.address }, guard, keySet, srcMapRef, + ownership, { it.keyAddress }, read, mkDstKeyId, @@ -400,6 +407,7 @@ internal class URefMapMemoryRegion( guard: UBoolExpr, keySet: URefSetRegion, srcMapRef: UHeapRef, + ownership: MutabilityOwnership, srcKeyConcreteAddress: (SrcKeyId) -> UConcreteHeapAddress, read: (SrcKeyId) -> UExpr, mkDstKeyId: (UConcreteHeapAddress) -> DstKeyId, @@ -409,7 +417,7 @@ internal class URefMapMemoryRegion( val srcValue = read(srcKeyId) val keyRef = guard.uctx.mkConcreteHeapRef(srcKeyAddress) - val srcContains = keySet.read(URefSetEntryLValue(srcMapRef, keyRef, mapType)) + val srcContains = keySet.read(URefSetEntryLValue(srcMapRef, keyRef, mapType), ownership) val mergedGuard = guard.uctx.mkAnd(srcContains, guard) write(result, mkDstKeyId(srcKeyAddress), srcValue, mergedGuard) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt index b66dba4dc4..1eb6bb396a 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt @@ -27,6 +27,6 @@ internal fun UWritableMemory<*>.refMapMerge( "refMapMerge is not applicable to set $region" } - val newRegion = region.merge(srcRef, dstRef, mapType, sort, keySet, guard) + val newRegion = region.merge(srcRef, dstRef, mapType, sort, keySet, guard, ownership) setRegion(regionId, newRegion) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionTranslator.kt index 422249e38c..c955e4ecc0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionTranslator.kt @@ -153,7 +153,7 @@ private class UAllocatedRefMapUpdatesTranslator( previous, update, update.sourceCollection as USymbolicCollection, Any, ValueSort>, - update.adapter as USymbolicRefMapMergeAdapter<*, Any, UHeapRef, *> + update.adapter as USymbolicRefMapMergeAdapter<*, Any, UHeapRef, *>, ) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/USetCollectionDecoder.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/USetCollectionDecoder.kt index 5af60da358..3dc300ed58 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/USetCollectionDecoder.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/USetCollectionDecoder.kt @@ -5,7 +5,7 @@ import io.ksmt.expr.KExpr import io.ksmt.expr.KFunctionApp import io.ksmt.sort.KBoolSort import io.ksmt.utils.uncheckedCast -import kotlinx.collections.immutable.persistentHashMapOf +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort @@ -41,7 +41,7 @@ abstract class USetCollectionDecoder { val usedSetKeys = hashSetOf>() assertions.flatMapTo(usedSetKeys) { appCollector.applyVisitor(it) } - val entries = persistentHashMapOf, UBoolExpr>().builder() + var entries = persistentHashMapOf, UBoolExpr>() for (key in usedSetKeys) { val keyInSet = model.eval(key, isComplete = false) if (!keyInSet.isTrue) continue @@ -49,13 +49,13 @@ abstract class USetCollectionDecoder { val (rawSetRef, rawElement) = key.args val setRef: UHeapRef = rawSetRef.uncheckedCast() val element: UExpr = rawElement.uncheckedCast() - + val setRefModel = model.eval(setRef, isComplete = true).mapAddress(mapping) val elementModel = model.eval(element, isComplete = true).mapAddress(mapping) - entries[setRefModel to elementModel] = inputFunction.ctx.trueExpr + entries = entries.put(setRefModel to elementModel, inputFunction.ctx.trueExpr, evaluator.ctx.defaultOwnership) } - return UMemory2DArray(entries.build(), constValue = inputFunction.ctx.falseExpr) + return UMemory2DArray(entries, constValue = inputFunction.ctx.falseExpr) } } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt index 36ac911376..c881ddd529 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt @@ -8,6 +8,7 @@ import org.usvm.UBoolSort import org.usvm.UHeapRef import org.usvm.USort import org.usvm.collection.set.USetCollectionDecoder +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.isFalse import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UMemory2DArray @@ -21,18 +22,18 @@ abstract class USetModelRegion>( USetReadOnlyRegion { abstract val inputSet: UMemory2DArray - override fun read(key: USetEntryLValue): UBoolExpr { + override fun read(key: USetEntryLValue, ownership: MutabilityOwnership): UBoolExpr { val setRef = modelEnsureConcreteInputRef(key.setRef) - return inputSet.read(setRef to key.setElement) + return inputSet.read(setRef to key.setElement, ownership) } - override fun setEntries(ref: UHeapRef): UPrimitiveSetEntries = with(regionId) { + override fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): UPrimitiveSetEntries = with(regionId) { val setRef = modelEnsureConcreteInputRef(ref) check(inputSet.constValue.isFalse) { "Set model is not complete" } val result = UPrimitiveSetEntries() - inputSet.values.keys.forEach { + inputSet.values.keys().forEach { if (it.first == setRef) { result.add(USetEntryLValue(elementSort, setRef, it.second, setType, elementInfo)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt index 74ec7eeed3..35921cd7fe 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt @@ -1,7 +1,6 @@ package org.usvm.collection.set.primitive -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UConcreteHeapAddress @@ -11,6 +10,8 @@ import org.usvm.USort import org.usvm.collection.set.USymbolicSetEntries import org.usvm.collection.set.USymbolicSetElement import org.usvm.collection.set.USymbolicSetElementsCollector +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -62,14 +63,14 @@ typealias UPrimitiveSetEntries = USymbolicSetEntries< interface USetReadOnlyRegion> : UReadOnlyMemoryRegion, UBoolSort> { - fun setEntries(ref: UHeapRef): UPrimitiveSetEntries + fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): UPrimitiveSetEntries } interface USetRegion> : USetReadOnlyRegion, UMemoryRegion, UBoolSort> { - fun allocatedSetElements(address: UConcreteHeapAddress): UAllocatedSet + fun allocatedSetElements(address: UConcreteHeapAddress, ownership: MutabilityOwnership): UAllocatedSet fun inputSetElements(): UInputSet @@ -77,6 +78,7 @@ interface USetRegion> : srcRef: UHeapRef, dstRef: UHeapRef, operationGuard: UBoolExpr, + ownership: MutabilityOwnership ): USetRegion } @@ -84,7 +86,7 @@ internal class USetMemoryRegion> private val setType: SetType, private val elementSort: ElementSort, private val elementInfo: USymbolicCollectionKeyInfo, Reg>, - private var allocatedSets: PersistentMap, UAllocatedSet> = persistentHashMapOf(), + private var allocatedSets: UPersistentHashMap, UAllocatedSet> = persistentHashMapOf(), private var inputSet: UInputSet? = null, ) : USetRegion { init { @@ -93,24 +95,26 @@ internal class USetMemoryRegion> } } - override fun allocatedSetElements(address: UConcreteHeapAddress): UAllocatedSet = - getAllocatedSet(UAllocatedSetId(address, elementSort, setType, elementInfo)) + override fun allocatedSetElements( + address: UConcreteHeapAddress, + ownership: MutabilityOwnership + ): UAllocatedSet = + getAllocatedSet(UAllocatedSetId(address, elementSort, setType, elementInfo), ownership) private fun getAllocatedSet( - id: UAllocatedSetId + id: UAllocatedSetId, + ownership: MutabilityOwnership, ): UAllocatedSet { - var collection = allocatedSets[id] - if (collection == null) { - collection = id.emptyRegion() - allocatedSets = allocatedSets.put(id, collection) - } + val (updatesSets, collection) = allocatedSets.getOrPut(id, id.emptyRegion(), ownership) + allocatedSets = updatesSets return collection } private fun updateAllocatedSet( id: UAllocatedSetId, - updated: UAllocatedSet - ) = USetMemoryRegion(setType, elementSort, elementInfo, allocatedSets.put(id, updated), inputSet) + updated: UAllocatedSet, + ownership: MutabilityOwnership, + ) = USetMemoryRegion(setType, elementSort, elementInfo, allocatedSets.put(id, updated, ownership), inputSet) override fun inputSetElements(): UInputSet { if (inputSet == null) { @@ -122,29 +126,29 @@ internal class USetMemoryRegion> private fun updateInputSet(updated: UInputSet) = USetMemoryRegion(setType, elementSort, elementInfo, allocatedSets, updated) - override fun read(key: USetEntryLValue): UExpr = + override fun read(key: USetEntryLValue, ownership: MutabilityOwnership): UExpr = key.setRef.mapWithStaticAsSymbolic( - { concreteRef -> allocatedSetElements(concreteRef.address).read(key.setElement) }, - { symbolicRef -> inputSetElements().read(symbolicRef to key.setElement) } + { concreteRef -> allocatedSetElements(concreteRef.address, ownership).read(key.setElement, ownership) }, + { symbolicRef -> inputSetElements().read(symbolicRef to key.setElement, ownership) } ) - override fun write( key: USetEntryLValue, value: UExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership ) = foldHeapRefWithStaticAsSymbolic( ref = key.setRef, initial = this, initialGuard = guard, blockOnConcrete = { region, (concreteRef, guard) -> val id = UAllocatedSetId(concreteRef.address, elementSort, setType, elementInfo) - val newCollection = region.getAllocatedSet(id) - .write(key.setElement, value, guard) - region.updateAllocatedSet(id, newCollection) + val newCollection = region.getAllocatedSet(id, ownership) + .write(key.setElement, value, guard, ownership) + region.updateAllocatedSet(id, newCollection, ownership) }, blockOnSymbolic = { region, (symbolicRef, guard) -> val newCollection = region.inputSetElements() - .write(symbolicRef to key.setElement, value, guard) + .write(symbolicRef to key.setElement, value, guard, ownership) region.updateInputSet(newCollection) } ) @@ -152,7 +156,8 @@ internal class USetMemoryRegion> override fun union( srcRef: UHeapRef, dstRef: UHeapRef, - operationGuard: UBoolExpr + operationGuard: UBoolExpr, + ownership: MutabilityOwnership, ) = foldHeapRef2( ref0 = srcRef, ref1 = dstRef, @@ -160,18 +165,18 @@ internal class USetMemoryRegion> initialGuard = operationGuard, blockOnConcrete0Concrete1 = { region, srcConcrete, dstConcrete, guard -> val srcId = UAllocatedSetId(srcConcrete.address, elementSort, setType, elementInfo) - val srcCollection = region.getAllocatedSet(srcId) + val srcCollection = region.getAllocatedSet(srcId, ownership) val dstId = UAllocatedSetId(dstConcrete.address, elementSort, setType, elementInfo) - val dstCollection = region.getAllocatedSet(dstId) + val dstCollection = region.getAllocatedSet(dstId, ownership) val adapter = UAllocatedToAllocatedSymbolicSetUnionAdapter(srcCollection) val updated = dstCollection.copyRange(srcCollection, adapter, guard) - region.updateAllocatedSet(dstId, updated) + region.updateAllocatedSet(dstId, updated, ownership) }, blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard -> val srcId = UAllocatedSetId(srcConcrete.address, elementSort, setType, elementInfo) - val srcCollection = region.getAllocatedSet(srcId) + val srcCollection = region.getAllocatedSet(srcId, ownership) val dstCollection = region.inputSetElements() @@ -183,11 +188,11 @@ internal class USetMemoryRegion> val srcCollection = region.inputSetElements() val dstId = UAllocatedSetId(dstConcrete.address, elementSort, setType, elementInfo) - val dstCollection = region.getAllocatedSet(dstId) + val dstCollection = region.getAllocatedSet(dstId, ownership) val adapter = UInputToAllocatedSymbolicSetUnionAdapter(srcSymbolic, srcCollection) val updated = dstCollection.copyRange(srcCollection, adapter, guard) - region.updateAllocatedSet(dstId, updated) + region.updateAllocatedSet(dstId, updated, ownership) }, blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard -> val srcCollection = region.inputSetElements() @@ -199,13 +204,13 @@ internal class USetMemoryRegion> }, ) - override fun setEntries(ref: UHeapRef): UPrimitiveSetEntries = + override fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): UPrimitiveSetEntries = foldHeapRefWithStaticAsSymbolic( ref = ref, initial = UPrimitiveSetEntries(), initialGuard = ref.uctx.trueExpr, blockOnConcrete = { entries, (concreteRef, _) -> - val setElements = allocatedSetElements(concreteRef.address) + val setElements = allocatedSetElements(concreteRef.address, ownership) val elements = USymbolicSetElementsCollector.collect(setElements.updates) elements.elements.forEach { elem -> entries.add(USetEntryLValue(elementSort, concreteRef, elem, setType, elementInfo)) diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt index 5d463a20f8..b8cc054bd4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt @@ -4,6 +4,7 @@ import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.USymbolicCollectionKeyInfo import org.usvm.memory.UWritableMemory @@ -24,7 +25,7 @@ internal fun > UWritableMemory<*>.se "setUnion is not applicable to $region" } - val newRegion = region.union(srcRef, dstRef, guard) + val newRegion = region.union(srcRef, dstRef, guard, ownership) setRegion(regionId, newRegion) } @@ -38,5 +39,5 @@ fun > UReadOnlyMemory<*>.setEntries( val region = getRegion(regionId) as? USetReadOnlyRegion ?: return UPrimitiveSetEntries().apply { markAsInput() } - return region.setEntries(setRef) + return region.setEntries(setRef, ownership) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt index 6a387f8c57..de974e427b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt @@ -251,7 +251,7 @@ class UInputToInputSymbolicSetUnionAdapter( dstCollectionId.setType, dstCollectionId.elementSort, dstCollectionId.keyInfo() as USymbolicCollectionKeyInfo, Nothing>, - guard + guard ) } } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt index 36c8df5ff9..e0995de2b7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt @@ -7,6 +7,7 @@ import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UHeapRef import org.usvm.collection.set.USetCollectionDecoder +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.isFalse import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UMemory2DArray @@ -18,18 +19,18 @@ abstract class URefSetModelRegion( ) : UReadOnlyMemoryRegion, UBoolSort>, URefSetReadOnlyRegion { abstract val inputSet: UMemory2DArray - override fun read(key: URefSetEntryLValue): UBoolExpr { + override fun read(key: URefSetEntryLValue, ownership: MutabilityOwnership): UBoolExpr { val setRef = modelEnsureConcreteInputRef(key.setRef) - return inputSet.read(setRef to key.setElement) + return inputSet.read(setRef to key.setElement, ownership) } - override fun setEntries(ref: UHeapRef): URefSetEntries { + override fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): URefSetEntries { val setRef = modelEnsureConcreteInputRef(ref) check(inputSet.constValue.isFalse) { "Set model is not complete" } val result = URefSetEntries() - inputSet.values.keys.forEach { + inputSet.values.keys().forEach { if (it.first == setRef) { result.add(URefSetEntryLValue(setRef, it.second, regionId.setType)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt index 27de317e53..bf8281fccb 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt @@ -1,7 +1,5 @@ package org.usvm.collection.set.ref -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort @@ -10,6 +8,9 @@ import org.usvm.UHeapRef import org.usvm.collection.set.USymbolicSetEntries import org.usvm.collection.set.USymbolicSetElement import org.usvm.collection.set.USymbolicSetElementsCollector +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -62,33 +63,34 @@ typealias URefSetEntries = USymbolicSetEntries : UReadOnlyMemoryRegion, UBoolSort> { - fun setEntries(ref: UHeapRef): URefSetEntries + fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): URefSetEntries } interface URefSetRegion : URefSetReadOnlyRegion, UMemoryRegion, UBoolSort> { - fun allocatedSetWithInputElements(setRef: UConcreteHeapAddress): UAllocatedRefSetWithInputElements + fun allocatedSetWithInputElements(setRef: UConcreteHeapAddress, ownership: MutabilityOwnership): UAllocatedRefSetWithInputElements fun inputSetWithInputElements(): UInputRefSetWithInputElements fun union( srcRef: UHeapRef, dstRef: UHeapRef, operationGuard: UBoolExpr, + ownership: MutabilityOwnership ): URefSetRegion } internal class URefSetMemoryRegion( private val setType: SetType, private val sort: UBoolSort, - private var allocatedSetWithAllocatedElements: PersistentMap = persistentHashMapOf(), - private var allocatedSetWithInputElements: PersistentMap, UAllocatedRefSetWithInputElements> = persistentHashMapOf(), - private var inputSetWithAllocatedElements: PersistentMap, UInputRefSetWithAllocatedElements> = persistentHashMapOf(), + private var allocatedSetWithAllocatedElements: UPersistentHashMap = persistentHashMapOf(), + private var allocatedSetWithInputElements: UPersistentHashMap, UAllocatedRefSetWithInputElements> = persistentHashMapOf(), + private var inputSetWithAllocatedElements: UPersistentHashMap, UInputRefSetWithAllocatedElements> = persistentHashMapOf(), private var inputSetWithInputElements: UInputRefSetWithInputElements? = null ) : URefSetRegion { private fun updateAllocatedSetWithAllocatedElements( - updated: PersistentMap + updated: UPersistentHashMap ) = URefSetMemoryRegion( setType, sort, updated, @@ -101,26 +103,25 @@ internal class URefSetMemoryRegion( UAllocatedRefSetWithInputElementsId(setAddress, setType, sort) private fun getAllocatedSetWithInputElements( - id: UAllocatedRefSetWithInputElementsId + id: UAllocatedRefSetWithInputElementsId, + ownership: MutabilityOwnership ): UAllocatedRefSetWithInputElements { - var collection = allocatedSetWithInputElements[id] - if (collection == null) { - collection = id.emptyRegion() - allocatedSetWithInputElements = allocatedSetWithInputElements.put(id, collection) - } + val (updatedSet, collection) = allocatedSetWithInputElements.getOrPut(id, id.emptyRegion(), ownership) + allocatedSetWithInputElements = updatedSet return collection } - override fun allocatedSetWithInputElements(setRef: UConcreteHeapAddress) = - getAllocatedSetWithInputElements(allocatedSetWithInputElementsId(setRef)) + override fun allocatedSetWithInputElements(setRef: UConcreteHeapAddress, ownership: MutabilityOwnership) = + getAllocatedSetWithInputElements(allocatedSetWithInputElementsId(setRef), ownership) private fun updateAllocatedSetWithInputElements( id: UAllocatedRefSetWithInputElementsId, - updatedSet: UAllocatedRefSetWithInputElements + updatedSet: UAllocatedRefSetWithInputElements, + ownership: MutabilityOwnership ) = URefSetMemoryRegion( setType, sort, allocatedSetWithAllocatedElements, - allocatedSetWithInputElements.put(id, updatedSet), + allocatedSetWithInputElements.put(id, updatedSet, ownership), inputSetWithAllocatedElements, inputSetWithInputElements ) @@ -129,24 +130,26 @@ internal class URefSetMemoryRegion( UInputRefSetWithAllocatedElementsId(elementAddress, setType, sort) private fun getInputSetWithAllocatedElements( - id: UInputRefSetWithAllocatedElementsId + id: UInputRefSetWithAllocatedElementsId, + ownership: MutabilityOwnership ): UInputRefSetWithAllocatedElements { var collection = inputSetWithAllocatedElements[id] if (collection == null) { collection = id.emptyRegion() - inputSetWithAllocatedElements = inputSetWithAllocatedElements.put(id, collection) + inputSetWithAllocatedElements = inputSetWithAllocatedElements.put(id, collection, ownership) } return collection } private fun updateInputSetWithAllocatedElements( id: UInputRefSetWithAllocatedElementsId, - updatedSet: UInputRefSetWithAllocatedElements + updatedSet: UInputRefSetWithAllocatedElements, + ownership: MutabilityOwnership ) = URefSetMemoryRegion( setType, sort, allocatedSetWithAllocatedElements, allocatedSetWithInputElements, - inputSetWithAllocatedElements.put(id, updatedSet), + inputSetWithAllocatedElements.put(id, updatedSet, ownership), inputSetWithInputElements ) @@ -165,7 +168,7 @@ internal class URefSetMemoryRegion( updatedSet ) - override fun read(key: URefSetEntryLValue): UBoolExpr = + override fun read(key: URefSetEntryLValue, ownership: MutabilityOwnership): UBoolExpr = key.setRef.mapWithStaticAsSymbolic( { concreteRef -> key.setElement.mapWithStaticAsSymbolic( @@ -175,7 +178,7 @@ internal class URefSetMemoryRegion( }, { symbolicElem -> val id = allocatedSetWithInputElementsId(concreteRef.address) - getAllocatedSetWithInputElements(id).read(symbolicElem) + getAllocatedSetWithInputElements(id, ownership).read(symbolicElem, ownership) } ) }, @@ -183,10 +186,10 @@ internal class URefSetMemoryRegion( key.setElement.mapWithStaticAsSymbolic( { concreteElem -> val id = inputSetWithAllocatedElementsId(concreteElem.address) - getInputSetWithAllocatedElements(id).read(symbolicRef) + getInputSetWithAllocatedElements(id, ownership).read(symbolicRef, ownership) }, { symbolicElem -> - inputSetWithInputElements().read(symbolicRef to symbolicElem) + inputSetWithInputElements().read(symbolicRef to symbolicElem, ownership) } ) } @@ -195,7 +198,8 @@ internal class URefSetMemoryRegion( override fun write( key: URefSetEntryLValue, value: UBoolExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership ) = foldHeapRefWithStaticAsSymbolic( ref = key.setRef, initial = this, @@ -207,16 +211,16 @@ internal class URefSetMemoryRegion( initialGuard = setGuard, blockOnConcrete = { region, (concreteElemRef, guard) -> val id = UAllocatedRefSetWithAllocatedElementId(concreteSetRef.address, concreteElemRef.address) - val newMap = region.allocatedSetWithAllocatedElements.guardedWrite(id, value, guard) { + val newMap = region.allocatedSetWithAllocatedElements.guardedWrite(id, value, guard, ownership) { sort.uctx.falseExpr } region.updateAllocatedSetWithAllocatedElements(newMap) }, blockOnSymbolic = { region, (symbolicElemRef, guard) -> val id = allocatedSetWithInputElementsId(concreteSetRef.address) - val newMap = region.getAllocatedSetWithInputElements(id) - .write(symbolicElemRef, value, guard) - region.updateAllocatedSetWithInputElements(id, newMap) + val newMap = region.getAllocatedSetWithInputElements(id, ownership) + .write(symbolicElemRef, value, guard, ownership) + region.updateAllocatedSetWithInputElements(id, newMap, ownership) } ) }, @@ -227,13 +231,13 @@ internal class URefSetMemoryRegion( initialGuard = setGuard, blockOnConcrete = { region, (concreteElemRef, guard) -> val id = inputSetWithAllocatedElementsId(concreteElemRef.address) - val newMap = region.getInputSetWithAllocatedElements(id) - .write(symbolicSetRef, value, guard) - region.updateInputSetWithAllocatedElements(id, newMap) + val newMap = region.getInputSetWithAllocatedElements(id, ownership) + .write(symbolicSetRef, value, guard, ownership) + region.updateInputSetWithAllocatedElements(id, newMap, ownership) }, blockOnSymbolic = { region, (symbolicElemRef, guard) -> val newMap = region.inputSetWithInputElements() - .write(symbolicSetRef to symbolicElemRef, value, guard) + .write(symbolicSetRef to symbolicElemRef, value, guard, ownership) region.updateInputSetWithInputElements(newMap) } ) @@ -243,7 +247,8 @@ internal class URefSetMemoryRegion( override fun union( srcRef: UHeapRef, dstRef: UHeapRef, - operationGuard: UBoolExpr + operationGuard: UBoolExpr, + ownership: MutabilityOwnership ) = foldHeapRef2( ref0 = srcRef, ref1 = dstRef, @@ -258,20 +263,20 @@ internal class URefSetMemoryRegion( read = { initialAllocatedSetState[it] ?: sort.uctx.falseExpr }, mkDstKeyId = { UAllocatedRefSetWithAllocatedElementId(dstConcrete.address, it) }, write = { result, dstKeyId, value, g -> - result.guardedWrite(dstKeyId, value, g) { sort.uctx.falseExpr } + result.guardedWrite(dstKeyId, value, g, ownership) { sort.uctx.falseExpr } } ) val updatedRegion = region.updateAllocatedSetWithAllocatedElements(updatedAllocatedSet) val srcId = allocatedSetWithInputElementsId(srcConcrete.address) - val srcCollection = updatedRegion.getAllocatedSetWithInputElements(srcId) + val srcCollection = updatedRegion.getAllocatedSetWithInputElements(srcId, ownership) val dstId = allocatedSetWithInputElementsId(dstConcrete.address) - val dstCollection = updatedRegion.getAllocatedSetWithInputElements(dstId) + val dstCollection = updatedRegion.getAllocatedSetWithInputElements(dstId, ownership) val adapter = UAllocatedToAllocatedSymbolicRefSetUnionAdapter(srcCollection) val updated = dstCollection.copyRange(srcCollection, adapter, guard) - updatedRegion.updateAllocatedSetWithInputElements(dstId, updated) + updatedRegion.updateAllocatedSetWithInputElements(dstId, updated, ownership) }, blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard -> val initialAllocatedSetState = region.allocatedSetWithAllocatedElements @@ -280,14 +285,14 @@ internal class URefSetMemoryRegion( read = { initialAllocatedSetState[it] ?: sort.uctx.falseExpr }, mkDstKeyId = { inputSetWithAllocatedElementsId(it) }, write = { result, dstKeyId, value, g -> - val newMap = result.getInputSetWithAllocatedElements(dstKeyId) - .write(dstSymbolic, value, g) - result.updateInputSetWithAllocatedElements(dstKeyId, newMap) + val newMap = result.getInputSetWithAllocatedElements(dstKeyId, ownership) + .write(dstSymbolic, value, g, ownership) + result.updateInputSetWithAllocatedElements(dstKeyId, newMap, ownership) } ) val srcId = allocatedSetWithInputElementsId(srcConcrete.address) - val srcCollection = updatedRegion.getAllocatedSetWithInputElements(srcId) + val srcCollection = updatedRegion.getAllocatedSetWithInputElements(srcId, ownership) val dstCollection = updatedRegion.inputSetWithInputElements() @@ -299,10 +304,10 @@ internal class URefSetMemoryRegion( val updatedAllocatedSet = region.unionInputSetAllocatedElements( initial = region.allocatedSetWithAllocatedElements, guard = guard, - read = { region.getInputSetWithAllocatedElements(it).read(srcSymbolic) }, + read = { region.getInputSetWithAllocatedElements(it, ownership).read(srcSymbolic, ownership) }, mkDstKeyId = { UAllocatedRefSetWithAllocatedElementId(dstConcrete.address, it) }, write = { result, dstKeyId, value, g -> - result.guardedWrite(dstKeyId, value, g) { sort.uctx.falseExpr } + result.guardedWrite(dstKeyId, value, g, ownership) { sort.uctx.falseExpr } } ) val updatedRegion = region.updateAllocatedSetWithAllocatedElements(updatedAllocatedSet) @@ -310,21 +315,21 @@ internal class URefSetMemoryRegion( val srcCollection = updatedRegion.inputSetWithInputElements() val dstId = allocatedSetWithInputElementsId(dstConcrete.address) - val dstCollection = updatedRegion.getAllocatedSetWithInputElements(dstId) + val dstCollection = updatedRegion.getAllocatedSetWithInputElements(dstId, ownership) val adapter = UInputToAllocatedSymbolicRefSetUnionAdapter(srcSymbolic, srcCollection) val updated = dstCollection.copyRange(srcCollection, adapter, guard) - updatedRegion.updateAllocatedSetWithInputElements(dstId, updated) + updatedRegion.updateAllocatedSetWithInputElements(dstId, updated, ownership) }, blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard -> val updatedRegion = region.unionInputSetAllocatedElements( initial = region, guard = guard, - read = { region.getInputSetWithAllocatedElements(it).read(srcSymbolic) }, + read = { region.getInputSetWithAllocatedElements(it, ownership).read(srcSymbolic, ownership) }, mkDstKeyId = { inputSetWithAllocatedElementsId(it) }, write = { result, dstKeyId, value, g -> - val newMap = result.getInputSetWithAllocatedElements(dstKeyId) - .write(dstSymbolic, value, g) - result.updateInputSetWithAllocatedElements(dstKeyId, newMap) + val newMap = result.getInputSetWithAllocatedElements(dstKeyId, ownership) + .write(dstSymbolic, value, g, ownership) + result.updateInputSetWithAllocatedElements(dstKeyId, newMap, ownership) } ) val srcCollection = updatedRegion.inputSetWithInputElements() @@ -344,7 +349,7 @@ internal class URefSetMemoryRegion( write: (R, DstKeyId, UBoolExpr, UBoolExpr) -> R ) = unionAllocatedElements( initial, - inputSetWithAllocatedElements.keys, + inputSetWithAllocatedElements.keys(), guard, read, { mkDstKeyId(it.elementAddress) }, @@ -360,7 +365,7 @@ internal class URefSetMemoryRegion( write: (R, DstKeyId, UBoolExpr, UBoolExpr) -> R ) = unionAllocatedElements( initial, - allocatedSetWithAllocatedElements.keys.filter { it.setAddress == srcAddress }, + allocatedSetWithAllocatedElements.keys().filter { it.setAddress == srcAddress }, guard, read, { mkDstKeyId(it.elementAddress) }, @@ -382,13 +387,13 @@ internal class URefSetMemoryRegion( write(result, mkDstKeyId(srcKeyId), guard.uctx.trueExpr, mergedGuard) } - override fun setEntries(ref: UHeapRef): URefSetEntries = + override fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): URefSetEntries = foldHeapRefWithStaticAsSymbolic( ref = ref, initial = URefSetEntries(), initialGuard = ref.uctx.trueExpr, blockOnConcrete = { entries, (concreteRef, _) -> - allocatedSetWithAllocatedElements.keys.forEach { entry -> + allocatedSetWithAllocatedElements.keys().forEach { entry -> if (entry.setAddress == concreteRef.address) { val elem = ref.uctx.mkConcreteHeapRef(entry.elementAddress) entries.add(URefSetEntryLValue(concreteRef, elem, setType)) @@ -397,7 +402,7 @@ internal class URefSetMemoryRegion( val elementsId = allocatedSetWithInputElementsId(concreteRef.address) val elements = USymbolicSetElementsCollector.collect( - getAllocatedSetWithInputElements(elementsId).updates + getAllocatedSetWithInputElements(elementsId, ownership).updates ) elements.elements.forEach { elem -> entries.add(URefSetEntryLValue(concreteRef, elem, setType)) @@ -410,7 +415,7 @@ internal class URefSetMemoryRegion( entries }, blockOnSymbolic = { entries, (symbolicRef, _) -> - inputSetWithAllocatedElements.keys.forEach { entry -> + inputSetWithAllocatedElements.keys().forEach { entry -> val elem = ref.uctx.mkConcreteHeapRef(entry.elementAddress) entries.add(URefSetEntryLValue(symbolicRef, elem, setType)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt index ff77cf7e7b..91a5bb988b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt @@ -2,6 +2,7 @@ package org.usvm.collection.set.ref import org.usvm.UBoolExpr import org.usvm.UHeapRef +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.UWritableMemory import org.usvm.uctx @@ -19,7 +20,7 @@ internal fun UWritableMemory<*>.refSetUnion( "setUnion is not applicable to $region" } - val newRegion = region.union(srcRef, dstRef, guard) + val newRegion = region.union(srcRef, dstRef, guard, ownership) setRegion(regionId, newRegion) } @@ -31,5 +32,5 @@ fun UReadOnlyMemory<*>.refSetEntries( val region = getRegion(regionId) as? URefSetReadOnlyRegion ?: return URefSetEntries().apply { markAsInput() } - return region.setEntries(setRef) + return region.setEntries(setRef, ownership) } diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt index 877a8ee1eb..ae6add434f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt @@ -33,7 +33,7 @@ import org.usvm.solver.UExprTranslator */ class UEqualityConstraints private constructor( internal val ctx: UContext<*>, - private var ownership: MutabilityOwnership, + internal var ownership: MutabilityOwnership, private val equalReferences: DisjointSets, var distinctReferences: UPersistentHashSet, var referenceDisequalities: UPersistentMultiMap, @@ -47,10 +47,7 @@ class UEqualityConstraints private constructor( persistentHashMapOf(), persistentHashMapOf(), ) - - fun changeOwnership(newOwnership: MutabilityOwnership) { - ownership = newOwnership - } + /** * Determines whether a static ref could be assigned to a symbolic, according to additional information. */ diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt index 5fcd3286e4..87043c36d6 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt @@ -49,8 +49,8 @@ open class UPathConstraints( fun changeOwnership(newOwnership: MutabilityOwnership) { ownership = newOwnership - numericConstraints.changeOwnership(newOwnership) - equalityConstraints.changeOwnership(newOwnership) + numericConstraints.ownership = newOwnership + equalityConstraints.ownership = newOwnership } /** diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt index c3c9fa84fb..2b26a36c30 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt @@ -64,16 +64,12 @@ private typealias ConstraintTerms = UExpr class UNumericConstraints private constructor( private val ctx: UContext<*>, val sort: Sort, - private var ownership: MutabilityOwnership, + internal var ownership: MutabilityOwnership, private var numericConstraints: UPersistentHashMap, Constraint>, private var constraintWatchList: UPersistentMultiMap, ConstraintTerms>, ) : UOwnedMergeable, MutableMergeGuard> { constructor(ctx: UContext<*>, sort: Sort, ownership: MutabilityOwnership) : this(ctx, sort, ownership, persistentHashMapOf(), persistentHashMapOf()) - fun changeOwnership(newOwnership: MutabilityOwnership) { - ownership = newOwnership - } - private val constraintPropagationQueue = arrayListOf>() /** @@ -1965,8 +1961,8 @@ class UNumericConstraints private constructor( fun size(): Int = inferredTermLowerBounds.size + - termUpperBounds.size + - termDisequalities.size + termUpperBounds.size + + termDisequalities.size fun lowerBound(bias: KBitVecValue): ValueConstraint? = concreteLowerBounds[bias] @@ -2174,11 +2170,15 @@ class UNumericConstraints private constructor( class TermConstraintSet( val termConstraints: UPersistentMultiMap, KBitVecValue>, val termDependency: UPersistentMultiMap, TermsConstraint>, - val size : Int + val size: Int ) { constructor() : this(persistentHashMapOf(), persistentHashMapOf(), 0) - fun addTermConstraint(bias: KBitVecValue, constraint: TermsConstraint, ownership: MutabilityOwnership): TermConstraintSet { + fun addTermConstraint( + bias: KBitVecValue, + constraint: TermsConstraint, + ownership: MutabilityOwnership + ): TermConstraintSet { var newSize = size val constraints = termConstraints[constraint].also { if (it == null) newSize++ } ?: persistentHashSetOf() val updatedConstraints = constraints.add(bias, ownership) diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt index 3b704321fa..d0d2dba8f1 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt @@ -1,7 +1,5 @@ package org.usvm.memory -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.INITIAL_CONCRETE_ADDRESS import org.usvm.INITIAL_STATIC_ADDRESS import org.usvm.UBoolExpr @@ -14,10 +12,13 @@ import org.usvm.UIndexedMocker import org.usvm.UMockEvaluator import org.usvm.UMocker import org.usvm.USort +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.constraints.UTypeConstraints import org.usvm.constraints.UTypeEvaluator import org.usvm.merging.MergeGuard -import org.usvm.merging.UMergeable +import org.usvm.merging.UOwnedMergeable interface UMemoryRegionId { val sort: Sort @@ -26,11 +27,11 @@ interface UMemoryRegionId { } interface UReadOnlyMemoryRegion { - fun read(key: Key): UExpr + fun read(key: Key, ownership: MutabilityOwnership): UExpr } interface UMemoryRegion : UReadOnlyMemoryRegion { - fun write(key: Key, value: UExpr, guard: UBoolExpr): UMemoryRegion + fun write(key: Key, value: UExpr, guard: UBoolExpr, ownership: MutabilityOwnership): UMemoryRegion } interface ULValue { @@ -62,13 +63,14 @@ class UAddressCounter { } interface UReadOnlyMemory { + val ownership : MutabilityOwnership val stack: UReadOnlyRegistersStack val mocker: UMockEvaluator val types: UTypeEvaluator private fun read(regionId: UMemoryRegionId, key: Key): UExpr { val region = getRegion(regionId) - return region.read(key) + return region.read(key, ownership) } fun read(lvalue: ULValue) = read(lvalue.memoryRegionId, lvalue.key) @@ -92,13 +94,17 @@ interface UWritableMemory : UReadOnlyMemory { @Suppress("MemberVisibilityCanBePrivate") class UMemory( internal val ctx: UContext<*>, + override var ownership: MutabilityOwnership, override val types: UTypeConstraints, override val stack: URegistersStack = URegistersStack(), - private val mocks: UIndexedMocker = UIndexedMocker(), - persistentRegions: PersistentMap, UMemoryRegion<*, *>> = persistentHashMapOf(), -) : UWritableMemory, UMergeable, MergeGuard> { - private val regions = persistentRegions.builder() + private val mocks: UIndexedMocker = UIndexedMocker(ownership = ownership), + private var regions: UPersistentHashMap, UMemoryRegion<*, *>> = persistentHashMapOf(), +) : UWritableMemory, UOwnedMergeable, MergeGuard> { + fun changeOwnership(newOwnership: MutabilityOwnership) { + ownership = newOwnership + mocks.ownership = newOwnership + } override val mocker: UMocker get() = mocks @@ -106,9 +112,9 @@ class UMemory( override fun getRegion(regionId: UMemoryRegionId): UMemoryRegion { if (regionId is URegisterStackId) return stack as UMemoryRegion - return regions.getOrPut(regionId) { - regionId.emptyRegion() - } as UMemoryRegion + val (updatedRegions, region) = regions.getOrPut(regionId, regionId.emptyRegion(), ownership) + regions = updatedRegions + return region as UMemoryRegion } override fun setRegion( @@ -119,7 +125,7 @@ class UMemory( check(newRegion === stack) { "Stack is mutable" } return } - regions[regionId] = newRegion + regions = regions.put(regionId, newRegion, ownership) } override fun write(lvalue: ULValue, rvalue: UExpr, guard: UBoolExpr) = @@ -132,7 +138,7 @@ class UMemory( guard: UBoolExpr ) { val region = getRegion(regionId) - val newRegion = region.write(key, value, guard) + val newRegion = region.write(key, value, guard, ownership) setRegion(regionId, newRegion) } @@ -152,13 +158,13 @@ class UMemory( override fun nullRef(): UHeapRef = ctx.nullRef - fun clone(typeConstraints: UTypeConstraints): UMemory = - UMemory(ctx, typeConstraints, stack.clone(), mocks.clone(), regions.build()) + fun clone(typeConstraints: UTypeConstraints, ownership: MutabilityOwnership): UMemory = + UMemory(ctx, ownership, typeConstraints, stack.clone(), mocks.clone(ownership), regions) override fun toWritableMemory() = // To be perfectly rigorous, we should clone stack and types here. // But in fact they should not be used, so to optimize things up, we don't touch them. - UMemory(ctx, types, stack, mocks, regions.build()) + UMemory(ctx, ownership, types, stack, mocks, regions) /** @@ -172,9 +178,9 @@ class UMemory( * * @return the merged memory. */ - override fun mergeWith(other: UMemory, by: MergeGuard): UMemory? { - val ids = regions.keys - val otherIds = other.regions.keys + override fun mergeWith(other: UMemory, by: MergeGuard, ownership: MutabilityOwnership): UMemory? { + val ids = regions.keys() + val otherIds = other.regions.keys() if (ids != otherIds) { return null } @@ -189,10 +195,10 @@ class UMemory( } } - val mergedRegions = regions.build() + val mergedRegions = regions val mergedStack = stack.mergeWith(other.stack, by) ?: return null - val mergedMocks = mocks.mergeWith(other.mocks, by) ?: return null + val mergedMocks = mocks.mergeWith(other.mocks, by, ownership) ?: return null - return UMemory(ctx, types, mergedStack, mergedMocks, mergedRegions) + return UMemory(ctx, ownership, types, mergedStack, mergedMocks, mergedRegions) } } diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt b/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt index f5375d2149..e4f484a7a7 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt @@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.USort +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.isTrue import org.usvm.merging.MergeGuard import org.usvm.merging.UMergeable @@ -30,7 +31,8 @@ class URegisterStackLValue( interface UReadOnlyRegistersStack : UReadOnlyMemoryRegion, USort> { fun readRegister(index: Int, sort: Sort): KExpr - override fun read(key: URegisterStackLValue<*>): UExpr = readRegister(key.idx, key.sort) + override fun read(key: URegisterStackLValue<*>, ownership: MutabilityOwnership): UExpr = + readRegister(key.idx, key.sort) } class URegistersStack( @@ -54,6 +56,7 @@ class URegistersStack( key: URegisterStackLValue<*>, value: UExpr, guard: UBoolExpr, + ownership: MutabilityOwnership ): UMemoryRegion, USort> { check(guard.isTrue) { "Guarded writes are not supported for register" } writeRegister(key.idx, value) 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 921e1d1f88..2f21046594 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt @@ -7,6 +7,8 @@ import org.usvm.UComposer import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.isFalse import org.usvm.isTrue import org.usvm.uctx @@ -116,7 +118,8 @@ data class USymbolicCollection, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership, ): USymbolicCollection { assert(value.sort == sort) @@ -213,7 +216,7 @@ data class USymbolicCollection = read(key, composer = null) + override fun read(key: Key, ownership: MutabilityOwnership): UExpr = read(key, composer = null) override fun toString(): String = buildString { @@ -245,16 +248,17 @@ class GuardBuilder(nonMatchingUpdates: UBoolExpr) { get() = nonMatchingUpdatesGuard.isFalse } -inline fun PersistentMap>.guardedWrite( +inline fun UPersistentHashMap>.guardedWrite( key: K, value: UExpr, guard: UBoolExpr, + ownership: MutabilityOwnership, defaultValue: () -> UExpr -): PersistentMap> { +): UPersistentHashMap> { val guardedValue = guard.uctx.mkIte( guard, { value }, { get(key) ?: defaultValue() } ) - return put(key, guardedValue) + return put(key, guardedValue, ownership) } 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 9309b8ef0e..819f615a89 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt @@ -226,7 +226,7 @@ class URangedUpdateNode, dstCollectionId: USymbolicCollectionId, key: DstKey, - composer: UComposer<*, *>, + composer: UComposer<*, *> ) { val convertedKey = adapter.convert(key, composer) sourceCollection.applyTo(memory, convertedKey, composer) @@ -236,7 +236,7 @@ class URangedUpdateNode { * @return Merged entity with new ownership or `null` if `this` and [other] are non-mergeable. */ fun mergeWith(other: Entity, by: By, ownership: MutabilityOwnership): Entity? - } diff --git a/usvm-core/src/main/kotlin/org/usvm/merging/MergingPathSelector.kt b/usvm-core/src/main/kotlin/org/usvm/merging/MergingPathSelector.kt index 6e4d41b251..3061af3558 100644 --- a/usvm-core/src/main/kotlin/org/usvm/merging/MergingPathSelector.kt +++ b/usvm-core/src/main/kotlin/org/usvm/merging/MergingPathSelector.kt @@ -37,7 +37,7 @@ class MergingPathSelector>( val resultState = when (val selectorState = selectorState) { is SelectorState.Advancing -> { val closeState = closeStatesSearcher.findCloseStates(state).firstOrNull() ?: return state - val mergedState = state.mergeWith(closeState, Unit, MutabilityOwnership()) + val mergedState = state.mergeWith(closeState, Unit) if (mergedState == null) { selectorState.steps++ if (selectorState.steps == advanceLimit) { 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 9743188f61..ec6fc9f924 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt @@ -14,6 +14,7 @@ import org.usvm.UContext import org.usvm.UExpr import org.usvm.UMockEvaluator import org.usvm.USort +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UMemoryRegionId import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.solver.UExprTranslator @@ -141,6 +142,6 @@ open class ULazyModelDecoder( private val regionId: UMemoryRegionId, private val value: UExpr ) : UReadOnlyMemoryRegion { - override fun read(key: Key): UExpr = value + override fun read(key: Key, ownership: MutabilityOwnership): UExpr = value } } 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 59feb5405f..39a0c42a44 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/Model.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt @@ -10,6 +10,7 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UMockEvaluator import org.usvm.USort +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.ULValue import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -37,6 +38,7 @@ open class UModelBase( override val mocker: UMockEvaluator, val regions: Map, UReadOnlyMemoryRegion<*, *>>, val nullRef: UConcreteHeapRef, + override val ownership: MutabilityOwnership = ctx.defaultOwnership, ) : UModel, UWritableMemory { @Suppress("LeakingThis") protected open val composer = ctx.composer(this) diff --git a/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt b/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt index 5604612f43..a7061cc4bb 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt @@ -1,10 +1,11 @@ package org.usvm.model import io.ksmt.expr.KExpr -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UExpr import org.usvm.USort +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.memory.UMemoryRegion import org.usvm.memory.UReadOnlyMemoryRegion @@ -13,7 +14,7 @@ import org.usvm.memory.UReadOnlyMemoryRegion * A specific [UMemoryRegion] for one-dimensional regions generalized by a single expression of a [KeySort]. */ class UMemory1DArray internal constructor( - private val values: PersistentMap, UExpr>, + private val values: UPersistentHashMap, UExpr>, private val constValue: UExpr, ) : UReadOnlyMemoryRegion, Sort> { @@ -25,7 +26,7 @@ class UMemory1DArray internal constructor( mappedConstValue: UExpr, ) : this(persistentHashMapOf(), mappedConstValue) - override fun read(key: KExpr): UExpr = values.getOrDefault(key, constValue) + override fun read(key: KExpr, ownership: MutabilityOwnership): UExpr = values.getOrDefault(key, constValue) } /** @@ -33,7 +34,7 @@ class UMemory1DArray internal constructor( * of two expressions with [Key1Sort] and [Key2Sort] sorts. */ class UMemory2DArray internal constructor( - val values: PersistentMap, UExpr>, UExpr>, + val values: UPersistentHashMap, UExpr>, UExpr>, val constValue: UExpr, ) : UReadOnlyMemoryRegion, KExpr>, Sort> { /** @@ -44,7 +45,7 @@ class UMemory2DArray internal mappedConstValue: UExpr, ) : this(persistentHashMapOf(), mappedConstValue) - override fun read(key: Pair, KExpr>): UExpr { + override fun read(key: Pair, KExpr>, ownership: MutabilityOwnership): UExpr { return values.getOrDefault(key, constValue) } } diff --git a/usvm-core/src/main/kotlin/org/usvm/model/UModelEvaluator.kt b/usvm-core/src/main/kotlin/org/usvm/model/UModelEvaluator.kt index be68857e07..0bb7e7e2c0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/UModelEvaluator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/UModelEvaluator.kt @@ -27,7 +27,7 @@ import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort import io.ksmt.utils.uncheckedCast -import kotlinx.collections.immutable.persistentHashMapOf +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.NULL_ADDRESS import org.usvm.UContext import org.usvm.UExpr @@ -114,20 +114,20 @@ open class UModelEvaluator( ): UMemory1DArray { val interpretation = model.interpretation(translated) - val stores = persistentHashMapOf, UExpr>().builder() + var stores = persistentHashMapOf, UExpr>() val defaultValue = interpretation?.let { traverse1DArrayEntries(interpretation) { idx, value -> - stores[idx.mapAddress(addressesMapping)] = value.mapAddress(addressesMapping) + stores = stores.put(idx.mapAddress(addressesMapping), value.mapAddress(addressesMapping), ctx.defaultOwnership) } } if (defaultValue != null) { - return UMemory1DArray(stores.build(), defaultValue.mapAddress(addressesMapping)) + return UMemory1DArray(stores, defaultValue.mapAddress(addressesMapping)) } return completed1DArrays.getOrPut(translated) { val completedDefault = translated.sort.range.accept(this) - UMemory1DArray(stores.build(), completedDefault.uncheckedCast()) + UMemory1DArray(stores, completedDefault.uncheckedCast()) }.uncheckedCast() } @@ -136,26 +136,26 @@ open class UModelEvaluator( * Complete model according to the array range (value) sort if array is free in the model. * */ open fun evalAndCompleteArray2DMemoryRegion( - translated: KDecl>, + translated: KDecl> ): UMemory2DArray { val interpretation = model.interpretation(translated) - val stores = persistentHashMapOf, UExpr>, UExpr>().builder() + var stores = persistentHashMapOf, UExpr>, UExpr>() val defaultValue = interpretation?.let { traverse2DArrayEntries(interpretation) { idx1, idx2, value -> val mappedIdx1 = idx1.mapAddress(addressesMapping) val mappedIdx2 = idx2.mapAddress(addressesMapping) - stores[mappedIdx1 to mappedIdx2] = value.mapAddress(addressesMapping) + stores = stores.put(mappedIdx1 to mappedIdx2, value.mapAddress(addressesMapping), ctx.defaultOwnership) } } if (defaultValue != null) { - return UMemory2DArray(stores.build(), defaultValue.mapAddress(addressesMapping)) + return UMemory2DArray(stores, defaultValue.mapAddress(addressesMapping)) } return completed2DArrays.getOrPut(translated) { val completedDefault = translated.sort.range.accept(this) - UMemory2DArray(stores.build(), completedDefault.uncheckedCast()) + UMemory2DArray(stores, completedDefault.uncheckedCast()) }.uncheckedCast() } diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt index da88a0d0da..8c270cc04f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt @@ -136,7 +136,7 @@ private fun createPathSelector( wrappedSelectors.first().add(initialStates.toList()) wrappedSelectors.drop(1).forEach { - it.add(initialStates.map { it.clone(MutabilityOwnership()) }.toList()) + it.add(initialStates.map { it.clone() }.toList()) } ParallelPathSelector(wrappedSelectors) 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 a50473d866..e9487e3888 100644 --- a/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt +++ b/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt @@ -57,7 +57,7 @@ abstract class U1DUpdatesTranslator( override fun visitUpdate( previous: KExpr>, - update: UUpdateNode, Sort>, + update: UUpdateNode, Sort> ): KExpr> = with(previous.uctx) { when (update) { is UPinpointUpdateNode -> { diff --git a/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt b/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt index b8a6c973d9..ec66ed1aaf 100644 --- a/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt +++ b/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt @@ -27,7 +27,7 @@ internal fun UState.isSat(): Boolean { @Suppress("MoveVariableDeclarationIntoWhen") internal fun > State.checkSat(condition: UBoolExpr): State? { - val conditionalState = clone(MutabilityOwnership()) + val conditionalState = clone() conditionalState.pathConstraints += condition // If this state did not fork at all or was sat at the last fork point, it must be still sat, so we can just diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt index 62e12db253..3b077f9e39 100644 --- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt @@ -27,6 +27,7 @@ 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.collections.immutable.internal.MutabilityOwnership import org.usvm.constraints.UTypeEvaluator import org.usvm.memory.UFlatUpdates import org.usvm.memory.UMemory @@ -54,6 +55,7 @@ internal class CompositionTest { private lateinit var memory: UReadOnlyMemory private lateinit var ctx: UContext + private lateinit var ownership: MutabilityOwnership private lateinit var concreteNull: UConcreteHeapRef private lateinit var composer: UComposer @@ -63,6 +65,7 @@ internal class CompositionTest { every { components.mkTypeSystem(any()) } returns mockk() ctx = UContext(components) + ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory -> UComposer(ctx, memory) } } @@ -255,7 +258,7 @@ internal class CompositionTest { val fstValueFromHeap = 42.toBv() val sndValueFromHeap = 43.toBv() - val heapToComposeWith = UMemory>, Any>(ctx, mockk()) + val heapToComposeWith = UMemory>, Any>(ctx, MutabilityOwnership(), mockk()) heapToComposeWith.writeArrayLength(fstConcreteAddress, fstValueFromHeap, arrayType, sizeSort) heapToComposeWith.writeArrayLength(sndConcreteAddress, sndValueFromHeap, arrayType, sizeSort) @@ -310,7 +313,7 @@ internal class CompositionTest { val answer = 43.toBv() - val composer = UComposer(ctx, UMemory, Any>(ctx, mockk())) // TODO replace with jacoDB type + val composer = UComposer(ctx, UMemory, Any>(ctx, MutabilityOwnership(), mockk())) // TODO replace with jacoDB type every { fstAddress.accept(composer) } returns sndAddress every { fstIndex.accept(composer) } returns sndIndex @@ -340,13 +343,13 @@ internal class CompositionTest { // create a reading from the region val fstArrayIndexReading = mkInputArrayReading(region, fstAddress, fstIndex) - val sndMemory = UMemory, Any>(ctx, mockk(), mockk()) + val sndMemory = UMemory, Any>(ctx, MutabilityOwnership(), mockk(), mockk()) // create a heap with a record: (sndAddress, sndIndex) = 2 sndMemory.writeArrayIndex(sndAddress, sndIndex, arrayType, mkBv32Sort(), 2.toBv(), mkTrue()) val sndComposer = UComposer(ctx, sndMemory) - val fstMemory = UMemory, Any>(ctx, mockk(), mockk()) + val fstMemory = UMemory, Any>(ctx, ownership, mockk(), mockk()) // create a heap with a record: (fstAddress, fstIndex) = 1 fstMemory.writeArrayIndex(fstAddress, fstIndex, arrayType, mkBv32Sort(), 1.toBv(), mkTrue()) @@ -416,7 +419,7 @@ internal class CompositionTest { val fstValue = 42.toBv() val sndValue = 43.toBv() - val heapToComposeWith = UMemory>, Any>(ctx, mockk()) + val heapToComposeWith = UMemory>, Any>(ctx, MutabilityOwnership(), mockk()) heapToComposeWith.writeArrayIndex( fstAddressForCompose, concreteIndex, arrayType, regionArray.sort, fstValue, guard = trueExpr @@ -448,8 +451,8 @@ internal class CompositionTest { val regionArray = UAllocatedArrayId<_, _, USizeSort>(arrayType, addressSort, 0) .emptyRegion() - .write(mkBv(0), symbolicAddress, trueExpr) - .write(mkBv(1), mkConcreteHeapRef(1), trueExpr) + .write(mkBv(0), symbolicAddress, trueExpr, ownership) + .write(mkBv(1), mkConcreteHeapRef(1), trueExpr, ownership) val reading = mkAllocatedArrayReading(regionArray, symbolicIndex) @@ -487,7 +490,7 @@ internal class CompositionTest { val region = USymbolicCollection( UInputFieldId(field, bv32Sort), updates, - ).write(aAddress, 43.toBv(), guard = trueExpr) + ).write(aAddress, 43.toBv(), guard = trueExpr, ownership) every { aAddress.accept(any()) } returns aAddress every { bAddress.accept(any()) } returns aAddress @@ -505,7 +508,7 @@ internal class CompositionTest { val answer = 43.toBv() - val composeMemory = UMemory(ctx, mockk()) + val composeMemory = UMemory(ctx, MutabilityOwnership(), mockk()) composeMemory.writeField(aAddress, field, bv32Sort, 42.toBv(), guard = trueExpr) val composer = UComposer(ctx, composeMemory) @@ -556,7 +559,7 @@ internal class CompositionTest { val symbolicRef2 = mkRegisterReading(2, addressSort) as UHeapRef val composedSymbolicHeapRef = mkConcreteHeapRef(1) - val composeMemory = UMemory(ctx, mockk()) + val composeMemory = UMemory(ctx, MutabilityOwnership(), mockk()) composeMemory.writeArrayIndex(composedSymbolicHeapRef, mkBv(3), arrayType, bv32Sort, mkBv(1337), trueExpr) @@ -570,7 +573,7 @@ internal class CompositionTest { val fromRegion0 = UInputArrayId<_, _, USizeSort>(arrayType, bv32Sort) .emptyRegion() - .write(symbolicRef0 to mkBv(0), mkBv(42), trueExpr) + .write(symbolicRef0 to mkBv(0), mkBv(42), trueExpr, ownership) val adapter1 = USymbolicArrayInputToInputCopyAdapter( symbolicRef0 to mkSizeExpr(0), @@ -594,7 +597,7 @@ internal class CompositionTest { val idx0 = mkRegisterReading(3, bv32Sort) - val reading0 = fromRegion2.read(symbolicRef2 to idx0) + val reading0 = fromRegion2.read(symbolicRef2 to idx0, ownership) val composedExpr0 = composer.compose(reading0) val composedReading0 = assertIs>(composedExpr0) @@ -627,7 +630,7 @@ internal class CompositionTest { val composer = UComposer(this, composedMemory) val region = UAllocatedArrayId<_, _, USizeSort>(mockk(), addressSort, 1).emptyRegion() - val reading = region.read(mkRegisterReading(0, sizeSort)) + val reading = region.read(mkRegisterReading(0, sizeSort), ownership) val expr = composer.compose(reading) assertSame(concreteNull, expr) @@ -645,10 +648,10 @@ internal class CompositionTest { val region = UInputFieldId(field, bv32Sort) .emptyRegion() - .write(ref0, mkBv(0), trueExpr) - .write(ref1, mkBv(1), trueExpr) + .write(ref0, mkBv(0), trueExpr, ownership) + .write(ref1, mkBv(1), trueExpr, ownership) - val reading = region.read(ref2) + val reading = region.read(ref2, ownership) val composer = spyk(UComposer(this, composedMemory)) diff --git a/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt b/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt index 54cc603ec2..461d7ba251 100644 --- a/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt +++ b/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt @@ -48,7 +48,7 @@ internal class TestState( override val entrypoint: TestMethod = "" ) : UState, TestTarget, TestState>(ctx, ownership, callStack, pathConstraints, memory, models, pathLocation, PathNode.root(), targetTrees) { - override fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints?): TestState = this + override fun clone(newConstraints: UPathConstraints?): TestState = this override val isExceptional = false } diff --git a/usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt b/usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt index 6b0e87f7b8..587f921dbc 100644 --- a/usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt +++ b/usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt @@ -65,7 +65,7 @@ abstract class SymbolicCollectionTestBase { pathConstraints = UPathConstraints(ctx, ownership) - memory = UMemory(ctx, pathConstraints.typeConstraints) + memory = UMemory(ctx, ownership, pathConstraints.typeConstraints) scope = StepScope(StateStub(ctx, ownership, pathConstraints, memory), UForkBlackList.createDefault()) } @@ -80,9 +80,11 @@ abstract class SymbolicCollectionTestBase { ctx, ownership, UCallStack(), pathConstraints, memory, emptyList(), PathNode.root(), PathNode.root(), UTargetsSet.empty() ) { - override fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints?): StateStub { - val clonedConstraints = newConstraints ?: pathConstraints.clone(ownership) - return StateStub(ctx, ownership, clonedConstraints, memory.clone(clonedConstraints.typeConstraints)) + override fun clone(newConstraints: UPathConstraints?): StateStub { + this.changeOwnership(MutabilityOwnership()) + val cloneOwnership = MutabilityOwnership() + val clonedConstraints = newConstraints ?: pathConstraints.clone(cloneOwnership) + return StateStub(ctx, cloneOwnership, clonedConstraints, memory.clone(clonedConstraints.typeConstraints, cloneOwnership)) } override val isExceptional: Boolean diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt index ee4cb4455d..1f932ec13e 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt @@ -30,7 +30,7 @@ class HeapMemCpyTest { every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } val eqConstraints = UEqualityConstraints(ctx, ownership) val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints) - heap = UMemory(ctx, typeConstraints) + heap = UMemory(ctx, ownership, typeConstraints) arrayType = mockk() arrayValueSort = ctx.sizeSort } diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt index 8cb3e75fb4..68dbe2c17f 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt @@ -40,7 +40,7 @@ class HeapMemsetTest { every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } val eqConstraints = UEqualityConstraints(ctx, ownership) val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints) - heap = UMemory(ctx, typeConstraints) + heap = UMemory(ctx, ownership, typeConstraints) arrayType = mockk() arrayValueSort = ctx.addressSort } diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt index eb0854c5c8..35770d17ad 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt @@ -10,18 +10,21 @@ import org.usvm.UComponents import org.usvm.UContext import org.usvm.USizeSort import org.usvm.api.allocateConcreteRef +import org.usvm.collections.immutable.internal.MutabilityOwnership import kotlin.test.assertSame class HeapRefEqTest { private lateinit var ctx: UContext private lateinit var heap: UMemory + private lateinit var ownership : MutabilityOwnership @BeforeEach fun initializeContext() { val components: UComponents = mockk() every { components.mkTypeSystem(any()) } returns mockk() ctx = UContext(components) - heap = UMemory(ctx, mockk()) + ownership = MutabilityOwnership() + heap = UMemory(ctx, ownership, mockk()) } @Test @@ -156,4 +159,4 @@ class HeapRefEqTest { val expected = concreteRef1EqConcreteRef2 or (symbolicRefEqGuard and symbolicIteEq) assertSame(expected, refsEq) } -} \ No newline at end of file +} diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt index 7b9c7b2df7..5379221a3e 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt @@ -37,7 +37,7 @@ import kotlin.test.assertSame class HeapRefSplittingTest { private lateinit var ctx: UContext private lateinit var heap: UMemory - private val ownership = MutabilityOwnership() + private lateinit var ownership : MutabilityOwnership private lateinit var valueFieldDescr: Pair private lateinit var addressFieldDescr: Pair @@ -48,10 +48,11 @@ class HeapRefSplittingTest { val components: UComponents = mockk() every { components.mkTypeSystem(any()) } returns mockk() ctx = UContext(components) + ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } val eqConstraints = UEqualityConstraints(ctx, ownership) val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints) - heap = UMemory(ctx, typeConstraints) + heap = UMemory(ctx, ownership, typeConstraints) valueFieldDescr = mockk() to ctx.bv32Sort addressFieldDescr = mockk() to ctx.addressSort diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt index b1ec385875..b66a51da33 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt @@ -16,6 +16,7 @@ import org.usvm.UHeapRef import org.usvm.USizeSort import org.usvm.collection.array.UAllocatedArrayId import org.usvm.collection.array.UInputArrayId +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.mkSizeExpr import org.usvm.regions.SetRegion import org.usvm.regions.emptyRegionTree @@ -26,12 +27,14 @@ import kotlin.test.assertTrue class MemoryRegionTest { private lateinit var ctx: UContext + private lateinit var ownership : MutabilityOwnership @BeforeEach fun initializeContext() { val components: UComponents = mockk() every { components.mkTypeSystem(any()) } returns mockk() ctx = UContext(components) + ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } } @@ -98,15 +101,15 @@ class MemoryRegionTest { val memoryRegion = UAllocatedArrayId<_, _, USizeSort>(mockk(), sizeSort, 0) .emptyRegion() - .write(idx1, mkBv(0), trueExpr) - .write(idx2, mkBv(1), trueExpr) + .write(idx1, mkBv(0), trueExpr, ownership) + .write(idx2, mkBv(1), trueExpr, ownership) val updatesBefore = memoryRegion.updates.toList() assertEquals(2, updatesBefore.size) assertTrue(updatesBefore.first().includesConcretely(idx1, trueExpr)) assertTrue(updatesBefore.last().includesConcretely(idx2, trueExpr)) - val memoryRegionAfter = memoryRegion.write(idx2, mkBv(2), trueExpr) + val memoryRegionAfter = memoryRegion.write(idx2, mkBv(2), trueExpr, ownership) val updatesAfter = memoryRegionAfter.updates.toList() assertEquals(2, updatesAfter.size) @@ -141,13 +144,13 @@ class MemoryRegionTest { val idx = indices.random(random) val value = refs.random(random) - memoryRegion = memoryRegion.write(ref to idx, value, trueExpr) + memoryRegion = memoryRegion.write(ref to idx, value, trueExpr, ownership) } val readRef = symbolicRefs.random(random) val readIdx = indices.random(random) - memoryRegion.read(readRef to readIdx) + memoryRegion.read(readRef to readIdx, ownership) } } -} \ No newline at end of file +} diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt index f5aa639763..bc8aa31e81 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt @@ -42,7 +42,7 @@ class SetEntriesTest { every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } val eqConstraints = UEqualityConstraints(ctx, ownership) val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints) - heap = UMemory(ctx, typeConstraints) + heap = UMemory(ctx, ownership, typeConstraints) setType = mockk() } diff --git a/usvm-core/src/test/kotlin/org/usvm/merging/MemoryMergingTest.kt b/usvm-core/src/test/kotlin/org/usvm/merging/MemoryMergingTest.kt index b46c9efea8..2967d7ba43 100644 --- a/usvm-core/src/test/kotlin/org/usvm/merging/MemoryMergingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/merging/MemoryMergingTest.kt @@ -49,8 +49,8 @@ class MemoryMergingTest { fun `Empty memory`() = with(ctx) { val byCondition = mkConst("cond", boolSort) val pathConstraints = UPathConstraints(this, ownership) - val memoryLeft = UMemory(this, pathConstraints.typeConstraints) - val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints) + val memoryLeft = UMemory(this, ownership, pathConstraints.typeConstraints) + val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints, ownership) checkMergedEqualsToOriginal( memoryLeft, @@ -67,12 +67,12 @@ class MemoryMergingTest { val byCondition = mkConst("cond", boolSort) val pathConstraints = UPathConstraints(this, ownership) - val memoryLeft = UMemory(this, pathConstraints.typeConstraints) + val memoryLeft = UMemory(this, ownership, pathConstraints.typeConstraints) memoryLeft.stack.push(3) memoryLeft.stack.writeRegister(0, mkBv(42)) memoryLeft.stack.writeRegister(1, mkBv(1337)) - val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints) + val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints, MutabilityOwnership()) memoryRight.stack.writeRegister(0, mkBv(13)) memoryRight.stack.writeRegister(2, mkBv(9)) @@ -92,7 +92,8 @@ class MemoryMergingTest { val byCondition = mkConst("cond", boolSort) val pathConstraints = UPathConstraints(this, ownership) - val memoryLeft = UMemory(this, pathConstraints.typeConstraints) + val leftOwnership = ownership + val memoryLeft = UMemory(this, leftOwnership, pathConstraints.typeConstraints) val ref1 = allocateConcreteRef() val ref2 = allocateConcreteRef() @@ -102,7 +103,7 @@ class MemoryMergingTest { memoryLeft.writeField(ref2, Unit, addressSort, mkRegisterReading(2, addressSort), trueExpr) memoryLeft.writeField(ref3, Unit, addressSort, mkRegisterReading(3, addressSort), trueExpr) - val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints) + val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints, MutabilityOwnership()) memoryRight.writeField(ref1, Unit, addressSort, mkRegisterReading(-1, addressSort), trueExpr) memoryRight.writeField(ref2, Unit, addressSort, mkRegisterReading(-2, addressSort), trueExpr) memoryRight.writeField(ref3, Unit, addressSort, mkRegisterReading(-3, addressSort), trueExpr) @@ -125,7 +126,7 @@ class MemoryMergingTest { vararg getters: (UMemory) -> UExpr, ) = with(ctx) { val mergeGuard = MutableMergeGuard(this).apply { appendThis(sequenceOf(byCondition)) } - val mergedMemory = checkNotNull(memoryLeft.mergeWith(memoryRight, mergeGuard)) + val mergedMemory = checkNotNull(memoryLeft.mergeWith(memoryRight, mergeGuard, MutabilityOwnership())) for (getter in getters) { val leftExpr: UExpr = getter(memoryLeft).uncheckedCast() diff --git a/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt index 5d9ad247bb..90223020d4 100644 --- a/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt @@ -2,7 +2,7 @@ package org.usvm.model import io.mockk.every import io.mockk.mockk -import kotlinx.collections.immutable.persistentMapOf +import org.usvm.collections.immutable.persistentHashMapOf import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test @@ -37,6 +37,7 @@ import kotlin.test.assertSame class ModelCompositionTest { private lateinit var ctx: UContext + private lateinit var ownership: MutabilityOwnership private lateinit var concreteNull: UConcreteHeapRef @BeforeEach @@ -44,6 +45,7 @@ class ModelCompositionTest { val components: UComponents<*, USizeSort> = mockk() every { components.mkTypeSystem(any()) } returns mockk() ctx = UContext(components) + ownership = MutabilityOwnership() every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory -> UComposer(ctx, memory) } } every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } @@ -62,11 +64,11 @@ class ModelCompositionTest { val region = UAllocatedArrayId<_, _, USizeSort>(mockk(), bv32Sort, 1) .emptyRegion() - .write(0.toBv(), 0.toBv(), trueExpr) - .write(1.toBv(), 1.toBv(), trueExpr) - .write(mkRegisterReading(1, sizeSort), 2.toBv(), trueExpr) - .write(mkRegisterReading(2, sizeSort), 3.toBv(), trueExpr) - val reading = region.read(mkRegisterReading(0, sizeSort)) + .write(0.toBv(), 0.toBv(), trueExpr, ownership) + .write(1.toBv(), 1.toBv(), trueExpr, ownership) + .write(mkRegisterReading(1, sizeSort), 2.toBv(), trueExpr, ownership) + .write(mkRegisterReading(2, sizeSort), 3.toBv(), trueExpr, ownership) + val reading = region.read(mkRegisterReading(0, sizeSort), ownership) val expr = composer.compose(reading) assertSame(mkBv(2), expr) @@ -79,8 +81,9 @@ class ModelCompositionTest { val composedSymbolicHeapRef = ctx.mkConcreteHeapRef(-1) val inputArray = UMemory2DArray( - persistentMapOf((composedSymbolicHeapRef to mkBv(0)) to mkBv(1)), mkBv(0) + persistentHashMapOf(ownership, (composedSymbolicHeapRef to mkBv(0)) to mkBv(1)), mkBv(0) ) + val arrayModel = UArrayEagerModelRegion(arrayMemoryId, inputArray) val stackModel = URegistersStackEagerModel( @@ -111,7 +114,7 @@ class ModelCompositionTest { val idx = mkRegisterReading(1, sizeSort) - val reading = concreteRegion.read(idx) + val reading = concreteRegion.read(idx, ownership) val expr = composer.compose(reading) assertSame(mkBv(1), expr) @@ -132,7 +135,7 @@ class ModelCompositionTest { val arrayType = mockk() val arrayLengthMemoryId = UArrayLengthsRegionId(sizeSort, arrayType) - val inputLength = UMemory1DArray(persistentMapOf(composedRef0 to mkBv(42)), mkBv(0)) + val inputLength = UMemory1DArray(persistentHashMapOf(ownership, composedRef0 to mkBv(42)), mkBv(0)) val arrayLengthModel = UArrayLengthEagerModelRegion(arrayLengthMemoryId, inputLength) val stackModel = URegistersStackEagerModel( @@ -153,10 +156,10 @@ class ModelCompositionTest { val region = UInputArrayLengthId(arrayType, bv32Sort) .emptyRegion() - .write(symbolicRef1, 0.toBv(), trueExpr) - .write(symbolicRef2, 1.toBv(), trueExpr) - .write(symbolicRef3, 2.toBv(), trueExpr) - val reading = region.read(symbolicRef0) + .write(symbolicRef1, 0.toBv(), trueExpr, ownership) + .write(symbolicRef2, 1.toBv(), trueExpr, ownership) + .write(symbolicRef3, 2.toBv(), trueExpr, ownership) + val reading = region.read(symbolicRef0, ownership) val expr = composer.compose(reading) assertSame(mkBv(42), expr) @@ -177,7 +180,7 @@ class ModelCompositionTest { val field = mockk() val fieldMemoryId = UFieldsRegionId(field, addressSort) - val inputField = UMemory1DArray(persistentMapOf(composedRef0 to composedRef0), concreteNull) + val inputField = UMemory1DArray(persistentHashMapOf(ownership, composedRef0 to composedRef0), concreteNull) val fieldModel = UFieldsEagerModelRegion(fieldMemoryId, inputField) val stackModel = URegistersStackEagerModel( @@ -198,10 +201,10 @@ class ModelCompositionTest { val region = UInputFieldId(field, addressSort) .emptyRegion() - .write(symbolicRef1, symbolicRef1, trueExpr) - .write(symbolicRef2, symbolicRef2, trueExpr) - .write(symbolicRef3, symbolicRef3, trueExpr) - val reading = region.read(symbolicRef0) + .write(symbolicRef1, symbolicRef1, trueExpr, ownership) + .write(symbolicRef2, symbolicRef2, trueExpr, ownership) + .write(symbolicRef3, symbolicRef3, trueExpr, ownership) + val reading = region.read(symbolicRef0, ownership) val expr = composer.compose(reading) assertSame(composedRef0, expr) @@ -230,9 +233,9 @@ class ModelCompositionTest { run { val region = emptyRegion - .write(index0, nonDefaultValue0, trueGuard) - .write(index0, nonDefaultValue1, falseGuard) - val reading = region.read(index0) + .write(index0, nonDefaultValue0, trueGuard, ownership) + .write(index0, nonDefaultValue1, falseGuard, ownership) + val reading = region.read(index0, ownership) val expr = composer.compose(reading) assertEquals(nonDefaultValue0, expr) @@ -240,9 +243,9 @@ class ModelCompositionTest { run { val region = emptyRegion - .write(index1, nonDefaultValue0, trueGuard) - .write(index0, nonDefaultValue1, falseGuard) - val reading = region.read(index0) + .write(index1, nonDefaultValue0, trueGuard, ownership) + .write(index0, nonDefaultValue1, falseGuard, ownership) + val reading = region.read(index0, ownership) val expr = composer.compose(reading) assertEquals(defaultValue, expr) diff --git a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt index 03d4054171..c110617472 100644 --- a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt @@ -74,8 +74,8 @@ class ModelDecodingTest { stack = URegistersStack() stack.push(10) - mocker = UIndexedMocker() - heap = UMemory(ctx, pc.typeConstraints, stack, mocker) + mocker = UIndexedMocker(ownership = ownership) + heap = UMemory(ctx, ownership, pc.typeConstraints, stack, mocker) } @Test diff --git a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt index 1566188f85..5b50a547a3 100644 --- a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt @@ -132,11 +132,11 @@ open class SoftConstraintsTest { val secondInputRef = mkRegisterReading(1, addressSort) val region = UInputArrayLengthId(arrayType, sizeSort) .emptyRegion() - .write(inputRef, mkRegisterReading(3, sizeSort), guard = trueExpr) + .write(inputRef, mkRegisterReading(3, sizeSort), guard = trueExpr, ownership) val size = 25 - val reading = region.read(secondInputRef) + val reading = region.read(secondInputRef, ownership) val pc = UPathConstraints(ctx, ownership) pc += reading eq size.toBv() @@ -158,7 +158,7 @@ open class SoftConstraintsTest { val inputRef = mkRegisterReading(0, addressSort) val region = UInputArrayLengthId(arrayType, sizeSort) .emptyRegion() - .write(inputRef, mkRegisterReading(3, sizeSort), guard = trueExpr) + .write(inputRef, mkRegisterReading(3, sizeSort), guard = trueExpr, ownership) val pc = UPathConstraints(ctx, ownership) pc += (inputRef eq nullRef).not() 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 16a05dcad3..7569676364 100644 --- a/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt @@ -32,6 +32,7 @@ import org.usvm.collection.array.USymbolicArrayInputToInputCopyAdapter import org.usvm.collection.array.length.UInputArrayLengthId import org.usvm.collection.field.UInputFieldId import org.usvm.collection.map.ref.URefMapEntryLValue +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UMemory import org.usvm.mkSizeExpr import org.usvm.memory.key.USizeExprKeyInfo @@ -41,6 +42,7 @@ import kotlin.test.assertSame class TranslationTest { private lateinit var ctx: RecordingCtx + private lateinit var ownership: MutabilityOwnership private lateinit var heap: UMemory private lateinit var translator: UExprTranslator @@ -69,8 +71,9 @@ class TranslationTest { every { components.mkTypeSystem(any()) } returns mockk() ctx = RecordingCtx(components) + ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } - heap = UMemory(ctx, mockk()) + heap = UMemory(ctx, ownership, mockk()) translator = UExprTranslator(ctx) valueFieldDescr = mockk() to ctx.bv32Sort @@ -144,13 +147,13 @@ class TranslationTest { val region = UInputArrayId<_, _, USizeSort>(valueArrayDescr, bv32Sort) .emptyRegion() - .write(ref1 to idx1, val1, trueExpr) - .write(ref2 to idx2, val2, trueExpr) + .write(ref1 to idx1, val1, trueExpr, ownership) + .write(ref2 to idx2, val2, trueExpr, ownership) val ref3 = mkRegisterReading(4, addressSort) val idx3 = mkRegisterReading(5, sizeSort) - val reading = region.read(ref3 to idx3) + val reading = region.read(ref3 to idx3, ownership) val translated = translator.translate(reading) @@ -175,8 +178,8 @@ class TranslationTest { val region = UInputArrayId<_, _, USizeSort>(valueArrayDescr, bv32Sort) .emptyRegion() - .write(ref1 to idx1, val1, trueExpr) - .write(ref2 to idx2, val2, trueExpr) + .write(ref1 to idx1, val1, trueExpr, ownership) + .write(ref2 to idx2, val2, trueExpr, ownership) val concreteRef = allocateConcreteRef() @@ -193,13 +196,13 @@ class TranslationTest { .copyRange(region, adapter, trueExpr) val idx = mkRegisterReading(4, sizeSort) - val reading = concreteRegion.read(idx) + val reading = concreteRegion.read(idx, ownership) val keyInfo = region.collectionId.keyInfo() val key = keyInfo.mapKey(adapter.convert(translator.translate(idx), composer = null), translator) val innerReading = - translator.translate(region.read(key)) + translator.translate(region.read(key, ownership)) val guard = translator.translate((mkBvSignedLessOrEqualExpr(mkBv(0), idx)) and mkBvSignedLessOrEqualExpr(idx, mkBv(5))) val expected = mkIte(guard, innerReading, mkBv(0)) @@ -227,12 +230,12 @@ class TranslationTest { val region = UInputFieldId(mockk(), bv32Sort) .emptyRegion() - .write(ref1, mkBv(1), g1) - .write(ref2, mkBv(2), g2) - .write(ref3, mkBv(3), g3) + .write(ref1, mkBv(1), g1, ownership) + .write(ref2, mkBv(2), g2, ownership) + .write(ref3, mkBv(3), g3, ownership) val ref0 = mkRegisterReading(0, addressSort) - val reading = region.read(ref0) + val reading = region.read(ref0, ownership) val ref0Eq1Or2Or3 = (ref0 eq ref1) or (ref0 eq ref2) or (ref0 eq ref3) val readingNeq123 = (reading neq mkBv(1)) and (reading neq mkBv(2)) and (reading neq mkBv(3)) @@ -253,12 +256,12 @@ class TranslationTest { val region = UInputArrayLengthId(mockk(), bv32Sort) .emptyRegion() - .write(ref1, mkBv(1), trueExpr) - .write(ref2, mkBv(2), trueExpr) - .write(ref3, mkBv(3), trueExpr) + .write(ref1, mkBv(1), trueExpr, ownership) + .write(ref2, mkBv(2), trueExpr, ownership) + .write(ref3, mkBv(3), trueExpr, ownership) val ref0 = mkRegisterReading(0, addressSort) - val reading = region.read(ref0) + val reading = region.read(ref0, ownership) val ref0Eq1Or2Or3 = (ref0 eq ref1) or (ref0 eq ref2) or (ref0 eq ref3) val readingNeq123 = (reading neq mkBv(1)) and (reading neq mkBv(2)) and (reading neq mkBv(3)) @@ -283,8 +286,8 @@ class TranslationTest { val inputRegion1 = UInputArrayId<_, _, USizeSort>(valueArrayDescr, bv32Sort) .emptyRegion() - .write(ref1 to idx1, val1, trueExpr) - .write(ref2 to idx2, val2, trueExpr) + .write(ref1 to idx1, val1, trueExpr, ownership) + .write(ref2 to idx2, val2, trueExpr, ownership) val adapter = USymbolicArrayInputToInputCopyAdapter( @@ -297,12 +300,12 @@ class TranslationTest { var inputRegion2 = UInputArrayId<_, _, USizeSort>(valueArrayDescr, bv32Sort).emptyRegion() val idx = mkRegisterReading(4, sizeSort) - val reading1 = inputRegion2.read(ref2 to idx) + val reading1 = inputRegion2.read(ref2 to idx, ownership) inputRegion2 = inputRegion2 .copyRange(inputRegion1, adapter, trueExpr) - val reading2 = inputRegion2.read(ref2 to idx) + val reading2 = inputRegion2.read(ref2 to idx, ownership) val expr = (reading1 neq reading2) and (ref1 neq ref2) val translated = translator.translate(expr) @@ -383,8 +386,8 @@ class TranslationTest { val inputRegion1 = UInputArrayId<_, _, USizeSort>(valueArrayDescr, addressSort) .emptyRegion() - .write(ref1 to idx1, val1, trueExpr) - .write(ref2 to idx2, val2, trueExpr) + .write(ref1 to idx1, val1, trueExpr, ownership) + .write(ref2 to idx2, val2, trueExpr, ownership) val adapter = USymbolicArrayInputToInputCopyAdapter( ref1 to mkSizeExpr(0), @@ -396,12 +399,12 @@ class TranslationTest { var inputRegion2 = UInputArrayId<_, _, USizeSort>(valueArrayDescr, addressSort).emptyRegion() val idx = mkRegisterReading(4, sizeSort) - val reading1 = inputRegion2.read(ref2 to idx) + val reading1 = inputRegion2.read(ref2 to idx, ownership) inputRegion2 = inputRegion2 .copyRange(inputRegion1, adapter, trueExpr) - val reading2 = inputRegion2.read(ref2 to idx) + val reading2 = inputRegion2.read(ref2 to idx, ownership) val expr = (reading1 neq reading2) and (ref1 neq ref2) val translated = translator.translate(expr) @@ -424,8 +427,8 @@ class TranslationTest { val allocatedRegion1 = UAllocatedArrayId<_, _, USizeSort>(valueArrayDescr, addressSort, 1) .emptyRegion() - .write(idx1, val1, trueExpr) - .write(idx2, val2, trueExpr) + .write(idx1, val1, trueExpr, ownership) + .write(idx2, val2, trueExpr, ownership) val adapter = USymbolicArrayAllocatedToAllocatedCopyAdapter( mkSizeExpr(0), mkSizeExpr(0), mkSizeExpr(5), USizeExprKeyInfo() @@ -435,12 +438,12 @@ class TranslationTest { .emptyRegion() val idx = mkRegisterReading(4, sizeSort) - val readingBeforeCopy = allocatedRegion2.read(idx) + val readingBeforeCopy = allocatedRegion2.read(idx, ownership) allocatedRegion2 = allocatedRegion2 .copyRange(allocatedRegion1, adapter, trueExpr) - val readingAfterCopy = allocatedRegion2.read(idx) + val readingAfterCopy = allocatedRegion2.read(idx, ownership) val outsideOfCopy = mkBvSignedLessExpr(idx, mkBv(0)) or mkBvSignedLessExpr(mkBv(5), idx) val expr = (readingBeforeCopy neq readingAfterCopy) and outsideOfCopy @@ -458,15 +461,15 @@ class TranslationTest { fun testCachingOfTranslatedMemoryUpdates() = with(ctx) { val allocatedRegion = UAllocatedArrayId<_, _, USizeSort>(valueArrayDescr, sizeSort, 0) .emptyRegion() - .write(mkRegisterReading(0, sizeSort), mkBv(0), trueExpr) - .write(mkRegisterReading(1, sizeSort), mkBv(1), trueExpr) + .write(mkRegisterReading(0, sizeSort), mkBv(0), trueExpr, ownership) + .write(mkRegisterReading(1, sizeSort), mkBv(1), trueExpr, ownership) val allocatedRegionExtended = allocatedRegion - .write(mkRegisterReading(2, sizeSort), mkBv(2), trueExpr) - .write(mkRegisterReading(3, sizeSort), mkBv(3), trueExpr) + .write(mkRegisterReading(2, sizeSort), mkBv(2), trueExpr, ownership) + .write(mkRegisterReading(3, sizeSort), mkBv(3), trueExpr, ownership) - val reading = allocatedRegion.read(mkRegisterReading(4, sizeSort)) - val readingExtended = allocatedRegionExtended.read(mkRegisterReading(5, sizeSort)) + val reading = allocatedRegion.read(mkRegisterReading(4, sizeSort), ownership) + val readingExtended = allocatedRegionExtended.read(mkRegisterReading(5, sizeSort), ownership) translator.translate(reading) diff --git a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt index 676abc5f32..83df9804c0 100644 --- a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt @@ -79,8 +79,7 @@ class TypeSolverTest { } private val pc = UPathConstraints(ctx, ownership) - private val memory = UMemory(ctx, pc.typeConstraints) - + private val memory = UMemory(ctx, ownership, pc.typeConstraints) @Test fun `Test concrete ref -- open type inheritance`() { val ref = memory.allocConcrete(base1) @@ -346,18 +345,18 @@ class TypeSolverTest { val idx2 = 0.toBv() val field = mockk() - val heap = UMemory(ctx, mockk()) + val heap = UMemory(ctx, ownership, mockk()) heap.writeField(val1, field, bv32Sort, 1.toBv(), trueExpr) heap.writeField(val2, field, bv32Sort, 2.toBv(), trueExpr) val inputRegion = UInputArrayId<_, _, USizeSort>(mockk(), addressSort) .emptyRegion() - .write(arr1 to idx1, val1, trueExpr) - .write(arr2 to idx2, val2, trueExpr) + .write(arr1 to idx1, val1, trueExpr, ownership) + .write(arr2 to idx2, val2, trueExpr, ownership) - val firstReading = inputRegion.read(arr1 to idx1) - val secondReading = inputRegion.read(arr2 to idx2) + val firstReading = inputRegion.read(arr1 to idx1, ownership) + val secondReading = inputRegion.read(arr2 to idx2, ownership) pc += mkIsSubtypeExpr(arr1, base1) pc += mkIsSubtypeExpr(arr2, base1) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt index 253aeaf092..a91e2c6de9 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt @@ -10,6 +10,7 @@ import org.usvm.UContext import org.usvm.UExpr import org.usvm.USort import org.usvm.UTransformer +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.machine.interpreter.statics.JcStaticFieldLValue import org.usvm.machine.interpreter.statics.JcStaticFieldReading import org.usvm.machine.interpreter.statics.JcStaticFieldRegionId @@ -62,7 +63,7 @@ class JcStaticFieldModel( private val translatedFields: Map>, private val translator: UExprTranslator<*, *> ) : UReadOnlyMemoryRegion, Sort> { - override fun read(key: JcStaticFieldLValue): UExpr { + override fun read(key: JcStaticFieldLValue, ownership: MutabilityOwnership): UExpr { val translated = translatedFields[key.field] ?: translator.translate( key.sort.jctx.mkStaticFieldReading(key.memoryRegionId as JcStaticFieldRegionId, key.field, key.sort) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt index c40114a44e..aa565921ff 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt @@ -1,13 +1,14 @@ package org.usvm.machine.interpreter -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf +import org.usvm.collections.immutable.persistentHashMapOf import org.jacodb.api.jvm.cfg.JcLambdaExpr import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UConcreteHeapAddress import org.usvm.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.machine.JcContext import org.usvm.memory.UMemoryRegion import org.usvm.memory.UMemoryRegionId @@ -22,21 +23,22 @@ class JcLambdaCallSiteRegionId(private val ctx: JcContext) : UMemoryRegionId = persistentHashMapOf() + private val callSites: UPersistentHashMap = persistentHashMapOf() ) : UMemoryRegion { - fun writeCallSite(callSite: JcLambdaCallSite) = - JcLambdaCallSiteMemoryRegion(ctx, callSites.put(callSite.ref.address, callSite)) + fun writeCallSite(callSite: JcLambdaCallSite, ownership: MutabilityOwnership) = + JcLambdaCallSiteMemoryRegion(ctx, callSites.put(callSite.ref.address, callSite, ownership)) fun findCallSite(ref: UConcreteHeapRef): JcLambdaCallSite? = callSites[ref.address] - override fun read(key: Nothing): UExpr { + override fun read(key: Nothing, ownership: MutabilityOwnership): UExpr { error("Unsupported operation for call site region") } override fun write( key: Nothing, value: UExpr, - guard: UBoolExpr + guard: UBoolExpr, + ownership: MutabilityOwnership ): UMemoryRegion { error("Unsupported operation for call site region") } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt index 3b2f49f8e7..577f26a165 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt @@ -424,7 +424,7 @@ class JcExprResolver( private fun UWritableMemory.writeCallSite(callSite: JcLambdaCallSite) { val callSiteRegion = getRegion(ctx.lambdaCallSiteRegionId) as JcLambdaCallSiteMemoryRegion - val updatedRegion = callSiteRegion.writeCallSite(callSite) + val updatedRegion = callSiteRegion.writeCallSite(callSite, ownership) setRegion(ctx.lambdaCallSiteRegionId, updatedRegion) } @@ -637,7 +637,7 @@ class JcExprResolver( val enumValuesFieldLengthLValue = UArrayLengthLValue(enumValuesRef, enumValuesArrayDescriptor, sizeSort) val enumValuesFieldLengthBeforeClinit = - enumValuesFieldLengthLValue.memoryRegionId.emptyRegion().read(enumValuesFieldLengthLValue) + enumValuesFieldLengthLValue.memoryRegionId.emptyRegion().read(enumValuesFieldLengthLValue, ownership) val enumValuesFieldLengthAfterClinit = memory.read(enumValuesFieldLengthLValue) // Ensure that $VALUES in a model has the same length as the $VALUES in the memory @@ -652,13 +652,13 @@ class JcExprResolver( UArrayIndexLValue(addressSort, enumValuesRef, mkSizeExpr(ordinal), cp.objectType) val enumConstantRefAfterClinit = memory.read(enumConstantLValue) val enumConstantRefBeforeClinit = - enumConstantLValue.memoryRegionId.emptyRegion().read(enumConstantLValue) + enumConstantLValue.memoryRegionId.emptyRegion().read(enumConstantLValue, ownership) val ordinalFieldLValue = UFieldLValue(sizeSort, enumConstantRefAfterClinit, enumOrdinalField) val ordinalFieldValueAfterClinit = memory.read(ordinalFieldLValue) val ordinalEmptyRegion = ordinalFieldLValue.memoryRegionId.emptyRegion() - val ordinalFieldValueBeforeClinit = ordinalEmptyRegion.read(ordinalFieldLValue) + val ordinalFieldValueBeforeClinit = ordinalEmptyRegion.read(ordinalFieldLValue, ownership) // Ensure that the ordinal of each enum constant equals to the real ordinal value scope.assert(mkEq(ordinalFieldValueAfterClinit, ordinalFieldValueBeforeClinit)) @@ -1008,7 +1008,7 @@ class JcExprResolver( if (sort === voidSort) return@forEach val memoryRegion = memory.getRegion(JcStaticFieldRegionId(sort)) as JcStaticFieldsMemoryRegion<*> - memoryRegion.mutatePrimitiveStaticFieldValuesToSymbolic(staticInitializer.enclosingClass) + memoryRegion.mutatePrimitiveStaticFieldValuesToSymbolic(staticInitializer.enclosingClass, scope.ownership) } } } @@ -1154,4 +1154,4 @@ class JcSimpleValueResolver( scope.calcOnState { mkStringConstRef(value) } -} \ No newline at end of file +} diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt index 87e58f9244..8f8db30c97 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt @@ -1,8 +1,6 @@ package org.usvm.machine.interpreter.statics import kotlinx.collections.immutable.PersistentList -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import kotlinx.collections.immutable.persistentListOf import org.jacodb.api.jvm.JcClassOrInterface import org.jacodb.api.jvm.JcField @@ -16,6 +14,9 @@ import org.usvm.UBoolExpr import org.usvm.UBoolSort import org.usvm.UExpr import org.usvm.USort +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership +import org.usvm.collections.immutable.persistentHashMapOf import org.usvm.isTrue import org.usvm.machine.JcContext import org.usvm.machine.jctx @@ -46,13 +47,14 @@ data class JcStaticFieldRegionId( internal class JcStaticFieldsMemoryRegion( private val sort: Sort, - private var fieldValuesByClass: PersistentMap>> = persistentHashMapOf(), + // TODO multimap + private var fieldValuesByClass: UPersistentHashMap>> = persistentHashMapOf(), private var initialStatics: PersistentList = persistentListOf() ) : UMemoryRegion, Sort> { val mutableStaticFields: List get() = initialStatics - override fun read(key: JcStaticFieldLValue): UExpr { + override fun read(key: JcStaticFieldLValue, ownership: MutabilityOwnership): UExpr { val field = key.field return fieldValuesByClass[field.enclosingClass]?.get(field) ?: sort.jctx.mkStaticFieldReading(key.memoryRegionId as JcStaticFieldRegionId, field, sort) @@ -62,36 +64,32 @@ internal class JcStaticFieldsMemoryRegion( key: JcStaticFieldLValue, value: UExpr, guard: UBoolExpr, + ownership: MutabilityOwnership ): UMemoryRegion, Sort> { val field = key.field - val enclosingClass = field.enclosingClass - if (enclosingClass !in fieldValuesByClass) { - fieldValuesByClass = fieldValuesByClass.put(enclosingClass, persistentHashMapOf()) - } - - val newFieldValues = fieldValuesByClass - .getValue(enclosingClass) - .guardedWrite(key.field, value, guard) { key.sort.sampleUValue() } - val newFieldsByClass = fieldValuesByClass.put(enclosingClass, newFieldValues) + val classFields = fieldValuesByClass.getOrDefault(enclosingClass, persistentHashMapOf()) + + val newFieldValues = classFields.guardedWrite(key.field, value, guard, ownership) { key.sort.sampleUValue() } + val newFieldsByClass = fieldValuesByClass.put(enclosingClass, newFieldValues, ownership) return JcStaticFieldsMemoryRegion(sort, newFieldsByClass, initialStatics) } - fun mutatePrimitiveStaticFieldValuesToSymbolic(enclosingClass: JcClassOrInterface) { + fun mutatePrimitiveStaticFieldValuesToSymbolic(enclosingClass: JcClassOrInterface, ownership: MutabilityOwnership) { val staticFields = fieldValuesByClass[enclosingClass] ?: return val staticsToRemove = staticFields - .keys + .keys() .filter { fieldShouldBeSymbolic(it) } initialStatics = initialStatics.addAll(staticsToRemove) // Remove concrete fields from the region val updatedStaticFields = staticsToRemove.fold(staticFields) { acc, field -> - acc.remove(field) + acc.remove(field, ownership) } - fieldValuesByClass = fieldValuesByClass.put(enclosingClass, updatedStaticFields) + fieldValuesByClass = fieldValuesByClass.put(enclosingClass, updatedStaticFields, ownership) } companion object { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt index 39cbc40b4f..9bd688be4a 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt @@ -21,7 +21,7 @@ class JcState( override val entrypoint: JcMethod, callStack: UCallStack = UCallStack(), pathConstraints: UPathConstraints = UPathConstraints(ctx, ownership), - memory: UMemory = UMemory(ctx, pathConstraints.typeConstraints), + memory: UMemory = UMemory(ctx, ownership, pathConstraints.typeConstraints), models: List> = listOf(), pathNode: PathNode = PathNode.root(), forkPoints: PathNode> = PathNode.root(), @@ -38,15 +38,17 @@ class JcState( forkPoints, targets ) { - override fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints?): JcState { - val clonedConstraints = newConstraints ?: pathConstraints.clone(ownership) + override fun clone(newConstraints: UPathConstraints?): JcState { + this.changeOwnership(MutabilityOwnership()) + val cloneOwnership = MutabilityOwnership() + val clonedConstraints = newConstraints ?: pathConstraints.clone(cloneOwnership) return JcState( ctx, - ownership, + cloneOwnership, entrypoint, callStack.clone(), clonedConstraints, - memory.clone(clonedConstraints.typeConstraints), + memory.clone(clonedConstraints.typeConstraints, cloneOwnership), models, pathNode, forkPoints, @@ -60,7 +62,10 @@ class JcState( * * @return the merged state. TODO: Now it may reuse some of the internal components of the former states. */ - override fun mergeWith(other: JcState, by: Unit, ownership: MutabilityOwnership): JcState? { + override fun mergeWith(other: JcState, by: Unit): JcState? { + this.changeOwnership(MutabilityOwnership()) + other.changeOwnership(MutabilityOwnership()) + val newOwnership = MutabilityOwnership() require(entrypoint == other.entrypoint) { "Cannot merge states with different entrypoints" } // TODO: copy-paste @@ -69,11 +74,11 @@ class JcState( val mergeGuard = MutableMergeGuard(ctx) val mergedCallStack = callStack.mergeWith(other.callStack, Unit) ?: return null - val mergedPathConstraints = pathConstraints.mergeWith(other.pathConstraints, mergeGuard, ownership) + val mergedPathConstraints = pathConstraints.mergeWith(other.pathConstraints, mergeGuard, newOwnership) ?: return null val mergedMemory = - memory.clone(mergedPathConstraints.typeConstraints) - .mergeWith(other.memory, mergeGuard) + memory.clone(mergedPathConstraints.typeConstraints, newOwnership) + .mergeWith(other.memory, mergeGuard, newOwnership) ?: return null val mergedModels = models + other.models val methodResult = if (other.methodResult == JcMethodResult.NoCall && methodResult == JcMethodResult.NoCall) { @@ -86,7 +91,7 @@ class JcState( return JcState( ctx, - ownership, + newOwnership, entrypoint, mergedCallStack, mergedPathConstraints, diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt index d1dfd600eb..a42718d0c9 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt @@ -2,6 +2,7 @@ package org.usvm.machine import org.usvm.UMachine import org.usvm.UPathSelector +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.language.PyCallable import org.usvm.language.PyPinnedCallable import org.usvm.language.PyProgram @@ -60,10 +61,12 @@ class PyMachine( ) private fun getInitialState(target: PyUnpinnedCallable): PyState { - val pathConstraints = PyPathConstraints(ctx) + val initOwnership = MutabilityOwnership() + val pathConstraints = PyPathConstraints(ctx,initOwnership ) val memory = UMemory( ctx, - pathConstraints.typeConstraints + initOwnership, + pathConstraints.typeConstraints, ).apply { stack.push(target.numberOfArguments) } @@ -78,6 +81,7 @@ class PyMachine( return PyState( ctx, + initOwnership, target, symbols, pathConstraints, diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyPathConstraints.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyPathConstraints.kt index c7384dd257..c2a91fbee8 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyPathConstraints.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyPathConstraints.kt @@ -5,6 +5,7 @@ import kotlinx.collections.immutable.persistentHashSetOf import org.usvm.UBoolExpr import org.usvm.UBv32Sort import org.usvm.UContext +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.constraints.UEqualityConstraints import org.usvm.constraints.ULogicalConstraints import org.usvm.constraints.UNumericConstraints @@ -14,26 +15,28 @@ import org.usvm.machine.types.PythonType class PyPathConstraints( ctx: UContext<*>, + ownership: MutabilityOwnership, logicalConstraints: ULogicalConstraints = ULogicalConstraints.empty(), - equalityConstraints: UEqualityConstraints = UEqualityConstraints(ctx), + equalityConstraints: UEqualityConstraints = UEqualityConstraints(ctx, ownership), typeConstraints: UTypeConstraints = UTypeConstraints( ctx.typeSystem(), equalityConstraints ), - numericConstraints: UNumericConstraints = UNumericConstraints(ctx, sort = ctx.bv32Sort), + numericConstraints: UNumericConstraints = UNumericConstraints(ctx, sort = ctx.bv32Sort, ownership = ownership), var pythonSoftConstraints: PersistentSet = persistentHashSetOf(), ) : UPathConstraints( ctx, + ownership, logicalConstraints, equalityConstraints, typeConstraints, numericConstraints ) { - override fun clone(): PyPathConstraints { + override fun clone(ownership: MutabilityOwnership): PyPathConstraints { val clonedLogicalConstraints = logicalConstraints.clone() - val clonedEqualityConstraints = equalityConstraints.clone() + val clonedEqualityConstraints = equalityConstraints.clone(ownership) val clonedTypeConstraints = typeConstraints.clone(clonedEqualityConstraints) - val clonedNumericConstraints = numericConstraints.clone() + val clonedNumericConstraints = numericConstraints.clone(ownership) return PyPathConstraints( ctx = ctx, logicalConstraints = clonedLogicalConstraints, @@ -41,6 +44,7 @@ class PyPathConstraints( typeConstraints = clonedTypeConstraints, numericConstraints = clonedNumericConstraints, pythonSoftConstraints = pythonSoftConstraints, + ownership = ownership ) } } diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt index 1c4c3e3150..881f0d1439 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt @@ -10,6 +10,7 @@ import org.usvm.UCallStack import org.usvm.UMockSymbol import org.usvm.UPathSelector import org.usvm.UState +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.constraints.UPathConstraints import org.usvm.language.PyCallable import org.usvm.language.PyInstruction @@ -32,6 +33,7 @@ private val targets = UTargetsSet.empty() class PyState( ctx: PyContext, + ownership: MutabilityOwnership, private val pythonCallable: PyUnpinnedCallable, val inputSymbols: List, override val pathConstraints: PyPathConstraints, @@ -50,6 +52,7 @@ class PyState( var uniqueInstructions: PersistentSet = persistentSetOf(), ) : UState( ctx, + ownership, callStack, pathConstraints, memory, @@ -60,10 +63,13 @@ class PyState( ) { override fun clone(newConstraints: UPathConstraints?): PyState { require(newConstraints is PyPathConstraints?) - val newPathConstraints = newConstraints ?: pathConstraints.clone() - val newMemory = memory.clone(newPathConstraints.typeConstraints) + this.changeOwnership(ownership) + val cloneOwnership = MutabilityOwnership() + val newPathConstraints = newConstraints ?: pathConstraints.clone(cloneOwnership) + val newMemory = memory.clone(newPathConstraints.typeConstraints, cloneOwnership) return PyState( ctx, + cloneOwnership, pythonCallable, inputSymbols, newPathConstraints, diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayIndexRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayIndexRegion.kt index d1ef3676d8..fd413321c6 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayIndexRegion.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayIndexRegion.kt @@ -6,6 +6,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.machine.PyContext import org.usvm.machine.model.PyModel import org.usvm.machine.model.getConcreteType @@ -18,8 +19,8 @@ class WrappedArrayIndexRegion( private val ctx: PyContext, private val nullRef: UConcreteHeapRef, ) : UReadOnlyMemoryRegion, UAddressSort> { - override fun read(key: UArrayIndexLValue): UExpr { - val underlyingResult = region.read(key) + override fun read(key: UArrayIndexLValue, ownership: MutabilityOwnership): UExpr { + val underlyingResult = region.read(key, ownership) val array = key.ref as UConcreteHeapRef if (array.address > 0) { // allocated object diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayLengthRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayLengthRegion.kt index 11fdd51c16..92d5210d8e 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayLengthRegion.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayLengthRegion.kt @@ -3,6 +3,7 @@ package org.usvm.machine.model.regions import io.ksmt.sort.KIntSort import org.usvm.UExpr import org.usvm.collection.array.length.UArrayLengthLValue +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.isTrue import org.usvm.machine.PyContext import org.usvm.machine.types.ArrayType @@ -12,8 +13,8 @@ class WrappedArrayLengthRegion( private val ctx: PyContext, private val region: UReadOnlyMemoryRegion, KIntSort>, ) : UReadOnlyMemoryRegion, KIntSort> { - override fun read(key: UArrayLengthLValue): UExpr { - val underlyingResult = region.read(key) + override fun read(key: UArrayLengthLValue, ownership: MutabilityOwnership): UExpr { + val underlyingResult = region.read(key, ownership) if (ctx.mkArithLt(underlyingResult, ctx.mkIntNum(0)).isTrue) { return ctx.mkIntNum(0) } diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefMapRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefMapRegion.kt index fb4ed5b2ef..16ac0e336b 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefMapRegion.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefMapRegion.kt @@ -4,6 +4,7 @@ import org.usvm.UAddressSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.collection.map.ref.URefMapEntryLValue +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.machine.PyContext import org.usvm.machine.types.PythonType import org.usvm.memory.UReadOnlyMemoryRegion @@ -15,10 +16,10 @@ class WrappedRefMapRegion( private val keys: Set, private val underlyingModel: UModelBase, ) : UReadOnlyMemoryRegion, UAddressSort> { - override fun read(key: URefMapEntryLValue): UExpr { + override fun read(key: URefMapEntryLValue, ownership: MutabilityOwnership): UExpr { if (key.mapKey !in keys) { return underlyingModel.eval(ctx.nullRef) } - return region.read(key) + return region.read(key, ownership) } } diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefSetRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefSetRegion.kt index 7b5dbb7244..7b335fc0d9 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefSetRegion.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefSetRegion.kt @@ -4,6 +4,7 @@ import org.usvm.UBoolSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.collection.set.ref.URefSetEntryLValue +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.PyContext import org.usvm.memory.UReadOnlyMemoryRegion @@ -13,10 +14,10 @@ class WrappedRefSetRegion( private val region: UReadOnlyMemoryRegion, UBoolSort>, private val keys: Set, ) : UReadOnlyMemoryRegion, UBoolSort> { - override fun read(key: URefSetEntryLValue): UExpr { + override fun read(key: URefSetEntryLValue, ownership: MutabilityOwnership): UExpr { if (!isAllocatedConcreteHeapRef(key.setRef) && key.setElement !in keys) { return ctx.falseExpr } - return region.read(key) + return region.read(key, ownership) } } diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedSetRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedSetRegion.kt index aaa34c92df..b2cc479dea 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedSetRegion.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedSetRegion.kt @@ -5,6 +5,7 @@ import io.ksmt.sort.KIntSort import org.usvm.UBoolSort import org.usvm.UExpr import org.usvm.collection.set.primitive.USetEntryLValue +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.PyContext import org.usvm.memory.UReadOnlyMemoryRegion @@ -15,10 +16,10 @@ class WrappedSetRegion( private val region: UReadOnlyMemoryRegion, UBoolSort>, private val keys: Set>, ) : UReadOnlyMemoryRegion, UBoolSort> { - override fun read(key: USetEntryLValue): UExpr { + override fun read(key: USetEntryLValue, ownership: MutabilityOwnership): UExpr { if (!isAllocatedConcreteHeapRef(key.setRef) && key.setElement !in keys) { return ctx.falseExpr } - return region.read(key) + return region.read(key, ownership) } } diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt index 4904a4720e..7d923cc7cb 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt +++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt @@ -25,7 +25,7 @@ class SampleState( override val entrypoint: Method<*>, callStack: UCallStack, Stmt> = UCallStack(), pathConstraints: UPathConstraints = UPathConstraints(ctx, ownership), - memory: UMemory> = UMemory(ctx, pathConstraints.typeConstraints), + memory: UMemory> = UMemory(ctx, ownership, pathConstraints.typeConstraints), models: List> = listOf(), pathNode: PathNode = PathNode.root(), forkPoints: PathNode> = PathNode.root(), @@ -43,15 +43,17 @@ class SampleState( forkPoints, targets ) { - override fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints?): SampleState { - val clonedConstraints = newConstraints ?: pathConstraints.clone(ownership) + override fun clone(newConstraints: UPathConstraints?): SampleState { + this.changeOwnership(MutabilityOwnership()) + val cloneOwnership = MutabilityOwnership() + val clonedConstraints = newConstraints ?: pathConstraints.clone(cloneOwnership) return SampleState( ctx, - ownership, + cloneOwnership, entrypoint, callStack.clone(), clonedConstraints, - memory.clone(clonedConstraints.typeConstraints), + memory.clone(clonedConstraints.typeConstraints, cloneOwnership), models, pathNode, forkPoints, @@ -76,7 +78,7 @@ class SampleState( val mergedCallStack = callStack.mergeWith(other.callStack, Unit) ?: return null val mergedPathConstraints = pathConstraints.mergeWith(other.pathConstraints, mergeGuard, ownership) ?: return null - val mergedMemory = memory.clone(mergedPathConstraints.typeConstraints).mergeWith(other.memory, mergeGuard) + val mergedMemory = memory.clone(mergedPathConstraints.typeConstraints, ownership).mergeWith(other.memory, mergeGuard, ownership) ?: return null val mergedModels = models + other.models val mergedReturnRegister = if (returnRegister == null && other.returnRegister == null) { diff --git a/usvm-util/src/main/kotlin/org/usvm/algorithms/PersistentMultiMapBuilder.kt b/usvm-util/src/main/kotlin/org/usvm/algorithms/PersistentMultiMapBuilder.kt index efe5545e5a..a216983104 100644 --- a/usvm-util/src/main/kotlin/org/usvm/algorithms/PersistentMultiMapBuilder.kt +++ b/usvm-util/src/main/kotlin/org/usvm/algorithms/PersistentMultiMapBuilder.kt @@ -21,8 +21,8 @@ fun UPersistentMultiMap.addToSet( value: V, ownership: MutabilityOwnership, ): UPersistentMultiMap { - val current = this[key] - val updated = current?.add(value, ownership) ?: persistentHashSetOf().add(value, ownership) + val current = getOrDefault(key, persistentHashSetOf()) + val updated = current.add(value, ownership) return this.put(key, updated, ownership) } @@ -31,8 +31,8 @@ fun UPersistentMultiMap.addAll( values: Set, ownership: MutabilityOwnership, ) : UPersistentMultiMap { - val current = this[key] - val updated = current?.addAll(values, ownership) ?: persistentHashSetOf().addAll(values, ownership) + val current = getOrDefault(key, persistentHashSetOf()) + val updated = current.addAll(values, ownership) return this.put(key, updated, ownership) } diff --git a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/extensions.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/extensions.kt index 752d84614e..6a070ce91d 100644 --- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/extensions.kt +++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/extensions.kt @@ -61,6 +61,8 @@ fun persistentHashMapOf(): UPersistentHashMap = UPersistentHashMap. fun persistentHashMapOf(map : Map, owner : MutabilityOwnership): UPersistentHashMap = persistentHashMapOf().putAll(map, owner) +fun persistentHashMapOf(owner : MutabilityOwnership, vararg pairs : Pair ): UPersistentHashMap = + pairs.fold(persistentHashMapOf()) { acc, (k, v) -> acc.put(k, v, owner) } /** * Returns a persistent map containing all entries from this map. diff --git a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieIterator.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieIterator.kt index 321d0d841f..d0205d55f3 100644 --- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieIterator.kt +++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieIterator.kt @@ -173,3 +173,6 @@ internal abstract class UPersistentHashMapBaseIterator( internal class UPersistentHashMapEntriesIterator(node: TrieNode) : UPersistentHashMapBaseIterator>(node, Array(TRIE_MAX_HEIGHT + 1) { TrieNodeEntriesIterator() }) + +internal class UPersistentHashMapKeysIterator(node: TrieNode) + : UPersistentHashMapBaseIterator(node, Array(TRIE_MAX_HEIGHT + 1) { TrieNodeKeysIterator() }) diff --git a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt index b9c3034538..9e6200e202 100644 --- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt +++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt @@ -716,15 +716,24 @@ class TrieNode( nodePositions -= mask } } + + fun keys() = UPersistentHashMapKeysIterator(this).asSequence().toSet() fun isEmpty() = singleOrNull() == null fun isNotEmpty() = singleOrNull() != null - + fun containsKey(key: K) : Boolean = containsKey(key.hashCode(), key, 0) operator fun contains(key : K) = containsKey(key) operator fun get(key : K) = get(key.hashCode(), key, 0) + + fun getOrDefault(key : K, defaultValue : V) = get(key) ?: defaultValue + fun getOrPut(key : K, value : V, owner: MutabilityOwnership) : Pair, V> { + val current = get(key) ?: return put(key, value, owner) to value + return this to current + } + fun put(key : K, value : V, owner: MutabilityOwnership) : TrieNode = mutablePut(key.hashCode(), key, value, 0, owner) diff --git a/usvm-util/src/main/kotlin/org/usvm/regions/RegionTree.kt b/usvm-util/src/main/kotlin/org/usvm/regions/RegionTree.kt index be61e46e36..f41dc17cda 100644 --- a/usvm-util/src/main/kotlin/org/usvm/regions/RegionTree.kt +++ b/usvm-util/src/main/kotlin/org/usvm/regions/RegionTree.kt @@ -58,7 +58,7 @@ class RegionTree( // 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 outside = entries.remove(region) val disjointRegionTree = RegionTree(outside) return RecursiveSplitResult(completelyCoveredRegionTree, disjointRegionTree)