Skip to content

Stepanov/jvm instrumentation persistent descriptors #112

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
merged 5 commits into from
Nov 18, 2023
Merged

Stepanov/jvm instrumentation persistent descriptors #112

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
609d076
concept of persistent descriptors implemented
DaniilStepanov Nov 16, 2023
5386aed
assume fix for concrete execution
DaniilStepanov Nov 16, 2023
eebca39
Now it is possible to run specific classes with specific test resolvi…
DaniilStepanov Nov 16, 2023
1a07b10
fix of JcType.toJcClass() function
DaniilStepanov Nov 17, 2023
698e3bb
minor
DaniilStepanov Nov 17, 2023
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
4 changes: 2 additions & 2 deletions usvm-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/rd/InstrumentedProcess.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,14 @@ class InstrumentedProcess private constructor() {
}

private suspend fun initProcess(classpath: String) {
fileClassPath = classpath.split(':').map { File(it) }
fileClassPath = classpath.split(File.pathSeparatorChar).map { File(it) }
val db = jacodb {
loadByteCode(fileClassPath)
installFeatures(InMemoryHierarchy)
jre = File(InstrumentationModuleConstants.pathToJava)
//persistent(location = "/home/.usvm/jcdb.db", clearOnStart = false)
}
jcClasspath = db.asyncClasspath(fileClassPath).get()
jcClasspath = db.classpath(fileClassPath)
serializationCtx = SerializationContext(jcClasspath)
ucp = URLClassPathLoader(fileClassPath)
uTestExecutor = UTestExecutor(jcClasspath, ucp)
Expand Down
20 changes: 5 additions & 15 deletions usvm-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/rd/UTestExecutor.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,7 @@ import org.usvm.instrumentation.instrumentation.JcInstructionTracer
import org.usvm.instrumentation.mock.MockHelper
import org.usvm.instrumentation.testcase.UTest
import org.usvm.instrumentation.testcase.api.*
import org.usvm.instrumentation.testcase.descriptor.StaticDescriptorsBuilder
import org.usvm.instrumentation.testcase.descriptor.UTestExceptionDescriptor
import org.usvm.instrumentation.testcase.descriptor.Value2DescriptorConverter
import org.usvm.instrumentation.testcase.descriptor.*
import org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor
import org.usvm.instrumentation.util.InstrumentationModuleConstants
import org.usvm.instrumentation.util.URLClassPathLoader
Expand Down Expand Up @@ -94,15 +92,6 @@ class UTestExecutor(
accessedStatics = hashSetOf()
)

executor.clearCache()
executor.executeUTestInsts(uTest.initStatements)
?.onFailure {
return UTestExecutionInitFailedResult(
cause = buildExceptionDescriptor(initStateDescriptorBuilder, it, false),
trace = JcInstructionTracer.getTrace().trace
)
}

val methodInvocationResult =
executor.executeUTestInst(callMethodExpr)
val resultStateDescriptorBuilder =
Expand Down Expand Up @@ -157,7 +146,8 @@ class UTestExecutor(
exception: Throwable,
raisedByUserCode: Boolean
): UTestExceptionDescriptor {
val descriptor = builder.buildDescriptorResultFromAny(any = exception, type = null).getOrNull() as? UTestExceptionDescriptor
val descriptor =
builder.buildDescriptorResultFromAny(any = exception, type = null).getOrNull() as? UTestExceptionDescriptor
return descriptor
?.also { it.raisedByUserCode = raisedByUserCode }
?: UTestExceptionDescriptor(
Expand All @@ -174,14 +164,14 @@ class UTestExecutor(
descriptorBuilder: Value2DescriptorConverter,
accessedStatics: MutableSet<Pair<JcField, JcInstructionTracer.StaticFieldAccessType>>
): UTestExecutionState = with(descriptorBuilder) {
descriptorBuilder.uTestExecutorCache.addAll(executor.objectToInstructionsCache)
uTestExecutorCache.addAll(executor.objectToInstructionsCache)
val instanceDescriptor = callMethodExpr.instance?.let {
buildDescriptorFromUTestExpr(it, executor).getOrNull()
}
val argsDescriptors = callMethodExpr.args.map {
buildDescriptorFromUTestExpr(it, executor).getOrNull()
}
val isInit = descriptorBuilder.previousState == null
val isInit = previousState == null
val statics = if (isInit) {
staticDescriptorsBuilder.builtInitialDescriptors
.mapValues { it.value!! }
Expand Down
182 changes: 7 additions & 175 deletions ...ion/src/main/kotlin/org/usvm/instrumentation/serializer/UTestValueDescriptorSerializer.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,15 +38,7 @@ class UTestValueDescriptorSerializer(private val ctx: SerializationContext) {
UTestValueDescriptorKind.NULL -> deserializeNull()
UTestValueDescriptorKind.STRING -> deserializeString()
UTestValueDescriptorKind.CYCLIC_REF -> deserializeCyclicRef()
UTestValueDescriptorKind.INT_ARRAY -> deserializeIntArray()
UTestValueDescriptorKind.BOOLEAN_ARRAY -> deserializeBooleanArray()
UTestValueDescriptorKind.BYTE_ARRAY -> deserializeByteArray()
UTestValueDescriptorKind.SHORT_ARRAY -> deserializeShortArray()
UTestValueDescriptorKind.LONG_ARRAY -> deserializeLongArray()
UTestValueDescriptorKind.DOUBLE_ARRAY -> deserializeDoubleArray()
UTestValueDescriptorKind.FLOAT_ARRAY -> deserializeFloatArray()
UTestValueDescriptorKind.CHAR_ARRAY -> deserializeCharArray()
UTestValueDescriptorKind.OBJECT_ARRAY -> deserializeArray()
UTestValueDescriptorKind.ARRAY -> deserializeArray()
UTestValueDescriptorKind.ENUM_VALUE -> deserializeEnumValue()
UTestValueDescriptorKind.CLASS -> deserializeClass()
UTestValueDescriptorKind.EXCEPTION -> deserializeException()
Expand All @@ -59,16 +51,8 @@ class UTestValueDescriptorSerializer(private val ctx: SerializationContext) {
private fun AbstractBuffer.serializeUTestValueDescriptor(uTestValueDescriptor: UTestValueDescriptor) {
if (ctx.serializedDescriptors.contains(uTestValueDescriptor)) return
when (uTestValueDescriptor) {
is UTestArrayDescriptor.Array -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor.BooleanArray -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor.ByteArray -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor.CharArray -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor.DoubleArray -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor.FloatArray -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor.IntArray -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor.LongArray -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor.ShortArray -> serialize(uTestValueDescriptor)
is UTestConstantDescriptor.Boolean -> serialize(uTestValueDescriptor)
is UTestArrayDescriptor -> serialize(uTestValueDescriptor)
is UTestConstantDescriptor.Byte -> serialize(uTestValueDescriptor)
is UTestConstantDescriptor.Char -> serialize(uTestValueDescriptor)
is UTestConstantDescriptor.Double -> serialize(uTestValueDescriptor)
Expand All @@ -86,10 +70,10 @@ class UTestValueDescriptorSerializer(private val ctx: SerializationContext) {
}
}

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.Array) =
private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.OBJECT_ARRAY,
kind = UTestValueDescriptorKind.ARRAY,
serializeInternals = {
value.forEach { serializeUTestValueDescriptor(it) }
},
Expand All @@ -101,163 +85,19 @@ class UTestValueDescriptorSerializer(private val ctx: SerializationContext) {
}
)

private fun AbstractBuffer.deserializeArray(): UTestArrayDescriptor.Array {
private fun AbstractBuffer.deserializeArray(): UTestArrayDescriptor {
val elementType = readJcType(jcClasspath) ?: jcClasspath.objectType
val refId = readInt()
val length = readInt()
val values = readList { readUTestValueDescriptor() }
return UTestArrayDescriptor.Array(
return UTestArrayDescriptor(
elementType = elementType,
length = length,
value = values,
refId = refId
)
}

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.BooleanArray) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.BOOLEAN_ARRAY,
serializeInternals = {},
serialize = {
writeInt(length)
writeBooleanArray(value)
}
)

private fun AbstractBuffer.deserializeBooleanArray(): UTestArrayDescriptor.BooleanArray =
UTestArrayDescriptor.BooleanArray(
elementType = jcClasspath.boolean,
length = readInt(),
value = readBooleanArray()
)

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.ByteArray) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.BYTE_ARRAY,
serializeInternals = {},
serialize = {
writeInt(length)
writeByteArray(value)
}
)

private fun AbstractBuffer.deserializeByteArray(): UTestArrayDescriptor.ByteArray =
UTestArrayDescriptor.ByteArray(
elementType = jcClasspath.byte,
length = readInt(),
value = readByteArray()
)

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.ShortArray) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.SHORT_ARRAY,
serializeInternals = {},
serialize = {
writeInt(length)
writeShortArray(value)
}
)

private fun AbstractBuffer.deserializeShortArray(): UTestArrayDescriptor.ShortArray =
UTestArrayDescriptor.ShortArray(
elementType = jcClasspath.short,
length = readInt(),
value = readShortArray()
)

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.IntArray) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.INT_ARRAY,
serializeInternals = {},
serialize = {
writeInt(length)
writeIntArray(value)
}
)

