numeric constraints: reorder remove and get

UnitTestBot · Jul 21, 2024 · 1b433cb · 1b433cb
1 parent 6f97c4a
commit 1b433cb
Show file tree

Hide file tree

Showing 22 changed files with 224 additions and 135 deletions.
diff --git a/usvm-core/src/main/kotlin/org/usvm/CallStack.kt b/usvm-core/src/main/kotlin/org/usvm/CallStack.kt
@@ -1,6 +1,5 @@
 package org.usvm
 
-import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.merging.UMergeable
 
 data class UCallStackFrame<Method, Statement>(

diff --git a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt
@@ -27,14 +27,14 @@ interface UMocker<Method> : UMockEvaluator {
 
     fun getTrackedExpression(trackedLiteral: TrackedLiteral): UExpr<USort>
 
-    fun clone(ownership: MutabilityOwnership): UMocker<Method>
+    fun clone(thisOwnership: MutabilityOwnership, cloneOwnership: MutabilityOwnership): UMocker<Method>
 }
 
 class UIndexedMocker<Method>(
     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(),
-    internal var ownership: MutabilityOwnership,
+    private var ownership: MutabilityOwnership,
 ) : UMocker<Method>, UOwnedMergeable<UIndexedMocker<Method>, MergeGuard> {
     override fun <Sort : USort> call(
         method: Method,
@@ -76,8 +76,8 @@ class UIndexedMocker<Method>(
         return trackedSymbols[trackedLiteral]!!.cast()
     }
 
-    override fun clone(ownership: MutabilityOwnership): UIndexedMocker<Method> =
-        UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols, ownership)
+    override fun clone(thisOwnership: MutabilityOwnership, cloneOwnership: MutabilityOwnership): UIndexedMocker<Method> =
+        UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols, cloneOwnership).also { ownership = thisOwnership }
 
     /**
      * Check if this [UIndexedMocker] can be merged with [other] indexed mocker.
@@ -86,14 +86,22 @@ class UIndexedMocker<Method>(
      *
      * @return the merged indexed mocker.
      */
-    override fun mergeWith(other: UIndexedMocker<Method>, by: MergeGuard, ownership: MutabilityOwnership): UIndexedMocker<Method>? {
+    override fun mergeWith(
+        other: UIndexedMocker<Method>,
+        by: MergeGuard,
+        thisOwnership: MutabilityOwnership,
+        otherOwnership: MutabilityOwnership,
+        mergedOwnership: MutabilityOwnership
+    ): UIndexedMocker<Method>? {
         if (methodMockClauses !== other.methodMockClauses
             || trackedSymbols !== other.trackedSymbols
             || untrackedSymbols !== other.untrackedSymbols
         ) {
             return null
         }
-        this.ownership = ownership
+
+        this.ownership = mergedOwnership
+        other.ownership = otherOwnership
         return this
     }
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt
@@ -37,12 +37,6 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
 
     open var ownership = initOwnership
         protected set
-
-    protected fun changeOwnership(newOwnership: MutabilityOwnership) {
-        ownership = newOwnership
-        pathConstraints.changeOwnership(ownership)
-        memory.changeOwnership(ownership)
-    }
 
     /**
      * Creates new state structurally identical to this.

diff --git a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt
@@ -145,8 +145,9 @@ object WithSolverStateForker : StateForker {
         newConstraintToForkedState: UBoolExpr,
         stateToCheck: StateToCheck,
     ): T? {
-        val newOwnership = MutabilityOwnership()
-        val constraintsToCheck = state.pathConstraints.clone(newOwnership)
+        val thisOwnership = MutabilityOwnership()
+        val cloneOwnership = MutabilityOwnership()
+        val constraintsToCheck = state.pathConstraints.clone(thisOwnership, cloneOwnership)
 
         constraintsToCheck += if (stateToCheck) {
             newConstraintToForkedState
@@ -194,8 +195,7 @@ object NoSolverStateForker : StateForker {
     ): ForkResult<T> {
         val (trueModels, falseModels, _) = splitModelsByCondition(state.models, condition)
         val notCondition = state.ctx.mkNot(condition)
-        val newOwnership = MutabilityOwnership()
-        val clonedPathConstraints = state.pathConstraints.clone(newOwnership)
+        val clonedPathConstraints = state.pathConstraints.clone(MutabilityOwnership(), MutabilityOwnership())
         clonedPathConstraints += condition
 
         val (posState, negState) = if (clonedPathConstraints.isFalse) {
@@ -228,8 +228,7 @@ object NoSolverStateForker : StateForker {
         val result = mutableListOf<T?>()
         for (condition in conditions) {
             val (trueModels, _) = splitModelsByCondition(curState.models, condition)
-            val newOwnership = MutabilityOwnership()
-            val clonedConstraints = curState.pathConstraints.clone(newOwnership)
+            val clonedConstraints = curState.pathConstraints.clone(MutabilityOwnership(), MutabilityOwnership())
             clonedConstraints += condition
 
             if (clonedConstraints.isFalse) {

diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt
@@ -380,10 +380,11 @@ class UEqualityConstraints private constructor(
      * Creates a mutable copy of this structure.
      * Note that current subscribers get unsubscribed!
      */
-    fun clone(ownership: MutabilityOwnership): UEqualityConstraints {
+    fun clone(thisOwnership: MutabilityOwnership, clonerOwnership: MutabilityOwnership): UEqualityConstraints {
+        this.ownership = thisOwnership
         if (isContradicting) {
             val result = UEqualityConstraints(
-                ctx, ownership, DisjointSets(),
+                ctx, clonerOwnership, DisjointSets(),
                 persistentHashSetOf(),
                 persistentHashMapOf(),
                 persistentHashMapOf()
@@ -394,7 +395,7 @@ class UEqualityConstraints private constructor(
 
         return UEqualityConstraints(
             ctx,
-            ownership,
+            clonerOwnership,
             equalReferences.clone(),
             distinctReferences,
             referenceDisequalities,
@@ -415,7 +416,13 @@ class UEqualityConstraints private constructor(
      *
      * @return the merged equality constraints.
      */
-    override fun mergeWith(other: UEqualityConstraints, by: MutableMergeGuard, ownership: MutabilityOwnership): UEqualityConstraints? {
+    override fun mergeWith(
+        other: UEqualityConstraints,
+        by: MutableMergeGuard,
+        thisOwnership: MutabilityOwnership,
+        otherOwnership: MutabilityOwnership,
+        mergedOwnership: MutabilityOwnership
+    ): UEqualityConstraints? {
         // TODO: refactor it
         if (distinctReferences != other.distinctReferences) {
             return null
@@ -430,8 +437,9 @@ class UEqualityConstraints private constructor(
             return null
         }
 
+        other.ownership = otherOwnership
         // Clone because of mutable [isStaticRefAssignableToSymbolic]
-        return clone(ownership)
+        return clone(thisOwnership, mergedOwnership)
     }
 
     fun constraints(translator: UExprTranslator<*, *>): Sequence<UBoolExpr> {

diff --git 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<Type>(
     protected val ctx: UContext<*>,
-    protected var ownership: MutabilityOwnership,
+    ownership: MutabilityOwnership,
     protected val logicalConstraints: ULogicalConstraints = ULogicalConstraints.empty(),
     /**
      * Specially represented equalities and disequalities between objects, used in various part of constraints management.
@@ -46,13 +46,8 @@ open class UPathConstraints<Type>(
         // Use the information from the type constraints to check whether any static ref is assignable to any symbolic ref
         equalityConstraints.setTypesCheck(typeConstraints::canStaticRefBeEqualToSymbolic)
     }
-
-    fun changeOwnership(newOwnership: MutabilityOwnership) {
-       ownership = newOwnership
-       numericConstraints.ownership = newOwnership
-       equalityConstraints.ownership = newOwnership
-    }
-
+    var ownership : MutabilityOwnership = ownership
+        private set
     /**
      * Constraints solved by SMT solver.
      */
@@ -63,19 +58,19 @@ open class UPathConstraints<Type>(
 
     val isFalse: Boolean
         get() = equalityConstraints.isContradicting ||
-            typeConstraints.isContradicting ||
-            numericConstraints.isContradicting ||
-            logicalConstraints.isContradicting
+                typeConstraints.isContradicting ||
+                numericConstraints.isContradicting ||
+                logicalConstraints.isContradicting
 
     // TODO: refactor
     fun constraints(translator: UExprTranslator<Type, *>): Sequence<UBoolExpr> {
         if (isFalse) {
             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")
@@ -121,21 +116,21 @@ open class UPathConstraints<Type>(
                     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
@@ -168,14 +163,15 @@ open class UPathConstraints<Type>(
             }
         }
 
-    open fun clone(ownership: MutabilityOwnership): UPathConstraints<Type> {
+    open fun clone(thisOwnership: MutabilityOwnership, cloneOwnership: MutabilityOwnership): UPathConstraints<Type> {
         val clonedLogicalConstraints = logicalConstraints.clone()
-        val clonedEqualityConstraints = equalityConstraints.clone(ownership)
+        val clonedEqualityConstraints = equalityConstraints.clone(thisOwnership, cloneOwnership)
         val clonedTypeConstraints = typeConstraints.clone(clonedEqualityConstraints)
-        val clonedNumericConstraints = numericConstraints.clone(ownership)
+        val clonedNumericConstraints = numericConstraints.clone(thisOwnership, cloneOwnership)
+        this.ownership = thisOwnership
         return UPathConstraints(
             ctx = ctx,
-            ownership,
+            cloneOwnership,
             logicalConstraints = clonedLogicalConstraints,
             equalityConstraints = clonedEqualityConstraints,
             typeConstraints = clonedTypeConstraints,
@@ -201,18 +197,26 @@ open class UPathConstraints<Type>(
      *
      * @return the merged path constraints.
      */
-    override fun mergeWith(other: UPathConstraints<Type>, by: MutableMergeGuard, ownership: MutabilityOwnership): UPathConstraints<Type>? {
+    override fun mergeWith(
+        other: UPathConstraints<Type>,
+        by: MutableMergeGuard,
+        thisOwnership: MutabilityOwnership,
+        otherOwnership: MutabilityOwnership,
+        mergedOwnership: MutabilityOwnership
+    ): UPathConstraints<Type>? {
         // TODO: elaborate on some merge parameters here
-        val mergedLogicalConstraints = logicalConstraints.mergeWith(other.logicalConstraints, by, ownership)
-        val mergedEqualityConstraints = equalityConstraints.mergeWith(other.equalityConstraints, by, ownership) ?: return null
+        val mergedLogicalConstraints =
+            logicalConstraints.mergeWith(other.logicalConstraints, by, thisOwnership, otherOwnership, mergedOwnership)
+        val mergedEqualityConstraints =
+            equalityConstraints.mergeWith(other.equalityConstraints, by, thisOwnership, otherOwnership, mergedOwnership) ?: return null
         val mergedTypeConstraints = typeConstraints
             .clone(mergedEqualityConstraints)
             .mergeWith(other.typeConstraints, by) ?: return null
-        val mergedNumericConstraints = numericConstraints.mergeWith(other.numericConstraints, by, ownership)
+        val mergedNumericConstraints = numericConstraints.mergeWith(other.numericConstraints, by, thisOwnership, otherOwnership, mergedOwnership)
 
         return UPathConstraints(
             ctx,
-            ownership,
+            mergedOwnership,
             mergedLogicalConstraints,
             mergedEqualityConstraints,
             mergedTypeConstraints,

diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/ULogicalConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/ULogicalConstraints.kt
@@ -46,8 +46,14 @@ class ULogicalConstraints private constructor(
      *
      * @return the logical constraints.
      */
-    override fun mergeWith(other: ULogicalConstraints, by: MutableMergeGuard, ownership: MutabilityOwnership): ULogicalConstraints {
-        val (overlap, uniqueThis, uniqueOther) = constraints.separate(other.constraints, ownership)
+    override fun mergeWith(
+        other: ULogicalConstraints,
+        by: MutableMergeGuard,
+        thisOwnership: MutabilityOwnership,
+        otherOwnership: MutabilityOwnership,
+        mergedOwnership: MutabilityOwnership
+    ): ULogicalConstraints {
+        val (overlap, uniqueThis, uniqueOther) = constraints.separate(other.constraints, mergedOwnership)
         by.appendThis(uniqueThis.asSequence())
         by.appendOther(uniqueOther.asSequence())
         return ULogicalConstraints(overlap)