Skip to content

Commit 8cd425b

Browse files
authored
Fix terminated states handling (#59)
1 parent 2021212 commit 8cd425b

File tree

5 files changed

+11
-9
lines changed

5 files changed

+11
-9
lines changed

usvm-core/src/main/kotlin/org/usvm/Machine.kt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,15 +49,15 @@ abstract class UMachine<State> : AutoCloseable {
4949
} else {
5050
// TODO: distinguish between states terminated by exception (runtime or user) and
5151
// those which just exited
52-
observer.onStateTerminated(forkedState)
52+
observer.onStateTerminated(forkedState, stateReachable = true)
5353
}
5454
}
5555

5656
if (originalStateAlive) {
5757
pathSelector.update(state)
5858
} else {
5959
pathSelector.remove(state)
60-
observer.onStateTerminated(state)
60+
observer.onStateTerminated(state, stateReachable = stateAlive)
6161
}
6262

6363
if (aliveForkedStates.isNotEmpty()) {

usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,9 @@ class CoverageStatistics<Method, Statement, State : UState<*, Method, Statement,
9292
}
9393

9494
// TODO: don't consider coverage of runtime exceptions states
95-
override fun onStateTerminated(state: State) {
95+
override fun onStateTerminated(state: State, stateReachable: Boolean) {
96+
if (!stateReachable) return
97+
9698
for (statement in state.reversedPath) {
9799
val method = applicationGraph.methodOf(statement)
98100

usvm-core/src/main/kotlin/org/usvm/statistics/CoveredNewStatesCollector.kt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,14 +16,14 @@ class CoveredNewStatesCollector<State>(
1616

1717
private var previousCoverage = coverageStatistics.getTotalCoverage()
1818

19-
override fun onStateTerminated(state: State) {
19+
override fun onStateTerminated(state: State, stateReachable: Boolean) {
2020
val currentCoverage = coverageStatistics.getTotalCoverage()
2121
if (isException(state)) {
2222
mutableCollectedStates.add(state)
2323
return
2424
}
2525

26-
if (currentCoverage > previousCoverage) {
26+
if (stateReachable && currentCoverage > previousCoverage) {
2727
previousCoverage = currentCoverage
2828
mutableCollectedStates.add(state)
2929
}

usvm-core/src/main/kotlin/org/usvm/statistics/TerminatedStateRemover.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ import org.usvm.UState
1111
* It costs additional memory, but might be useful for debug purposes.
1212
*/
1313
class TerminatedStateRemover<State : UState<*, *, *, *, State>> : UMachineObserver<State> {
14-
override fun onStateTerminated(state: State) {
14+
override fun onStateTerminated(state: State, stateReachable: Boolean) {
1515
state.pathLocation.states.remove(state)
1616
}
1717
}

usvm-core/src/main/kotlin/org/usvm/statistics/UMachineObserver.kt

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ interface UMachineObserver<State> {
88
/**
99
* Called when the execution of the state is terminated (by exception or return).
1010
*/
11-
fun onStateTerminated(state: State) { }
11+
fun onStateTerminated(state: State, stateReachable: Boolean) { }
1212

1313
/**
1414
* Called on each symbolic execution step. If the state has forked, [forks] are not empty.
@@ -19,8 +19,8 @@ interface UMachineObserver<State> {
1919
class CompositeUMachineObserver<State>(private val observers: List<UMachineObserver<State>>) : UMachineObserver<State> {
2020
constructor(vararg observers: UMachineObserver<State>) : this(observers.toList())
2121

22-
override fun onStateTerminated(state: State) {
23-
observers.forEach { it.onStateTerminated(state) }
22+
override fun onStateTerminated(state: State, stateReachable: Boolean) {
23+
observers.forEach { it.onStateTerminated(state, stateReachable) }
2424
}
2525

2626
override fun onState(parent: State, forks: Sequence<State>) {

0 commit comments

Comments
 (0)