From ca356d07ac65334d5db47b0c774d06afcfa9669a Mon Sep 17 00:00:00 2001 From: tochilinak Date: Tue, 23 Sep 2025 13:09:55 +0300 Subject: [PATCH 1/2] Made `plusAssign` of `UPathConstraints` non-recursive --- .../org/usvm/constraints/PathConstraints.kt | 21 +++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) 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 4098e4f2a3..8d855f1057 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt @@ -94,8 +94,17 @@ open class UPathConstraints( typeConstraints.constraints() } + operator fun plusAssign(constraint: UBoolExpr) { + val queue = ArrayDeque() + queue.add(constraint) + while (queue.isNotEmpty()) { + val c = queue.removeFirst() + addConstraint(c, queue) + } + } + @Suppress("UNCHECKED_CAST") - open operator fun plusAssign(constraint: UBoolExpr): Unit = + protected open fun addConstraint(constraint: UBoolExpr, queue: ArrayDeque): Unit = with(constraint.uctx) { when { constraint == falseExpr -> contradiction(this) @@ -131,27 +140,27 @@ open class UPathConstraints( typeConstraints.addSubtype(constraint.ref, constraint.subtype as Type) } - constraint is UAndExpr -> constraint.args.forEach(::plusAssign) + constraint is UAndExpr -> queue.addAll(constraint.args) constraint is UNotExpr -> { 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 @@ -172,7 +181,7 @@ open class UPathConstraints( notConstraint in logicalConstraints -> contradiction(ctx) - notConstraint is UOrExpr -> notConstraint.args.forEach { plusAssign(ctx.mkNot(it)) } + notConstraint is UOrExpr -> queue.addAll(notConstraint.args.map(::mkNot)) else -> logicalConstraints.add(constraint, ownership) } From babc35dd7b7a384b665a455be58bc4066b32163c Mon Sep 17 00:00:00 2001 From: tochilinak Date: Tue, 23 Sep 2025 15:57:41 +0300 Subject: [PATCH 2/2] formatting --- .../src/main/kotlin/org/usvm/constraints/PathConstraints.kt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 8d855f1057..08e07417c4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt @@ -146,21 +146,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