Skip to content
Merged
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
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
Fix review comments
  • Loading branch information
sergeypospelov committed Jul 8, 2022
commit 33c61d15f57f96b22d4e6899720a51068b2b2eab
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ data class Edge(val src: Stmt, val dst: Stmt, val decisionNum: Int)
* [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 [Assumption]s.
* [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 result from [Assumption]s.
*/
enum class StateLabel {
INTERMEDIATE,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,7 @@ fun SootMethod.canRetrieveBody() =
*/
fun SootMethod.jimpleBody(): JimpleBody {
declaringClass.adjustLevel(BODIES)
require(canRetrieveBody()) { "Can't retrieve body for $this"}
return retrieveActiveBody() as JimpleBody
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ package org.utbot.engine

/**
* Represents a mutable _Context_ during the [ExecutionState] traversing. This _Context_ consists of all mutable and
* immutable properties and fields which are created and updated during analysis of **one** Jimple instruction.
* immutable properties and fields which are created and updated during analysis of a **single** Jimple instruction.
*
* Traverser functions should be implemented as an extension functions with [TraversalContext] as a receiver.
*
Expand All @@ -23,7 +23,7 @@ class TraversalContext {
}

/**
* New states from traversal.
* New states obtained from the traversal.
*/
val nextStates: Collection<ExecutionState>
get() = states
Expand Down
18 changes: 8 additions & 10 deletions utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ import kotlinx.collections.immutable.persistentSetOf
import kotlinx.collections.immutable.toPersistentList
import kotlinx.collections.immutable.toPersistentMap
import kotlinx.collections.immutable.toPersistentSet
import kotlinx.coroutines.CancellationException
import org.utbot.common.WorkaroundReason.HACK
import org.utbot.common.WorkaroundReason.REMOVE_ANONYMOUS_CLASSES
import org.utbot.common.findField
Expand Down Expand Up @@ -213,6 +212,7 @@ class Traverser(
private val classLoader: ClassLoader
get() = utContext.classLoader

// TODO: move this and other mutable fields to [TraversalContext]
lateinit var environment: Environment
Comment thread
SBOne-Kenobi marked this conversation as resolved.
private val solver: UtSolver
get() = environment.state.solver
Expand Down Expand Up @@ -281,13 +281,9 @@ class Traverser(
} catch (ex: Throwable) {
environment.state.close()

if (ex !is CancellationException) {
logger.error(ex) { "Test generation failed on stmt $currentStmt, symbolic stack trace:\n$symbolicStackTrace" }
// TODO: enrich with nice description for known issues
throw ex
} else {
logger.debug(ex) { "Cancellation happened" }
}
logger.error(ex) { "Test generation failed on stmt $currentStmt, symbolic stack trace:\n$symbolicStackTrace" }
// TODO: enrich with nice description for known issues
throw ex
}
queuedSymbolicStateUpdates = SymbolicStateUpdate()
return context.nextStates
Expand Down Expand Up @@ -2991,7 +2987,8 @@ class Traverser(
implicitlyThrowException(NullPointerException(), setOf(notMarkedAndNull))
}

queuedSymbolicStateUpdates += canNotBeNull.asHardConstraint() }
queuedSymbolicStateUpdates += canNotBeNull.asHardConstraint()
}

private fun TraversalContext.divisionByZeroCheck(denom: PrimitiveValue) {
val equalsToZero = Eq(denom, 0)
Expand Down Expand Up @@ -3363,7 +3360,8 @@ class Traverser(
return
}

//toplevel method
// toplevel method
// TODO: investigate very strange behavior when some constraints are not added leading to failing CodegenExampleTest::firstExampleTest fails
val terminalExecutionState = environment.state.copy(
symbolicState = symbolicState,
methodResult = methodResult, // the way to put SymbolicResult into terminal state
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -351,6 +351,8 @@ class UtBotSymbolicEngine(
// So we need to make it throw CancelledException by method below:
currentCoroutineContext().job.ensureActive()
}

// TODO: think about concise modifying globalGraph in Traverser and UtBotSymbolicEngine
globalGraph.visitNode(state)
Comment thread
SBOne-Kenobi marked this conversation as resolved.
}
}
Expand Down