From 1dc45cfc7cb91c3ee1be1599b51ec3c6246988f5 Mon Sep 17 00:00:00 2001 From: Sergey Loktev <71882967+zishkaz@users.noreply.github.com> Date: Mon, 7 Oct 2024 17:08:11 +0300 Subject: [PATCH] Extract common API + comment --- .github/workflows/build-and-run-tests.yml | 3 +- .../src/main/kotlin/org/usvm/Expressions.kt | 38 ++++ .../src/main/kotlin/org/usvm/StateForker.kt | 78 ++++---- .../src/main/kotlin/org/usvm/TSComponents.kt | 3 - .../src/main/kotlin/org/usvm/TSExpressions.kt | 31 ---- usvm-ts/src/main/kotlin/org/usvm/Utils.kt | 3 - .../kotlin/org/usvm/state/TSStateForker.kt | 168 ------------------ 7 files changed, 78 insertions(+), 246 deletions(-) delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/state/TSStateForker.kt diff --git a/.github/workflows/build-and-run-tests.yml b/.github/workflows/build-and-run-tests.yml index ac42b55dc0..11422b9740 100644 --- a/.github/workflows/build-and-run-tests.yml +++ b/.github/workflows/build-and-run-tests.yml @@ -39,7 +39,8 @@ jobs: REPO_URL="https://gitee.com/Lipenx/arkanalyzer.git" DEST_DIR="arkanalyzer" MAX_RETRIES=10 - RETRY_DELAY=3 # Delay between retries in seconds + RETRY_DELAY=3 # Delay between retries in seconds +# Set the same as in jacodb/neo branch, since we get jacodb artifact from that branch. BRANCH="neo/2024-08-16" for ((i=1; i<=MAX_RETRIES; i++)); do diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt index 927c8168ba..a80b84630c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt @@ -315,9 +315,47 @@ class UIsSupertypeExpr internal constructor( //endregion +//region Utility Expressions + +/** + * Utility class for merging expressions with [UBoolSort] sort. + * + * Mainly created for [not] function used in StateForker. + */ +class UJoinedBoolExpr( + ctx: UContext<*>, + val exprs: List +) : UBoolExpr(ctx) { + override val sort: UBoolSort + get() = ctx.boolSort + + private val joinedExprs = ctx.mkAnd(exprs) + + fun not(): UBoolExpr = ctx.mkAnd(exprs.map(ctx::mkNot)) + + override fun accept(transformer: KTransformerBase): KExpr { + return transformer.apply(joinedExprs) + } + + override fun internEquals(other: Any): Boolean = structurallyEqual(other) + + override fun internHashCode(): Int = hash() + + override fun print(printer: ExpressionPrinter) { + printer.append("joined(") + joinedExprs.print(printer) + printer.append(")") + } +} + +//endregion + //region Utils val UBoolExpr.isFalse get() = this == ctx.falseExpr val UBoolExpr.isTrue get() = this == ctx.trueExpr +fun UExpr<*>.unwrapJoinedExpr(ctx: UContext<*>): UExpr = + if (this is UJoinedBoolExpr) ctx.mkAnd(exprs) else this + //endregion diff --git a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt index 20d55451da..31e4115717 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt @@ -1,6 +1,6 @@ package org.usvm -import org.usvm.StateForker.Companion.splitModelsByCondition +import io.ksmt.utils.cast import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.model.UModelBase import org.usvm.solver.USatResult @@ -12,39 +12,7 @@ private typealias StateToCheck = Boolean private const val ForkedState = true private const val OriginalState = false -interface StateForker { - - companion object { - /** - * Splits the passed [models] with this [condition] to the three categories: - * - models that satisfy this [condition]; - * - models that are in contradiction with this [condition]; - * - models that can not evaluate this [condition]. - */ - fun splitModelsByCondition( - models: List>, - condition: UBoolExpr, - ): SplittedModels { - val trueModels = mutableListOf>() - val falseModels = mutableListOf>() - val unknownModels = mutableListOf>() - - models.forEach { model -> - val holdsInModel = model.eval(condition) - - when { - holdsInModel.isTrue -> trueModels += model - holdsInModel.isFalse -> falseModels += model - // Sometimes we cannot evaluate the condition – for example, a result for a division by symbolic expression - // that is evaluated to 0 is unknown - else -> unknownModels += model - } - } - - return SplittedModels(trueModels, falseModels, unknownModels) - } - } - +sealed interface StateForker { /** * Implements symbolic branching. * Checks if [condition] and ![condition] are satisfiable within [state]. @@ -78,9 +46,10 @@ object WithSolverStateForker : StateForker { state: T, condition: UBoolExpr, ): ForkResult { - val (trueModels, falseModels, _) = splitModelsByCondition(state.models, condition) + val unwrappedCondition: UBoolExpr = condition.unwrapJoinedExpr(state.ctx).cast() + val (trueModels, falseModels, _) = splitModelsByCondition(state.models, unwrappedCondition) - val notCondition = state.ctx.mkNot(condition) + val notCondition = if (condition is UJoinedBoolExpr) condition.not() else state.ctx.mkNot(unwrappedCondition) val (posState, negState) = when { trueModels.isNotEmpty() && falseModels.isNotEmpty() -> { @@ -89,7 +58,7 @@ object WithSolverStateForker : StateForker { posState.models = trueModels negState.models = falseModels - posState.pathConstraints += condition + posState.pathConstraints += unwrappedCondition negState.pathConstraints += notCondition posState to negState @@ -97,7 +66,7 @@ object WithSolverStateForker : StateForker { trueModels.isNotEmpty() -> state to forkIfSat( state, - newConstraintToOriginalState = condition, + newConstraintToOriginalState = unwrappedCondition, newConstraintToForkedState = notCondition, stateToCheck = ForkedState ) @@ -105,7 +74,7 @@ object WithSolverStateForker : StateForker { falseModels.isNotEmpty() -> { val forkedState = forkIfSat( state, - newConstraintToOriginalState = condition, + newConstraintToOriginalState = unwrappedCondition, newConstraintToForkedState = notCondition, stateToCheck = OriginalState ) @@ -287,12 +256,41 @@ object NoSolverStateForker : StateForker { } } +/** + * Splits the passed [models] with this [condition] to the three categories: + * - models that satisfy this [condition]; + * - models that are in contradiction with this [condition]; + * - models that can not evaluate this [condition]. + */ +private fun splitModelsByCondition( + models: List>, + condition: UBoolExpr, +): SplittedModels { + val trueModels = mutableListOf>() + val falseModels = mutableListOf>() + val unknownModels = mutableListOf>() + + models.forEach { model -> + val holdsInModel = model.eval(condition) + + when { + holdsInModel.isTrue -> trueModels += model + holdsInModel.isFalse -> falseModels += model + // Sometimes we cannot evaluate the condition – for example, a result for a division by symbolic expression + // that is evaluated to 0 is unknown + else -> unknownModels += model + } + } + + return SplittedModels(trueModels, falseModels, unknownModels) +} + data class ForkResult( val positiveState: T?, val negativeState: T?, ) -data class SplittedModels( +private data class SplittedModels( val trueModels: List>, val falseModels: List>, val unknownModels: List>, diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt index bf9969fc45..e83cb1e135 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSComponents.kt @@ -6,7 +6,6 @@ import io.ksmt.symfpu.solver.KSymFpuSolver import org.jacodb.ets.base.EtsType import org.usvm.solver.USolverBase import org.usvm.solver.UTypeSolver -import org.usvm.state.TSStateForker import org.usvm.types.UTypeSystem class TSComponents( @@ -41,8 +40,6 @@ class TSComponents( return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, options.solverTimeout) } - override fun mkStatesForkProvider(): StateForker = TSStateForker - fun close() { closeableResources.forEach(AutoCloseable::close) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt index 97539456dc..557df7c8b1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/TSExpressions.kt @@ -36,37 +36,6 @@ class TSUndefinedValue(ctx: TSContext) : UExpr(ctx) { } } -/** - * Utility class for merging expressions with [UBoolSort] sort. - * - * Mainly created for [not] function used in TSStateForker. - */ -class UJoinedBoolExpr( - ctx: TSContext, - val exprs: List -) : UBoolExpr(ctx) { - override val sort: UBoolSort - get() = ctx.boolSort - - private val joinedExprs = ctx.mkAnd(exprs) - - fun not(): UBoolExpr = ctx.mkAnd(exprs.map(ctx::mkNot)) - - override fun accept(transformer: KTransformerBase): KExpr { - return transformer.apply(joinedExprs) - } - - override fun internEquals(other: Any): Boolean = structurallyEqual(other) - - override fun internHashCode(): Int = hash() - - override fun print(printer: ExpressionPrinter) { - printer.append("joined(") - joinedExprs.print(printer) - printer.append(")") - } -} - /** * [UExpr] wrapper that handles type coercion. * diff --git a/usvm-ts/src/main/kotlin/org/usvm/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/Utils.kt index ea1333d7e0..db6fb13773 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/Utils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/Utils.kt @@ -16,9 +16,6 @@ fun UContext<*>.boolToFpSort(expr: UExpr) = fun UContext<*>.fpToBoolSort(expr: UExpr) = mkIte(mkFpEqualExpr(expr, mkFp64(0.0)), mkFalse(), mkTrue()) -fun UExpr<*>.unwrapJoinedExpr(ctx: UContext<*>): UExpr = - if (this is UJoinedBoolExpr) ctx.mkAnd(exprs) else this - fun UExpr.extractOrThis(): UExpr = if (this is TSWrappedValue) value else this fun MutableMap>.copy(): MutableMap> = this.entries.associate { (k, v) -> diff --git a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateForker.kt b/usvm-ts/src/main/kotlin/org/usvm/state/TSStateForker.kt deleted file mode 100644 index 7a237463c7..0000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/state/TSStateForker.kt +++ /dev/null @@ -1,168 +0,0 @@ -package org.usvm.state - -import io.ksmt.utils.cast -import org.usvm.ForkResult -import org.usvm.StateForker -import org.usvm.StateForker.Companion.splitModelsByCondition -import org.usvm.UBoolExpr -import org.usvm.UContext -import org.usvm.UJoinedBoolExpr -import org.usvm.UState -import org.usvm.solver.USatResult -import org.usvm.solver.UUnknownResult -import org.usvm.solver.UUnsatResult -import org.usvm.unwrapJoinedExpr - -private typealias StateToCheck = Boolean - -private const val ForkedState = true -private const val OriginalState = false - -// TODO: No copy-paste implementation with USVM API rework. -object TSStateForker : StateForker { - override fun , Type, Context : UContext<*>> fork( - state: T, - condition: UBoolExpr, - ): ForkResult { - val unwrappedCondition: UBoolExpr = condition.unwrapJoinedExpr(state.ctx).cast() - val (trueModels, falseModels, _) = splitModelsByCondition(state.models, unwrappedCondition) - - val notCondition = if (condition is UJoinedBoolExpr) condition.not() else state.ctx.mkNot(unwrappedCondition) - val (posState, negState) = when { - - trueModels.isNotEmpty() && falseModels.isNotEmpty() -> { - val posState = state - val negState = state.clone() - - posState.models = trueModels - negState.models = falseModels - posState.pathConstraints += unwrappedCondition - negState.pathConstraints += notCondition - - posState to negState - } - - trueModels.isNotEmpty() -> state to forkIfSat( - state, - newConstraintToOriginalState = unwrappedCondition, - newConstraintToForkedState = notCondition, - stateToCheck = ForkedState - ) - - falseModels.isNotEmpty() -> { - val forkedState = forkIfSat( - state, - newConstraintToOriginalState = unwrappedCondition, - newConstraintToForkedState = notCondition, - stateToCheck = OriginalState - ) - - if (forkedState != null) { - state to forkedState - } else { - null to state - } - } - - else -> error("[trueModels] and [falseModels] are both empty, that has to be impossible by construction!") - } - - return ForkResult(posState, negState) - } - - override fun , Type, Context : UContext<*>> forkMulti( - state: T, - conditions: Iterable, - ): List { - var curState = state - val result = mutableListOf() - for (condition in conditions) { - val unwrappedCondition: UBoolExpr = condition.unwrapJoinedExpr(state.ctx).cast() - val (trueModels, _, _) = splitModelsByCondition(curState.models, unwrappedCondition) - - val nextRoot = if (trueModels.isNotEmpty()) { - val root = curState.clone() - curState.models = trueModels - curState.pathConstraints += unwrappedCondition - - root - } else { - val root = forkIfSat( - curState, - newConstraintToOriginalState = unwrappedCondition, - newConstraintToForkedState = unwrappedCondition.ctx.trueExpr, - stateToCheck = OriginalState - ) - - root - } - - if (nextRoot != null) { - result += curState - curState = nextRoot - } else { - result += null - } - } - - return result - } - - /** - * Checks [newConstraintToOriginalState] or [newConstraintToForkedState], depending on the value of [stateToCheck]. - * Depending on the result of checking this condition, do the following: - * - On [UUnsatResult] - returns `null`; - * - On [UUnknownResult] - adds [newConstraintToOriginalState] to the path constraints of the [state], - * and returns null; - * - On [USatResult] - clones the original state and adds the [newConstraintToForkedState] to it, adds [newConstraintToOriginalState] - * to the original state, sets the satisfiable model to the corresponding state depending on the [stateToCheck], and returns the - * forked state. - * - */ - @Suppress("MoveVariableDeclarationIntoWhen") - private fun , Type, Context : UContext<*>> forkIfSat( - state: T, - newConstraintToOriginalState: UBoolExpr, - newConstraintToForkedState: UBoolExpr, - stateToCheck: StateToCheck, - ): T? { - val constraintsToCheck = state.pathConstraints.clone() - - constraintsToCheck += if (stateToCheck) { - newConstraintToForkedState - } else { - newConstraintToOriginalState - } - val solver = state.ctx.solver() - val satResult = solver.check(constraintsToCheck) - - return when (satResult) { - is UUnsatResult -> null - - is USatResult -> { - // Note that we cannot extract common code here due to - // heavy plusAssign operator in path constraints. - // Therefore, it is better to reuse already constructed [constraintToCheck]. - if (stateToCheck) { - val forkedState = state.clone(constraintsToCheck) - state.pathConstraints += newConstraintToOriginalState - forkedState.models = listOf(satResult.model) - forkedState - } else { - val forkedState = state.clone() - state.pathConstraints += newConstraintToOriginalState - state.models = listOf(satResult.model) - // TODO: implement path condition setter (don't forget to reset UMemoryBase:types!) - forkedState.pathConstraints += newConstraintToForkedState - forkedState - } - } - - is UUnknownResult -> { - state.pathConstraints += if (stateToCheck) newConstraintToOriginalState else newConstraintToForkedState - - null - } - } - } -}