Skip to content
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

Extract Traverser from UtBotSymbolicEngine #307

Merged
merged 19 commits into from
Jul 8, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
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
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@

/**
* Auxiliary class with static methods without implementation.
* These static methods are just markers for <code>UtBotSymbolicEngine</code>,
* These static methods are just markers for {@link org.utbot.engine.Traverser}.,
* to do some corresponding behavior, that can't be represent
* with java instructions.
* <p>
Expand All @@ -15,7 +15,7 @@
@SuppressWarnings("unused")
public class UtArrayMock {
/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of {@link java.util.Arrays#copyOf(Object[], int)}
* if length is less or equals to src.length, otherwise first
* src.length elements are equal to src, but the rest are undefined.
Expand Down Expand Up @@ -45,7 +45,7 @@ public static char[] copyOf(char[] src, int length) {
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand All @@ -67,7 +67,7 @@ public static void arraycopy(Object[] src, int srcPos, Object[] dst, int destPos
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand All @@ -83,7 +83,7 @@ public static void arraycopy(boolean[] src, int srcPos, boolean[] dst, int destP
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand All @@ -99,7 +99,7 @@ public static void arraycopy(byte[] src, int srcPos, byte[] dst, int destPos, in
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand All @@ -115,7 +115,7 @@ public static void arraycopy(char[] src, int srcPos, char[] dst, int destPos, in
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand All @@ -131,7 +131,7 @@ public static void arraycopy(short[] src, int srcPos, short[] dst, int destPos,
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand All @@ -147,7 +147,7 @@ public static void arraycopy(int[] src, int srcPos, int[] dst, int destPos, int
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand All @@ -163,7 +163,7 @@ public static void arraycopy(long[] src, int srcPos, long[] dst, int destPos, in
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand All @@ -179,7 +179,7 @@ public static void arraycopy(float[] src, int srcPos, float[] dst, int destPos,
}

/**
* Traversing this instruction by <code>UtBotSymbolicEngine</code> should
* Traversing this instruction by {@link org.utbot.engine.Traverser} should
* behave similar to call of
* {@link java.lang.System#arraycopy(Object, int, Object, int, int)}
* if all the arguments are valid.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

/**
* Auxiliary class with static methods without implementation.
* These static methods are just markers for <code>UtBotSymbolicEngine</code>,
* These static methods are just markers for {@link org.utbot.engine.Traverser},
* to do some corresponding behavior, that can be represented with smt expressions.
* <p>
* <code>UtLogicMock</code> is used to store bool smt bool expressions in
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@

/**
* Auxiliary class with static methods without implementation.
* These static methods are just markers for UtBotSymbolicEngine,
* These static methods are just markers for {@link org.utbot.engine.Traverser},
* to do some corresponding behavior, that can't be represent
* with java instructions.
*
* Set of methods in UtOverrideMock is used in code of classes,
* that override implementation of some standard class by new implementation,
* that is more simple for UtBotSymbolicEngine to traverse.
* that is more simple for {@link org.utbot.engine.Traverser} to traverse.
*/
@SuppressWarnings("unused")
public class UtOverrideMock {
Expand All @@ -25,7 +25,7 @@ public static boolean alreadyVisited(Object o) {
}

/**
* If UtBotSymbolicEngine meets invoke of this method in code,
* If {@link org.utbot.engine.Traverser} meets invoke of this method in code,
* then it marks the address of object o in memory as visited
* and creates new MemoryUpdate with parameter isVisited, equal to o.addr
* @param o parameter, that need to be marked as visited.
Expand All @@ -34,7 +34,7 @@ public static void visit(Object o) {
}

/**
* If UtBotSymbolicEngine meets invoke of this method in code,
* If {@link org.utbot.engine.Traverser} meets invoke of this method in code,
* then it marks the method, where met instruction is placed,
* and all the methods that will be traversed in nested invokes
* as methods that couldn't throw exceptions.
Expand All @@ -44,7 +44,7 @@ public static void doesntThrow() {
}

/**
* If UtBotSymbolicEngine meets invoke of this method in code,
* If {@link org.utbot.engine.Traverser} meets invoke of this method in code,
* then it assumes that the specified object is parameter,
* and need to be marked as parameter.
* As address space of parameters in engine is non-positive, while
Expand All @@ -63,7 +63,7 @@ public static void parameter(Object[] objects) {
}

/**
* If UtBotSymbolicEngine meets invoke of this method in code,
* If {@link org.utbot.engine.Traverser} meets invoke of this method in code,
* then it starts concrete execution from this point.
*/
public static void executeConcretely() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@


/**
* Class represents hybrid implementation (java + engine instructions) of List interface for UtBotSymbolicEngine.
* Class represents hybrid implementation (java + engine instructions) of List interface for {@link org.utbot.engine.Traverser}.
* <p>
* Implementation is based on org.utbot.engine.overrides.collections.RangeModifiableArray.
* Should behave similar to {@link java.util.ArrayList}.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@


/**
* Class represents hybrid implementation (java + engine instructions) of Map interface for UtBotSymbolicEngine.
* Class represents hybrid implementation (java + engine instructions) of Map interface for {@link org.utbot.engine.Traverser}.
* <p>
* Implementation is based on using org.utbot.engine.overrides.collections.RangeModifiableArray as keySet
* and org.utbot.engine.overrides.collections.UtArray as associative array from keys to values.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
import static org.utbot.engine.overrides.UtOverrideMock.visit;

/**
* Class represents hybrid implementation (java + engine instructions) of Set interface for UtBotSymbolicEngine.
* Class represents hybrid implementation (java + engine instructions) of Set interface for {@link org.utbot.engine.Traverser}.
* <p>
* Implementation is based on RangedModifiableArray, and all operations are linear.
* Should behave similar to
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
import static org.utbot.engine.overrides.UtOverrideMock.visit;

/**
* Class represents hybrid implementation (java + engine instructions) of Optional for UtBotSymbolicEngine.
* Class represents hybrid implementation (java + engine instructions) of Optional for {@link org.utbot.engine.Traverser}.
* <p>
* Should behave the same as {@link java.util.Optional}.
* @see org.utbot.engine.OptionalWrapper
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
import static org.utbot.engine.overrides.UtOverrideMock.visit;

/**
* Class represents hybrid implementation (java + engine instructions) of OptionalDouble for UtBotSymbolicEngine.
* Class represents hybrid implementation (java + engine instructions) of OptionalDouble for {@link org.utbot.engine.Traverser}.
* <p>
* Should behave the same as {@link java.util.OptionalDouble}.
* @see org.utbot.engine.OptionalWrapper
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
import static org.utbot.engine.overrides.UtOverrideMock.visit;

/**
* Class represents hybrid implementation (java + engine instructions) of OptionalInt for UtBotSymbolicEngine.
* Class represents hybrid implementation (java + engine instructions) of OptionalInt for {@link org.utbot.engine.Traverser}.
* <p>
* Should behave the same as {@link java.util.OptionalInt}.
* @see org.utbot.engine.OptionalWrapper
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
import static org.utbot.engine.overrides.UtOverrideMock.visit;

/**
* Class represents hybrid implementation (java + engine instructions) of Optional for UtBotSymbolicEngine.
* Class represents hybrid implementation (java + engine instructions) of Optional for {@link org.utbot.engine.Traverser}.
* <p>
* Should behave the same as {@link java.util.Optional}.
* @see org.utbot.engine.OptionalWrapper
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ import soot.SootMethod
val rangeModifiableArrayId: ClassId = RangeModifiableUnlimitedArray::class.id

class RangeModifiableUnlimitedArrayWrapper : WrapperInterface {
override fun UtBotSymbolicEngine.invoke(
override fun Traverser.invoke(
wrapper: ObjectValue,
method: SootMethod,
parameters: List<SymbolicValue>
Expand Down Expand Up @@ -203,10 +203,10 @@ class RangeModifiableUnlimitedArrayWrapper : WrapperInterface {
}
}

private fun UtBotSymbolicEngine.getStorageArrayField(addr: UtAddrExpression) =
private fun Traverser.getStorageArrayField(addr: UtAddrExpression) =
getArrayField(addr, rangeModifiableArrayClass, storageField)

private fun UtBotSymbolicEngine.getStorageArrayExpression(
private fun Traverser.getStorageArrayExpression(
wrapper: ObjectValue
): UtExpression = selectArrayExpressionFromMemory(getStorageArrayField(wrapper.addr))

Expand Down Expand Up @@ -285,7 +285,7 @@ class AssociativeArrayWrapper : WrapperInterface {
private val storageField = associativeArrayClass.getField("java.lang.Object[] storage")


override fun UtBotSymbolicEngine.invoke(
override fun Traverser.invoke(
wrapper: ObjectValue,
method: SootMethod,
parameters: List<SymbolicValue>
Expand Down Expand Up @@ -414,16 +414,16 @@ class AssociativeArrayWrapper : WrapperInterface {
return model
}

private fun UtBotSymbolicEngine.getStorageArrayField(addr: UtAddrExpression) =
private fun Traverser.getStorageArrayField(addr: UtAddrExpression) =
getArrayField(addr, associativeArrayClass, storageField)

private fun UtBotSymbolicEngine.getTouchedArrayField(addr: UtAddrExpression) =
private fun Traverser.getTouchedArrayField(addr: UtAddrExpression) =
getArrayField(addr, associativeArrayClass, touchedField)

private fun UtBotSymbolicEngine.getTouchedArrayExpression(wrapper: ObjectValue): UtExpression =
private fun Traverser.getTouchedArrayExpression(wrapper: ObjectValue): UtExpression =
selectArrayExpressionFromMemory(getTouchedArrayField(wrapper.addr))

private fun UtBotSymbolicEngine.getStorageArrayExpression(
private fun Traverser.getStorageArrayExpression(
wrapper: ObjectValue
): UtExpression = selectArrayExpressionFromMemory(getStorageArrayField(wrapper.addr))
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ abstract class BaseOverriddenWrapper(protected val overriddenClassName: String)
*
* @see invoke
*/
protected abstract fun UtBotSymbolicEngine.overrideInvoke(
protected abstract fun Traverser.overrideInvoke(
wrapper: ObjectValue,
method: SootMethod,
parameters: List<SymbolicValue>
Expand All @@ -65,11 +65,11 @@ abstract class BaseOverriddenWrapper(protected val overriddenClassName: String)
*
* Multiple GraphResults are returned because, we shouldn't substitute invocation of specified
* that was called inside substituted method of object with the same address as specified [wrapper].
* (For example UtArrayList.<init> invokes AbstractList.<init> that also leads to UtBotSymbolicEngine.invoke,
* (For example UtArrayList.<init> invokes AbstractList.<init> that also leads to [Traverser.invoke],
* and shouldn't be substituted with UtArrayList.<init> again). Only one GraphResult is valid, that is
* guaranteed by contradictory to each other sets of constraints, added to them.
*/
override fun UtBotSymbolicEngine.invoke(
override fun Traverser.invoke(
wrapper: ObjectValue,
method: SootMethod,
parameters: List<SymbolicValue>
Expand Down Expand Up @@ -162,7 +162,7 @@ abstract class BaseContainerWrapper(containerClassName: String) : BaseOverridden
}

abstract class BaseGenericStorageBasedContainerWrapper(containerClassName: String) : BaseContainerWrapper(containerClassName) {
override fun UtBotSymbolicEngine.overrideInvoke(
override fun Traverser.overrideInvoke(
wrapper: ObjectValue,
method: SootMethod,
parameters: List<SymbolicValue>
Expand Down Expand Up @@ -283,7 +283,7 @@ class SetWrapper : BaseGenericStorageBasedContainerWrapper(UtHashSet::class.qual
* entries, then real behavior of generated test can differ from expected and undefined.
*/
class MapWrapper : BaseContainerWrapper(UtHashMap::class.qualifiedName!!) {
override fun UtBotSymbolicEngine.overrideInvoke(
override fun Traverser.overrideInvoke(
wrapper: ObjectValue,
method: SootMethod,
parameters: List<SymbolicValue>
Expand Down Expand Up @@ -418,14 +418,14 @@ val HASH_MAP_TYPE: RefType
val STREAM_TYPE: RefType
get() = Scene.v().getSootClass(java.util.stream.Stream::class.java.canonicalName).type

internal fun UtBotSymbolicEngine.getArrayField(
internal fun Traverser.getArrayField(
addr: UtAddrExpression,
wrapperClass: SootClass,
field: SootField
): ArrayValue =
createFieldOrMock(wrapperClass.type, addr, field, mockInfoGenerator = null) as ArrayValue

internal fun UtBotSymbolicEngine.getIntFieldValue(wrapper: ObjectValue, field: SootField): UtExpression {
internal fun Traverser.getIntFieldValue(wrapper: ObjectValue, field: SootField): UtExpression {
val chunkId = hierarchy.chunkIdForField(field.declaringClass.type, field)
val descriptor = MemoryChunkDescriptor(chunkId, field.declaringClass.type, IntType.v())
val array = memory.findArray(descriptor, MemoryState.CURRENT)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ data class OverrideResult(
* there is only one usage of it: to support instanceof for arrays we have to update them in the memory.
*
* @see UtInstanceOfExpression
* @see UtBotSymbolicEngine.resolveIfCondition
* @see Traverser.resolveIfCondition
*/
data class ResolvedCondition(
val condition: UtBoolExpression,
Expand Down
Loading