diff --git a/usvm-core/src/main/kotlin/org/usvm/CallStack.kt b/usvm-core/src/main/kotlin/org/usvm/CallStack.kt index 2e62e8bd0..ca615309c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/CallStack.kt +++ b/usvm-core/src/main/kotlin/org/usvm/CallStack.kt @@ -5,6 +5,11 @@ data class UCallStackFrame( val returnSite: Statement?, ) +data class UStackTraceFrame( + val method: Method, + val instruction: Statement, +) + class UCallStack private constructor( private val stack: ArrayDeque>, ) : Collection> by stack { @@ -29,4 +34,24 @@ class UCallStack private constructor( newStack.addAll(stack) return UCallStack(newStack) } + + fun stackTrace(currentInstruction: Statement): List> { + val stacktrace = stack + .asSequence() + .zipWithNext { first, second -> UStackTraceFrame(first.method, second.returnSite!!) } + .toMutableList() + + stacktrace += UStackTraceFrame(stack.last().method, currentInstruction) + + return stacktrace + } + + override fun toString(): String { + var frameCounter = 0 + + return joinToString( + prefix = "Call stack (contains $size frame${if (size > 1) "s" else ""}):${System.lineSeparator()}", + separator = System.lineSeparator() + ) { "\t${frameCounter++}: $it" } + } } diff --git a/usvm-core/src/main/kotlin/org/usvm/Machine.kt b/usvm-core/src/main/kotlin/org/usvm/Machine.kt index 679f65bde..c94db7a7f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Machine.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Machine.kt @@ -64,6 +64,10 @@ abstract class UMachine : AutoCloseable { pathSelector.add(aliveForkedStates) } } + + if (!pathSelector.isEmpty()) { + logger.debug { stopStrategy.stopReason() } + } } } diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt index a48d6c55c..e65ff50ad 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. @@ -38,69 +38,78 @@ abstract class UState( // TODO or last? Do we add a current stmt into the path immediately? val currentStatement: Statement? get() = path.lastOrNull() + + /** + * A property containing information about whether the state is exceptional or not. + */ + abstract val isExceptional: Boolean } -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 +157,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 +183,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-core/src/main/kotlin/org/usvm/ps/ExceptionPropagationPathSelector.kt b/usvm-core/src/main/kotlin/org/usvm/ps/ExceptionPropagationPathSelector.kt new file mode 100644 index 000000000..f29107b14 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/ps/ExceptionPropagationPathSelector.kt @@ -0,0 +1,104 @@ +package org.usvm.ps + +import org.usvm.UPathSelector +import org.usvm.UState +import java.util.IdentityHashMap + +/** + * A class designed to give the highest priority to the states containing exceptions. + */ +class ExceptionPropagationPathSelector>( + private val selector: UPathSelector, +) : UPathSelector { + // An internal queue for states containing exceptions. + // Note that we use an identity map here to be able + // to determine whether some state is already in the queue or not + // without extra time consumption. + // We use only keys from this map. + private val exceptionalStates = IdentityHashMap() + + // An identity map of the states that were added in the internal selector. + // That means that these states present not only in the internal queue, but in + // the queue of the selector, and we have to process them as well. + // We use only keys from this map. + private val statesInSelector = IdentityHashMap() + + override fun isEmpty(): Boolean = exceptionalStates.isEmpty() && selector.isEmpty() + + /** + * Returns an exceptional state from the internal queue if it is not empty, or + * the result of [peek] method called on the wrapper selector. + */ + override fun peek(): State = exceptionalStates.keys.lastOrNull() ?: selector.peek() + + override fun update(state: State) { + val alreadyInExceptionalStates = state in exceptionalStates + val isExceptional = state.isExceptional + + when { + // A case when the state became exceptional, but at the + // previous step it didn't contain any exceptions. + // We add this exceptional state to the internal queue. + isExceptional && !alreadyInExceptionalStates -> { + exceptionalStates += state to null + } + // A case when the state contained an exception at the previous step, + // but it doesn't contain it anymore. There are two possibilities: + // this state was either added directly in the internal queue, + // e.g., after a fork operation, or was transformed from a regular one. + // In the first case, we have to add it to the selector and remove from the + // exceptional queue, in the second one just removal is enough since + // it was added in the selector earlier. + !isExceptional && alreadyInExceptionalStates -> { + exceptionalStates -= state + + if (state !in statesInSelector) { + selector.add(listOf(state)) + statesInSelector += state to null + } + } + + // Other operations don't cause queues transformations. + else -> Unit // do nothing + } + + // If the state is contained in the selector, we must call `update` operation for it. + if (state in statesInSelector) { + selector.update(state) + } + } + + /** + * Add the [states] in the selector. Depending on whether it + * is exceptional or not, it will be added in the exceptional + * state queue or in the wrapper selector. + */ + override fun add(states: Collection) { + val statesToAdd = mutableListOf() + + states.forEach { + // It if it is an exceptional state, we don't have to worry whether it + // is contains in the selector or not. It was either already added in it, + // or will be added later if required, when it becomes unexceptional one. + if (it.isExceptional) { + exceptionalStates += it to null + } else { + // Otherwise, we simply add it to the selector directly. + statesToAdd += it + statesInSelector += it to null + } + } + + selector.add(statesToAdd) + } + + override fun remove(state: State) { + if (state in exceptionalStates) { + exceptionalStates -= state + } + + if (state in statesInSelector) { + selector.remove(state) + } + } +} diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt index f848664aa..0db86489e 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt @@ -8,8 +8,8 @@ import org.usvm.UState import org.usvm.statistics.CoverageStatistics import org.usvm.statistics.DistanceStatistics import org.usvm.statistics.PathsTreeStatistics -import org.usvm.util.RandomizedPriorityCollection import org.usvm.util.DeterministicPriorityCollection +import org.usvm.util.RandomizedPriorityCollection import kotlin.math.max import kotlin.random.Random @@ -18,8 +18,8 @@ fun > createPathSelec options: UMachineOptions, pathsTreeStatistics: () -> PathsTreeStatistics? = { null }, coverageStatistics: () -> CoverageStatistics? = { null }, - distanceStatistics: () -> DistanceStatistics? = { null } -) : UPathSelector { + distanceStatistics: () -> DistanceStatistics? = { null }, +): UPathSelector { val strategies = options.pathSelectionStrategies require(strategies.isNotEmpty()) { "At least one path selector strategy should be specified" } @@ -30,22 +30,26 @@ fun > createPathSelec PathSelectionStrategy.BFS -> BfsPathSelector() PathSelectionStrategy.DFS -> DfsPathSelector() PathSelectionStrategy.RANDOM_PATH -> RandomTreePathSelector( - requireNotNull(pathsTreeStatistics()) { "Paths tree statistics is required for random tree path selector" }, - { random.nextInt(0, Int.MAX_VALUE) } + pathsTreeStatistics = requireNotNull(pathsTreeStatistics()) { "Paths tree statistics is required for random tree path selector" }, + randomNonNegativeInt = { random.nextInt(0, Int.MAX_VALUE) } ) + PathSelectionStrategy.DEPTH -> createDepthPathSelector() PathSelectionStrategy.DEPTH_RANDOM -> createDepthPathSelector(random) PathSelectionStrategy.FORK_DEPTH -> createForkDepthPathSelector( requireNotNull(pathsTreeStatistics()) { "Paths tree statistics is required for fork depth path selector" } ) + PathSelectionStrategy.FORK_DEPTH_RANDOM -> createForkDepthPathSelector( requireNotNull(pathsTreeStatistics()) { "Paths tree statistics is required for fork depth path selector" }, random ) + PathSelectionStrategy.CLOSEST_TO_UNCOVERED -> createClosestToUncoveredPathSelector( requireNotNull(coverageStatistics()) { "Coverage statistics is required for closest to uncovered path selector" }, requireNotNull(distanceStatistics()) { "Distance statistics is required for closest to uncovered path selector" } ) + PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM -> createClosestToUncoveredPathSelector( requireNotNull(coverageStatistics()) { "Coverage statistics is required for closest to uncovered path selector" }, requireNotNull(distanceStatistics()) { "Distance statistics is required for closest to uncovered path selector" }, @@ -54,71 +58,107 @@ fun > createPathSelec } } - if (selectors.size == 1) { - val selector = selectors.single() - selector.add(listOf(initialState)) - return selector + val propagateExceptions = options.exceptionsPropagation + + selectors.singleOrNull()?.let { selector -> + val resultSelector = selector.wrapIfRequired(propagateExceptions) + resultSelector.add(listOf(initialState)) + return resultSelector } - return when (options.pathSelectorCombinationStrategy) { + require(selectors.size >= 2) { "Cannot create collaborative path selector from less than 2 selectors" } + + val selector = when (options.pathSelectorCombinationStrategy) { PathSelectorCombinationStrategy.INTERLEAVED -> { - val interleavedPathSelector = InterleavedPathSelector(selectors) + // Since all selectors here work as one, we can wrap an interleaved selector only. + val interleavedPathSelector = InterleavedPathSelector(selectors).wrapIfRequired(propagateExceptions) interleavedPathSelector.add(listOf(initialState)) interleavedPathSelector } + PathSelectorCombinationStrategy.PARALLEL -> { - selectors.first().add(listOf(initialState)) - selectors.drop(1).forEach { + // Here we should wrap all selectors independently since they work in parallel. + val wrappedSelectors = selectors.map { it.wrapIfRequired(propagateExceptions) } + + wrappedSelectors.first().add(listOf(initialState)) + wrappedSelectors.drop(1).forEach { @Suppress("UNCHECKED_CAST") it.add(listOf(initialState.clone() as State)) } - ParallelPathSelector(selectors) + + ParallelPathSelector(wrappedSelectors) } } + + return selector } +/** + * Wraps the selector into an [ExceptionPropagationPathSelector] if [propagateExceptions] is true. + */ +private fun > UPathSelector.wrapIfRequired(propagateExceptions: Boolean) = + if (propagateExceptions && this !is ExceptionPropagationPathSelector) { + ExceptionPropagationPathSelector(this) + } else { + this + } + private fun > compareById(): Comparator = compareBy { it.id } private fun > createDepthPathSelector(random: Random? = null): UPathSelector { if (random == null) { - return WeightedPathSelector({ DeterministicPriorityCollection(Comparator.naturalOrder()) }) { it.path.size } + return WeightedPathSelector( + priorityCollectionFactory = { DeterministicPriorityCollection(Comparator.naturalOrder()) }, + weighter = { it.path.size } + ) } // Notice: random never returns 1.0 - return WeightedPathSelector({ RandomizedPriorityCollection(compareById()) { random.nextDouble() } }) { 1.0 / max(it.path.size, 1) } + return WeightedPathSelector( + priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } }, + weighter = { 1.0 / max(it.path.size, 1) } + ) } private fun > createClosestToUncoveredPathSelector( coverageStatistics: CoverageStatistics, distanceStatistics: DistanceStatistics, - random: Random? = null + random: Random? = null, ): UPathSelector { val weighter = ShortestDistanceToTargetsStateWeighter( - coverageStatistics.getUncoveredStatements(), - distanceStatistics::getShortestCfgDistance, - distanceStatistics::getShortestCfgDistanceToExitPoint + targets = coverageStatistics.getUncoveredStatements(), + getCfgDistance = distanceStatistics::getShortestCfgDistance, + getCfgDistanceToExitPoint = distanceStatistics::getShortestCfgDistanceToExitPoint ) coverageStatistics.addOnCoveredObserver { _, method, statement -> weighter.removeTarget(method, statement) } if (random == null) { - return WeightedPathSelector({ DeterministicPriorityCollection(Comparator.naturalOrder()) }, weighter) + return WeightedPathSelector( + priorityCollectionFactory = { DeterministicPriorityCollection(Comparator.naturalOrder()) }, + weighter = weighter + ) } - return WeightedPathSelector({ RandomizedPriorityCollection(compareById()) { random.nextDouble() } }) { - 1.0 / max(weighter.weight(it).toDouble(), 1.0) - } + return WeightedPathSelector( + priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } }, + weighter = { 1.0 / max(weighter.weight(it).toDouble(), 1.0) } + ) } private fun > createForkDepthPathSelector( pathsTreeStatistics: PathsTreeStatistics, - random: Random? = null + random: Random? = null, ): UPathSelector { if (random == null) { - return WeightedPathSelector({ DeterministicPriorityCollection(Comparator.naturalOrder()) }) { pathsTreeStatistics.getStateDepth(it) } + return WeightedPathSelector( + priorityCollectionFactory = { DeterministicPriorityCollection(Comparator.naturalOrder()) }, + weighter = { pathsTreeStatistics.getStateDepth(it) } + ) } - return WeightedPathSelector({ RandomizedPriorityCollection(compareById()) { random.nextDouble() } }) { - 1.0 / max(pathsTreeStatistics.getStateDepth(it).toDouble(), 1.0) - } + return WeightedPathSelector( + priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } }, + weighter = { 1.0 / max(pathsTreeStatistics.getStateDepth(it).toDouble(), 1.0) } + ) } diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt index 5acbcc54a..402b1afd0 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt @@ -29,14 +29,30 @@ class CoverageStatistics() as MutableSet) { acc, stmt -> acc.add(stmt); acc } - uncoveredStatements[method] = methodStatements - totalUncoveredStatements += methodStatements.size - coveredStatements[method] = HashSet() + addCoverageZone(method) } } + /** + * Adds a new zone of coverage retrieved from the method. + * This method might be useful to add coverage zones dynamically, + * e.g., like in the [TransitiveCoverageZoneObserver]. + */ + fun addCoverageZone(method: Method) { + if (method in uncoveredStatements) return + + val methodStatements = bfsTraversal( + applicationGraph.entryPoints(method).toList(), + applicationGraph::successors + ).fold(ConcurrentHashMap.newKeySet() as MutableSet) { acc, stmt -> + acc.add(stmt); acc + } + + uncoveredStatements[method] = methodStatements + totalUncoveredStatements += methodStatements.size + coveredStatements[method] = HashSet() + } + private fun computeCoverage(covered: Int, uncovered: Int): Float { if (uncovered == 0) { return 100f diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/TransitiveCoverageZoneObserver.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/TransitiveCoverageZoneObserver.kt new file mode 100644 index 000000000..81387dd54 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/TransitiveCoverageZoneObserver.kt @@ -0,0 +1,30 @@ +package org.usvm.statistics + +/** + * Adds new coverage zones if some state contains an instruction + * that doesn't belong to any of the already known coverage zones. + * + * [ignoreMethod] is a predicate allowing to filter out some methods, + * e.g., the ones that belong to the system libraries. + */ +class TransitiveCoverageZoneObserver( + initialMethod: Method, + private val methodExtractor: (State) -> Method, + private val addCoverageZone: (Method) -> Unit, + private val ignoreMethod: (Method) -> Boolean, +) : UMachineObserver { + private val collectedMethods: MutableSet = mutableSetOf(initialMethod) + + override fun onState(parent: State, forks: Sequence) { + addInstructionsToCover(parent) + forks.forEach { addInstructionsToCover(it) } + } + + private fun addInstructionsToCover(state: State) { + val method = methodExtractor(state) + if (method in collectedMethods || ignoreMethod(method)) return + + collectedMethods += method + addCoverageZone(method) + } +} \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt index 29e11abfb..e2d428741 100644 --- a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt +++ b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt @@ -7,6 +7,6 @@ class StepLimitStopStrategy(private val limit: ULong) : StopStrategy { private var counter = 0UL override fun shouldStop(): Boolean { - return counter++ < limit + return counter++ > limit } } diff --git a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepsFromLastCoveredStopStrategy.kt b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepsFromLastCoveredStopStrategy.kt new file mode 100644 index 000000000..df3860f36 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepsFromLastCoveredStopStrategy.kt @@ -0,0 +1,23 @@ +package org.usvm.stopstrategies + +/** + * A stop strategy that checks how many steps were made since the last collected states. + */ +class StepsFromLastCoveredStopStrategy( + private val limit: ULong, + private val collectedStateCount: () -> Int, +) : StopStrategy { + private var counter = 0UL + private var lastStatesCounter = collectedStateCount() + + override fun shouldStop(): Boolean { + val collectedStates = collectedStateCount() + + if (collectedStates > lastStatesCounter) { + counter = 0UL + lastStatesCounter = collectedStates + } + + return counter++ > limit + } +} \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategy.kt b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategy.kt index 3fcdc37f4..43626088f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategy.kt +++ b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategy.kt @@ -9,12 +9,18 @@ fun interface StopStrategy { * If true, symbolic execution process is terminated. */ fun shouldStop(): Boolean + + fun stopReason(): String = "Stop reason: ${this::class.simpleName ?: this}" } class GroupedStopStrategy( - private val strategies: List + private val strategies: List, ) : StopStrategy { constructor(vararg strategies: StopStrategy) : this(strategies.toList()) override fun shouldStop() = strategies.any { it.shouldStop() } + + override fun stopReason(): String = strategies + .filter { it.shouldStop() } + .joinToString(prefix = "Stop reasons: ", separator = ", ") { "${it::class.simpleName ?: it}" } } diff --git a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategyFactory.kt b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategyFactory.kt index 9c6c0ccc5..f1e78d344 100644 --- a/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategyFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/stopstrategies/StopStrategyFactory.kt @@ -6,7 +6,7 @@ import org.usvm.statistics.CoverageStatistics fun createStopStrategy( options: UMachineOptions, coverageStatistics: () -> CoverageStatistics<*, *, *>? = { null }, - getCollectedStatesCount: (() -> Int)? = null + getCollectedStatesCount: (() -> Int)? = null, ) : StopStrategy { val stopStrategies = mutableListOf() @@ -15,19 +15,34 @@ fun createStopStrategy( stopStrategies.add(StepLimitStopStrategy(stepLimit)) } if (options.stopOnCoverage in 1..100) { - val coverageStatisticsValue = requireNotNull(coverageStatistics()) { "Coverage statistics is required for stopping on expected coverage achieved" } - stopStrategies.add(StopStrategy { coverageStatisticsValue.getTotalCoverage() >= options.stopOnCoverage }) + val coverageStatisticsValue = requireNotNull(coverageStatistics()) { + "Coverage statistics is required for stopping on expected coverage achieved" + } + val coverageStopStrategy = StopStrategy { coverageStatisticsValue.getTotalCoverage() >= options.stopOnCoverage } + stopStrategies.add(coverageStopStrategy) } val collectedStatesLimit = options.collectedStatesLimit if (collectedStatesLimit != null && collectedStatesLimit > 0) { - requireNotNull(getCollectedStatesCount) { "Collected states count getter is required for stopping on collected states limit" } - stopStrategies.add(StopStrategy { getCollectedStatesCount() >= collectedStatesLimit }) + requireNotNull(getCollectedStatesCount) { + "Collected states count getter is required for stopping on collected states limit" + } + val collectedStatesCountStopStrategy = StopStrategy { getCollectedStatesCount() >= collectedStatesLimit } + stopStrategies.add(collectedStatesCountStopStrategy) } val timeoutMs = options.timeoutMs if (timeoutMs != null) { stopStrategies.add(TimeoutStopStrategy(timeoutMs, System::currentTimeMillis)) } + val stepsFromLastCovered = options.stepsFromLastCovered + if (stepsFromLastCovered != null && getCollectedStatesCount != null) { + val stepsFromLastCoveredStopStrategy = StepsFromLastCoveredStopStrategy( + stepsFromLastCovered.toULong(), + getCollectedStatesCount + ) + stopStrategies.add(stepsFromLastCoveredStopStrategy) + } + if (stopStrategies.isEmpty()) { return StopStrategy { false } } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt index 46c6b400d..63513aa8f 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt @@ -45,7 +45,6 @@ import org.usvm.machine.extractLong import org.usvm.machine.extractShort import org.usvm.machine.state.JcMethodResult import org.usvm.machine.state.JcState -import org.usvm.machine.state.WrappedException import org.usvm.machine.state.localIdx import org.usvm.memory.UReadOnlySymbolicMemory import org.usvm.model.UModelBase @@ -79,7 +78,7 @@ class JcTestResolver( val result = when (val res = state.methodResult) { is JcMethodResult.NoCall -> error("No result found") is JcMethodResult.Success -> with(afterScope) { Result.success(resolveExpr(res.value, method.returnType)) } - is JcMethodResult.Exception -> Result.failure(resolveException(res.exception)) + is JcMethodResult.JcException -> Result.failure(resolveException(res, afterScope)) } val coverage = resolveCoverage(method, state) @@ -92,11 +91,12 @@ class JcTestResolver( ) } - private fun resolveException(exception: Exception): Throwable = - when (exception) { - is WrappedException -> Reflection.allocateInstance(classLoader.loadClass(exception.name)) as Throwable - else -> exception - } + private fun resolveException( + exception: JcMethodResult.JcException, + afterMemory: MemoryScope + ): Throwable = with(afterMemory) { + resolveExpr(exception.address, exception.type) as Throwable + } @Suppress("UNUSED_PARAMETER") private fun resolveCoverage(method: JcTypedMethod, state: JcState): JcCoverage { @@ -231,11 +231,15 @@ class JcTestResolver( val instance = Reflection.allocateInstance(clazz) resolvedCache[ref.address] = instance + // TODO skips throwable construction for now + if (instance is Throwable) { + return instance + } + val fields = generateSequence(type.jcClass) { it.superClass } .map { it.toType() } .flatMap { it.declaredFields } .filter { !it.isStatic } - for (field in fields) { val lvalue = UFieldLValue(ctx.typeToSort(field.fieldType), heapRef, field.field) val fieldValue = resolveLValue(lvalue, field.fieldType) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt index 9a6d3dd54..f0a0e2bb4 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt @@ -11,7 +11,6 @@ import org.jacodb.impl.features.SyncUsagesExtension import org.usvm.statistics.ApplicationGraph import java.util.concurrent.ConcurrentHashMap -// TODO: add trap handlers /** * A [JcApplicationGraphImpl] wrapper. */ diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt index ecd1c9055..90aca0059 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt @@ -1,6 +1,5 @@ package org.usvm.machine -import io.ksmt.expr.KBitVec32Value import io.ksmt.utils.asExpr import io.ksmt.utils.cast import org.jacodb.api.JcArrayType @@ -100,8 +99,8 @@ import org.usvm.machine.operator.wideTo32BitsIfNeeded import org.usvm.machine.state.JcMethodResult import org.usvm.machine.state.JcState import org.usvm.machine.state.addNewMethodCall -import org.usvm.machine.state.lastStmt -import org.usvm.machine.state.throwException +import org.usvm.machine.state.throwExceptionWithoutStackFrameDrop +import org.usvm.util.extractJcRefType /** * An expression resolver based on JacoDb 3-address code. A result of resolving is `null`, iff @@ -398,7 +397,7 @@ class JcExprResolver( null } - is JcMethodResult.Exception -> error("Exception should be handled earlier") + is JcMethodResult.JcException -> error("Exception should be handled earlier") } } @@ -542,15 +541,17 @@ class JcExprResolver( // region implicit exceptions + private fun allocateException(type: JcRefType): (JcState) -> Unit = { state -> + val address = state.memory.alloc(type) + state.throwExceptionWithoutStackFrameDrop(address, type) + } + private fun checkArrayIndex(idx: USizeExpr, length: USizeExpr) = with(ctx) { val inside = (mkBvSignedLessOrEqualExpr(mkBv(0), idx)) and (mkBvSignedLessExpr(idx, length)) scope.fork( inside, - blockOnFalseState = { - val exception = ArrayIndexOutOfBoundsException((models.first().eval(idx) as KBitVec32Value).intValue) - throwException(exception) - } + blockOnFalseState = allocateException(arrayIndexOutOfBoundsExceptionType) ) } @@ -559,28 +560,21 @@ class JcExprResolver( val lengthIsNonNegative = mkBvSignedLessOrEqualExpr(mkBv(0), length) - scope.fork(lengthIsNonNegative, - blockOnFalseState = { - val ln = lastStmt.lineNumber - val exception = NegativeArraySizeException("[negative array size] $ln") - throwException(exception) - } + scope.fork( + lengthIsNonNegative, + blockOnFalseState = allocateException(negativeArraySizeExceptionType) ) } - private fun checkDivisionByZero(expr: UExpr) = with(ctx) { val sort = expr.sort if (sort !is UBvSort) { return Unit } val neqZero = mkEq(expr.cast(), mkBv(0, sort)).not() - scope.fork(neqZero, - blockOnFalseState = { - val ln = lastStmt.lineNumber - val exception = ArithmeticException("[division by zero] $ln") - throwException(exception) - } + scope.fork( + neqZero, + blockOnFalseState = allocateException(arithmeticExceptionType) ) } @@ -588,11 +582,7 @@ class JcExprResolver( val neqNull = mkHeapRefEq(ref, nullRef).not() scope.fork( neqNull, - blockOnFalseState = { - val ln = lastStmt.lineNumber - val exception = NullPointerException("[null pointer dereference] $ln") - throwException(exception) - } + blockOnFalseState = allocateException(nullPointerExceptionType) ) } @@ -672,11 +662,7 @@ class JcExprResolver( ?: return null scope.fork( isExpr, - blockOnFalseState = { - val ln = lastStmt.lineNumber - val exception = ClassCastException("[class cast exception] $ln") - throwException(exception) - } + blockOnFalseState = allocateException(classCastExceptionType) ) ?: return null expr } else { @@ -737,6 +723,26 @@ class JcExprResolver( return block(result0, result1) } + private val arrayIndexOutOfBoundsExceptionType by lazy { + ctx.extractJcRefType(IndexOutOfBoundsException::class) + } + + private val negativeArraySizeExceptionType by lazy { + ctx.extractJcRefType(NegativeArraySizeException::class) + } + + private val arithmeticExceptionType by lazy { + ctx.extractJcRefType(ArithmeticException::class) + } + + private val nullPointerExceptionType by lazy { + ctx.extractJcRefType(NullPointerException::class) + } + + private val classCastExceptionType by lazy { + ctx.extractJcRefType(ClassCastException::class) + } + companion object { /** * Synthetic field to track static field initialization state. 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..1ff9d28f8 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt @@ -10,30 +10,35 @@ 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.UBoolExpr import org.usvm.UHeapRef import org.usvm.UInterpreter import org.usvm.URegisterLValue import org.usvm.machine.state.JcMethodResult import org.usvm.machine.state.JcState -import org.usvm.machine.state.WrappedException import org.usvm.machine.state.addEntryMethodCall import org.usvm.machine.state.lastStmt import org.usvm.machine.state.localIdx import org.usvm.machine.state.newStmt import org.usvm.machine.state.parametersWithThisCount import org.usvm.machine.state.returnValue -import org.usvm.machine.state.throwException +import org.usvm.machine.state.throwExceptionAndDropStackFrame +import org.usvm.machine.state.throwExceptionWithoutStackFrameDrop import org.usvm.solver.USatResult typealias JcStepScope = StepScope @@ -93,8 +98,8 @@ class JcInterpreter( // handle exception firstly val result = state.methodResult - if (result is JcMethodResult.Exception) { - handleException(scope, result.exception, stmt) + if (result is JcMethodResult.JcException) { + handleException(scope, result, stmt) return scope.stepResult() } @@ -114,12 +119,49 @@ class JcInterpreter( private fun handleException( scope: JcStepScope, - exception: Exception, + exception: JcMethodResult.JcException, lastStmt: JcInst, ) { - applicationGraph.successors(lastStmt) // TODO: check catchers for lastStmt + val catchStatements = applicationGraph.successors(lastStmt).filterIsInstance().toList() - scope.calcOnState { throwException(exception) } + val typeConstraintsNegations = mutableListOf() + val catchForks = mutableListOf Unit>>() + + val blockToFork: (JcCatchInst) -> (JcState) -> Unit = { catchInst: JcCatchInst -> + block@{ state: JcState -> + val lValue = exprResolverWithScope(scope).resolveLValue(catchInst.throwable) ?: return@block + val exceptionResult = state.methodResult as JcMethodResult.JcException + + state.memory.write(lValue, exceptionResult.address) + + state.methodResult = JcMethodResult.NoCall + state.newStmt(catchInst.nextStmt) + } + } + + catchStatements.forEach { catchInst -> + val throwableTypes = catchInst.throwableTypes + + val typeConstraint = scope.calcOnState { + val currentTypeConstraints = throwableTypes.map { memory.types.evalIs(exception.address, it) } + val result = ctx.mkAnd(typeConstraintsNegations + ctx.mkOr(currentTypeConstraints)) + + typeConstraintsNegations += currentTypeConstraints.map { ctx.mkNot(it) } + + result + } ?: return@forEach + + catchForks += typeConstraint to blockToFork(catchInst) + } + + val typeConditionToMiss = ctx.mkAnd(typeConstraintsNegations) + val functionBlockOnMiss = block@{ _: JcState -> + scope.calcOnState { throwExceptionAndDropStackFrame() } ?: return@block + } + + val catchSectionMiss = typeConditionToMiss to functionBlockOnMiss + + scope.forkMulti(catchForks + catchSectionMiss) } private fun visitAssignInst(scope: JcStepScope, stmt: JcAssignInst) { @@ -173,17 +215,40 @@ class JcInterpreter( @Suppress("UNUSED_PARAMETER") private fun visitCatchStmt(scope: JcStepScope, stmt: JcCatchInst) { - TODO("Not yet implemented") + error("The catch instruction must be unfolded during processing of the instructions led to it. Encountered inst: $stmt") } - @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) { + val resolver = exprResolverWithScope(scope) + val address = resolver.resolveJcExpr(stmt.throwable)?.asExpr(ctx.addressSort) ?: return + scope.calcOnState { - throwException(WrappedException(stmt.throwable.type.typeName)) + throwExceptionWithoutStackFrameDrop(address, stmt.throwable.type) } } @@ -221,6 +286,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/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt index 9a7c11a76..a70ce3945 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt @@ -11,12 +11,14 @@ import org.usvm.UMachine import org.usvm.UMachineOptions import org.usvm.machine.state.JcMethodResult import org.usvm.machine.state.JcState +import org.usvm.machine.state.lastStmt import org.usvm.ps.createPathSelector import org.usvm.statistics.CompositeUMachineObserver import org.usvm.statistics.CoverageStatistics import org.usvm.statistics.CoveredNewStatesCollector import org.usvm.statistics.DistanceStatistics import org.usvm.statistics.PathsTreeStatistics +import org.usvm.statistics.TransitiveCoverageZoneObserver import org.usvm.statistics.UMachineObserver import org.usvm.stopstrategies.createStopStrategy @@ -48,13 +50,17 @@ class JcMachine( val methodsToTrackCoverage = when (options.coverageZone) { CoverageZone.METHOD -> setOf(method) + CoverageZone.TRANSITIVE -> setOf(method) // TODO: more adequate method filtering. !it.isConstructor is used to exclude default constructor which is often not covered CoverageZone.CLASS -> method.enclosingClass.methods.filter { it.enclosingClass == method.enclosingClass && !it.isConstructor }.toSet() } - val coverageStatistics: CoverageStatistics = CoverageStatistics(methodsToTrackCoverage, applicationGraph) + val coverageStatistics: CoverageStatistics = CoverageStatistics( + methodsToTrackCoverage, + applicationGraph + ) val pathsTreeStatistics = PathsTreeStatistics(initialState) val pathSelector = createPathSelector( @@ -65,13 +71,31 @@ class JcMachine( { distanceStatistics } ) - val statesCollector = CoveredNewStatesCollector(coverageStatistics) { it.methodResult is JcMethodResult.Exception } - val stopStrategy = createStopStrategy(options, { coverageStatistics }, { statesCollector.collectedStates.size }) + val statesCollector = CoveredNewStatesCollector(coverageStatistics) { + it.methodResult is JcMethodResult.JcException + } + val stopStrategy = createStopStrategy( + options, + coverageStatistics = { coverageStatistics }, + getCollectedStatesCount = { statesCollector.collectedStates.size } + ) val observers = mutableListOf>(coverageStatistics) + if (!disablePathsTreeStatistics) { observers.add(pathsTreeStatistics) } + + if (options.coverageZone == CoverageZone.TRANSITIVE) { + observers.add( + TransitiveCoverageZoneObserver( + initialMethod = method, + methodExtractor = { state -> state.lastStmt.location.method }, + addCoverageZone = { coverageStatistics.addCoverageZone(it) }, + ignoreMethod = { false } // TODO replace with a configurable setting + ) + ) + } observers.add(statesCollector) run( @@ -86,7 +110,7 @@ class JcMachine( } private fun isStateTerminated(state: JcState): Boolean { - return state.callStack.isEmpty() || state.methodResult is JcMethodResult.Exception + return state.callStack.isEmpty() } override fun close() { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcMethodResult.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcMethodResult.kt index 7de5d9cdc..f0f05b266 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcMethodResult.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcMethodResult.kt @@ -1,8 +1,12 @@ package org.usvm.machine.state import org.jacodb.api.JcMethod +import org.jacodb.api.JcType +import org.jacodb.api.cfg.JcInst import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.UStackTraceFrame /** * Represents a result of a method invocation. @@ -18,19 +22,17 @@ sealed interface JcMethodResult { */ class Success( val method: JcMethod, - val value: UExpr + val value: UExpr, ) : JcMethodResult /** - * A method threw an [exception]. + * A method threw an exception with [type] type. */ - class Exception( - val exception: kotlin.Exception - ) : JcMethodResult - + open class JcException( + val address: UHeapRef, + val type: JcType, + val symbolicStackTrace: List> + ) : JcMethodResult { + override fun toString(): String = "${this::class.simpleName}: Address: $address, type: ${type.typeName}" + } } - -// TODO: stub for symbolic exceptions -class WrappedException( - val name: String -) : kotlin.Exception() diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt index 68a809660..58dff6176 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt @@ -10,7 +10,6 @@ import org.usvm.UCallStack import org.usvm.UContext import org.usvm.UState import org.usvm.constraints.UPathConstraints -import org.usvm.machine.JcContext import org.usvm.memory.UMemoryBase import org.usvm.model.UModelBase @@ -42,4 +41,13 @@ class JcState( methodResult, ) } + + override val isExceptional: Boolean + get() = methodResult is JcMethodResult.JcException + + override fun toString(): String = buildString { + appendLine("Instruction: $lastStmt") + if (isExceptional) appendLine("Exception: $methodResult") + appendLine(callStack) + } } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt index 77e16548c..342520e28 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt @@ -1,10 +1,12 @@ package org.usvm.machine.state import org.jacodb.api.JcMethod +import org.jacodb.api.JcType import org.jacodb.api.cfg.JcArgument import org.jacodb.api.cfg.JcInst import org.jacodb.api.ext.cfg.locals import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort import org.usvm.machine.JcApplicationGraph @@ -28,16 +30,24 @@ fun JcState.returnValue(valueToReturn: UExpr) { } } -fun JcState.throwException(exception: Exception) { +/** + * Create an unprocessed exception with the [address] and the [type] and assign it to the [JcState.methodResult]. + */ +fun JcState.throwExceptionWithoutStackFrameDrop(address: UHeapRef, type: JcType) { + methodResult = JcMethodResult.JcException(address, type, callStack.stackTrace(lastStmt)) +} + +fun JcState.throwExceptionAndDropStackFrame() { + // Exception is allowed to be thrown only after + // it is created via `throwExceptionWithoutStackFrameDrop` function + require(methodResult is JcMethodResult.JcException) + // TODO: think about it later val returnSite = callStack.pop() if (callStack.isNotEmpty()) { memory.stack.pop() } - // TODO: the last place where we distinguish implicitly thrown and explicitly thrown exceptions - methodResult = JcMethodResult.Exception(exception) - if (returnSite != null) { newStmt(returnSite) } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt new file mode 100644 index 000000000..007450ac0 --- /dev/null +++ b/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt @@ -0,0 +1,10 @@ +package org.usvm.util + +import org.jacodb.api.JcRefType +import org.jacodb.api.JcType +import org.usvm.machine.JcContext +import kotlin.reflect.KClass + +fun JcContext.extractJcType(clazz: KClass<*>): JcType = cp.findTypeOrNull(clazz.qualifiedName!!)!! + +fun JcContext.extractJcRefType(clazz: KClass<*>): JcRefType = extractJcType(clazz) as JcRefType \ No newline at end of file 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/samples/java/org/usvm/samples/exceptions/ExceptionExamples.java b/usvm-jvm/src/samples/java/org/usvm/samples/exceptions/ExceptionExamples.java index ee56df141..09c2d9318 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/exceptions/ExceptionExamples.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/exceptions/ExceptionExamples.java @@ -1,5 +1,7 @@ package org.usvm.samples.exceptions; +import java.nio.file.InvalidPathException; + public class ExceptionExamples { public int initAnArray(int n) { try { @@ -32,14 +34,14 @@ public int doNotCatchNested(int i) { private int checkAll(int i) { if (i < 0) { - throw new IllegalArgumentException("Negative"); + throw new IllegalArgumentException(); } return checkPositive(i); } private int checkPositive(int i) { if (i > 0) { - throw new NullPointerException("Positive"); + throw new NullPointerException(); } return 0; } @@ -51,7 +53,7 @@ public int finallyThrowing(int i) { } catch (NullPointerException e) { throw e; } finally { - throw new IllegalStateException("finally"); + throw new IllegalStateException(); } } @@ -99,7 +101,7 @@ public int catchExceptionAfterOtherPossibleException(int i) { } public IllegalArgumentException createException() { - return new IllegalArgumentException("Here we are: " + Math.sqrt(10)); + return new IllegalArgumentException(); } public int hangForSeconds(int seconds) throws InterruptedException { @@ -119,8 +121,28 @@ private int callNestedWithThrow(int i) { private int nestedWithThrow(int i) { if (i < 0) { - throw new IllegalArgumentException("Negative"); + throw new IllegalArgumentException(); } return i; } + + public int symbolicExceptionCheck(Exception e) { + try { + throw e; + } catch (NumberFormatException | InvalidPathException exception) { + if (e instanceof NumberFormatException) { + return 1; + } + + return 2; + } catch (RuntimeException exception) { + if (e instanceof NumberFormatException) { + return -1; // unreachable + } + + return 3; + } catch (Exception exception) { + return 4; + } + } } \ No newline at end of file diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/mock/MockStaticFieldExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/mock/MockStaticFieldExample.java index 597a6cba0..18a51add2 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/mock/MockStaticFieldExample.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/mock/MockStaticFieldExample.java @@ -20,7 +20,6 @@ public int calculate(int threshold) { return a + b + 1; } - // This test is associated with https://github.com/UnitTestBot/UTBotJava/issues/1533 public int checkMocksInLeftAndRightAssignPartFinalField() { staticFinalField.intField = 5; staticFinalField.anotherIntField = staticFinalField.foo(); @@ -28,7 +27,6 @@ public int checkMocksInLeftAndRightAssignPartFinalField() { return staticFinalField.anotherIntField; } - // This test is associated with https://github.com/UnitTestBot/UTBotJava/issues/1533 public int checkMocksInLeftAndRightAssignPart() { staticField.intField = 5; staticField.anotherIntField = staticField.foo(); diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/stream/BaseStreamExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/stream/BaseStreamExample.java index 4614114a7..b6af87d00 100644 --- a/usvm-jvm/src/samples/java/org/usvm/samples/stream/BaseStreamExample.java +++ b/usvm-jvm/src/samples/java/org/usvm/samples/stream/BaseStreamExample.java @@ -2,8 +2,6 @@ import org.jetbrains.annotations.NotNull; -import static org.usvm.api.mock.UMockKt.assume; - import java.util.Arrays; import java.util.Collection; import java.util.Iterator; @@ -20,6 +18,8 @@ import java.util.stream.Collectors; import java.util.stream.Stream; +import static org.usvm.api.mock.UMockKt.assume; + @SuppressWarnings({"IfStatementWithIdenticalBranches", "RedundantOperationOnEmptyContainer"}) public class BaseStreamExample { Stream returningStreamAsParameterExample(Stream s) { @@ -485,7 +485,6 @@ long closedStreamExample(List values) { } @SuppressWarnings({"ReplaceInefficientStreamCount", "ConstantConditions"}) - // TODO wrong generic type for data field https://github.com/UnitTestBot/UTBotJava/issues/730 long customCollectionStreamExample(CustomCollection customCollection) { assume(customCollection != null && customCollection.data != null); diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt index ef3a24a0c..5d01c681e 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt @@ -3,6 +3,7 @@ package org.usvm.samples import org.jacodb.api.ext.findClass import org.jacodb.api.ext.toType import org.junit.jupiter.api.TestInstance +import org.usvm.CoverageZone import org.usvm.UMachineOptions import org.usvm.api.JcClassCoverage import org.usvm.api.JcParametersState @@ -712,9 +713,17 @@ open class JavaMethodTestRunner : TestRunner, KClass<*>?, J private val testResolver = JcTestResolver() override val typeTransformer: (Any?) -> KClass<*>? = { value -> value?.let { it::class } } + override val checkType: (KClass<*>?, KClass<*>?) -> Boolean = { expected, actual -> actual == null || expected != null && expected.java.isAssignableFrom(actual.java) } + override var options: UMachineOptions = UMachineOptions().copy( + coverageZone = CoverageZone.TRANSITIVE, + exceptionsPropagation = true, + timeoutMs = 60_000, + stepsFromLastCovered = 3500L, + ) + override val runner: (KFunction<*>, UMachineOptions) -> List = { method, options -> val declaringClassName = requireNotNull(method.declaringClass?.name) val jcClass = cp.findClass(declaringClassName).toType() diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CycleDependedConditionTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CycleDependedConditionTest.kt index df0bacc3d..0f3eadde6 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CycleDependedConditionTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/CycleDependedConditionTest.kt @@ -49,7 +49,7 @@ internal class CycleDependedConditionTest : JavaMethodTestRunner() { eq(3), { _, x, r -> x <= 0 && r == 0 }, { _, x, r -> x in 1..100 && r == 0 }, - { _, x, r -> x > 100 && r == 1 && r == 1 } + { _, x, r -> x > 100 && r == 1 } ) } } \ No newline at end of file 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/exceptions/ExceptionExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/exceptions/ExceptionExamplesTest.kt index 20f3b0424..2374f010b 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/exceptions/ExceptionExamplesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/exceptions/ExceptionExamplesTest.kt @@ -6,8 +6,8 @@ import org.usvm.samples.JavaMethodTestRunner import org.usvm.test.util.checkers.eq import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults import org.usvm.util.isException +import java.nio.file.InvalidPathException -@Disabled("Unsupported") internal class ExceptionExamplesTest : JavaMethodTestRunner() { @Test fun testInitAnArray() { @@ -63,6 +63,7 @@ internal class ExceptionExamplesTest : JavaMethodTestRunner() { } @Test + @Disabled("Native methods support") fun testThrowException() { checkDiscoveredPropertiesWithExceptions( ExceptionExamples::throwException, @@ -81,9 +82,6 @@ internal class ExceptionExamplesTest : JavaMethodTestRunner() { ) } - /** - * Used for path generation check in [org.utbot.engine.Traverser.fullPath] - */ @Test fun testCatchDeepNestedThrow() { checkDiscoveredPropertiesWithExceptions( @@ -94,9 +92,6 @@ internal class ExceptionExamplesTest : JavaMethodTestRunner() { ) } - /** // TODO do we want to have this???? - * Covers [#656](https://github.com/UnitTestBot/UTBotJava/issues/656). - */ @Test fun testCatchExceptionAfterOtherPossibleException() { checkDiscoveredPropertiesWithExceptions( @@ -108,9 +103,6 @@ internal class ExceptionExamplesTest : JavaMethodTestRunner() { ) } - /** - * Used for path generation check in [org.utbot.engine.Traverser.fullPath] - */ @Test fun testDontCatchDeepNestedThrow() { checkDiscoveredPropertiesWithExceptions( @@ -120,4 +112,17 @@ internal class ExceptionExamplesTest : JavaMethodTestRunner() { { _, i, r -> i >= 0 && r.getOrThrow() == i }, ) } + + @Test + @Disabled("Wait for instanceof support") + fun testSymbolicExceptions() { + checkDiscoveredProperties( + ExceptionExamples::symbolicExceptionCheck, + eq(4), + { _, e, r -> e is NumberFormatException && r == 1 }, + { _, e, r -> e is InvalidPathException && r == 2 }, + { _, e, r -> e is RuntimeException && e !is NumberFormatException && e !is InvalidPathException && r == 3 }, + { _, e, r -> e !is RuntimeException && r == 4 }, + ) + } } \ No newline at end of file diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/ArgumentsMockTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/ArgumentsMockTest.kt index a2725bc50..e3c2ea0c9 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/ArgumentsMockTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/ArgumentsMockTest.kt @@ -10,9 +10,9 @@ //import org.usvm.test.util.checkers.eq // // -//import org.utbot.testing.isParameter -//import org.utbot.testing.mocksMethod -//import org.utbot.testing.value +//import org.usvm.testing.isParameter +//import org.usvm.testing.mocksMethod +//import org.usvm.testing.value // //internal class ArgumentsMockTest : JavaMethodTestRunner() { // @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/FieldMockTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/FieldMockTest.kt index 6b0f05aaa..c2b8f8024 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/FieldMockTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/FieldMockTest.kt @@ -13,8 +13,8 @@ //import org.usvm.test.util.checkers.eq // // -//import org.utbot.testing.mocksMethod -//import org.utbot.testing.value +//import org.usvm.testing.mocksMethod +//import org.usvm.testing.value // //internal class FieldMockTest : JavaMethodTestRunner( // testClass = ServiceWithField::class, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/InnerMockWithFieldChecker.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/InnerMockWithFieldChecker.kt index c54b7b748..968e4655b 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/InnerMockWithFieldChecker.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/InnerMockWithFieldChecker.kt @@ -3,14 +3,14 @@ // //import org.junit.jupiter.api.Test //import org.usvm.samples.JavaMethodTestRunner.OTHER_PACKAGES -//import org.utbot.framework.plugin.api.UtModel -//import org.utbot.framework.plugin.api.isMockModel -//import org.utbot.framework.plugin.api.isNotNull -//import org.utbot.framework.plugin.api.isNull +//import org.usvm.framework.plugin.api.UtModel +//import org.usvm.framework.plugin.api.isMockModel +//import org.usvm.framework.plugin.api.isNotNull +//import org.usvm.framework.plugin.api.isNull //import org.usvm.test.util.checkers.eq -//import org.utbot.testing.UtModelTestCaseChecker -//import org.utbot.testing.getOrThrow -//import org.utbot.testing.primitiveValue +//import org.usvm.testing.UtModelTestCaseChecker +//import org.usvm.testing.getOrThrow +//import org.usvm.testing.primitiveValue // //internal class InnerMockWithFieldChecker : UtModelTestCaseChecker(testClass = InnerMockWithFieldExample::class) { // @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockFinalClassTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockFinalClassTest.kt index 5517ee8ae..c43824a34 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockFinalClassTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockFinalClassTest.kt @@ -9,8 +9,8 @@ //.OTHER_CLASSES //import org.usvm.test.util.checkers.ge // -//import org.utbot.testing.singleMock -//import org.utbot.testing.value +//import org.usvm.testing.singleMock +//import org.usvm.testing.value // //internal class MockFinalClassTest : JavaMethodTestRunner( // testClass = MockFinalClassExample::class, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockRandomTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockRandomTest.kt index 10006c3de..196e8d116 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockRandomTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockRandomTest.kt @@ -4,19 +4,18 @@ // //import org.junit.jupiter.api.Test //import org.usvm.samples.JavaMethodTestRunner -//import org.utbot.framework.plugin.api.UtCompositeModel -//import org.utbot.framework.plugin.api.UtNewInstanceInstrumentation +//import org.usvm.framework.plugin.api.UtCompositeModel +//import org.usvm.framework.plugin.api.UtNewInstanceInstrumentation //import org.usvm.test.util.checkers.eq -//import org.utbot.testing.TestExecution +//import org.usvm.testing.TestExecution // -//import org.utbot.testing.isParameter -//import org.utbot.testing.mockValues -//import org.utbot.testing.mocksMethod -//import org.utbot.testing.singleMock -//import org.utbot.testing.value +//import org.usvm.testing.isParameter +//import org.usvm.testing.mockValues +//import org.usvm.testing.mocksMethod +//import org.usvm.testing.singleMock +//import org.usvm.testing.value //import java.util.Random // -//// TODO Kotlin mocks generics https://github.com/UnitTestBot/UTBotJava/issues/88 //internal class MockRandomTest : JavaMethodTestRunner( // testClass = MockRandomExamples::class, // testCodeGeneration = true, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockReturnObjectExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockReturnObjectExampleTest.kt index 6a4dc5488..4adfd4cab 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockReturnObjectExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockReturnObjectExampleTest.kt @@ -9,10 +9,10 @@ //.OTHER_PACKAGES //import org.usvm.test.util.checkers.eq // -//import org.utbot.testing.mockValue -//import org.utbot.testing.singleMock -//import org.utbot.testing.singleMockOrNull -//import org.utbot.testing.value +//import org.usvm.testing.mockValue +//import org.usvm.testing.singleMock +//import org.usvm.testing.singleMockOrNull +//import org.usvm.testing.value // //internal class MockReturnObjectExampleTest : JavaMethodTestRunner(testClass = MockReturnObjectExample::class) { // @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockStaticFieldExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockStaticFieldExampleTest.kt index 566e0502f..d7e31f49b 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockStaticFieldExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockStaticFieldExampleTest.kt @@ -6,18 +6,18 @@ //import org.usvm.samples.mock.others.ClassWithStaticField //import org.usvm.samples.mock.others.Generator // -//import org.utbot.framework.plugin.api.FieldMockTarget -//import org.utbot.framework.plugin.api.MockInfo +//import org.usvm.framework.plugin.api.FieldMockTarget +//import org.usvm.framework.plugin.api.MockInfo //.OTHER_PACKAGES -//import org.utbot.framework.plugin.api.UtCompositeModel -//import org.utbot.framework.plugin.api.UtNewInstanceInstrumentation +//import org.usvm.framework.plugin.api.UtCompositeModel +//import org.usvm.framework.plugin.api.UtNewInstanceInstrumentation //import org.usvm.test.util.checkers.eq //import org.usvm.test.util.checkers.withoutConcrete -//import org.utbot.testing.TestExecution +//import org.usvm.testing.TestExecution // -//import org.utbot.testing.singleMock -//import org.utbot.testing.singleMockOrNull -//import org.utbot.testing.value +//import org.usvm.testing.singleMock +//import org.usvm.testing.singleMockOrNull +//import org.usvm.testing.value //import kotlin.reflect.KClass // //internal class MockStaticFieldExampleTest : JavaMethodTestRunner( @@ -25,7 +25,6 @@ // testCodeGeneration = true, // pipelines = listOf( // TestLastStage(CodegenLanguage.JAVA, lastStage = TestExecution), -// // disabled due to https://github.com/UnitTestBot/UTBotJava/issues/88 // TestLastStage(CodegenLanguage.KOTLIN, lastStage = CodeGeneration) // ) //) { diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockStaticMethodExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockStaticMethodExampleTest.kt index 0ab5a1c0e..e4fcda478 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockStaticMethodExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockStaticMethodExampleTest.kt @@ -4,16 +4,15 @@ //import org.junit.jupiter.api.Test //import org.usvm.samples.JavaMethodTestRunner // -//import org.utbot.framework.plugin.api.UtPrimitiveModel -//import org.utbot.framework.plugin.api.util.id -//import org.utbot.framework.util.singleModel -//import org.utbot.framework.util.singleStaticMethod -//import org.utbot.framework.util.singleValue +//import org.usvm.framework.plugin.api.UtPrimitiveModel +//import org.usvm.framework.plugin.api.util.id +//import org.usvm.framework.util.singleModel +//import org.usvm.framework.util.singleStaticMethod +//import org.usvm.framework.util.singleValue //import org.usvm.test.util.checkers.eq -//import org.utbot.testing.TestExecution +//import org.usvm.testing.TestExecution // // -//// TODO Kotlin mocks generics https://github.com/UnitTestBot/UTBotJava/issues/88 //internal class MockStaticMethodExampleTest : JavaMethodTestRunner( // testClass = MockStaticMethodExample::class, // testCodeGeneration = true, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockWithFieldChecker.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockWithFieldChecker.kt index 17919479e..c20a96ef9 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockWithFieldChecker.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/MockWithFieldChecker.kt @@ -4,13 +4,13 @@ // //import org.junit.jupiter.api.Test //import org.usvm.samples.JavaMethodTestRunner.OTHER_PACKAGES -//import org.utbot.framework.plugin.api.UtModel -//import org.utbot.framework.plugin.api.isMockModel -//import org.utbot.framework.plugin.api.isNull +//import org.usvm.framework.plugin.api.UtModel +//import org.usvm.framework.plugin.api.isMockModel +//import org.usvm.framework.plugin.api.isNull //import org.usvm.test.util.checkers.eq -//import org.utbot.testing.UtModelTestCaseChecker -//import org.utbot.testing.getOrThrow -//import org.utbot.testing.primitiveValue +//import org.usvm.testing.UtModelTestCaseChecker +//import org.usvm.testing.getOrThrow +//import org.usvm.testing.primitiveValue // //internal class MockWithFieldChecker : UtModelTestCaseChecker(testClass = MockWithFieldExample::class) { // @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/StaticFieldMockTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/StaticFieldMockTest.kt index 9ad842775..eeb1a066f 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/StaticFieldMockTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/StaticFieldMockTest.kt @@ -9,8 +9,8 @@ //.OTHER_PACKAGES //import org.usvm.test.util.checkers.eq // -//import org.utbot.testing.mocksMethod -//import org.utbot.testing.value +//import org.usvm.testing.mocksMethod +//import org.usvm.testing.value // //internal class StaticFieldMockTest : JavaMethodTestRunner(testClass = ServiceWithStaticField::class) { // diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/UseNetworkTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/UseNetworkTest.kt index f9e8d9dbc..4a2bdf021 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/UseNetworkTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/UseNetworkTest.kt @@ -3,7 +3,7 @@ // //import org.junit.jupiter.api.Test //import org.usvm.samples.JavaMethodTestRunner -//import org.utbot.framework.plugin.api.UtConcreteValue +//import org.usvm.framework.plugin.api.UtConcreteValue //import org.usvm.test.util.checkers.eq // //internal class UseNetworkTest : JavaMethodTestRunner(testClass = UseNetwork::class) { diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/model/FieldMockChecker.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/model/FieldMockChecker.kt index c52665538..8dfa94f12 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/model/FieldMockChecker.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/model/FieldMockChecker.kt @@ -6,12 +6,12 @@ //import org.usvm.samples.mock.service.impl.ServiceWithField //import org.usvm.samples.mock.service.impl.ServiceWithField //.OTHER_PACKAGES -//import org.utbot.framework.plugin.api.UtModel -//import org.utbot.framework.plugin.api.isNotNull -//import org.utbot.framework.plugin.api.isNull +//import org.usvm.framework.plugin.api.UtModel +//import org.usvm.framework.plugin.api.isNotNull +//import org.usvm.framework.plugin.api.isNull //import org.usvm.test.util.checkers.eq -//import org.utbot.testing.UtModelTestCaseChecker -//import org.utbot.testing.primitiveValue +//import org.usvm.testing.UtModelTestCaseChecker +//import org.usvm.testing.primitiveValue // //internal class FieldMockChecker : UtModelTestCaseChecker() { // @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/model/UseNetworkModelBasedTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/model/UseNetworkModelBasedTest.kt index 061ebde3f..75729ea82 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/model/UseNetworkModelBasedTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mock/model/UseNetworkModelBasedTest.kt @@ -4,10 +4,10 @@ //import org.usvm.samples.JavaMethodTestRunner //import org.usvm.samples.mock.UseNetwork // -//import org.utbot.framework.plugin.api.UtCompositeModel -//import org.utbot.framework.plugin.api.UtVoidModel +//import org.usvm.framework.plugin.api.UtCompositeModel +//import org.usvm.framework.plugin.api.UtVoidModel //import org.usvm.test.util.checkers.eq -//import org.utbot.testing.UtModelTestCaseChecker +//import org.usvm.testing.UtModelTestCaseChecker // //internal class UseNetworkModelBasedTest : UtModelTestCaseChecker(testClass = UseNetwork::class) { // @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/models/CompositeModelMinimizationChecker.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/models/CompositeModelMinimizationChecker.kt index 02367ad24..7563da621 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/models/CompositeModelMinimizationChecker.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/models/CompositeModelMinimizationChecker.kt @@ -3,13 +3,13 @@ // //import org.junit.Test // -//import org.utbot.framework.plugin.api.FieldId -//import org.utbot.framework.plugin.api.UtAssembleModel -//import org.utbot.framework.plugin.api.UtCompositeModel -//import org.utbot.framework.plugin.api.UtModel -//import org.utbot.framework.plugin.api.UtReferenceModel +//import org.usvm.framework.plugin.api.FieldId +//import org.usvm.framework.plugin.api.UtAssembleModel +//import org.usvm.framework.plugin.api.UtCompositeModel +//import org.usvm.framework.plugin.api.UtModel +//import org.usvm.framework.plugin.api.UtReferenceModel //import org.usvm.test.util.checkers.eq -//import org.utbot.testing.UtModelTestCaseChecker +//import org.usvm.testing.UtModelTestCaseChecker // //internal class CompositeModelMinimizationChecker : UtModelTestCaseChecker( // testClass = CompositeModelMinimizationExample::class, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/models/ModelsIdEqualityChecker.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/models/ModelsIdEqualityChecker.kt index 8530a40af..e09473a9e 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/models/ModelsIdEqualityChecker.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/models/ModelsIdEqualityChecker.kt @@ -3,13 +3,13 @@ // //import org.junit.jupiter.api.Test //import org.usvm.samples.JavaMethodTestRunner -//import org.utbot.framework.plugin.api.UtArrayModel -//import org.utbot.framework.plugin.api.UtAssembleModel -//import org.utbot.framework.plugin.api.UtDirectSetFieldModel -//import org.utbot.framework.plugin.api.UtExecutionSuccess -//import org.utbot.framework.plugin.api.UtReferenceModel +//import org.usvm.framework.plugin.api.UtArrayModel +//import org.usvm.framework.plugin.api.UtAssembleModel +//import org.usvm.framework.plugin.api.UtDirectSetFieldModel +//import org.usvm.framework.plugin.api.UtExecutionSuccess +//import org.usvm.framework.plugin.api.UtReferenceModel //import org.usvm.test.util.checkers.eq -//import org.utbot.testing.UtModelTestCaseChecker +//import org.usvm.testing.UtModelTestCaseChecker // //// TODO failed Kotlin compilation SAT-1332 //internal class ModelsIdEqualityChecker : UtModelTestCaseChecker( 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, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt index 6e0d4be33..dfa9de436 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/recursion/RecursionTest.kt @@ -15,17 +15,18 @@ import org.usvm.util.isException import kotlin.math.pow -// TODO Kotlin mocks generics https://github.com/UnitTestBot/UTBotJava/issues/88 internal class RecursionTest : JavaMethodTestRunner() { - @Test - fun testFactorial() { - checkDiscoveredPropertiesWithExceptions( - Recursion::factorial, - eq(3), - { _, x, r -> x < 0 && r.isException() }, - { _, x, r -> x == 0 && r.getOrNull() == 1 }, - { _, x, r -> x > 0 && r.getOrNull() == (1..x).reduce { a, b -> a * b } } - ) + @UsvmTest([Options([PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM])]) + fun testFactorial(options: UMachineOptions) { + withOptions(options) { + checkDiscoveredPropertiesWithExceptions( + Recursion::factorial, + eq(3), + { _, x, r -> x < 0 && r.isException() }, + { _, x, r -> x == 0 && r.getOrNull() == 1 }, + { _, x, r -> x > 0 && r.getOrNull() == (1..x).reduce { a, b -> a * b } } + ) + } } @UsvmTest([Options([PathSelectionStrategy.RANDOM_PATH])]) @@ -43,7 +44,6 @@ internal class RecursionTest : JavaMethodTestRunner() { } @Test -// @Disabled("Freezes the execution when snd != 0 JIRA:1293") @Disabled("Native method invocation: java.lang.Float.floatToRawIntBits") fun testSum() { checkDiscoveredProperties( @@ -52,18 +52,21 @@ internal class RecursionTest : JavaMethodTestRunner() { { _, x, y, r -> y == 0 && r == x }, { _, x, y, r -> y != 0 && r == x + y } ) + } - @Test - fun testPow() { - checkDiscoveredPropertiesWithExceptions( - Recursion::pow, - eq(4), - { _, _, y, r -> y < 0 && r.isException() }, - { _, _, y, r -> y == 0 && r.getOrNull() == 1 }, - { _, x, y, r -> y % 2 == 1 && r.getOrNull() == x.toDouble().pow(y.toDouble()).toInt() }, - { _, x, y, r -> y % 2 != 1 && r.getOrNull() == x.toDouble().pow(y.toDouble()).toInt() } - ) + @UsvmTest([Options([PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM])]) + fun testPow(options: UMachineOptions) { + withOptions(options) { + checkDiscoveredPropertiesWithExceptions( + Recursion::pow, + eq(4), + { _, _, y, r -> y < 0 && r.isException() }, + { _, _, y, r -> y == 0 && r.getOrNull() == 1 }, + { _, x, y, r -> y % 2 == 1 && r.getOrNull() == x.toDouble().pow(y.toDouble()).toInt() }, + { _, x, y, r -> y % 2 != 1 && r.getOrNull() == x.toDouble().pow(y.toDouble()).toInt() } + ) + } } @Test diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/stdlib/StaticsPathDiversionTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/stdlib/StaticsPathDiversionTest.kt index 76cfa905c..e00e5de29 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/stdlib/StaticsPathDiversionTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/stdlib/StaticsPathDiversionTest.kt @@ -11,12 +11,6 @@ internal class StaticsPathDiversionTest : JavaMethodTestRunner() { @Test @Disabled("Unexpected lvalue org.usvm.machine.JcStaticFieldRef@3f95a1b3") fun testJavaIOFile() { - // TODO Here we have a path diversion example - the static field `java.io.File#separator` is considered as not meaningful, - // so it is not passed to the concrete execution because of absence in the `stateBefore` models. - // So, the symbolic engine has 2 results - true and false, as expected, but the concrete executor may produce 1 or 2, - // depending on the model for the argument of the MUT produced by the solver. - // Such diversion was predicted to some extent - see `org.utbot.common.WorkaroundReason.IGNORE_STATICS_FROM_TRUSTED_LIBRARIES` - // and the corresponding issue https://github.com/UnitTestBot/UTBotJava/issues/716 checkDiscoveredProperties( StaticsPathDiversion::separatorEquality, ge(2), // We cannot guarantee the exact number of branches without minimization diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/BaseStreamExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/BaseStreamExampleTest.kt index a6b21c49c..0154255ca 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/BaseStreamExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/BaseStreamExampleTest.kt @@ -134,7 +134,6 @@ class BaseStreamExampleTest : JavaMethodTestRunner() { @Test @Tag("slow") @Disabled("Not implemented: virtual calls with abstract methods") - // TODO slow sorting https://github.com/UnitTestBot/UTBotJava/issues/188 fun testSortedExample() { checkDiscoveredProperties( BaseStreamExample::sortedExample, @@ -209,7 +208,7 @@ class BaseStreamExampleTest : JavaMethodTestRunner() { ignoreNumberOfAnalysisResults, { _, c, r -> c.isEmpty() && r.getOrThrow() == Optional.empty() }, { _, c, r -> c.isNotEmpty() && c.single() == null && r.isException() }, - { _, c, r -> c.isNotEmpty() && r.getOrThrow() == Optional.of(c.sum()) }, // TODO 2 instructions are uncovered https://github.com/UnitTestBot/UTBotJava/issues/193 + { _, c, r -> c.isNotEmpty() && r.getOrThrow() == Optional.of(c.sum()) }, ) } @@ -238,7 +237,7 @@ class BaseStreamExampleTest : JavaMethodTestRunner() { BaseStreamExample::collectExample, eq(2), // 3 executions instead of 2 expected { _, c, r -> null in c && r.isException() }, - { _, c, r -> null !in c && c.sum() == r.getOrThrow() }, // TODO 2 instructions are uncovered https://github.com/UnitTestBot/UTBotJava/issues/193 + { _, c, r -> null !in c && c.sum() == r.getOrThrow() }, ) } @@ -249,7 +248,7 @@ class BaseStreamExampleTest : JavaMethodTestRunner() { ignoreNumberOfAnalysisResults, { _, c, r -> c.isEmpty() && r.getOrThrow() == Optional.empty() }, { _, c, r -> c.isNotEmpty() && c.all { it == null } && r.isException() }, - { _, c, r -> c.isNotEmpty() && r.getOrThrow() == Optional.of(c.minOrNull()!!) }, // TODO 2 instructions are uncovered https://github.com/UnitTestBot/UTBotJava/issues/193 + { _, c, r -> c.isNotEmpty() && r.getOrThrow() == Optional.of(c.minOrNull()!!) }, ) } @@ -260,7 +259,7 @@ class BaseStreamExampleTest : JavaMethodTestRunner() { ignoreNumberOfAnalysisResults, { _, c, r -> c.isEmpty() && r.getOrThrow() == Optional.empty() }, { _, c, r -> c.isNotEmpty() && c.all { it == null } && r.isException() }, - { _, c, r -> c.isNotEmpty() && r.getOrThrow() == Optional.of(c.maxOrNull()!!) }, // TODO 2 instructions are uncovered https://github.com/UnitTestBot/UTBotJava/issues/193 + { _, c, r -> c.isNotEmpty() && r.getOrThrow() == Optional.of(c.maxOrNull()!!) }, ) } diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/DoubleStreamExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/DoubleStreamExampleTest.kt index 757ef1c92..045576580 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/DoubleStreamExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/DoubleStreamExampleTest.kt @@ -150,7 +150,6 @@ class DoubleStreamExampleTest : JavaMethodTestRunner() { @Test @Tag("slow") @Disabled("Not implemented: virtual calls with abstract methods") - // TODO slow sorting https://github.com/UnitTestBot/UTBotJava/issues/188 fun testSortedExample() { checkDiscoveredProperties( DoubleStreamExample::sortedExample, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/IntStreamExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/IntStreamExampleTest.kt index 95733d0c8..c29473e60 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/IntStreamExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/IntStreamExampleTest.kt @@ -147,7 +147,6 @@ class IntStreamExampleTest : JavaMethodTestRunner() { @Test @Tag("slow") - // TODO slow sorting https://github.com/UnitTestBot/UTBotJava/issues/188 fun testSortedExample() { checkDiscoveredProperties( IntStreamExample::sortedExample, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/LongStreamExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/LongStreamExampleTest.kt index c4dbc4ffb..27c98658c 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/LongStreamExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/stream/LongStreamExampleTest.kt @@ -148,7 +148,6 @@ class LongStreamExampleTest : JavaMethodTestRunner() { @Test @Tag("slow") @Disabled("Not implemented: virtual calls with abstract methods") - // TODO slow sorting https://github.com/UnitTestBot/UTBotJava/issues/188 fun testSortedExample() { checkDiscoveredProperties( LongStreamExample::sortedExample, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/MinStackExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/MinStackExampleTest.kt index f8b8e9fe5..592ba0fd4 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/MinStackExampleTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/structures/MinStackExampleTest.kt @@ -85,6 +85,7 @@ internal class MinStackExampleTest : JavaMethodTestRunner() { } @Test + @Disabled("Not yet implemented visitJcClassConstant(JcExprResolver.kt:287)") fun testConstruct() { checkDiscoveredProperties( MinStackExample::construct, diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/symbolic/ClassWithComplicatedMethodsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/symbolic/ClassWithComplicatedMethodsTest.kt index 316744cbb..911e237d2 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/symbolic/ClassWithComplicatedMethodsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/symbolic/ClassWithComplicatedMethodsTest.kt @@ -8,7 +8,7 @@ // //import org.usvm.test.util.checkers.eq //import org.usvm.test.util.checkers.withoutConcrete -//import org.utbot.testing.Compilation +//import org.usvm.testing.Compilation // //import kotlin.math.abs //import kotlin.math.sqrt diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/ExecutorServiceExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/ExecutorServiceExamplesTest.kt index 34d61095d..d17cdf5ad 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/ExecutorServiceExamplesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/ExecutorServiceExamplesTest.kt @@ -9,7 +9,6 @@ import org.usvm.util.isException // IMPORTANT: most of the these tests test only the symbolic engine // and should not be used for testing conrete or code generation since they are possibly flaky in the concrete execution -// (see https://github.com/UnitTestBot/UTBotJava/issues/1610) class ExecutorServiceExamplesTest : JavaMethodTestRunner() { @Test @Disabled("Index 1 out of bounds for length 1") diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/FutureExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/FutureExamplesTest.kt index c691b02ca..c4860dc84 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/FutureExamplesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/FutureExamplesTest.kt @@ -9,7 +9,6 @@ import java.util.concurrent.ExecutionException // IMPORTANT: most of the these tests test only the symbolic engine // and should not be used for testing conrete or code generation since they are possibly flaky in the concrete execution -// (see https://github.com/UnitTestBot/UTBotJava/issues/1610) class FutureExamplesTest : JavaMethodTestRunner() { @Test @Disabled("Support invokedynamic") diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/ThreadExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/ThreadExamplesTest.kt index aa45b192e..b737e2be2 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/ThreadExamplesTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/threads/ThreadExamplesTest.kt @@ -9,7 +9,6 @@ import org.usvm.util.isException // IMPORTANT: most of the these tests test only the symbolic engine // and should not be used for testing conrete or code generation since they are possibly flaky in the concrete execution -// (see https://github.com/UnitTestBot/UTBotJava/issues/1610) class ThreadExamplesTest : JavaMethodTestRunner() { @Test @Disabled("Support invokedynamic") diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/unsafe/UnsafeOperationsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/unsafe/UnsafeOperationsTest.kt index f0267f4a6..f8c5a92a7 100644 --- a/usvm-jvm/src/test/kotlin/org/usvm/samples/unsafe/UnsafeOperationsTest.kt +++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/unsafe/UnsafeOperationsTest.kt @@ -26,7 +26,6 @@ internal class UnsafeOperationsTest : JavaMethodTestRunner() { // eq(1), // { _, r -> r != null && r > 0 }, // // Coverage matcher fails (branches: 0/0, instructions: 15/21, lines: 0/0) -// // TODO: check coverage calculation: https://github.com/UnitTestBot/UTBotJava/issues/807, // mockStrategy = MockStrategyApi.OTHER_CLASSES // ) // } diff --git a/usvm-jvm/src/test/resources/burningwave.static.properties b/usvm-jvm/src/test/resources/burningwave.static.properties new file mode 100644 index 000000000..6c188ddc3 --- /dev/null +++ b/usvm-jvm/src/test/resources/burningwave.static.properties @@ -0,0 +1,2 @@ +banner.hide=true +managed-logger.repository.enabled=false \ No newline at end of file diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt index 33f04dd71..8db235429 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt +++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt @@ -48,6 +48,9 @@ class SampleState( exceptionRegister ) } + + override val isExceptional: Boolean + get() = exceptionRegister != null } val SampleState.lastStmt get() = path.last() diff --git a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt index e9d84706c..9731bc250 100644 --- a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt +++ b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt @@ -76,7 +76,11 @@ enum class CoverageZone { /** * Coverage of methods in target method's class id considered. */ - CLASS + CLASS, + /** + * Coverage of methods transitively reachable from a start method. + */ + TRANSITIVE } data class UMachineOptions( @@ -112,13 +116,21 @@ data class UMachineOptions( /** * Optional timeout in milliseconds to stop execution on. */ - val timeoutMs: Long? = 20000, + val timeoutMs: Long? = 20_000, + /** + * A number of steps from the last terminated state. + */ + val stepsFromLastCovered: Long? = null, /** * Scope of methods which coverage is considered. * * @see CoverageZone */ val coverageZone: CoverageZone = CoverageZone.METHOD, + /** + * Whether we should prefer exceptional state in the queue to the regular ones. + */ + val exceptionsPropagation: Boolean = true, /** * SMT solver type used for path constraint solving. */ diff --git a/usvm-util/src/main/kotlin/org/usvm/test/util/TestRunner.kt b/usvm-util/src/main/kotlin/org/usvm/test/util/TestRunner.kt index 08e0dacaa..aef160c6c 100644 --- a/usvm-util/src/main/kotlin/org/usvm/test/util/TestRunner.kt +++ b/usvm-util/src/main/kotlin/org/usvm/test/util/TestRunner.kt @@ -1,11 +1,13 @@ package org.usvm.test.util -import org.usvm.CoverageZone +import mu.KLogging import org.usvm.UMachineOptions import org.usvm.test.util.TestRunner.CheckMode.MATCH_EXECUTIONS import org.usvm.test.util.TestRunner.CheckMode.MATCH_PROPERTIES import org.usvm.test.util.checkers.AnalysisResultsNumberMatcher +val logger = object : KLogging() {}.logger + /** * A base class for test runners for all interpreters. * @@ -27,13 +29,13 @@ abstract class TestRunner { abstract val runner: (Target, UMachineOptions) -> List abstract val coverageRunner: (List) -> Coverage - private var options = UMachineOptions() + abstract var options: UMachineOptions /** * Parametrizes [runner] with given options and executes [action]. */ protected fun withOptions(options: UMachineOptions, action: () -> T): T { - val prevOptions = options + val prevOptions = this.options try { this.options = options return action() @@ -65,8 +67,16 @@ abstract class TestRunner { ) { val analysisResults = runner(target, options) - //println(createStringFromResults(analysisResults)) - //println() + logger.debug { options } + + logger.info { + buildString { + appendLine("${analysisResults.size} executions were found:") + analysisResults.forEach { appendLine("\t$it") } + appendLine("Extracted values:") + analysisResults.forEach { appendLine("\t${extractValuesToCheck(it)}") } + } + } if (checkMode != MATCH_EXECUTIONS) { require(analysisResultsNumberMatcher(analysisResults.size)) { @@ -83,8 +93,8 @@ abstract class TestRunner { // TODO should I add a comparison between real run and symbolic one? when (checkMode) { - MATCH_EXECUTIONS -> matchExecutions(analysisResults, valuesToCheck, analysisResultsMatchers) - MATCH_PROPERTIES -> checkDiscoveredProperties(analysisResults, valuesToCheck, analysisResultsMatchers) + MATCH_EXECUTIONS -> matchExecutions(valuesToCheck, analysisResultsMatchers) + MATCH_PROPERTIES -> checkDiscoveredProperties(valuesToCheck, analysisResultsMatchers) } val coverageResult = coverageRunner(analysisResults) @@ -147,7 +157,6 @@ abstract class TestRunner { } private fun checkDiscoveredProperties( - analysisResults: List, valuesToCheck: List>, propertiesToDiscover: Array>, ) { @@ -160,12 +169,10 @@ abstract class TestRunner { "Some properties were not discovered at positions (from 0): $unsatisfiedPositions" }, - analysisResults ) } private fun matchExecutions( - analysisResults: List, valuesToCheck: List>, predicates: Array>, ) { @@ -190,7 +197,6 @@ abstract class TestRunner { append(message) } }, - analysisResults ) } @@ -199,7 +205,6 @@ abstract class TestRunner { predicates: Array>, successCriteria: (IntArray) -> Boolean, errorMessage: (IntArray) -> String, - analysisResults: List, ) { val satisfied = IntArray(predicates.size) { 0 } @@ -217,21 +222,10 @@ abstract class TestRunner { check(isSuccess) { buildString { appendLine(errorMessage(satisfied)) - appendLine() - - val analysisResultsString = createStringFromResults(analysisResults) - - appendLine(analysisResultsString) } } } - private fun createStringFromResults(analysisResults: List): String = - analysisResults.joinToString( - prefix = "Analysis results: ${System.lineSeparator()}", - separator = System.lineSeparator() - ) - /** * Modes for strategy of checking result matchers. *