From 947418fc44a2bb062b72209ec596248500ed4377 Mon Sep 17 00:00:00 2001 From: Roman Pozharskiy Date: Wed, 24 Jul 2024 16:13:02 +0300 Subject: [PATCH] fix ownership flow; add ownership in type constraints --- .../src/main/kotlin/org/usvm/StateForker.kt | 6 +- .../src/main/kotlin/org/usvm/StepScope.kt | 2 +- .../usvm/constraints/EqualityConstraints.kt | 6 +- .../org/usvm/constraints/PathConstraints.kt | 45 ++++++---- .../org/usvm/constraints/TypeConstraints.kt | 83 +++++++++++-------- .../usvm/constraints/UNumericConstraints.kt | 6 +- .../kotlin/org/usvm/memory/HeapMemCpyTest.kt | 2 +- .../kotlin/org/usvm/memory/HeapMemsetTest.kt | 2 +- .../org/usvm/memory/HeapRefSplittingTest.kt | 2 +- .../kotlin/org/usvm/memory/SetEntriesTest.kt | 2 +- .../kotlin/org/usvm/machine/state/JcState.kt | 17 ++-- .../implementations/immutableMap/TrieNode.kt | 19 +++-- 12 files changed, 109 insertions(+), 83 deletions(-) diff --git a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt index c0112a0b36..068e2dbcb2 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt @@ -145,9 +145,7 @@ object WithSolverStateForker : StateForker { newConstraintToForkedState: UBoolExpr, stateToCheck: StateToCheck, ): T? { - val thisOwnership = MutabilityOwnership() - val cloneOwnership = MutabilityOwnership() - val constraintsToCheck = state.pathConstraints.clone(thisOwnership, cloneOwnership) + val constraintsToCheck = state.pathConstraints.clone() constraintsToCheck += if (stateToCheck) { newConstraintToForkedState @@ -195,7 +193,7 @@ object NoSolverStateForker : StateForker { ): ForkResult { val (trueModels, falseModels, _) = splitModelsByCondition(state.models, condition) val notCondition = state.ctx.mkNot(condition) - val clonedPathConstraints = state.pathConstraints.clone(MutabilityOwnership(), MutabilityOwnership()) + val clonedPathConstraints = state.pathConstraints.clone() clonedPathConstraints += condition val (posState, negState) = if (clonedPathConstraints.isFalse) { diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt index 780635c3d3..c590a27532 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt @@ -43,7 +43,7 @@ class StepScope, Type, Statement, val isDead: Boolean get() = stepScopeState === DEAD - val ownership = originalState.ownership + val ownership get() = originalState.ownership /** * Executes [block] on a state. 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 af1e175e65..4901aae883 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt @@ -387,11 +387,11 @@ class UEqualityConstraints private constructor( * Creates a mutable copy of this structure. * Note that current subscribers get unsubscribed! */ - fun clone(thisOwnership: MutabilityOwnership, clonerOwnership: MutabilityOwnership): UEqualityConstraints { + fun clone(thisOwnership: MutabilityOwnership, cloneOwnership: MutabilityOwnership): UEqualityConstraints { this.ownership = thisOwnership if (isContradicting) { val result = UEqualityConstraints( - ctx, clonerOwnership, DisjointSets(), + ctx, cloneOwnership, DisjointSets(), persistentHashSetOf(), persistentHashMapOf(), persistentHashMapOf() @@ -402,7 +402,7 @@ class UEqualityConstraints private constructor( return UEqualityConstraints( ctx, - clonerOwnership, + cloneOwnership, equalReferences.clone(), distinctReferences, referenceDisequalities, 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 c881fff48f..b115682f9b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt @@ -24,7 +24,7 @@ import org.usvm.uctx */ open class UPathConstraints( protected val ctx: UContext<*>, - ownership: MutabilityOwnership, + private var ownership: MutabilityOwnership, protected val logicalConstraints: ULogicalConstraints = ULogicalConstraints.empty(), /** * Specially represented equalities and disequalities between objects, used in various part of constraints management. @@ -34,6 +34,7 @@ open class UPathConstraints( * Constraints solved by type solver. */ val typeConstraints: UTypeConstraints = UTypeConstraints( + ownership, ctx.typeSystem(), equalityConstraints ), @@ -48,8 +49,15 @@ open class UPathConstraints( equalityConstraints.setTypesCheck(typeConstraints::canStaticRefBeEqualToSymbolic) } - var ownership: MutabilityOwnership = ownership - protected set + /** + * Recursively changes ownership for all nested data structures that use persistent maps. + */ + fun setOwnership(ownership: MutabilityOwnership) { + this.ownership = ownership + numericConstraints.ownership = ownership + equalityConstraints.ownership = ownership + typeConstraints.ownership = ownership + } /** * Constraints solved by SMT solver. @@ -61,9 +69,9 @@ open class UPathConstraints( val isFalse: Boolean get() = equalityConstraints.isContradicting || - typeConstraints.isContradicting || - numericConstraints.isContradicting || - logicalConstraints.isContradicting + typeConstraints.isContradicting || + numericConstraints.isContradicting || + logicalConstraints.isContradicting // TODO: refactor fun constraints(translator: UExprTranslator): Sequence { @@ -71,9 +79,9 @@ open class UPathConstraints( return sequenceOf(ctx.falseExpr) } return logicalConstraints.asSequence().map(translator::translate) + - equalityConstraints.constraints(translator) + - numericConstraints.constraints(translator) + - typeConstraints.constraints(translator) + equalityConstraints.constraints(translator) + + numericConstraints.constraints(translator) + + typeConstraints.constraints(translator) } @Suppress("UNCHECKED_CAST") @@ -119,21 +127,21 @@ open class UPathConstraints( val notConstraint = constraint.arg when { notConstraint is UEqExpr<*> && - isSymbolicHeapRef(notConstraint.lhs) && isSymbolicHeapRef(notConstraint.rhs) -> + isSymbolicHeapRef(notConstraint.lhs) && isSymbolicHeapRef(notConstraint.rhs) -> equalityConstraints.makeNonEqual( notConstraint.lhs as USymbolicHeapRef, notConstraint.rhs as USymbolicHeapRef ) notConstraint is UEqExpr<*> && - isSymbolicHeapRef(notConstraint.lhs) && isStaticHeapRef(notConstraint.rhs) -> + isSymbolicHeapRef(notConstraint.lhs) && isStaticHeapRef(notConstraint.rhs) -> equalityConstraints.makeNonEqual( notConstraint.lhs as USymbolicHeapRef, notConstraint.rhs as UConcreteHeapRef ) notConstraint is UEqExpr<*> && - isStaticHeapRef(notConstraint.lhs) && isSymbolicHeapRef(notConstraint.rhs) -> + isStaticHeapRef(notConstraint.lhs) && isSymbolicHeapRef(notConstraint.rhs) -> equalityConstraints.makeNonEqual( notConstraint.rhs as USymbolicHeapRef, notConstraint.lhs as UConcreteHeapRef @@ -166,15 +174,18 @@ open class UPathConstraints( } } - open fun clone(thisOwnership: MutabilityOwnership, cloneOwnership: MutabilityOwnership): UPathConstraints { + open fun clone( + thisOwnership: MutabilityOwnership = ownership, + cloneOwnership: MutabilityOwnership = MutabilityOwnership(), // clone ownership must be brand new because of plus assign operations + ): UPathConstraints { val clonedLogicalConstraints = logicalConstraints.clone() val clonedEqualityConstraints = equalityConstraints.clone(thisOwnership, cloneOwnership) - val clonedTypeConstraints = typeConstraints.clone(clonedEqualityConstraints) + val clonedTypeConstraints = typeConstraints.clone(clonedEqualityConstraints, thisOwnership, cloneOwnership) val clonedNumericConstraints = numericConstraints.clone(thisOwnership, cloneOwnership) this.ownership = thisOwnership return UPathConstraints( ctx = ctx, - cloneOwnership, + ownership = cloneOwnership, logicalConstraints = clonedLogicalConstraints, equalityConstraints = clonedEqualityConstraints, typeConstraints = clonedTypeConstraints, @@ -214,8 +225,8 @@ open class UPathConstraints( equalityConstraints.mergeWith(other.equalityConstraints, by, thisOwnership, otherOwnership, mergedOwnership) ?: return null val mergedTypeConstraints = typeConstraints - .clone(mergedEqualityConstraints) - .mergeWith(other.typeConstraints, by) ?: return null + .clone(mergedEqualityConstraints, thisOwnership, otherOwnership) + .mergeWith(other.typeConstraints, by, thisOwnership, otherOwnership, mergedOwnership) ?: return null val mergedNumericConstraints = numericConstraints.mergeWith(other.numericConstraints, by, thisOwnership, otherOwnership, mergedOwnership) diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt index 0cf8921575..35efaa2227 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt @@ -1,19 +1,20 @@ package org.usvm.constraints -import kotlinx.collections.immutable.PersistentMap -import kotlinx.collections.immutable.persistentHashMapOf import org.usvm.UBoolExpr import org.usvm.UConcreteHeapAddress import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UHeapRef -import org.usvm.UNullRef import org.usvm.USymbolicHeapRef +import org.usvm.UNullRef import org.usvm.isStatic import org.usvm.isStaticHeapRef +import org.usvm.collections.immutable.persistentHashMapOf +import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.mapWithStaticAsConcrete import org.usvm.merging.MutableMergeGuard -import org.usvm.merging.UMergeable +import org.usvm.merging.UOwnedMergeable import org.usvm.solver.UExprTranslator import org.usvm.types.USingleTypeStream import org.usvm.types.UTypeRegion @@ -21,6 +22,7 @@ import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem import org.usvm.uctx + interface UTypeEvaluator { /** @@ -51,20 +53,23 @@ interface UTypeEvaluator { * precisely, thus we can evaluate the subtyping constraints for them concretely (modulo generic type variables). */ class UTypeConstraints( + internal var ownership: MutabilityOwnership, private val typeSystem: UTypeSystem, private val equalityConstraints: UEqualityConstraints, - private var concreteRefToType: PersistentMap = persistentHashMapOf(), - private var symbolicRefToTypeRegion: PersistentMap> = persistentHashMapOf(), -) : UTypeEvaluator, UMergeable, MutableMergeGuard> { + private var concreteRefToType: UPersistentHashMap = persistentHashMapOf(), + private var symbolicRefToTypeRegion: UPersistentHashMap> = persistentHashMapOf(), +) : UTypeEvaluator, UOwnedMergeable, MutableMergeGuard> { private val ctx: UContext<*> get() = equalityConstraints.ctx init { equalityConstraints.subscribeEquality(::intersectRegions) } + @Suppress("UNCHECKED_CAST") val inputRefToTypeRegion: Map> get(): Map> { - val inputTypeRegions: MutableMap> = symbolicRefToTypeRegion.toMutableMap() + val inputTypeRegions: MutableMap> = + symbolicRefToTypeRegion.toMutableMap() as MutableMap> // Add all static refs for ((address, type) in concreteRefToType) { @@ -99,7 +104,7 @@ class UTypeConstraints( * Binds concrete heap address [ref] to its [type]. */ fun allocate(ref: UConcreteHeapAddress, type: Type) { - concreteRefToType = concreteRefToType.put(ref, type) + concreteRefToType = concreteRefToType.put(ref, type, ownership) equalityConstraints.updateDisequality(ctx.mkConcreteHeapRef(ref)) } @@ -146,7 +151,7 @@ class UTypeConstraints( } ?: topTypeRegion } - return symbolicRefToTypeRegion[representative] ?: topTypeRegion + return symbolicRefToTypeRegion.getOrDefault(representative as USymbolicHeapRef, topTypeRegion) } @@ -157,7 +162,7 @@ class UTypeConstraints( return } - symbolicRefToTypeRegion = symbolicRefToTypeRegion.put(representative as USymbolicHeapRef, value) + symbolicRefToTypeRegion = symbolicRefToTypeRegion.put(representative as USymbolicHeapRef, value, ownership) } /** @@ -173,7 +178,7 @@ class UTypeConstraints( is UNullRef -> return is UConcreteHeapRef -> { - val concreteType = concreteRefToType.getValue(ref.address) + val concreteType = concreteRefToType[ref.address]!! if (!typeSystem.isSupertype(supertype, concreteType)) { contradiction() } @@ -200,7 +205,7 @@ class UTypeConstraints( is UNullRef -> contradiction() // the [ref] can't be equal to null is UConcreteHeapRef -> { - val concreteType = concreteRefToType.getValue(ref.address) + val concreteType = concreteRefToType[ref.address]!! if (typeSystem.isSupertype(supertype, concreteType)) { contradiction() } @@ -227,7 +232,7 @@ class UTypeConstraints( is UNullRef -> contradiction() is UConcreteHeapRef -> { - val concreteType = concreteRefToType.getValue(ref.address) + val concreteType = concreteRefToType[ref.address]!! if (!typeSystem.isSupertype(concreteType, subtype)) { contradiction() } @@ -255,7 +260,7 @@ class UTypeConstraints( is UNullRef -> return is UConcreteHeapRef -> { - val concreteType = concreteRefToType.getValue(ref.address) + val concreteType = concreteRefToType[ref.address]!! if (typeSystem.isSupertype(concreteType, subtype)) { contradiction() } @@ -303,8 +308,8 @@ class UTypeConstraints( to is UConcreteHeapRef && from is UConcreteHeapRef -> { // For both concrete refs we need to check types are the same - val toType = concreteRefToType.getValue(to.address) - val fromType = concreteRefToType.getValue(from.address) + val toType = concreteRefToType[to.address] + val fromType = concreteRefToType[from.address] if (toType != fromType) { contradiction() @@ -313,7 +318,7 @@ class UTypeConstraints( to is UConcreteHeapRef -> { // Here we have a pair of symbolic-concrete refs - val concreteToType = concreteRefToType.getValue(to.address) + val concreteToType = concreteRefToType[to.address]!! val symbolicFromType = getTypeRegion(from as USymbolicHeapRef, useRepresentative = false) if (symbolicFromType.addSupertype(concreteToType).isEmpty) { @@ -323,7 +328,7 @@ class UTypeConstraints( from is UConcreteHeapRef -> { // Here to is symbolic and from is concrete - val concreteType = concreteRefToType.getValue(from.address) + val concreteType = concreteRefToType[from.address]!! val symbolicType = getTypeRegion(to as USymbolicHeapRef) // We need to set only the concrete type instead of all these symbolic types - make it using both subtype/supertype val regionFromConcreteType = symbolicType.addSubtype(concreteType).addSupertype(concreteType) @@ -350,7 +355,7 @@ class UTypeConstraints( contradiction() return } - for ((key, value) in symbolicRefToTypeRegion.entries) { + for ((key, value) in symbolicRefToTypeRegion) { // TODO: cache intersections? if (key != ref && value.intersect(newRegion).isEmpty) { // If we have two inputs of incomparable reference types, then they are non equal @@ -372,7 +377,7 @@ class UTypeConstraints( if (newRegion.isEmpty) { equalityConstraints.makeEqual(ref, ref.uctx.nullRef) } - for ((key, value) in symbolicRefToTypeRegion.entries) { + for ((key, value) in symbolicRefToTypeRegion) { // TODO: cache intersections? if (key != ref && value.intersect(newRegion).isEmpty) { // If we have two inputs of incomparable reference types, then they are non equal or both null @@ -388,7 +393,7 @@ class UTypeConstraints( override fun evalIsSubtype(ref: UHeapRef, supertype: Type): UBoolExpr = ref.mapWithStaticAsConcrete( concreteMapper = { concreteRef -> - val concreteType = concreteRefToType.getValue(concreteRef.address) + val concreteType = concreteRefToType[concreteRef.address]!! if (typeSystem.isSupertype(supertype, concreteType)) { concreteRef.ctx.trueExpr } else { @@ -414,7 +419,7 @@ class UTypeConstraints( override fun evalIsSupertype(ref: UHeapRef, subtype: Type): UBoolExpr = ref.mapWithStaticAsConcrete( concreteMapper = { concreteRef -> - val concreteType = concreteRefToType.getValue(concreteRef.address) + val concreteType = concreteRefToType[concreteRef.address]!! if (typeSystem.isSupertype(concreteType, subtype)) { concreteRef.ctx.trueExpr } else { @@ -440,13 +445,17 @@ class UTypeConstraints( /** * Creates a mutable copy of these constraints connected to new instance of [equalityConstraints]. */ - fun clone(equalityConstraints: UEqualityConstraints) = - UTypeConstraints( - typeSystem, - equalityConstraints, - concreteRefToType, - symbolicRefToTypeRegion - ) + fun clone( + equalityConstraints: UEqualityConstraints, + thisOwnership: MutabilityOwnership, + cloneOwnership: MutabilityOwnership + ) = UTypeConstraints( + cloneOwnership, + typeSystem, + equalityConstraints, + concreteRefToType, + symbolicRefToTypeRegion + ).also { this.ownership = thisOwnership } /** * Check if this [UTypeConstraints] can be merged with [other] type constraints. @@ -456,13 +465,21 @@ class UTypeConstraints( * * @return the merged type constraints. */ - override fun mergeWith(other: UTypeConstraints, by: MutableMergeGuard): UTypeConstraints? { + override fun mergeWith( + other: UTypeConstraints, + by: MutableMergeGuard, + thisOwnership: MutabilityOwnership, + otherOwnership: MutabilityOwnership, + mergedOwnership: MutabilityOwnership + ): UTypeConstraints? { // TODO: should we check equality constraints? if (symbolicRefToTypeRegion != other.symbolicRefToTypeRegion) { return null } - val mergedConcreteRefs = concreteRefToType.builder().apply { putAll(other.concreteRefToType) }.build() - return UTypeConstraints(typeSystem, equalityConstraints, mergedConcreteRefs, symbolicRefToTypeRegion) + val mergedConcreteRefs = concreteRefToType.putAll(other.concreteRefToType, mergedOwnership) + this.ownership = thisOwnership + other.ownership = otherOwnership + return UTypeConstraints(mergedOwnership, typeSystem, equalityConstraints, mergedConcreteRefs, symbolicRefToTypeRegion) } 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 d8b418e23f..c10b9a6039 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt @@ -63,7 +63,7 @@ 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> { @@ -1965,8 +1965,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] 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 1f932ec13e..cbfd870413 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt @@ -29,7 +29,7 @@ class HeapMemCpyTest { ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } val eqConstraints = UEqualityConstraints(ctx, ownership) - val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints) + val typeConstraints = UTypeConstraints(ownership, components.mkTypeSystem(ctx), eqConstraints) 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 68dbe2c17f..2ae6dfff8a 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt @@ -39,7 +39,7 @@ class HeapMemsetTest { ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } val eqConstraints = UEqualityConstraints(ctx, ownership) - val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints) + val typeConstraints = UTypeConstraints(ownership, components.mkTypeSystem(ctx), eqConstraints) heap = UMemory(ctx, ownership, typeConstraints) arrayType = mockk() arrayValueSort = ctx.addressSort 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 5a9d5f85cc..9488981e04 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt @@ -51,7 +51,7 @@ class HeapRefSplittingTest { ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } val eqConstraints = UEqualityConstraints(ctx, ownership) - val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints) + val typeConstraints = UTypeConstraints(ownership, components.mkTypeSystem(ctx), eqConstraints) heap = UMemory(ctx, ownership, typeConstraints) valueFieldDescr = mockk() to ctx.bv32Sort 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 bc8aa31e81..6f8bb729d6 100644 --- a/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt @@ -41,7 +41,7 @@ class SetEntriesTest { ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } val eqConstraints = UEqualityConstraints(ctx, ownership) - val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints) + val typeConstraints = UTypeConstraints(ownership, components.mkTypeSystem(ctx), eqConstraints) heap = UMemory(ctx, ownership, typeConstraints) setType = mockk() } 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 3bc1e7afa3..3b1b38361c 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 @@ -41,14 +41,11 @@ class JcState( override fun clone(newConstraints: UPathConstraints?): JcState { var newThisOwnership = MutabilityOwnership() var cloneOwnership = MutabilityOwnership() - val clonedConstraints = newConstraints.also { - if (it != null) { - // if newConstraints is not null it was cloned with new ownership - newThisOwnership = this.pathConstraints.ownership - cloneOwnership = it.ownership - } - } - ?: pathConstraints.clone(newThisOwnership, cloneOwnership) + val clonedConstraints = newConstraints?.also { + this.pathConstraints.setOwnership(newThisOwnership) + it.setOwnership(cloneOwnership) + } ?: pathConstraints.clone(newThisOwnership, cloneOwnership) + this.ownership = newThisOwnership return JcState( ctx, cloneOwnership, @@ -83,8 +80,8 @@ class JcState( val mergeGuard = MutableMergeGuard(ctx) val mergedCallStack = callStack.mergeWith(other.callStack, Unit) ?: return null val mergedPathConstraints = pathConstraints.mergeWith( - other.pathConstraints, mergeGuard, newThisOwnership, newOtherOwnership, mergedOwnership - ) ?: return null + other.pathConstraints, mergeGuard, newThisOwnership, newOtherOwnership, mergedOwnership + ) ?: return null val mergedMemory = memory.clone(mergedPathConstraints.typeConstraints, newThisOwnership, newOtherOwnership) .mergeWith(other.memory, mergeGuard, newThisOwnership, newOtherOwnership, mergedOwnership) 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 803d9c7c3b..2a04b3a949 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 @@ -77,7 +77,7 @@ class TrieNode( // positionMask — an int in form 2^n, i.e. having the single bit set, whose ordinal is a logical position in buffer - /** Returns true if the data bit map has the bit specified by [positionMask] set, indicating there's a data entry + /** Returns true if the data bit map has the bit specified by [positionMask] set, indicating there's a data entry * in the buffer at that position. */ internal fun hasEntryAt(positionMask: Int): Boolean { return dataMap and positionMask != 0 @@ -192,7 +192,7 @@ class TrieNode( val storedKeyHash = storedKey.hashCode() val storedValue = valueAtKeyIndex(keyIndex) val newNode = makeNode(storedKeyHash, storedKey, storedValue, - newKeyHash, newKey, newValue, shift + LOG_MAX_BRANCHING_FACTOR, owner) + newKeyHash, newKey, newValue, shift + LOG_MAX_BRANCHING_FACTOR, owner) val nodeIndex = nodeIndex(positionMask) + 1 // place where to insert new node in the current buffer @@ -346,7 +346,7 @@ class TrieNode( tempBuffer[i] = otherNode.buffer[j] tempBuffer[i + 1] = otherNode.buffer[j + 1] i += ENTRY_SIZE - } + } } return when (val newSize = i) { @@ -706,9 +706,9 @@ class TrieNode( } private fun accept( - visitor: (node: TrieNode, shift: Int, hash: Int, dataMap: Int, nodeMap: Int) -> Unit, - hash: Int, - shift: Int + visitor: (node: TrieNode, shift: Int, hash: Int, dataMap: Int, nodeMap: Int) -> Unit, + hash: Int, + shift: Int ) { visitor(this, shift, hash, dataMap, nodeMap) @@ -738,7 +738,7 @@ class TrieNode( 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> { + 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 } @@ -756,7 +756,7 @@ class TrieNode( fun removeAll(keys: Iterable, owner: MutabilityOwnership): TrieNode = keys.fold(this) {node, k -> node.remove(k, owner)} - + fun removeAndGetValue(key: K, owner: MutabilityOwnership): Pair, V?> { val (node, value) = mutableRemoveAndGetValue(key.hashCode(), key, 0, owner) @Suppress("UNCHECKED_CAST") @@ -773,6 +773,9 @@ class TrieNode( return result } + fun toMutableMap() : MutableMap = mutableMapOf().also { + this.forEach {entry -> it[entry.key] = entry.value } } + @Suppress("UNCHECKED_CAST") fun clear() = EMPTY as TrieNode