Skip to content

Extract Traverser from UtBotSymbolicEngine #307

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sergeypospelov merged 19 commits into from
Jul 8, 2022
Merged

Extract Traverser from UtBotSymbolicEngine #307

Changes from 1 commit
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
f7cb267
Add highlighting link to UtBotSymbolicEngine in the comments
sergeypospelov Jun 23, 2022
258c8f5
Rename UtBotSymbolicEngine to Traverser
sergeypospelov Jun 23, 2022
58ae325
Introduce StateLabel
sergeypospelov Jun 23, 2022
f1f2a73
Move function from TypeRegistry to Traverser
sergeypospelov Jun 23, 2022
8dce048
Remove strange hack on nullable SymbolicResult for only void return
sergeypospelov Jun 23, 2022
cd2e1ee
Refactor resolve function: turn receiver parameter into argument
sergeypospelov Jun 23, 2022
a42d75c
Remove isInNestedMethod function from engine
sergeypospelov Jun 23, 2022
fbc0541
Split processResult
sergeypospelov Jun 23, 2022
259078b
Refactor: remove graph parameter from Traverser constructor
sergeypospelov Jun 23, 2022
d226672
Refactor: remove useless environment field usage
sergeypospelov Jun 23, 2022
a5cb81c
Refactor entryMethodPath function
sergeypospelov Jun 23, 2022
b3137a9
Move function isInsideStaticInitializer to ExecutionState.kt
sergeypospelov Jun 27, 2022
6046b22
Refactor: move negativeArraySizeCheck from createNewArray to call site
sergeypospelov Jun 27, 2022
1d7017a
Introduce TraversingContext
sergeypospelov Jun 27, 2022
33f21b7
Split Traverser.kt into Traverser.kt and UtBotSymbolicEngine.kt
sergeypospelov Jun 27, 2022
8ca4645
Change logger back
sergeypospelov Jun 27, 2022
c266e98
Fix comments
sergeypospelov Jun 27, 2022
3f01700
Fix strange behaviour
sergeypospelov Jun 28, 2022
33c61d1
Fix review comments
sergeypospelov Jun 29, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Introduce StateLabel
  • Loading branch information
@sergeypospelov
sergeypospelov committed Jul 8, 2022
commit 58ae325f74e9a82b50134fd377c52d482a7cca32
27 changes: 26 additions & 1 deletion utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,24 @@ const val CALL_DECISION_NUM = -2

data class Edge(val src: Stmt, val dst: Stmt, val decisionNum: Int)

/**
* Possible state types. Engine matches on them and processes differently.
*
* [INTERMEDIATE] is a label for an intermediate state which is suitable for further symbolic analysis.
*
* [TERMINAL] is a label for a terminal state from which we might (or might not) execute concretely and construct
* UtExecution. This state represents the final state of the program execution, that is a throw or return from the outer
* method.
*
* [CONCRETE] is a label for a state which is not suitable for further symbolic analysis and it is also not a terminal
* state. Such states are only suitable for a concrete execution and may appear from Assumptions constraints
Comment thread
sergeypospelov marked this conversation as resolved.
Outdated
*/
enum class StateLabel {
INTERMEDIATE,
TERMINAL,
CONCRETE
}

/**
* The stack element of the [ExecutionState].
* Contains properties, that are suitable for specified method in call stack.
Expand Down Expand Up @@ -112,6 +130,7 @@ data class ExecutionState(
val lastMethod: SootMethod? = null,
val methodResult: MethodResult? = null,
val exception: SymbolicFailure? = null,
val label: StateLabel = StateLabel.INTERMEDIATE,
private var stateAnalyticsProperties: StateAnalyticsProperties = StateAnalyticsProperties()
) : AutoCloseable {
val solver: UtSolver by symbolicState::solver
Expand Down Expand Up @@ -161,6 +180,7 @@ data class ExecutionState(
lastEdge = edge,
lastMethod = executionStack.last().method,
exception = exception,
label = label,
stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this)
)
}
Expand All @@ -187,7 +207,8 @@ data class ExecutionState(
pathLength = pathLength + 1,
lastEdge = edge,
lastMethod = executionStack.last().method,
methodResult,
methodResult = methodResult,
label = label,
stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this)
)
}
Expand Down Expand Up @@ -226,6 +247,7 @@ data class ExecutionState(
pathLength = pathLength + 1,
lastEdge = edge,
lastMethod = stackElement.method,
label = label,
stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this)
)
}
Expand Down Expand Up @@ -271,6 +293,7 @@ data class ExecutionState(
pathLength = pathLength + 1,
lastEdge = edge,
lastMethod = stackElement.method,
label = label,
stateAnalyticsProperties = stateAnalyticsProperties.successorProperties(this)
)
}
Expand All @@ -284,6 +307,8 @@ data class ExecutionState(
solver.expectUndefined = true
}

fun withLabel(newLabel: StateLabel) = copy(label = newLabel)

override fun close() {
solver.close()
}
Expand Down