fix ownership flow; add ownership in type constraints

UnitTestBot · Jul 24, 2024 · 947418f · 947418f
1 parent 1079834
commit 947418f
Show file tree

Hide file tree

Showing 12 changed files with 109 additions and 83 deletions.
diff --git 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<T> {
         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
@@ -43,7 +43,7 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, 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
@@ -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
@@ -24,7 +24,7 @@ import org.usvm.uctx
  */
 open class UPathConstraints<Type>(
     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<Type>(
      * Constraints solved by type solver.
      */
     val typeConstraints: UTypeConstraints<Type> = UTypeConstraints(
+        ownership,
         ctx.typeSystem(),
         equalityConstraints
     ),
@@ -48,8 +49,15 @@ open class UPathConstraints<Type>(
         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,19 +69,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")
@@ -119,21 +127,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
@@ -166,15 +174,18 @@ open class UPathConstraints<Type>(
             }
         }
 
-    open fun clone(thisOwnership: MutabilityOwnership, cloneOwnership: MutabilityOwnership): UPathConstraints<Type> {
+    open fun clone(
+        thisOwnership: MutabilityOwnership = ownership,
+        cloneOwnership: MutabilityOwnership = MutabilityOwnership(), // clone ownership must be brand new because of plus assign operations
+    ): UPathConstraints<Type> {
         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<Type>(
             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)