Merge pull request #85 from vorpal-research/async-crash-reproduction

parallelized crash reproduction checker

core/src/main/kotlin/org/vorpal/research/kex/util/rt.kt

@@ -10,7 +10,7 @@ import org.vorpal.research.kthelper.logging.log
 import java.nio.file.Path
 import kotlin.io.path.readLines
 
-val Config.outputDirectory: Path get() = getPathValue("kex", "outputDir")!!
+val Config.outputDirectory: Path get() = getPathValue("kex", "outputDir")!!.normalize()
 
 val Config.instrumentedCodeDirectory: Path
     get() {
@@ -19,7 +19,7 @@ val Config.instrumentedCodeDirectory: Path
         if (!getBooleanValue("debug", "saveInstrumentedCode", false)) {
             deleteOnExit(instrumentedCodeDir)
         }
-        return instrumentedCodeDir
+        return instrumentedCodeDir.normalize()
     }
 
 val Config.compiledCodeDirectory: Path
@@ -29,21 +29,21 @@ val Config.compiledCodeDirectory: Path
         if (!getBooleanValue("debug", "saveCompiledCode", false)) {
             deleteOnExit(compiledCodeDir)
         }
-        return compiledCodeDir
+        return compiledCodeDir.normalize()
     }
 
 val Config.testcaseDirectory: Path
     get() {
         val testcaseDirName = getPathValue("testGen", "testsDir", "tests")
-        return outputDirectory.resolve(testcaseDirName).toAbsolutePath()
+        return outputDirectory.resolve(testcaseDirName).toAbsolutePath().normalize()
     }
 
 val Config.runtimeDepsPath: Path?
