Fix bug with tracing of approximated methods

UnitTestBot · Dec 1, 2023 · 1185f3b · 1185f3b
1 parent 0c208ff
commit 1185f3b
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/usvm-jvm-instrumentation/build.gradle.kts b/usvm-jvm-instrumentation/build.gradle.kts
@@ -43,6 +43,7 @@ kotlin {
 dependencies {
     implementation("org.jacodb:jacodb-core:${Versions.jcdb}")
     implementation("org.jacodb:jacodb-analysis:${Versions.jcdb}")
+    implementation("org.jacodb:jacodb-approximations:${Versions.jcdb}")
 
     implementation("com.jetbrains.rd:rd-framework:${Versions.rd}")
     implementation("org.ini4j:ini4j:${Versions.ini4j}")

diff --git a/...-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/executor/RdProcessRunner.kt b/...-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/executor/RdProcessRunner.kt
@@ -10,7 +10,7 @@ import kotlinx.coroutines.delay
 import org.jacodb.api.JcClassOrInterface
 import org.jacodb.api.JcClasspath
 import org.jacodb.api.cfg.JcInst
-import org.jacodb.api.ext.methods
+import org.jacodb.approximation.JcEnrichedVirtualMethod
 import org.usvm.instrumentation.generated.models.*
 import org.usvm.instrumentation.rd.*
 import org.usvm.instrumentation.util.findFieldByFullNameOrNull
@@ -196,13 +196,16 @@ class RdProcessRunner(
                 val jcClass =
                     deserializedClassesCache.getOrPut(classId) {
                         val className = coveredClasses.find { it.classId == classId }
-                            ?: error("Deserialization error")
-                        jcClasspath.findClassOrNull(className.className) ?: error("Deserialization error")
+                            ?: error("Trace deserialization error")
+                        jcClasspath.findClassOrNull(className.className) ?: error("Trace deserialization error")
                     }
-                val jcMethod = jcClass.methods.sortedBy { it.description }[methodId.toInt()]
+                if (jcClass.declaredMethods.any { it is JcEnrichedVirtualMethod }) {
+                    return listOf()
+                }
+                val jcMethod = jcClass.declaredMethods.sortedBy { it.description }[methodId.toInt()]
                 jcMethod.instList
                     .find { it.location.index == instructionId }
-                    ?: error("Deserialization error")
+                    ?: error("Trace deserialization error")
             }
         }
 

diff --git a/...mentation/src/main/kotlin/org/usvm/instrumentation/instrumentation/JcInstructionTracer.kt b/...mentation/src/main/kotlin/org/usvm/instrumentation/instrumentation/JcInstructionTracer.kt
@@ -6,7 +6,6 @@ import org.jacodb.api.JcField
 import org.jacodb.api.JcMethod
 import org.jacodb.api.cfg.JcInst
 import org.jacodb.api.cfg.JcRawFieldRef
-import org.jacodb.api.ext.methods
 import org.usvm.instrumentation.collector.trace.TraceCollector
 import org.usvm.instrumentation.instrumentation.JcInstructionTracer.StaticFieldAccessType
 import org.usvm.instrumentation.util.enclosingClass
@@ -75,7 +74,7 @@ object JcInstructionTracer : Tracer<Trace> {
 
     private fun encodeMethod(jcClass: JcClassOrInterface, jcMethod: JcMethod): EncodedMethod {
         val encodedClass = encodeClass(jcClass)
-        val methodIndex = jcClass.methods
+        val methodIndex = jcClass.declaredMethods
             .sortedBy { it.description }
             .indexOf(jcMethod)
             .also { if (it == -1) error("Encoding error") }