private fun AbstractBuffer.deserializeIntArray(): UTestArrayDescriptor.IntArray =
UTestArrayDescriptor.IntArray(
elementType = jcClasspath.int,
length = readInt(),
value = readIntArray()
)

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.LongArray) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.LONG_ARRAY,
serializeInternals = {},
serialize = {
writeInt(length)
writeLongArray(value)
}
)

private fun AbstractBuffer.deserializeLongArray(): UTestArrayDescriptor.LongArray =
UTestArrayDescriptor.LongArray(
elementType = jcClasspath.long,
length = readInt(),
value = readLongArray()
)

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.FloatArray) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.FLOAT_ARRAY,
serializeInternals = {},
serialize = {
writeInt(length)
writeFloatArray(value)
}
)

private fun AbstractBuffer.deserializeFloatArray(): UTestArrayDescriptor.FloatArray =
UTestArrayDescriptor.FloatArray(
elementType = jcClasspath.float,
length = readInt(),
value = readFloatArray()
)

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.DoubleArray) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.DOUBLE_ARRAY,
serializeInternals = {},
serialize = {
writeInt(length)
writeDoubleArray(value)
}
)

private fun AbstractBuffer.deserializeDoubleArray(): UTestArrayDescriptor.DoubleArray =
UTestArrayDescriptor.DoubleArray(
elementType = jcClasspath.double,
length = readInt(),
value = readDoubleArray()
)

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestArrayDescriptor.CharArray) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
kind = UTestValueDescriptorKind.CHAR_ARRAY,
serializeInternals = {},
serialize = {
writeInt(length)
writeCharArray(value)
}
)

private fun AbstractBuffer.deserializeCharArray(): UTestArrayDescriptor.CharArray =
UTestArrayDescriptor.CharArray(
elementType = jcClasspath.char,
length = readInt(),
value = readCharArray()
)

private fun AbstractBuffer.serialize(uTestValueDescriptor: UTestCyclicReferenceDescriptor) =
serialize(
uTestValueDescriptor = uTestValueDescriptor,
Expand Down Expand Up @@ -531,15 +371,7 @@ class UTestValueDescriptorSerializer(private val ctx: SerializationContext) {
CHAR,
NULL,
STRING,
INT_ARRAY,
BOOLEAN_ARRAY,
BYTE_ARRAY,
SHORT_ARRAY,
LONG_ARRAY,
DOUBLE_ARRAY,
FLOAT_ARRAY,
CHAR_ARRAY,
OBJECT_ARRAY,
ARRAY,
CYCLIC_REF,
ENUM_VALUE,
CLASS,
Expand Down
Loading