diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt index ecb44bf96..574b91908 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Composition.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Composition.kt @@ -15,6 +15,7 @@ import org.usvm.collection.set.primitive.UInputSetReading import org.usvm.collection.set.ref.UAllocatedRefSetWithInputElementsReading import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemory import org.usvm.memory.USymbolicCollectionId import org.usvm.regions.Region @@ -22,7 +23,8 @@ import org.usvm.regions.Region @Suppress("MemberVisibilityCanBePrivate") open class UComposer( ctx: UContext, - val memory: UReadOnlyMemory + val memory: UReadOnlyMemory, + val ownership: MutabilityOwnership ) : UExprTransformer(ctx) { open fun compose(expr: UExpr): UExpr = apply(expr) diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt index 61f40773a..47d688b98 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Context.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt @@ -62,9 +62,9 @@ open class UContext( private val solver by lazy { components.mkSolver(this) } private val typeSystem by lazy { components.mkTypeSystem(this) } private val softConstraintsProvider by lazy { components.mkSoftConstraintsProvider(this) } - private val composerBuilder: (UReadOnlyMemory<*>) -> UComposer<*, USizeSort> by lazy { + private val composerBuilder: (UReadOnlyMemory<*>, MutabilityOwnership) -> UComposer<*, USizeSort> by lazy { @Suppress("UNCHECKED_CAST") - components.mkComposer(this) as (UReadOnlyMemory<*>) -> UComposer<*, USizeSort> + components.mkComposer(this) as (UReadOnlyMemory<*>, MutabilityOwnership) -> UComposer<*, USizeSort> } val defaultOwnership = MutabilityOwnership() @@ -88,7 +88,8 @@ open class UContext( fun softConstraintsProvider(): USoftConstraintsProvider = softConstraintsProvider.cast() - fun composer(memory: UReadOnlyMemory): UComposer = composerBuilder(memory).cast() + fun composer(memory: UReadOnlyMemory, ownership: MutabilityOwnership): UComposer = + composerBuilder(memory, ownership).cast() val addressSort: UAddressSort = mkUninterpretedSort("Address") val nullRef: UNullRef = UNullRef(this) diff --git a/usvm-core/src/main/kotlin/org/usvm/UComponents.kt b/usvm-core/src/main/kotlin/org/usvm/UComponents.kt index 8dc74a92b..9b9bbf9d9 100644 --- a/usvm-core/src/main/kotlin/org/usvm/UComponents.kt +++ b/usvm-core/src/main/kotlin/org/usvm/UComponents.kt @@ -1,5 +1,6 @@ package org.usvm +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemory import org.usvm.model.ULazyModelDecoder import org.usvm.model.UModelDecoder @@ -34,8 +35,8 @@ interface UComponents { fun > mkComposer( ctx: Context, - ): (UReadOnlyMemory) -> UComposer = - { memory: UReadOnlyMemory -> UComposer(ctx, memory) } + ): (UReadOnlyMemory, MutabilityOwnership) -> UComposer = + { memory: UReadOnlyMemory, ownership : MutabilityOwnership -> UComposer(ctx, memory, ownership) } fun mkStatesForkProvider(): StateForker = if (useSolverForForks) WithSolverStateForker else NoSolverStateForker 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 d621bca82..856a30dea 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 @@ -52,7 +52,7 @@ class UAllocatedArrayId internal con return key.uctx.withSizeSort().mkAllocatedArrayReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } @@ -129,7 +129,7 @@ class UInputArrayId internal constru return sort.uctx.withSizeSort().mkInputArrayReading(collection, key.first, key.second) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt index 996f3ab87..76e7ca5bb 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/USymbolicArrayLengthId.kt @@ -35,7 +35,7 @@ class UInputArrayLengthId internal constructor( return key.uctx.withSizeSort().mkInputArrayLengthReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt index 910f41d32..62df6895e 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/field/USymbolicFieldId.kt @@ -35,7 +35,7 @@ class UInputFieldId internal constructor( return key.uctx.mkInputFieldReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt index a992e4bdc..6c2af2f65 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/USymbolicMapLengthId.kt @@ -32,7 +32,7 @@ class UInputMapLengthId internal constructor( return sort.uctx.withSizeSort().mkInputMapLengthReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt index e99d11579..ca8663c73 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapId.kt @@ -66,7 +66,7 @@ class UAllocatedMapId return sort.uctx.mkInputMapReading(collection, key.first, key.second) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt index b762a242c..1e69cd05a 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/USymbolicRefMapId.kt @@ -61,7 +61,7 @@ class UAllocatedRefMapWithInputKeysId( return key.uctx.mkAllocatedRefMapWithInputKeysReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } @@ -126,7 +126,7 @@ class UInputRefMapWithAllocatedKeysId( return key.uctx.mkInputRefMapWithAllocatedKeysReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } @@ -185,7 +185,7 @@ class UInputRefMapWithInputKeysId( return sort.uctx.mkInputRefMapWithInputKeysReading(collection, key.first, key.second) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt index 19e8bb62d..bf1f0f50d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetId.kt @@ -57,7 +57,7 @@ class UAllocatedSetId>( return sort.uctx.mkAllocatedSetReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } @@ -133,7 +133,7 @@ class UInputSetId>( return sort.uctx.mkInputSetReading(collection, key.first, key.second) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetId.kt index 791b4c1f7..6aafe2909 100644 --- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetId.kt +++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/USymbolicRefSetId.kt @@ -54,7 +54,7 @@ class UAllocatedRefSetWithInputElementsId( return key.uctx.mkAllocatedRefSetWithInputElementsReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } @@ -128,7 +128,7 @@ class UInputRefSetWithAllocatedElementsId( return key.uctx.mkInputRefSetWithAllocatedElementsReading(collection, key) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } @@ -197,7 +197,7 @@ class UInputRefSetWithInputElementsId( return sort.uctx.mkInputRefSetWithInputElementsReading(collection, key.first, key.second) } - val memory = composer.memory.toWritableMemory() + val memory = composer.memory.toWritableMemory(composer.ownership) collection.applyTo(memory, key, composer) return memory.read(mkLValue(key)) } 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 b52dfe0af..63802e8a8 100644 --- a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt @@ -79,7 +79,7 @@ interface UReadOnlyMemory { fun nullRef(): UHeapRef - fun toWritableMemory(): UWritableMemory + fun toWritableMemory(ownership: MutabilityOwnership): UWritableMemory } interface UWritableMemory : UReadOnlyMemory { @@ -163,7 +163,7 @@ class UMemory( ctx, cloneOwnership, typeConstraints, stack.clone(), mocks.clone(thisOwnership, cloneOwnership), regions ).also { ownership = thisOwnership } - override fun toWritableMemory() = + override fun toWritableMemory(ownership: MutabilityOwnership) = // 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, ownership, types, stack, mocks, regions) 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 39a0c42a4..fc7a5e2e5 100644 --- a/usvm-core/src/main/kotlin/org/usvm/model/Model.kt +++ b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt @@ -41,7 +41,7 @@ open class UModelBase( override val ownership: MutabilityOwnership = ctx.defaultOwnership, ) : UModel, UWritableMemory { @Suppress("LeakingThis") - protected open val composer = ctx.composer(this) + protected open val composer = ctx.composer(this, ownership) /** * The evaluator supports only expressions with symbols inheriting [org.usvm.USymbol]. @@ -63,7 +63,7 @@ open class UModelBase( override fun nullRef(): UHeapRef = nullRef - override fun toWritableMemory(): UWritableMemory = this + override fun toWritableMemory(ownership: MutabilityOwnership): UWritableMemory = this override fun setRegion( regionId: UMemoryRegionId, diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt index 23d616590..130f91318 100644 --- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt @@ -67,7 +67,7 @@ internal class CompositionTest { ctx = UContext(components) ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } - every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory -> UComposer(ctx, memory) } } + every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory, ownership : MutabilityOwnership -> UComposer(ctx, memory, ownership) } } concreteNull = ctx.mkConcreteHeapRef(NULL_ADDRESS) stackEvaluator = mockk() @@ -79,7 +79,7 @@ internal class CompositionTest { every { memory.stack } returns stackEvaluator every { memory.mocker } returns mockEvaluator - composer = UComposer(ctx, memory) + composer = UComposer(ctx, memory, ownership) } @Test @@ -263,7 +263,7 @@ internal class CompositionTest { heapToComposeWith.writeArrayLength(fstConcreteAddress, fstValueFromHeap, arrayType, sizeSort) heapToComposeWith.writeArrayLength(sndConcreteAddress, sndValueFromHeap, arrayType, sizeSort) - val composer = UComposer(ctx, heapToComposeWith) + val composer = UComposer(ctx, heapToComposeWith, MutabilityOwnership()) every { fstAddress.accept(composer) } returns fstConcreteAddress every { sndAddress.accept(composer) } returns sndConcreteAddress @@ -314,7 +314,7 @@ internal class CompositionTest { val answer = 43.toBv() // TODO replace with jacoDB type - val composer = UComposer(ctx, UMemory, Any>(ctx, MutabilityOwnership(), mockk())) + val composer = UComposer(ctx, UMemory, Any>(ctx, ownership, mockk()), MutabilityOwnership()) every { fstAddress.accept(composer) } returns sndAddress every { fstIndex.accept(composer) } returns sndIndex @@ -348,13 +348,13 @@ internal class CompositionTest { // create a heap with a record: (sndAddress, sndIndex) = 2 sndMemory.writeArrayIndex(sndAddress, sndIndex, arrayType, mkBv32Sort(), 2.toBv(), mkTrue()) - val sndComposer = UComposer(ctx, sndMemory) + val sndComposer = UComposer(ctx, sndMemory, MutabilityOwnership()) 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()) - val fstComposer = UComposer(ctx, fstMemory) // TODO replace with jacoDB type + val fstComposer = UComposer(ctx, fstMemory, MutabilityOwnership()) // TODO replace with jacoDB type // Both heaps leave everything untouched every { sndAddress.accept(sndComposer) } returns sndAddress @@ -429,7 +429,7 @@ internal class CompositionTest { sndAddressForCompose, concreteIndex, arrayType, regionArray.sort, sndValue, guard = trueExpr ) - val composer = UComposer(ctx, heapToComposeWith) + val composer = UComposer(ctx, heapToComposeWith, MutabilityOwnership()) every { fstSymbolicIndex.accept(composer) } returns concreteIndex every { sndSymbolicIndex.accept(composer) } returns concreteIndex @@ -463,7 +463,7 @@ internal class CompositionTest { ctx, mockk(), mockk(), mockk(), emptyMap(), concreteNullRef ) - val composer = spyk(UComposer(ctx, heapToComposeWith)) + val composer = spyk(UComposer(ctx, heapToComposeWith, MutabilityOwnership())) every { symbolicIndex.accept(composer) } returns mkBv(2) every { symbolicAddress.accept(composer) } returns mkConcreteHeapRef(-1) @@ -512,7 +512,7 @@ internal class CompositionTest { val composeMemory = UMemory(ctx, MutabilityOwnership(), mockk()) composeMemory.writeField(aAddress, field, bv32Sort, 42.toBv(), guard = trueExpr) - val composer = UComposer(ctx, composeMemory) + val composer = UComposer(ctx, composeMemory, MutabilityOwnership()) val composedExpression = composer.compose(expression) @@ -527,7 +527,7 @@ internal class CompositionTest { ) val model = UModelBase(ctx, stackModel, mockk(), mockk(), emptyMap(), concreteNull) - val composer = UComposer(this, model) + val composer = UComposer(this, model, MutabilityOwnership()) val heapRefEvalEq = mkHeapRefEq(mkRegisterReading(0, addressSort), mkRegisterReading(1, addressSort)) @@ -543,7 +543,7 @@ internal class CompositionTest { every { composedMemory.nullRef() } returns concreteNull every { composedMemory.stack } returns stackModel - val composer = UComposer(this, composedMemory) + val composer = UComposer(this, composedMemory, MutabilityOwnership()) val heapRefEvalEq = mkHeapRefEq(mkRegisterReading(0, addressSort), nullRef) @@ -570,7 +570,7 @@ internal class CompositionTest { composeMemory.stack.writeRegister(2, composedSymbolicHeapRef) composeMemory.stack.writeRegister(3, mkRegisterReading(3, bv32Sort)) - val composer = UComposer(ctx, composeMemory) + val composer = UComposer(ctx, composeMemory, MutabilityOwnership()) val fromRegion0 = UInputArrayId<_, _, USizeSort>(arrayType, bv32Sort) .emptyRegion() @@ -628,7 +628,7 @@ internal class CompositionTest { val stackModel = URegistersStackEagerModel(concreteNull, mapOf(0 to mkBv(0), 1 to mkBv(0), 2 to mkBv(2))) every { composedMemory.stack } returns stackModel - val composer = UComposer(this, composedMemory) + val composer = UComposer(this, composedMemory, MutabilityOwnership()) val region = UAllocatedArrayId<_, _, USizeSort>(mockk(), addressSort, 1).emptyRegion() val reading = region.read(mkRegisterReading(0, sizeSort)) @@ -654,7 +654,8 @@ internal class CompositionTest { val reading = region.read(ref2) - val composer = spyk(UComposer(this, composedMemory)) + val composerOwnership = MutabilityOwnership() + val composer = spyk(UComposer(this, composedMemory, composerOwnership)) val writableMemory: UWritableMemory = mockk() @@ -662,7 +663,7 @@ internal class CompositionTest { every { composer.transform(ref1) } returns ref1 every { composer.transform(ref2) } returns ref2 - every { composedMemory.toWritableMemory() } returns writableMemory + every { composedMemory.toWritableMemory(composerOwnership) } returns writableMemory every { val lvalue = UFieldLValue(bv32Sort, ref1, field) 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 22b4eab01..623337264 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 @@ -52,7 +52,7 @@ abstract class SymbolicCollectionTestBase { ownership = MutabilityOwnership() every { components.mkComposer(ctx) } answers { - { memory: UReadOnlyMemory -> UComposer(ctx, memory) } + { memory: UReadOnlyMemory, ownership : MutabilityOwnership -> UComposer(ctx, memory, ownership) } } val translator = UExprTranslator(ctx) 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 ba46d476d..b71b570bf 100644 --- a/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt @@ -47,7 +47,7 @@ class ModelCompositionTest { ctx = UContext(components) ownership = MutabilityOwnership() - every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory -> UComposer(ctx, memory) } } + every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory, ownership: MutabilityOwnership -> UComposer(ctx, memory, ownership) } } every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } concreteNull = ctx.mkConcreteHeapRef(NULL_ADDRESS) } @@ -60,7 +60,7 @@ class ModelCompositionTest { ) val model = UModelBase(ctx, stackModel, mockk(), mockk(), emptyMap(), concreteNull) - val composer = UComposer(this, model) + val composer = UComposer(this, model, defaultOwnership) val region = UAllocatedArrayId<_, _, USizeSort>(mockk(), bv32Sort, 1) .emptyRegion() @@ -93,7 +93,7 @@ class ModelCompositionTest { val model = UModelBase( ctx, stackModel, mockk(), mockk(), mapOf(arrayMemoryId to arrayModel), concreteNull ) - val composer = UComposer(this, model) + val composer = UComposer(this, model, defaultOwnership) val symbolicRef = mkRegisterReading(0, addressSort) as UHeapRef @@ -152,7 +152,7 @@ class ModelCompositionTest { ctx, stackModel, mockk(), mockk(), mapOf(arrayLengthMemoryId to arrayLengthModel), concreteNull ) - val composer = UComposer(this, model) + val composer = UComposer(this, model, defaultOwnership) val region = UInputArrayLengthId(arrayType, bv32Sort) .emptyRegion() @@ -197,7 +197,7 @@ class ModelCompositionTest { ctx, stackModel, mockk(), mockk(), mapOf(fieldMemoryId to fieldModel), concreteNull ) - val composer = UComposer(this, model) + val composer = UComposer(this, model, defaultOwnership) val region = UInputFieldId(field, addressSort) .emptyRegion() @@ -227,7 +227,7 @@ class ModelCompositionTest { ctx, stackModel, mockk(), mockk(), emptyMap(), concreteNull ) - val composer = UComposer(this, model) + val composer = UComposer(this, model, defaultOwnership) val emptyRegion = UAllocatedArrayId<_, _, USizeSort>(mockk(), bv32Sort, 1).emptyRegion() 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 ba2e15279..1b0cbe67d 100644 --- a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt @@ -63,7 +63,7 @@ class ModelDecodingTest { ctx = UContext(components) ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } - every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory -> UComposer(ctx, memory) } } + every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory, ownership: MutabilityOwnership -> UComposer(ctx, memory, ownership) } } val translator = UExprTranslator(ctx) val decoder = ULazyModelDecoder(translator) 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 64e34ed33..603b3205a 100644 --- a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt @@ -42,7 +42,7 @@ open class SoftConstraintsTest { ctx = UContext(components) ownership = MutabilityOwnership() every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } - every { components.mkComposer(any()) } answers { { memory: UReadOnlyMemory -> UComposer(ctx, memory) } } + every { components.mkComposer(any()) } answers { { memory: UReadOnlyMemory, ownership: MutabilityOwnership -> UComposer(ctx, memory, ownership) } } softConstraintsProvider = USoftConstraintsProvider(ctx) 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 6b66fe6f3..ba6acb47f 100644 --- a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt @@ -75,7 +75,7 @@ class TypeSolverTest { every { components.mkSolver(ctx) } returns solver every { components.mkTypeSystem(ctx) } returns typeSystem every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) } - every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory -> UComposer(ctx, memory) } } + every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory, ownership: MutabilityOwnership -> UComposer(ctx, memory, ownership) } } } private val pc = UPathConstraints(ctx, ownership) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt index b50d890df..42344b579 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt @@ -7,13 +7,13 @@ import org.usvm.UComposer import org.usvm.UContext import org.usvm.UMachineOptions import org.usvm.USizeExprProvider +import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.memory.UReadOnlyMemory import org.usvm.model.ULazyModelDecoder import org.usvm.solver.UExprTranslator import org.usvm.solver.USoftConstraintsProvider import org.usvm.solver.USolverBase import org.usvm.solver.UTypeSolver -import kotlin.time.Duration class JcComponents( private val typeSystem: JcTypeSystem, @@ -34,8 +34,8 @@ class JcComponents( override fun > mkComposer( ctx: Context - ): (UReadOnlyMemory) -> UComposer = - { memory: UReadOnlyMemory -> JcComposer(ctx, memory) } + ): (UReadOnlyMemory, MutabilityOwnership) -> UComposer = + { memory: UReadOnlyMemory, ownership: MutabilityOwnership -> JcComposer(ctx, memory, ownership) } override fun > mkSolver(ctx: Context): USolverBase { val (translator, decoder) = buildTranslatorAndLazyDecoder(ctx) 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 253aeaf09..50de13c8c 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 @@ -27,7 +28,8 @@ interface JcTransformer : UTransformer { class JcComposer( ctx: UContext, memory: UReadOnlyMemory, -) : UComposer(ctx, memory), JcTransformer { + ownership: MutabilityOwnership, +) : UComposer(ctx, memory, ownership), JcTransformer { override fun transform(expr: JcStaticFieldReading): UExpr = memory.read(JcStaticFieldLValue(expr.field, expr.sort)) }