diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt index a48d6c55c..acfc88b86 100644 --- a/usvm-core/src/main/kotlin/org/usvm/State.kt +++ b/usvm-core/src/main/kotlin/org/usvm/State.kt @@ -18,7 +18,7 @@ abstract class UState( open val pathConstraints: UPathConstraints, open val memory: UMemoryBase, open var models: List>, - open var path: PersistentList + open var path: PersistentList, ) { /** * Deterministic state id. @@ -40,67 +40,71 @@ abstract class UState( get() = path.lastOrNull() } -class ForkResult( +data class ForkResult( val positiveState: T?, val negativeState: T?, -) { - operator fun component1(): T? = positiveState - operator fun component2(): T? = negativeState -} +) + +private typealias StateToCheck = Boolean + +private const val ForkedState = true +private const val OriginalState = false /** - * Checks if [conditionToCheck] is satisfiable within path constraints of [state]. - * If it does, clones [state] and returns it with enriched constraints: - * - if [forkToSatisfied], then adds constraint [satisfiedCondition]; - * - if ![forkToSatisfied], then adds constraint [conditionToCheck]. - * Otherwise, returns null. - * If [conditionToCheck] is not unsatisfiable (i.e., solver returns sat or unknown), - * mutates [state] by adding new path constraint c: - * - if [forkToSatisfied], then c = [conditionToCheck] - * - if ![forkToSatisfied], then c = [satisfiedCondition] + * 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], + * iff [addConstraintOnUnknown] is `true`, 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. + * */ private fun , Type, Field> forkIfSat( state: T, - satisfiedCondition: UBoolExpr, - conditionToCheck: UBoolExpr, - forkToSatisfied: Boolean, + newConstraintToOriginalState: UBoolExpr, + newConstraintToForkedState: UBoolExpr, + stateToCheck: StateToCheck, + addConstraintOnUnknown: Boolean = true, ): T? { - val pathConstraints = state.pathConstraints.clone() - pathConstraints += conditionToCheck + val constraintsToCheck = state.pathConstraints.clone() - if (pathConstraints.isFalse) { - return null + constraintsToCheck += if (stateToCheck) { + newConstraintToForkedState + } else { + newConstraintToOriginalState } - - val solver = satisfiedCondition.uctx.solver() - val satResult = solver.check(pathConstraints, useSoftConstraints = true) + val solver = newConstraintToForkedState.uctx.solver() + val satResult = solver.check(constraintsToCheck, useSoftConstraints = true) return when (satResult) { + is UUnsatResult -> null + is USatResult -> { - if (forkToSatisfied) { + // 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) { @Suppress("UNCHECKED_CAST") - val forkedState = state.clone() as T - // TODO: implement path condition setter (don't forget to reset UMemoryBase:types!) - state.pathConstraints += conditionToCheck - state.models = listOf(satResult.model) - forkedState.pathConstraints += satisfiedCondition + val forkedState = state.clone(constraintsToCheck) as T + state.pathConstraints += newConstraintToOriginalState + forkedState.models = listOf(satResult.model) forkedState } else { @Suppress("UNCHECKED_CAST") - val forkedState = state.clone(pathConstraints) as T - state.pathConstraints += satisfiedCondition - forkedState.models = listOf(satResult.model) + val forkedState = state.clone() as T + 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 UUnsatResult -> null - is UUnknownResult -> { - if (forkToSatisfied) { - state.pathConstraints += conditionToCheck - } else { - state.pathConstraints += satisfiedCondition + if (addConstraintOnUnknown) { + state.pathConstraints += newConstraintToOriginalState } null } @@ -148,13 +152,18 @@ fun , Type, Field> fork( trueModels.isNotEmpty() -> state to forkIfSat( state, - condition, - notCondition, - forkToSatisfied = false + newConstraintToOriginalState = condition, + newConstraintToForkedState = notCondition, + stateToCheck = ForkedState ) falseModels.isNotEmpty() -> { - val forkedState = forkIfSat(state, notCondition, condition, forkToSatisfied = true) + val forkedState = forkIfSat( + state, + newConstraintToOriginalState = condition, + newConstraintToForkedState = notCondition, + stateToCheck = OriginalState + ) if (forkedState != null) { state to forkedState @@ -169,3 +178,55 @@ fun , Type, Field> fork( @Suppress("UNCHECKED_CAST") return ForkResult(posState, negState as T?) } + +/** + * Implements symbolic branching on few disjoint conditions. + * + * @return a list of states for each condition - `null` state + * means [UUnknownResult] or [UUnsatResult] of checking condition. + */ +fun , Type, Field> forkMulti( + state: T, + conditions: Iterable, +): List { + var curState = state + val result = mutableListOf() + for (condition in conditions) { + val (trueModels, _) = curState.models.partition { model -> + val holdsInModel = model.eval(condition) + check(holdsInModel is KInterpretedValue) { + "Evaluation in $model on condition $condition: expected true or false, but got $holdsInModel" + } + holdsInModel.isTrue + } + + val nextRoot = if (trueModels.isNotEmpty()) { + @Suppress("UNCHECKED_CAST") + val root = curState.clone() as T + + curState.models = trueModels + curState.pathConstraints += condition + + root + } else { + val root = forkIfSat( + curState, + newConstraintToOriginalState = condition, + newConstraintToForkedState = condition.ctx.trueExpr, + stateToCheck = OriginalState, + addConstraintOnUnknown = false + ) + + root + } + + if (nextRoot != null) { + result += curState + curState = nextRoot + } else { + result += null + } + } + + return result +} diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt index f49fc15c7..c3bd3d6e1 100644 --- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt +++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt @@ -1,24 +1,36 @@ package org.usvm +import org.usvm.StepScope.StepScopeState.CANNOT_BE_PROCESSED +import org.usvm.StepScope.StepScopeState.CAN_BE_PROCESSED +import org.usvm.StepScope.StepScopeState.DEAD + /** * An auxiliary class, which carefully maintains forks and asserts via [fork] and [assert]. * It should be created on every step in an interpreter. * You can think about an instance of [StepScope] as a monad `ExceptT null (State [T])`. * - * An underlying state is `null`, iff one of the `condition`s passed to the [fork] was unsatisfiable. + * This scope is considered as [DEAD], iff the condition in [assert] was unsatisfiable or unknown. + * The underlying state cannot be processed further (see [CANNOT_BE_PROCESSED]), + * if the first passed to [fork] or [forkMulti] condition was unsatisfiable or unknown. * * To execute some function on a state, you should use [doWithState] or [calcOnState]. `null` is returned, when - * the current state is `null`. + * this scope cannot be processed on the current step - see [CANNOT_BE_PROCESSED]. * * @param originalState an initial state. */ class StepScope, Type, Field>( - originalState: T, + private val originalState: T, ) { private val forkedStates = mutableListOf() - private var curState: T? = originalState - var alive: Boolean = true - private set + + private val alive: Boolean get() = stepScopeState != DEAD + private val canProcessFurtherOnCurrentStep: Boolean get() = stepScopeState == CAN_BE_PROCESSED + + /** + * Determines whether we interact this scope on the current step. + * @see [StepScopeState]. + */ + private var stepScopeState: StepScopeState = CAN_BE_PROCESSED /** * @return forked states and the status of initial state. @@ -30,45 +42,54 @@ class StepScope, Type, Field>( * * @return `null` if the underlying state is `null`. */ - fun doWithState(block: T.() -> Unit): Unit? { - val state = curState ?: return null - state.block() - return Unit - } + fun doWithState(block: T.() -> Unit): Unit? = + if (canProcessFurtherOnCurrentStep) { + originalState.block() + } else { + null + } /** * Executes [block] on a state. * * @return `null` if the underlying state is `null`, otherwise returns result of calling [block]. */ - fun calcOnState(block: T.() -> R): R? { - val state = curState ?: return null - return state.block() - } + fun calcOnState(block: T.() -> R): R? = + if (canProcessFurtherOnCurrentStep) { + originalState.block() + } else { + null + } /** * Forks on a [condition], performing [blockOnTrueState] on a state satisfying [condition] and * [blockOnFalseState] on a state satisfying [condition].not(). * - * If the [condition] is unsatisfiable, sets underlying state to `null`. + * If the [condition] is unsatisfiable or unknown, sets the scope state to the [CANNOT_BE_PROCESSED]. * - * @return `null` if the [condition] is unsatisfiable. + * @return `null` if the [condition] is unsatisfiable or unknown. */ fun fork( condition: UBoolExpr, blockOnTrueState: T.() -> Unit = {}, blockOnFalseState: T.() -> Unit = {}, ): Unit? { - val state = curState ?: return null + check(canProcessFurtherOnCurrentStep) - val (posState, negState) = fork(state, condition) + val (posState, negState) = fork(originalState, condition) posState?.blockOnTrueState() - curState = posState + + if (posState == null) { + stepScopeState = CANNOT_BE_PROCESSED + check(negState === originalState) + } else { + check(posState === originalState) + } if (negState != null) { negState.blockOnFalseState() - if (negState !== state) { + if (negState !== originalState) { forkedStates += negState } } @@ -77,23 +98,75 @@ class StepScope, Type, Field>( return posState?.let { } } + /** + * Forks on a few disjoint conditions using `forkMulti` in `State.kt` + * and executes the corresponding block on each not-null state. + * + * NOTE: always sets the [stepScopeState] to the [CANNOT_BE_PROCESSED] value. + */ + fun forkMulti(conditionsWithBlockOnStates: List Unit>>) { + check(canProcessFurtherOnCurrentStep) + + val conditions = conditionsWithBlockOnStates.map { it.first } + + val conditionStates = forkMulti(originalState, conditions) + + val forkedStates = conditionStates.mapIndexedNotNull { idx, positiveState -> + val block = conditionsWithBlockOnStates[idx].second + + positiveState?.apply(block) + } + + stepScopeState = CANNOT_BE_PROCESSED + if (forkedStates.isEmpty()) { + stepScopeState = DEAD + return + } + + val firstForkedState = forkedStates.first() + require(firstForkedState == originalState) { + "The original state $originalState was expected to become the first of forked states but $firstForkedState found" + } + + // Interpret the first state as original and others as forked + this.forkedStates += forkedStates.subList(1, forkedStates.size) + } + fun assert( constraint: UBoolExpr, block: T.() -> Unit = {}, ): Unit? { - val state = curState ?: return null + check(canProcessFurtherOnCurrentStep) - val (posState, _) = fork(state, constraint) + val (posState, _) = fork(originalState, constraint) posState?.block() - curState = posState if (posState == null) { - alive = false + stepScopeState = DEAD } return posState?.let { } } + + /** + * Represents the current state of this [StepScope]. + */ + private enum class StepScopeState { + /** + * Cannot be processed further with any actions. + */ + DEAD, + /** + * Cannot be forked or asserted using [fork], [forkMulti] or [assert], + * but is considered as alive from the Machine's point of view. + */ + CANNOT_BE_PROCESSED, + /** + * Can be forked using [fork] or [forkMulti] and asserted using [assert]. + */ + CAN_BE_PROCESSED; + } } /** diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt index 62846bedb..b2589634a 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt @@ -10,15 +10,19 @@ import org.jacodb.api.cfg.JcArgument import org.jacodb.api.cfg.JcAssignInst import org.jacodb.api.cfg.JcCallInst import org.jacodb.api.cfg.JcCatchInst +import org.jacodb.api.cfg.JcEqExpr import org.jacodb.api.cfg.JcGotoInst import org.jacodb.api.cfg.JcIfInst import org.jacodb.api.cfg.JcInst +import org.jacodb.api.cfg.JcInstList +import org.jacodb.api.cfg.JcInstRef import org.jacodb.api.cfg.JcLocal import org.jacodb.api.cfg.JcLocalVar import org.jacodb.api.cfg.JcReturnInst import org.jacodb.api.cfg.JcSwitchInst import org.jacodb.api.cfg.JcThis import org.jacodb.api.cfg.JcThrowInst +import org.jacodb.api.ext.boolean import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UHeapRef @@ -176,9 +180,29 @@ class JcInterpreter( TODO("Not yet implemented") } - @Suppress("UNUSED_PARAMETER") private fun visitSwitchStmt(scope: JcStepScope, stmt: JcSwitchInst) { - TODO("Not yet implemented") + val exprResolver = exprResolverWithScope(scope) + + val switchKey = stmt.key + // Note that the switch key can be an rvalue, for example, a simple int constant. + val instList = stmt.location.method.instList + + with(ctx) { + val caseStmtsWithConditions = stmt.branches.map { (caseValue, caseTargetStmt) -> + val nextStmt = instList[caseTargetStmt] + val jcEqExpr = JcEqExpr(cp.boolean, switchKey, caseValue) + val caseCondition = exprResolver.resolveJcExpr(jcEqExpr)?.asExpr(boolSort) ?: return + + caseCondition to { state: JcState -> state.newStmt(nextStmt) } + } + + // To make the default case possible, we need to ensure that all case labels are unsatisfiable + val defaultCaseWithCondition = mkAnd( + caseStmtsWithConditions.map { it.first.not() } + ) to { state: JcState -> state.newStmt(instList[stmt.default]) } + + scope.forkMulti(caseStmtsWithConditions + defaultCaseWithCondition) + } } private fun visitThrowStmt(scope: JcStepScope, stmt: JcThrowInst) { @@ -221,6 +245,7 @@ class JcInterpreter( } private val JcInst.nextStmt get() = location.method.instList[location.index + 1] + private operator fun JcInstList.get(instRef: JcInstRef): JcInst = this[instRef.index] private val classInstanceAllocatedRefs = mutableMapOf() diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/controlflow/Switch.java b/usvm-jvm/src/samples/java/org/usvm/samples/controlflow/Switch.java index 19078bc7d..5aeab581b 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/controlflow/Switch.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/controlflow/Switch.java @@ -18,6 +18,25 @@ public int simpleSwitch(int x) { } } + @SuppressWarnings("ConstantConditions") + public int simpleSwitchWithPrecondition(int x) { + if (x == 10 || x == 11) { + return 0; + } + switch (x) { + case 10: + return 10; + case 11: // fall-through + case 12: + return 12; + case 13: + return 13; + default: + return -1; + } + } + + public int lookupSwitch(int x) { switch (x) { case 0: @@ -55,21 +74,20 @@ public int charToIntSwitch(char c) { case 'C': return 100; case 'D': return 500; case 'M': return 1000; - default: throw new IllegalArgumentException("Unrecognized symbol: " + c); + default: throw new IllegalArgumentException(); } } - //TODO: String switch -// public int stringSwitch(String s) { -// switch (s) { -// case "ABC": -// return 1; -// case "DEF": // fall-through -// case "GHJ": -// return 2; -// default: -// return -1; -// } -// } + public int stringSwitch(String s) { + switch (s) { + case "ABC": + return 1; + case "DEF": // fall-through + case "GHJ": + return 2; + default: + return -1; + } + } } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/SwitchTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/SwitchTest.kt index b264e2c06..9d9dd3192 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/SwitchTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/SwitchTest.kt @@ -14,7 +14,6 @@ import java.math.RoundingMode.HALF_UP internal class SwitchTest : JavaMethodTestRunner() { @Test - @Disabled("Not implemented: switch") fun testSimpleSwitch() { checkDiscoveredProperties( Switch::simpleSwitch, @@ -27,7 +26,18 @@ internal class SwitchTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: switch") + fun testSimpleSwitchWithPrecondition() { + checkDiscoveredProperties( + Switch::simpleSwitchWithPrecondition, + ge(4), + { _, x, r -> (x == 10 || x == 11) && r == 0 }, + { _, x, r -> x == 12 && r == 12 }, + { _, x, r -> x == 13 && r == 13 }, + { _, x, r -> x !in 10..13 && r == -1 }, // one for default is enough + ) + } + + @Test fun testLookupSwitch() { checkDiscoveredProperties( Switch::lookupSwitch, @@ -54,4 +64,33 @@ internal class SwitchTest : JavaMethodTestRunner() { { _, m, r -> m !in setOf(HALF_DOWN, HALF_EVEN, HALF_UP, DOWN, CEILING) && r == -1 }, ) } + + @Test + fun testCharToIntSwitch() { + checkDiscoveredPropertiesWithExceptions( + Switch::charToIntSwitch, + ge(8), + { _, c, r -> c == 'I' && r.getOrThrow() == 1 }, + { _, c, r -> c == 'V' && r.getOrThrow() == 5 }, + { _, c, r -> c == 'X' && r.getOrThrow() == 10 }, + { _, c, r -> c == 'L' && r.getOrThrow() == 50 }, + { _, c, r -> c == 'C' && r.getOrThrow() == 100 }, + { _, c, r -> c == 'D' && r.getOrThrow() == 500 }, + { _, c, r -> c == 'M' && r.getOrThrow() == 1000 }, + { _, _, r -> r.exceptionOrNull() is IllegalArgumentException }, + ) + } + + @Test + @Disabled("An operation is not implemented: Not yet implemented. Support strings") + fun testStringSwitch() { + checkDiscoveredProperties( + Switch::stringSwitch, + ge(4), + { _, s, r -> s == "ABC" && r == 1 }, + { _, s, r -> s == "DEF" && r == 2 }, + { _, s, r -> s == "GHJ" && r == 2 }, + { _, _, r -> r == -1 }, + ) + } } \ No newline at end of file diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/CharExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/CharExamplesTest.kt index c630b4d04..d0a5f9a65 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/CharExamplesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/primitives/CharExamplesTest.kt @@ -1,6 +1,5 @@ package org.usvm.samples.primitives -import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq @@ -28,7 +27,6 @@ internal class CharExamplesTest : JavaMethodTestRunner() { } @Test - @Disabled("Not implemented: switch") fun testByteToChar() { checkDiscoveredProperties( CharExamples::byteToChar,