Allow configuring paths to instrumentation jars, approximation jars and java home (#166)

Author: IlyaMuravjov

usvm-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/agent/Agent.kt

@@ -11,7 +11,7 @@ class Agent {
     companion object {
         @JvmStatic
         fun premain(arguments: String?, instrumentation: Instrumentation) {
-            val collectorsJarPath = InstrumentationModuleConstants.pathToUsvmCollectorsJar
+            val collectorsJarPath = System.getenv(InstrumentationModuleConstants.envVarForPathToUsvmCollectorsJarPath)
             val collectorsJar = JarFile(File(collectorsJarPath))
             instrumentation.appendToBootstrapClassLoaderSearch(collectorsJar)
             val instrumenterFactoryClassname = arguments ?: JcRuntimeTraceInstrumenterFactory::class.java.name

usvm-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/executor/InstrumentationProcessPaths.kt

@@ -0,0 +1,7 @@
+package org.usvm.instrumentation.executor
+
+data class InstrumentationProcessPaths(
+    val pathToUsvmInstrumentationJar: String = System.getenv("usvm-jvm-instrumentation-jar"),
+    val pathToUsvmCollectorsJar: String = System.getenv("usvm-jvm-collectors-jar"),
+    val pathToJava: String = System.getenv()["JAVA_HOME"] ?: System.getProperty("java.home")
+)

usvm-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/executor/InstrumentationProcessRunner.kt

@@ -22,7 +22,7 @@ import kotlin.time.Duration
 class InstrumentationProcessRunner(
     private val testingProjectClasspath: String,
     private val jcClasspath: JcClasspath,
-    private val javaHome: String,
+    private val instrumentationProcessPaths: InstrumentationProcessPaths,
     private val jcPersistenceLocation: String?,
     private val instrumentationClassFactory: KClass<out JcInstrumenterFactory<out JcInstrumenter>>
 ) {
@@ -33,13 +33,13 @@ class InstrumentationProcessRunner(
     constructor(
         testingProjectClasspath: List<String>,
         jcClasspath: JcClasspath,
-        javaHome: String,
+        instrumentationProcessPaths: InstrumentationProcessPaths,
         jcPersistenceLocation: String?,
         instrumentationClassFactory: KClass<JcInstrumenterFactory<out JcInstrumenter>>
     ) : this(
         testingProjectClasspath.joinToString(File.pathSeparator),
         jcClasspath,
-        javaHome,
+        instrumentationProcessPaths,
         jcPersistenceLocation,
         instrumentationClassFactory
     )
@@ -49,14 +49,14 @@ class InstrumentationProcessRunner(
     private val jvmArgs: List<String> by lazy {
         val instrumentationClassNameFactoryName = instrumentationClassFactory.java.name
         val memoryLimit = listOf("-Xmx1g")
-        val pathToJava = Paths.get(InstrumentationModuleConstants.pathToJava)
+        val pathToJava = Paths.get(instrumentationProcessPaths.pathToJava)
         val usvmClasspath = System.getProperty("java.class.path")
         val javaVersionSpecificArguments = OpenModulesContainer.javaVersionSpecificArguments
         val instrumentedProcessClassName =
             InstrumentedProcess::class.qualifiedName ?: error("Can't find instumented process")
         listOf(pathToJava.resolve("bin${File.separatorChar}${osSpecificJavaExecutable()}").toString()) +
                 listOf("-ea") +
-                listOf("-javaagent:${InstrumentationModuleConstants.pathToUsvmInstrumentationJar}=$instrumentationClassNameFactoryName") +
+                listOf("-javaagent:${instrumentationProcessPaths.pathToUsvmInstrumentationJar}=$instrumentationClassNameFactoryName") +
                 memoryLimit +
                 javaVersionSpecificArguments +
                 listOf("-classpath", usvmClasspath) +
@@ -67,7 +67,7 @@ class InstrumentationProcessRunner(
         this += listOf("-cp", testingProjectClasspath)
         this += listOf("-t", "${InstrumentationModuleConstants.concreteExecutorProcessTimeout}")
         this += listOf("-p", "$rdPort")
-        this += listOf("-javahome", javaHome)
+        this += listOf("-javahome", instrumentationProcessPaths.pathToJava)
 
         if (jcPersistenceLocation != null) {
             this += listOf("-persistence", jcPersistenceLocation)
@@ -80,6 +80,8 @@ class InstrumentationProcessRunner(
         val rdPort = NetUtils.findFreePort(0)
         val workerCommand = jvmArgs + createWorkerProcessArgs(rdPort)
         val pb = ProcessBuilder(workerCommand).inheritIO()
+        pb.environment()[InstrumentationModuleConstants.envVarForPathToUsvmCollectorsJarPath] =
+            instrumentationProcessPaths.pathToUsvmCollectorsJar
         val process = pb.start()
         rdProcessRunner =
             RdProcessRunner(process = process, rdPort = rdPort, jcClasspath = jcClasspath, lifetime = processLifetime)

usvm-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/executor/UTestConcreteExecutor.kt

@@ -18,7 +18,7 @@ class UTestConcreteExecutor(
     instrumentationClassFactory: KClass<out JcInstrumenterFactory<*>>,
     testingProjectClasspath: String,
     private val jcClasspath: JcClasspath,
-    private val javaHome: String,
+    instrumentationProcessPaths: InstrumentationProcessPaths,
     private val jcPersistenceLocation: String?,
     private val timeout: Duration
 ) : AutoCloseable {
@@ -27,14 +27,14 @@ class UTestConcreteExecutor(
         instrumentationClassFactory: KClass<out JcInstrumenterFactory<*>>,
         testingProjectClasspath: List<String>,
         jcClasspath: JcClasspath,
-        javaHome: String,
+        instrumentationProcessPaths: InstrumentationProcessPaths,
         jcPersistenceLocation: String?,
         timeout: Duration
     ) : this(
         instrumentationClassFactory,
         testingProjectClasspath.joinToString(File.pathSeparator),
         jcClasspath,
-        javaHome,
+        instrumentationProcessPaths,
         jcPersistenceLocation,
         timeout
     )
@@ -44,7 +44,7 @@ class UTestConcreteExecutor(
     private val instrumentationProcessRunner = InstrumentationProcessRunner(
         testingProjectClasspath,
         jcClasspath,
-        javaHome,
+        instrumentationProcessPaths,
         jcPersistenceLocation,
         instrumentationClassFactory
     )

usvm-jvm-instrumentation/src/main/kotlin/org/usvm/instrumentation/util/Constants.kt

@@ -23,14 +23,6 @@ object InstrumentationModuleConstants {
 
     const val nameForExistingButNullString = "USVM_GENERATED_NULL_STRING"
 
-    //Passes as environment parameter
-    val pathToUsvmInstrumentationJar: String
-        get() = System.getenv("usvm-jvm-instrumentation-jar")
-
-    val pathToUsvmCollectorsJar: String
-        get() = System.getenv("usvm-jvm-collectors-jar")
-
-    val pathToJava: String
-        get() = System.getenv()["JAVA_HOME"] ?: System.getProperty("java.home")
-
+    //Environment variable used to pass path to collectors jar from main process to instrumented process
+    val envVarForPathToUsvmCollectorsJarPath = "usvm-jvm-collectors-jar"
 }

usvm-jvm-instrumentation/src/test/kotlin/org/usvm/instrumentation/executor/UTestConcreteExecutorTest.kt

@@ -18,6 +18,7 @@ abstract class UTestConcreteExecutorTest {
         lateinit var jcClasspath: JcClasspath
         lateinit var jcPersistenceLocation: String
         lateinit var uTestConcreteExecutor: UTestConcreteExecutor
+        var instrumentationProcessPaths = InstrumentationProcessPaths()
 
 
         @JvmStatic
@@ -27,7 +28,7 @@ abstract class UTestConcreteExecutorTest {
             val db = jacodb {
                 loadByteCode(cp)
                 installFeatures(InMemoryHierarchy)
-                jre = File(InstrumentationModuleConstants.pathToJava)
+                jre = File(instrumentationProcessPaths.pathToJava)
                 persistent(location = jcPersistenceLocation)
             }
             db.awaitBackgroundJobs()
@@ -40,7 +41,7 @@ abstract class UTestConcreteExecutorTest {
                 instrumentationClassFactory = JcRuntimeTraceInstrumenterFactory::class,
                 testingProjectClasspath = testJarPath,
                 jcClasspath = jcClasspath,
-                javaHome = InstrumentationModuleConstants.pathToJava,
+                instrumentationProcessPaths = instrumentationProcessPaths,
                 jcPersistenceLocation = jcPersistenceLocation,
                 timeout = InstrumentationModuleConstants.testExecutionTimeout
             )

usvm-jvm/src/main/kotlin/org/usvm/types/ClassScorer.kt

@@ -11,24 +11,21 @@ import org.jacodb.impl.fs.className
 import org.jacodb.impl.storage.withoutAutoCommit
 import org.jooq.DSLContext
 import org.objectweb.asm.tree.ClassNode
-import org.usvm.util.USVM_API_JAR_PATH
-import org.usvm.util.USVM_APPROXIMATIONS_JAR_PATH
+import org.usvm.util.ApproximationPaths
 import java.util.concurrent.ConcurrentHashMap
 
 typealias ScoreCache<Result> = ConcurrentHashMap<Long, Result>
 
-private val usvmApiJarPath = System.getenv(USVM_API_JAR_PATH)
-private val usvmApproximationsJarPath = System.getenv(USVM_APPROXIMATIONS_JAR_PATH)
-
 class ScorerIndexer<Result : Comparable<Result>>(
     private val persistence: JcDatabasePersistence,
     private val location: RegisteredLocation,
     private val cache: ScoreCache<Result>,
     private val scorer: (RegisteredLocation, ClassNode) -> Result,
+    approximationPaths: ApproximationPaths = ApproximationPaths(),
 ) : ByteCodeIndexer {
     private val interner = persistence.symbolInterner
 
-    private val bad: Boolean = usvmApiJarPath in location.path || usvmApproximationsJarPath in location.path
+    private val bad: Boolean = approximationPaths.presentPaths.any { it in location.path }
 
     override fun index(classNode: ClassNode) {
         val clazzSymbolId = interner.findOrNew(classNode.name.className)

usvm-jvm/src/main/kotlin/org/usvm/util/JcApproximationUtils.kt

@@ -11,8 +11,17 @@ import org.usvm.machine.logger
 import java.io.File
 import java.util.concurrent.ConcurrentHashMap
 
-const val USVM_API_JAR_PATH = "usvm.jvm.api.jar.path"
-const val USVM_APPROXIMATIONS_JAR_PATH = "usvm.jvm.approximations.jar.path"
+data class ApproximationPaths(
+    val usvmApiJarPath: String? = System.getenv("usvm.jvm.api.jar.path"),
+    val usvmApproximationsJarPath: String? = System.getenv("usvm.jvm.approximations.jar.path")
+) {
+    val namedPaths = mapOf(
+        "USVM API" to usvmApiJarPath,
+        "USVM Approximations" to usvmApproximationsJarPath
+    )
+    val presentPaths: Set<String> = namedPaths.values.filterNotNull().toSet()
+    val allPathsArePresent = namedPaths.values.all { it != null }
+}
 
 private val classpathApproximations: MutableMap<JcClasspath, Set<String>> = ConcurrentHashMap()
 
@@ -29,19 +38,21 @@ val JcClassType.isUsvmInternalClass: Boolean
 
 suspend fun JcDatabase.classpathWithApproximations(
     dirOrJars: List<File>,
-    features: List<JcClasspathFeature> = emptyList()
+    features: List<JcClasspathFeature> = emptyList(),
+    approximationPaths: ApproximationPaths = ApproximationPaths(),
 ): JcClasspath {
-    val usvmApiJarPath = System.getenv(USVM_API_JAR_PATH)
-    val usvmApproximationsJarPath = System.getenv(USVM_APPROXIMATIONS_JAR_PATH)
-
-    if (usvmApiJarPath == null || usvmApproximationsJarPath == null) {
+    if (!approximationPaths.allPathsArePresent) {
+        logger.warn {
+            "Classpath with approximations is requested, but some jar paths are missing: $approximationPaths"
+        }
         return classpath(dirOrJars, features)
     }
 
-    logger.info { "Load USVM API: $usvmApiJarPath" }
-    logger.info { "Load USVM Approximations: $usvmApproximationsJarPath" }
+    approximationPaths.namedPaths.forEach { (name, path) ->
+        logger.info { "Load $name: $path" }
+    }
 
-    val approximationsPath = setOf(File(usvmApiJarPath), File(usvmApproximationsJarPath))
+    val approximationsPath = approximationPaths.presentPaths.map { File(it) }
 
     val cpWithApproximations = dirOrJars + approximationsPath
     val featuresWithApproximations = features + listOf(Approximations)

usvm-jvm/src/test/kotlin/org/usvm/util/UTestRunner.kt

@@ -4,6 +4,7 @@ import org.jacodb.api.JcClasspath
 import org.usvm.instrumentation.executor.UTestConcreteExecutor
 import org.usvm.instrumentation.instrumentation.JcRuntimeTraceInstrumenterFactory
 import org.usvm.instrumentation.util.InstrumentationModuleConstants
+import org.usvm.instrumentation.executor.InstrumentationProcessPaths
 
 object UTestRunner {
 
@@ -16,7 +17,7 @@ object UTestRunner {
             instrumentationClassFactory = JcRuntimeTraceInstrumenterFactory::class,
             testingProjectClasspath = pathToJars,
             jcClasspath = classpath,
-            javaHome = InstrumentationModuleConstants.pathToJava,
+            instrumentationProcessPaths = InstrumentationProcessPaths(),
             jcPersistenceLocation = null,
             timeout = InstrumentationModuleConstants.testExecutionTimeout
         )