-    get() = getPathValue("kex", "runtimeDepsPath")
+    get() = getPathValue("kex", "runtimeDepsPath")?.normalize()
 
 val Config.libPath: Path?
     get() = getStringValue("kex", "libPath")?.let {
-        runtimeDepsPath?.resolve(it)
+        runtimeDepsPath?.resolve(it)?.normalize()
     }
 
 fun getRuntime(): Container? {

kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/crash/precondition/ExceptionPreconditionBuilder.kt

@@ -5,7 +5,61 @@ import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState
 import org.vorpal.research.kfg.ir.Class
 import org.vorpal.research.kfg.ir.value.instruction.Instruction
 
-interface ExceptionPreconditionBuilder {
+interface ExceptionPreconditionBuilder<T> {
     val targetException: Class
+
+    /**
+     * @return `true` if the precondition is successfully added
+     */
+    fun addPrecondition(precondition: T): Boolean
     fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState>
 }
+
+interface ExceptionPreconditionProvider<T> {
+    val targetException: Class
+    val hasNewPreconditions: Boolean
+    fun getNewPreconditions(): Map<Pair<Instruction, TraverserState>, Set<PersistentSymbolicState>>
+    fun getPreconditions(location: Instruction, state: TraverserState): Set<PersistentSymbolicState>
+}
+
+interface ExceptionPreconditionReceiver<T> {
+    fun addPrecondition(precondition: T)
+}
+
+class ExceptionPreconditionChannel<T>(
+    val name: String,
+    val builder: ExceptionPreconditionBuilder<T>
+) : ExceptionPreconditionProvider<T>, ExceptionPreconditionReceiver<T> {
+    private val mappings = mutableMapOf<Pair<Instruction, TraverserState>, MutableSet<PersistentSymbolicState>>()
+
+    override val targetException: Class
+        get() = builder.targetException
+
+    override var hasNewPreconditions = false
+        private set
+
+    private val lock = Any()
+
+    override fun addPrecondition(precondition: T): Unit = synchronized(lock) {
+        hasNewPreconditions = hasNewPreconditions || builder.addPrecondition(precondition)
+    }
+
+    override fun getNewPreconditions(): Map<Pair<Instruction, TraverserState>, Set<PersistentSymbolicState>> =
+        synchronized(lock) {
+            when {
+                hasNewPreconditions -> mappings
+                    .mapValues { (key, _) -> getPreconditions(key.first, key.second) }
+                    .filterValues { it.isNotEmpty() }
+                    .also { hasNewPreconditions = false }
+                else -> emptyMap()
+            }
+        }
+
+    override fun getPreconditions(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> =
+        synchronized(lock) {
+            val preconditions = builder.build(location, state)
+            val uncheckedPreconditions = preconditions - mappings.getOrPut(location to state, ::mutableSetOf)
+            mappings[location to state]!!.addAll(preconditions)
+            return uncheckedPreconditions
+        }
+}

kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/crash/precondition/ExceptionPreconditionManager.kt

@@ -25,12 +25,12 @@ import org.vorpal.research.kfg.stringClass
 import org.vorpal.research.kfg.stringIndexOOB
 
 
-class ExceptionPreconditionManager(
+class ExceptionPreconditionManager<T>(
     val ctx: ExecutionContext
 ) : TermBuilder {
     private val cm get() = ctx.cm
     private val tf get() = ctx.types
-    private val conditions = mutableMapOf<Method, MutableMap<Class, ExceptionPreconditionBuilder>>()
+    private val conditions = mutableMapOf<Method, MutableMap<Class, ExceptionPreconditionBuilder<T>>>()
 
 
     init {
@@ -39,10 +39,12 @@ class ExceptionPreconditionManager(
         val stringClass = cm.stringClass
 
         conditions.getOrPut(charSequenceClass.getMethod("charAt", tf.charType, tf.intType)) {
-            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder>()
-            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder {
+            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder<T>>()
+            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder<T> {
                 override val targetException get() = cm.stringIndexOOB
 
+                override fun addPrecondition(precondition: T): Boolean = false
+
                 override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
                     location as CallInst
                     val lengthMethod = charSequenceClass.getMethod("length", tf.intType)
@@ -74,10 +76,12 @@ class ExceptionPreconditionManager(
         }
 
         conditions.getOrPut(stringClass.getMethod("charAt", tf.charType, tf.intType)) {
-            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder>()
-            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder {
+            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder<T>>()
+            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder<T> {
                 override val targetException get() = cm.stringIndexOOB
 
+                override fun addPrecondition(precondition: T): Boolean = false
+
                 override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
                     location as CallInst
                     val lengthMethod = charSequenceClass.getMethod("length", tf.intType)
@@ -109,10 +113,12 @@ class ExceptionPreconditionManager(
         }
 
         conditions.getOrPut(stringClass.getMethod("substring", stringClass.asType, tf.intType)) {
-            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder>()
-            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder {
+            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder<T>>()
+            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder<T> {
                 override val targetException get() = cm.stringIndexOOB
 
+                override fun addPrecondition(precondition: T): Boolean = false
+
                 override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
                     location as CallInst
                     val lengthMethod = stringClass.getMethod("length", tf.intType)
@@ -144,10 +150,12 @@ class ExceptionPreconditionManager(
         }
 
         conditions.getOrPut(stringClass.getMethod("substring", stringClass.asType, tf.intType, tf.intType)) {
-            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder>()
-            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder {
+            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder<T>>()
+            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder<T> {
                 override val targetException get() = cm.stringIndexOOB
 
+                override fun addPrecondition(precondition: T): Boolean = false
+
                 override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
                     location as CallInst
                     val lengthMethod = stringClass.getMethod("length", tf.intType)
@@ -198,10 +206,12 @@ class ExceptionPreconditionManager(
         }
 
         conditions.getOrPut(integerClass.getMethod("decode", integerClass.asType, stringClass.asType)) {
-            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder>()
-            contracts[cm.numberFormatClass] = object : ExceptionPreconditionBuilder {
+            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder<T>>()
+            contracts[cm.numberFormatClass] = object : ExceptionPreconditionBuilder<T> {
                 override val targetException get() = cm.numberFormatClass
 
+                override fun addPrecondition(precondition: T): Boolean = false
+
                 override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
                     location as CallInst
 //                    val startsWithMethod = stringClass.getMethod("startsWith", tf.boolType, stringClass.asType)
@@ -246,10 +256,12 @@ class ExceptionPreconditionManager(
                 stringClass.asType
             )
         ) {
-            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder>()
-            contracts[cm.illegalArgumentClass] = object : ExceptionPreconditionBuilder {
+            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder<T>>()
+            contracts[cm.illegalArgumentClass] = object : ExceptionPreconditionBuilder<T> {
                 override val targetException get() = cm.illegalArgumentClass
 
+                override fun addPrecondition(precondition: T): Boolean = false
+
                 override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
                     location as CallInst
                     val lengthMethod = stringClass.getMethod("length", tf.intType)
@@ -285,10 +297,12 @@ class ExceptionPreconditionManager(
 
         val charClass = cm.charWrapper
         conditions.getOrPut(charClass.getMethod("codePointAt", tf.intType, charSequenceClass.asType, tf.intType)) {
-            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder>()
-            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder {
+            val contracts = mutableMapOf<Class, ExceptionPreconditionBuilder<T>>()
+            contracts[cm.stringIndexOOB] = object : ExceptionPreconditionBuilder<T> {
                 override val targetException get() = cm.stringIndexOOB
 
+                override fun addPrecondition(precondition: T): Boolean = false
+
                 override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
                     location as CallInst
                     val lengthMethod = charSequenceClass.getMethod("length", tf.intType)
@@ -321,7 +335,7 @@ class ExceptionPreconditionManager(
         }
     }
 
-    fun resolve(callInst: CallInst, exception: Class): ExceptionPreconditionBuilder? =
+    fun resolve(callInst: CallInst, exception: Class): ExceptionPreconditionBuilder<T>? =
         conditions.getOrDefault(callInst.method, emptyMap())[exception]
 }
 

kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/crash/precondition/builders.kt

@@ -39,12 +39,15 @@ import org.vorpal.research.kfg.nullptrClass
 import org.vorpal.research.kthelper.assert.unreachable
 import org.vorpal.research.kthelper.logging.log
 
-class ExceptionPreconditionBuilderImpl(
+class ExceptionPreconditionBuilderImpl<T>(
     val ctx: ExecutionContext,
     override val targetException: Class,
-) : ExceptionPreconditionBuilder {
+) : ExceptionPreconditionBuilder<T> {
     val cm get() = ctx.cm
-    private val preconditionManager = ExceptionPreconditionManager(ctx)
+    private val preconditionManager = ExceptionPreconditionManager<T>(ctx)
+
+    override fun addPrecondition(precondition: T) = false
+
     override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> =
         when (targetException) {
             cm.nullptrClass -> persistentSymbolicState(
@@ -173,8 +176,14 @@ class ExceptionPreconditionBuilderImpl(
 class DescriptorExceptionPreconditionBuilder(
     val ctx: ExecutionContext,
     override val targetException: Class,
-    private val parameterSet: Set<Parameters<Descriptor>>,
-) : ExceptionPreconditionBuilder {
+    parameterSet: Set<Parameters<Descriptor>>,
+) : ExceptionPreconditionBuilder<Parameters<Descriptor>> {
+    private val parameterSet = parameterSet.toMutableSet()
+
+    override fun addPrecondition(precondition: Parameters<Descriptor>): Boolean {
+        return parameterSet.add(precondition)
+    }
+
     override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
         val callInst = (location as? CallInst)
             ?: unreachable { log.error("Descriptor precondition is not valid for non-call instructions") }
@@ -344,8 +353,14 @@ data class ConstraintExceptionPrecondition(
 class ConstraintExceptionPreconditionBuilder(
     val ctx: ExecutionContext,
     override val targetException: Class,
-    private val parameterSet: Set<ConstraintExceptionPrecondition>,
-) : ExceptionPreconditionBuilder {
+    parameterSet: Set<ConstraintExceptionPrecondition>,
+) : ExceptionPreconditionBuilder<ConstraintExceptionPrecondition> {
+    private val parameterSet = parameterSet.toMutableSet()
+
+    override fun addPrecondition(precondition: ConstraintExceptionPrecondition): Boolean {
+        return parameterSet.add(precondition)
+    }
+
     override fun build(location: Instruction, state: TraverserState): Set<PersistentSymbolicState> {
         val callInst = (location as? CallInst)
             ?: unreachable { log.error("Descriptor precondition is not valid for non-call instructions") }

kex-runner/src/main/kotlin/org/vorpal/research/kex/launcher/CrashReproductionLauncher.kt

@@ -98,6 +98,9 @@ class CrashReproductionLauncher(
         executePipeline(context.cm, Package.defaultPackage) {
             +ClassInstantiationDetector(context, context.accessLevel)
         }
-        CrashReproductionChecker.runWithDescriptorPreconditions(context, stackTrace)
+        val testCases = CrashReproductionChecker.runWithDescriptorPreconditions(context, stackTrace)
+        if (testCases.isNotEmpty()) {
+            log.info("Reproducing test cases:\n${testCases.joinToString("\n")}")
+        }
     }
 }

kex-runner/src/main/kotlin/org/vorpal/research/kex/reanimator/codegen/javagen/ReflectionUtilsPrinter.kt

@@ -10,7 +10,7 @@ class ReflectionUtilsPrinter(
     val packageName: String
 ) {
     private val builder = JavaBuilder(packageName)
-    val klass = builder.run { klass(packageName, "ReflectionUtils") }
+    val klass = builder.run { klass(packageName, REFLECTION_UTILS_CLASS) }
     val newInstance: JavaBuilder.JavaFunction
     val newArray: JavaBuilder.JavaFunction
     val newObjectArray: JavaBuilder.JavaFunction
@@ -25,6 +25,7 @@ class ReflectionUtilsPrinter(
     val callMethod: JavaBuilder.JavaFunction
 
     companion object {
+        const val REFLECTION_UTILS_CLASS = "ReflectionUtils"
         private val reflectionUtilsInstances = mutableMapOf<Pair<Path, String>, ReflectionUtilsPrinter>()
         fun reflectionUtils(packageName: String): ReflectionUtilsPrinter {
             val testDirectory = kexConfig.testcaseDirectory
@@ -41,6 +42,7 @@ class ReflectionUtilsPrinter(
             }
         }
 
+        @Suppress("unused")
         fun invalidateAll() {
             reflectionUtilsInstances.clear()
         }

kex-test.ini

@@ -68,8 +68,8 @@ numberOfExecutors = 1
 searchStrategy = cgs
 
 [crash]
-globalTimeLimit = 600
-localTimeLimit = 100
+timeLimit = 100
+numberOfExecutors = 3
 stopAfterFirstCrash = false
 
 [annotations]

kex.ini

@@ -80,8 +80,8 @@ numberOfExecutors = 8
 searchStrategy = cgs
 
 [crash]
-globalTimeLimit = 600
-localTimeLimit = 600
+timeLimit = 100
+numberOfExecutors = 8
 stopAfterFirstCrash = false
 
 [random-runner]
@@ -108,7 +108,7 @@ maxDerollCount = 1
 
 [smt]
 engine = ksmt
-timeout = 100
+timeout = 10
 defaultAllocationSize = 512
 
 psInlining = true