Skip to content

Сoncrete values for enums #19

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.

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
merged 7 commits into from
May 29, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 1 addition & 1 deletion utbot-core/src/main/kotlin/org/utbot/common/KClassUtil.kt
Original file line number Diff line number Diff line change
Expand Up @@ -28,4 +28,4 @@ fun Method.invokeCatching(obj: Any?, args: List<Any?>) = try {
Result.success(invoke(obj, *args.toTypedArray()))
} catch (e: InvocationTargetException) {
Result.failure<Nothing>(e.targetException)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ internal class SettingDelegate<T>(val initializer: () -> T) {
/**
* Default concrete execution timeout (in milliseconds).
*/
const val DEFAULT_CONCRETE_EXECUTION_TIMEOUT_IN_CHILD_PROCESS_MS = 100L
const val DEFAULT_CONCRETE_EXECUTION_TIMEOUT_IN_CHILD_PROCESS_MS = 1000L

object UtSettings {
private val properties = Properties().also { props ->
Expand Down
28 changes: 27 additions & 1 deletion utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ import org.utbot.engine.pc.mkLong
import org.utbot.engine.pc.mkShort
import org.utbot.engine.pc.select
import org.utbot.engine.pc.store
import org.utbot.engine.util.statics.concrete.isEnumValuesFieldName
import org.utbot.engine.symbolic.asHardConstraint
import org.utbot.engine.z3.intValue
import org.utbot.engine.z3.value
Expand Down Expand Up @@ -82,6 +83,7 @@ import soot.PrimType
import soot.RefType
import soot.Scene
import soot.ShortType
import soot.SootClass
import soot.SootField
import soot.Type
import soot.VoidType
Expand Down Expand Up @@ -1068,7 +1070,7 @@ fun UtBotSymbolicEngine.toMethodResult(value: Any?, sootType: Type): MethodResul
arrayToMethodResult(value.size, elementType) {
if (value[it] == null) return@arrayToMethodResult nullObjectAddr

val addr = UtAddrExpression(mkBVConst("staticVariable${value.hashCode()}", UtInt32Sort))
val addr = UtAddrExpression(mkBVConst("staticVariable${value.hashCode()}_$it", UtInt32Sort))

val createdElement = if (elementType is RefType) {
val className = value[it]!!.javaClass.id.name
Expand Down Expand Up @@ -1141,6 +1143,30 @@ private fun UtBotSymbolicEngine.arrayToMethodResult(
)
}

fun UtBotSymbolicEngine.constructEnumStaticFieldResult(
fieldName: String,
fieldType: Type,
declaringClass: SootClass,
enumConstantSymbolicResultsByName: Map<String, MethodResult>,
staticFieldConcreteValue: Any?,
enumConstantSymbolicValues: List<ObjectValue>
): MethodResult =
if (isEnumValuesFieldName(fieldName)) {
// special case to fill $VALUES array with already created symbolic values for enum constants runtime values
arrayToMethodResult(enumConstantSymbolicValues.size, declaringClass.type) { i ->
enumConstantSymbolicValues[i].addr
}
} else {
if (fieldName in enumConstantSymbolicResultsByName) {
// it is field to store enum constant so we use already created symbolic value from runtime enum constant
enumConstantSymbolicResultsByName.getValue(fieldName)
} else {
// otherwise, it is a common static field,
// and we have to create new symbolic value for it using its concrete value
toMethodResult(staticFieldConcreteValue, fieldType)
}
}

private val Type.unsigned: Boolean
get() = this is CharType

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@ import soot.Scene
import soot.SootField
import soot.Type
import soot.VoidType
import sun.reflect.Reflection

class TypeResolver(private val typeRegistry: TypeRegistry, private val hierarchy: Hierarchy) {

Expand Down
137 changes: 125 additions & 12 deletions utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,12 @@ import org.utbot.engine.symbolic.SymbolicStateUpdate
import org.utbot.engine.symbolic.asHardConstraint
import org.utbot.engine.symbolic.asSoftConstraint
import org.utbot.engine.symbolic.asUpdate
import org.utbot.engine.util.statics.concrete.associateEnumSootFieldsWithConcreteValues
import org.utbot.engine.util.statics.concrete.isEnumAffectingExternalStatics
import org.utbot.engine.util.statics.concrete.isEnumValuesFieldName
import org.utbot.engine.util.statics.concrete.makeEnumNonStaticFieldsUpdates
import org.utbot.engine.util.statics.concrete.makeEnumStaticFieldsUpdates
import org.utbot.engine.util.statics.concrete.makeSymbolicValuesFromEnumConcreteValues
import org.utbot.framework.PathSelectorType
import org.utbot.framework.UtSettings
import org.utbot.framework.UtSettings.checkSolverTimeoutMillis
Expand Down Expand Up @@ -152,6 +158,7 @@ import kotlinx.collections.immutable.persistentHashMapOf
import kotlinx.collections.immutable.persistentListOf
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 kotlinx.coroutines.Job
Expand Down Expand Up @@ -196,7 +203,6 @@ import soot.jimple.Expr
import soot.jimple.FieldRef
import soot.jimple.FloatConstant
import soot.jimple.IdentityRef
import soot.jimple.InstanceFieldRef
import soot.jimple.IntConstant
import soot.jimple.InvokeExpr
import soot.jimple.LongConstant
Expand Down Expand Up @@ -876,7 +882,7 @@ class UtBotSymbolicEngine(
stmt: Stmt
): Boolean {
if (shouldProcessStaticFieldConcretely(fieldRef)) {
return processStaticFieldConcretely(fieldRef)
return processStaticFieldConcretely(fieldRef, stmt)
}

val field = fieldRef.field
Expand Down Expand Up @@ -922,7 +928,9 @@ class UtBotSymbolicEngine(
// Note that this list is not exhaustive, so it may be supplemented in the future.
val packagesToProcessConcretely = javaPackagesToProcessConcretely + sunPackagesToProcessConcretely

return packagesToProcessConcretely.any { className.startsWith(it) }
val declaringClass = fieldRef.field.declaringClass

val isFromPackageToProcessConcretely = packagesToProcessConcretely.any { className.startsWith(it) }
// it is required to remove classes we override, since
// we could accidentally initialize their final fields
// with values that will later affect our overridden classes
Expand All @@ -933,6 +941,13 @@ class UtBotSymbolicEngine(
//hardcoded string for class name is used cause class is not public
//this is a hack to avoid crashing on code with Math.random()
&& !className.endsWith("RandomNumberGeneratorHolder")

// we can process concretely only enums that does not affect the external system
val isEnumNotAffectingExternalStatics = declaringClass.let {
it.isEnum && !it.isEnumAffectingExternalStatics(typeResolver)
}

return isEnumNotAffectingExternalStatics || isFromPackageToProcessConcretely
}
}

Expand All @@ -954,7 +969,7 @@ class UtBotSymbolicEngine(
*
* Returns true if processing takes place and Engine should end traversal of current statement.
*/
private fun processStaticFieldConcretely(fieldRef: StaticFieldRef): Boolean {
private fun processStaticFieldConcretely(fieldRef: StaticFieldRef, stmt: Stmt): Boolean {
val field = fieldRef.field
val fieldId = field.fieldId
if (memory.isInitialized(fieldId)) {
Expand All @@ -963,26 +978,123 @@ class UtBotSymbolicEngine(

// Gets concrete value, converts to symbolic value
val declaringClass = field.declaringClass

val (edge, updates) = if (declaringClass.isEnum) {
makeConcreteUpdatesForEnums(fieldId, declaringClass, stmt)
} else {
makeConcreteUpdatesForNonEnumStaticField(field, fieldId, declaringClass)
}

val newState = environment.state.updateQueued(edge, updates)
pathSelector.offer(newState)

return true
}

private fun makeConcreteUpdatesForEnums(
fieldId: FieldId,
declaringClass: SootClass,
stmt: Stmt
): Pair<Edge, SymbolicStateUpdate> {
val type = declaringClass.type
val jClass = type.id.jClass

// symbolic value for enum class itself
val enumClassValue = findOrCreateStaticObject(type)

// values for enum constants
val enumConstantConcreteValues = jClass.enumConstants.filterIsInstance<Enum<*>>()

val (enumConstantSymbolicValues, enumConstantSymbolicResultsByName) =
makeSymbolicValuesFromEnumConcreteValues(type, enumConstantConcreteValues)

val enumFields = typeResolver.findFields(type)

val sootFieldsWithRuntimeValues =
associateEnumSootFieldsWithConcreteValues(enumFields, enumConstantConcreteValues)

val (staticFields, nonStaticFields) = sootFieldsWithRuntimeValues.partition { it.first.isStatic }

val (staticFieldUpdates, curFieldSymbolicValueForLocalVariable) = makeEnumStaticFieldsUpdates(
staticFields,
declaringClass,
enumConstantSymbolicResultsByName,
enumConstantSymbolicValues,
enumClassValue,
fieldId
)

val nonStaticFieldsUpdates = makeEnumNonStaticFieldsUpdates(enumConstantSymbolicValues, nonStaticFields)

// we do not mark static fields for enum constants and $VALUES as meaningful
// because we should not set them in generated code
val meaningfulStaticFields = staticFields.filterNot {
val name = it.first.name

name in enumConstantSymbolicResultsByName.keys || isEnumValuesFieldName(name)
}

val initializedStaticFieldsMemoryUpdate = MemoryUpdate(
initializedStaticFields = staticFields.associate { it.first.fieldId to it.second.single() }.toPersistentMap(),
meaningfulStaticFields = meaningfulStaticFields.map { it.first.fieldId }.toPersistentSet()
)

var allUpdates = staticFieldUpdates + nonStaticFieldsUpdates + initializedStaticFieldsMemoryUpdate

// we need to make locals update if it is an assignment statement
// for enums we have only two types for assignment with enums — enum constant or $VALUES field
// for example, a jimple body for Enum::values method starts with the following lines:
// public static ClassWithEnum$StatusEnum[] values()
// {
// ClassWithEnum$StatusEnum[] $r0, $r2;
// java.lang.Object $r1;
// $r0 = <ClassWithEnum$StatusEnum: ClassWithEnum$StatusEnum[] $VALUES>;
// $r1 = virtualinvoke $r0.<java.lang.Object: java.lang.Object clone()>();

// so, we have to make an update for the local $r0
if (stmt is JAssignStmt) {
val local = stmt.leftOp as JimpleLocal
val localUpdate = localMemoryUpdate(
local.variable to curFieldSymbolicValueForLocalVariable
)

allUpdates += localUpdate
}

// enum static initializer can be the first statement in method so there will be no last edge
// for example, as it is during Enum::values method analysis:
// public static ClassWithEnum$StatusEnum[] values()
// {
// ClassWithEnum$StatusEnum[] $r0, $r2;
// java.lang.Object $r1;

// $r0 = <ClassWithEnum$StatusEnum: ClassWithEnum$StatusEnum[] $VALUES>;
val edge = environment.state.lastEdge ?: globalGraph.succ(stmt)

return edge to allUpdates
}

private fun makeConcreteUpdatesForNonEnumStaticField(
field: SootField,
fieldId: FieldId,
declaringClass: SootClass
): Pair<Edge, SymbolicStateUpdate> {
val concreteValue = extractConcreteValue(field, declaringClass)
val (symbolicResult, symbolicStateUpdate) = toMethodResult(concreteValue, field.type)
val symbolicValue = (symbolicResult as SymbolicSuccess).value

// Collects memory updates
val initializedFieldUpdate =
MemoryUpdate(initializedStaticFields = persistentHashMapOf(fieldId to concreteValue))

val objectUpdate = objectUpdate(
instance = findOrCreateStaticObject(declaringClass.type),
field = field,
value = valueToExpression(symbolicValue, field.type)
)
val allUpdates = symbolicStateUpdate + initializedFieldUpdate + objectUpdate
pathSelector.offer(
environment.state.updateQueued(
edge = environment.state.lastEdge!!,
allUpdates
)
)
return true

return environment.state.lastEdge!! to allUpdates
}

// Some fields are inaccessible with reflection, so we have to instantiate it by ourselves.
Expand Down Expand Up @@ -1200,7 +1312,7 @@ class UtBotSymbolicEngine(
/**
* Converts value to expression with cast to target type for primitives.
*/
private fun valueToExpression(value: SymbolicValue, type: Type): UtExpression = when (value) {
fun valueToExpression(value: SymbolicValue, type: Type): UtExpression = when (value) {
is ReferenceValue -> value.addr
// TODO: shall we add additional constraint that aligned expression still equals original?
// BitVector can lose valuable bites during extraction
Expand Down Expand Up @@ -2028,6 +2140,7 @@ class UtBotSymbolicEngine(
val touchedStaticFields = persistentListOf(staticFieldMemoryUpdate)
queuedSymbolicStateUpdates += MemoryUpdate(staticFieldsUpdates = touchedStaticFields)

// TODO filter enum constant static fields JIRA:1681
if (!environment.method.isStaticInitializer && !fieldId.isSynthetic) {
queuedSymbolicStateUpdates += MemoryUpdate(meaningfulStaticFields = persistentSetOf(fieldId))
}
Expand Down
Loading