add ownership in memory

UnitTestBot · Jul 18, 2024 · 25d037a · 25d037a
1 parent d82fd86
commit 25d037a
Show file tree

Hide file tree

Showing 84 changed files with 704 additions and 570 deletions.
diff --git 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<USizeSort : USort>(
         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
@@ -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 <Sort : USort> eval(symbol: UMockSymbol<Sort>): UExpr<Sort>
@@ -26,14 +27,15 @@ interface UMocker<Method> : UMockEvaluator {
 
     fun getTrackedExpression(trackedLiteral: TrackedLiteral): UExpr<USort>
 
-    fun clone(): UMocker<Method>
+    fun clone(ownership: MutabilityOwnership): UMocker<Method>
 }
 
 class UIndexedMocker<Method>(
-    private var methodMockClauses: PersistentMap<Method, PersistentList<UMockSymbol<out USort>>> = persistentHashMapOf(),
-    private var trackedSymbols: PersistentMap<TrackedLiteral, UExpr<out USort>> = persistentHashMapOf(),
+    private var methodMockClauses: UPersistentHashMap<Method, PersistentList<UMockSymbol<out USort>>> = persistentHashMapOf(),
+    private var trackedSymbols: UPersistentHashMap<TrackedLiteral, UExpr<out USort>> = persistentHashMapOf(),
     private var untrackedSymbols: PersistentList<UExpr<out USort>> = persistentListOf(),
-) : UMocker<Method>, UMergeable<UIndexedMocker<Method>, MergeGuard> {
+    internal var ownership: MutabilityOwnership,
+) : UMocker<Method>, UOwnedMergeable<UIndexedMocker<Method>, MergeGuard> {
     override fun <Sort : USort> call(
         method: Method,
         args: Sequence<UExpr<out USort>>,
@@ -42,15 +44,15 @@ class UIndexedMocker<Method>(
         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
     }
 
     override fun <Sort : USort> eval(symbol: UMockSymbol<Sort>): UExpr<Sort> = symbol
 
     override val trackedLiterals: Collection<TrackedLiteral>
-        get() = trackedSymbols.keys
+        get() = trackedSymbols.keys()
 
     /**
      * Creates a mock symbol. If [trackedLiteral] is not null, created expression
@@ -60,7 +62,7 @@ class UIndexedMocker<Method>(
         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<Method>(
     override fun getTrackedExpression(trackedLiteral: TrackedLiteral): UExpr<USort> {
         if (trackedLiteral !in trackedSymbols) error("Access by unregistered track literal $trackedLiteral")
 
-        return trackedSymbols.getValue(trackedLiteral).cast()
+        return trackedSymbols[trackedLiteral]!!.cast()
     }
 
-    override fun clone(): UIndexedMocker<Method> = UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols)
+    override fun clone(ownership: MutabilityOwnership): UIndexedMocker<Method> =
+        UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols, ownership)
 
     /**
      * Check if this [UIndexedMocker] can be merged with [other] indexed mocker.
@@ -83,14 +86,14 @@ class UIndexedMocker<Method>(
      *
      * @return the merged indexed mocker.
      */
-    override fun mergeWith(other: UIndexedMocker<Method>, by: MergeGuard): UIndexedMocker<Method>? {
+    override fun mergeWith(other: UIndexedMocker<Method>, by: MergeGuard, ownership: MutabilityOwnership): UIndexedMocker<Method>? {
         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
@@ -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<Type, Method, Statement, Context, Target, State>(
     // TODO: add interpreter-specific information
     val ctx: Context,
-    private var ownership : MutabilityOwnership,
+    initOwnership : MutabilityOwnership,
     open val callStack: UCallStack<Method, Statement>,
     open val pathConstraints: UPathConstraints<Type>,
     open val memory: UMemory<Type, Method>,
@@ -26,7 +25,7 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
     open var pathNode: PathNode<Statement>,
     open var forkPoints: PathNode<PathNode<Statement>>,
     open val targets: UTargetsSet<Target, Statement>,
-) : UOwnedMergeable<State, Unit>
+) : UMergeable<State, Unit>
     where Context : UContext<*>,
           Target : UTarget<Statement, Target>,
           State : UState<Type, Method, Statement, Context, Target, State> {
@@ -35,19 +34,23 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
      * 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<Type>? = null): State
+    abstract fun clone(newConstraints: UPathConstraints<Type>? = 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
@@ -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
@@ -43,6 +43,8 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, 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
@@ -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 <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayType>.mems
     type: ArrayType,
     sort: Sort,
     sizeSort: USizeSort,
-    contents: Sequence<UExpr<Sort>>
+    contents: Sequence<UExpr<Sort>>,
 ) {
     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
@@ -158,6 +158,7 @@ object ListCollectionApi {
         srcFrom: UExpr<USizeSort>,
         dstFrom: UExpr<USizeSort>,
         length: UExpr<USizeSort>,
+
     ) {
         memory.memcpy(
             srcRef = srcRef,