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

Show file tree
Hide file tree
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
Fix strange behaviour
  • Loading branch information
@sergeypospelov
sergeypospelov committed Jul 8, 2022
commit 3f01700e2594d0ac9f76dfe33d8a46a6851616e2
16 changes: 9 additions & 7 deletions utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3330,12 +3330,12 @@ class Traverser(
queuedSymbolicStateUpdates += mkNot(mkEq(symbolicResult.value.addr, nullObjectAddr)).asHardConstraint()
}

val state = environment.state.update(queuedSymbolicStateUpdates)
val memory = state.memory
val solver = state.solver
val symbolicState = environment.state.symbolicState + queuedSymbolicStateUpdates
val memory = symbolicState.memory
val solver = symbolicState.solver

//no need to respect soft constraints in NestedMethod
val holder = solver.check(respectSoft = !state.isInNestedMethod())
val holder = solver.check(respectSoft = !environment.state.isInNestedMethod())

if (holder !is UtSolverStatusSAT) {
logger.trace { "processResult<${environment.method.signature}> UNSAT" }
Expand All @@ -3344,7 +3344,7 @@ class Traverser(
val methodResult = MethodResult(symbolicResult)

//execution frame from level 2 or above
if (state.isInNestedMethod()) {
if (environment.state.isInNestedMethod()) {
// static fields substitution
// TODO: JIRA:1610 -- better way of working with statics
val updates = if (environment.method.name == STATIC_INITIALIZER && substituteStaticsWithSymbolicVariable) {
Expand All @@ -3355,15 +3355,17 @@ class Traverser(
} else {
MemoryUpdate() // all memory updates are already added in [environment.state]
}
val stateToOffer = state.pop(methodResult.copy(symbolicStateUpdate = updates.asUpdate()))
val methodResultWithUpdates = methodResult.copy(symbolicStateUpdate = queuedSymbolicStateUpdates + updates)
val stateToOffer = environment.state.pop(methodResultWithUpdates)
offerState(stateToOffer)

logger.trace { "processResult<${environment.method.signature}> return from nested method" }
return
}

//toplevel method
val terminalExecutionState = state.copy(
val terminalExecutionState = environment.state.copy(
symbolicState = symbolicState,
methodResult = methodResult, // the way to put SymbolicResult into terminal state
label = StateLabel.TERMINAL
)
Expand Down
3 changes: 1 addition & 2 deletions utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -493,8 +493,7 @@ class UtBotSymbolicEngine(
val solver = state.solver
val parameters = state.parameters.map { it.value }
val symbolicResult = requireNotNull(state.methodResult?.symbolicResult) { "The state must have symbolicResult" }
// it's free to make a check, because in the result is SAT, it should be already cached
val holder = requireNotNull(solver.check(respectSoft = true) as? UtSolverStatusSAT) { "The state must be SAT!" }
val holder = requireNotNull(solver.lastStatus as? UtSolverStatusSAT) { "The state must be SAT!" }

val predictedTestName = Predictors.testName.predict(state.path)
Predictors.testName.provide(state.path, predictedTestName, "")
Expand Down