From d96f217e1fd9cc7645cc39375d70c39ee5283024 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Mon, 27 Nov 2023 15:52:37 +0100 Subject: [PATCH 1/9] rework of path selectors --- .../kex/trace/symbolic/SymbolicState.kt | 42 ++++++++++- .../trace/symbolic/SymbolicTraceBuilder.kt | 33 ++++---- .../research/kex/util/KfgClassLoader.kt | 11 +-- .../analysis/concolic/ConcolicPathSelector.kt | 6 ++ .../concolic/InstructionConcolicChecker.kt | 75 ++++++++++++------- .../analysis/concolic/bfs/BfsPathSelector.kt | 8 ++ .../concolic/cgs/ContextGuidedSelector.kt | 12 ++- .../research/kex/test/javadebug/JavaTest.java | 54 ++++++++----- 8 files changed, 165 insertions(+), 76 deletions(-) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt index 4cb1ce7a5..86e54eefb 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt @@ -293,11 +293,29 @@ abstract class SymbolicState { abstract operator fun plus(other: PathClause): SymbolicState abstract operator fun plus(other: ClauseList): SymbolicState abstract operator fun plus(other: PathCondition): SymbolicState + + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (javaClass != other?.javaClass) return false + + other as SymbolicState + + if (clauses != other.clauses) return false + if (path != other.path) return false + + return true + } + + override fun hashCode(): Int { + var result = clauses.hashCode() + result = 31 * result + path.hashCode() + return result + } } @Serializable @SerialName("SymbolicStateImpl") -internal data class SymbolicStateImpl( +internal class SymbolicStateImpl( override val clauses: ClauseList, override val path: PathCondition, override val concreteTypes: @Contextual Map, @@ -327,11 +345,21 @@ internal data class SymbolicStateImpl( override fun toString(): String { return "SymbolicStateImpl(clauses=$clauses, path=$path)" } + + fun copy( + clauses: ClauseList = this.clauses, + path: PathCondition = this.path, + concreteTypes: Map = this.concreteTypes, + concreteValues: Map = this.concreteValues, + termMap: Map = this.termMap, + ): SymbolicState = SymbolicStateImpl( + clauses, path, concreteTypes, concreteValues, termMap + ) } @Serializable @SerialName("PersistentSymbolicState") -data class PersistentSymbolicState( +class PersistentSymbolicState( override val clauses: PersistentClauseList, override val path: PersistentPathCondition, override val concreteTypes: @Contextual PersistentMap, @@ -359,6 +387,16 @@ data class PersistentSymbolicState( override fun plus(other: PathCondition): PersistentSymbolicState = copy( path = path + other, ) + + fun copy( + clauses: PersistentClauseList = this.clauses, + path: PersistentPathCondition = this.path, + concreteTypes: PersistentMap = this.concreteTypes, + concreteValues: PersistentMap = this.concreteValues, + termMap: PersistentMap = this.termMap, + ): PersistentSymbolicState = PersistentSymbolicState( + clauses, path, concreteTypes, concreteValues, termMap + ) } diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt index 4f89afd34..18a30504e 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicTraceBuilder.kt @@ -447,6 +447,7 @@ class SymbolicTraceBuilder( for ((value, term) in method.parameterValues.asList.zip(call.params.asList)) { valueMap[value] = term } + stateBuilder += StateClause(call.call, state { true equality true }) lastCall = null } else { if (!traceCollectingEnabled) return@safeCall @@ -713,9 +714,10 @@ class SymbolicTraceBuilder( predicate ) - /** - * we do not use 'postProcess' here, because actual call predicate may not end up in the final state - */ +// postProcess(instruction, state { true equality true }) +// /** +// * we do not use 'postProcess' here, because actual call predicate may not end up in the final state +// */ traceBuilder += instruction updateCatches(instruction) } @@ -1013,8 +1015,10 @@ class SymbolicTraceBuilder( * we do not use 'postProcess' here because jump instruction is not converted into any predicate */ previousBlock = instruction.parent - traceBuilder += instruction - updateCatches(instruction) + + postProcess(instruction, state { true equality true }) +// traceBuilder += instruction +// updateCatches(instruction) } override fun newArray( @@ -1123,14 +1127,10 @@ class SymbolicTraceBuilder( terms[termReceiver] = kfgReceiver.wrapped() concreteTypeMap[termReceiver] = concreteValue.getConcreteType(termReceiver.type) - stateBuilder += StateClause(instruction, predicate) + postProcess(instruction, predicate) + } else { + postProcess(instruction, state { true equality true }) } - - /** - * we do not use 'postProcess' here because return inst is not always converted into predicate - */ - traceBuilder += instruction - updateCatches(instruction) } private fun numericValue(value: Any?): Number = when (value) { @@ -1295,8 +1295,8 @@ class SymbolicTraceBuilder( val kfgValue = parseValue(value) val termValue = mkValue(kfgValue) - val descriptorValue = concreteValue.getAsDescriptor() - val kfgType = descriptorValue.type.getKfgType(ctx.types) + val concreteType = concreteValue.getConcreteType(termValue.type) + val kfgType = concreteType.getKfgType(ctx.types) if (termValue in typeChecked) { val checkedType = typeChecked.getValue(termValue) if (checkedType.isSubtypeOfCached(kfgType)) return@safeCall @@ -1304,7 +1304,7 @@ class SymbolicTraceBuilder( typeChecked[termValue] = kfgType val predicate = path { - (termValue `is` descriptorValue.type) equality true + (termValue `is` concreteType) equality true } processPath(PathClauseType.OVERLOAD_CHECK, instruction, predicate) @@ -1323,8 +1323,7 @@ class SymbolicTraceBuilder( val comparisonResult = when (concreteValue) { null -> false else -> { - val descriptorValue = concreteValue.getAsDescriptor() - val actualKfgType = descriptorValue.type.getKfgType(ctx.types) + val actualKfgType = concreteValue.getConcreteType(termValue.type).getKfgType(ctx.types) actualKfgType.isSubtypeOfCached(expectedKfgType) } } diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/util/KfgClassLoader.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/util/KfgClassLoader.kt index 8a8080d54..e61ddc45e 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/util/KfgClassLoader.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/util/KfgClassLoader.kt @@ -22,16 +22,7 @@ class KfgClassLoader( companion object { private val INCLUDES = setOf( - "class org.vorpal.research.kex.test.concolic.kaf.Lesson2", - "class org.vorpal.research.kex.test.concolic.kaf.Lesson6", - "class org.vorpal.research.kex.test.concolic.EnumConcolicTests", - "class org.vorpal.research.kex.test.concolic.ListConcolicTests", - "class org.vorpal.research.kex.test.concolic.Point", - "class org.vorpal.research.kex.test.concolic.PrimitiveConcolicTests", - "class org.vorpal.research.kex.test.concolic.SetConcolicTests", - "class org.vorpal.research.kex.test.concolic.StringConcolicTests", - "class org.vorpal.research.kex.test.concolic.TestEnum", - "class org.vorpal.research.kex.test.debug.ObjectGenerationTests", + "package org.vorpal.research.kex.test.*" ).mapTo(mutableSetOf()) { KfgTargetFilter.parse(it) } private val EXCLUDES = setOf( "package java.*", diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt index 1fe041c9a..88e4b01af 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt @@ -7,6 +7,12 @@ import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult import org.vorpal.research.kfg.ir.Method +interface ConcolicPathSelectorManager { + val ctx: ExecutionContext + val targets: Set + fun createPathSelectorFor(target: Method): ConcolicPathSelector +} + interface ConcolicPathSelector : SuspendableIterator { val ctx: ExecutionContext diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt index d3d45a190..84cd3b9a9 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt @@ -10,9 +10,9 @@ import kotlinx.coroutines.yield import kotlinx.serialization.ExperimentalSerializationApi import kotlinx.serialization.InternalSerializationApi import org.vorpal.research.kex.ExecutionContext -import org.vorpal.research.kex.asm.analysis.concolic.bfs.BfsPathSelectorImpl -import org.vorpal.research.kex.asm.analysis.concolic.cgs.ContextGuidedSelector -import org.vorpal.research.kex.asm.analysis.concolic.gui.GUIProxySelector +import org.vorpal.research.kex.asm.analysis.concolic.bfs.BfsPathSelectorManager +import org.vorpal.research.kex.asm.analysis.concolic.cgs.ContextGuidedSelectorManager +import org.vorpal.research.kex.asm.analysis.concolic.coverage.CoverageGuidedSelectorManager import org.vorpal.research.kex.asm.analysis.util.analyzeOrTimeout import org.vorpal.research.kex.asm.analysis.util.checkAsync import org.vorpal.research.kex.compile.CompilerHelper @@ -41,34 +41,66 @@ import java.util.concurrent.atomic.AtomicInteger import kotlin.time.Duration.Companion.seconds import kotlin.time.ExperimentalTime +interface TestNameGenerator { + fun generateName(method: Method, parameters: Parameters): String +} + +class TestNameGeneratorImpl : TestNameGenerator { + private var testIndex = AtomicInteger(0) + + override fun generateName(method: Method, parameters: Parameters): String = + method.klassName + testIndex.getAndIncrement() + +} + @ExperimentalSerializationApi @InternalSerializationApi class InstructionConcolicChecker( val ctx: ExecutionContext, + val pathSelector: ConcolicPathSelector, + val testNameGenerator: TestNameGenerator, ) { val cm: ClassManager get() = ctx.cm private val compilerHelper = CompilerHelper(ctx) - private val searchStrategy = kexConfig.getStringValue("concolic", "searchStrategy", "bfs") - private val guiEnabled = kexConfig.getBooleanValue("gui", "enabled", false) + companion object { - private var testIndex = AtomicInteger(0) + private fun buildSelectorManager( + ctx: ExecutionContext, + targets: Set, + strategyName: String, + ): ConcolicPathSelectorManager = when (strategyName) { + "bfs" -> BfsPathSelectorManager(ctx, targets) + "cgs" -> ContextGuidedSelectorManager(ctx, targets) + "coverage" -> CoverageGuidedSelectorManager(ctx, targets) + else -> unreachable { log.error("Unknown type of search strategy $strategyName") } + } - companion object { @ExperimentalTime @DelicateCoroutinesApi fun run(context: ExecutionContext, targets: Set) { val executors = kexConfig.getIntValue("concolic", "numberOfExecutors", 8) val timeLimit = kexConfig.getIntValue("concolic", "timeLimit", 100) + val searchStrategy = kexConfig.getStringValue("concolic", "searchStrategy", "bfs") val actualNumberOfExecutors = maxOf(1, minOf(executors, targets.size)) val coroutineContext = newFixedThreadPoolContextWithMDC(actualNumberOfExecutors, "concolic-dispatcher") + + val selectorManager = buildSelectorManager(context, targets, searchStrategy) + val testNameGenerator = TestNameGeneratorImpl() + runBlocking(coroutineContext) { withTimeoutOrNull(timeLimit.seconds) { targets.map { - async { InstructionConcolicChecker(context).visit(it) } + async { + InstructionConcolicChecker( + context, + selectorManager.createPathSelectorFor(it), + testNameGenerator + ).visit(it) + } }.awaitAll() } } @@ -101,7 +133,7 @@ class InstructionConcolicChecker( collectTrace(method, parameters.asDescriptors) private suspend fun collectTrace(method: Method, parameters: Parameters): ExecutionResult? = tryOrNull { - val generator = UnsafeGenerator(ctx, method, method.klassName + testIndex.getAndIncrement()) + val generator = UnsafeGenerator(ctx, method, testNameGenerator.generateName(method, parameters)) generator.generate(parameters) val testFile = generator.emit() @@ -123,16 +155,6 @@ class InstructionConcolicChecker( null } - private fun buildPathSelector(): ConcolicPathSelector { - val pathSelector = when (searchStrategy) { - "bfs" -> BfsPathSelectorImpl(ctx) - "cgs" -> ContextGuidedSelector(ctx) - else -> unreachable { log.error("Unknown type of search strategy $searchStrategy") } - } - - return if (guiEnabled) GUIProxySelector(pathSelector) else pathSelector - } - private suspend fun handleStartingTrace( method: Method, pathIterator: ConcolicPathSelector, @@ -147,17 +169,14 @@ class InstructionConcolicChecker( } private suspend fun processMethod(method: Method) { - testIndex = AtomicInteger(0) - val pathIterator = buildPathSelector() - - handleStartingTrace(method, pathIterator, getRandomTrace(method)) - if (pathIterator.isEmpty()) { - handleStartingTrace(method, pathIterator, getDefaultTrace(method)) + handleStartingTrace(method, pathSelector, getRandomTrace(method)) + if (pathSelector.isEmpty()) { + handleStartingTrace(method, pathSelector, getDefaultTrace(method)) } yield() - while (pathIterator.hasNext()) { - val state = pathIterator.next() + while (pathSelector.hasNext()) { + val state = pathSelector.next() log.debug { "Checking state: $state" } log.debug { "Path:\n${state.path.asState()}" } yield() @@ -166,7 +185,7 @@ class InstructionConcolicChecker( when (newState) { is ExecutionCompletedResult -> when { newState.trace.isEmpty() -> log.warn { "Collected empty state from $state" } - else -> pathIterator.addExecutionTrace(method, newState) + else -> pathSelector.addExecutionTrace(method, newState) } else -> log.warn("Failure during execution: $newState") diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt index b58be5a80..b23194316 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt @@ -2,6 +2,7 @@ package org.vorpal.research.kex.asm.analysis.concolic.bfs import org.vorpal.research.kex.ExecutionContext import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelector +import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelectorManager import org.vorpal.research.kex.state.predicate.DefaultSwitchPredicate import org.vorpal.research.kex.state.predicate.EqualityPredicate import org.vorpal.research.kex.state.predicate.InequalityPredicate @@ -25,6 +26,13 @@ import org.vorpal.research.kthelper.assert.unreachable import org.vorpal.research.kthelper.collection.dequeOf import org.vorpal.research.kthelper.logging.log +class BfsPathSelectorManager( + override val ctx: ExecutionContext, + override val targets: Set +) : ConcolicPathSelectorManager { + override fun createPathSelectorFor(target: Method): ConcolicPathSelector = + BfsPathSelectorImpl(ctx) +} class BfsPathSelectorImpl( override val ctx: ExecutionContext, diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt index c3f134b7b..9c799f59b 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt @@ -3,6 +3,7 @@ package org.vorpal.research.kex.asm.analysis.concolic.cgs import kotlinx.coroutines.yield import org.vorpal.research.kex.ExecutionContext import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelector +import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelectorManager import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException import org.vorpal.research.kex.asm.manager.instantiationManager import org.vorpal.research.kex.ktype.kexType @@ -37,8 +38,17 @@ import org.vorpal.research.kthelper.collection.dequeOf import org.vorpal.research.kthelper.logging.log import org.vorpal.research.kthelper.`try` -class ContextGuidedSelector( + +class ContextGuidedSelectorManager( override val ctx: ExecutionContext, + override val targets: Set +) : ConcolicPathSelectorManager { + override fun createPathSelectorFor(target: Method): ConcolicPathSelector = + ContextGuidedSelector(ctx) +} + +class ContextGuidedSelector( + override val ctx: ExecutionContext ) : ConcolicPathSelector { private val executionTree = ExecutionTree(ctx) private var currentDepth = 0 diff --git a/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java b/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java index 8c0259474..ed6177f46 100644 --- a/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java +++ b/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java @@ -1,27 +1,31 @@ package org.vorpal.research.kex.test.javadebug; +import org.vorpal.research.kex.test.concolic.Point; + import java.util.ArrayList; @SuppressWarnings("ALL") public class JavaTest { -// public int foo(Point a, Point b) { -// int ax = a.getX(); -// int bx = b.getX(); -// int mx = Math.max(ax, bx); -// -// int ay = a.getY(); -// int by = b.getY(); -// int my = Math.min(ay, by); -// int res; -// if (mx < my) { -// System.out.println("success"); -// res = mx - my; -// } else { -// System.out.println("fail"); -// res = my - mx; -// } -// return res; -// } + public int foo(Point a, Point b) { + int ax = a.getX(); + int bx = b.getX(); + int mx = Math.max(ax, bx); + + int ay = a.getY(); + int by = b.getY(); + int my = Math.min(ay, by); + int res; + if (mx < my) { + System.out.println("success"); + res = mx - my; + } else if (mx > my) { + System.out.println("fail"); + res = my - mx; + } else { + throw new IllegalArgumentException(); + } + return res; + } public int testWrapper(ArrayList b) { if (b.get(0) < 0) { @@ -29,5 +33,19 @@ public int testWrapper(ArrayList b) { } return b.size(); } + + public boolean testFoo(boolean b) { + if (b) { + foo(new Point(100, 100), new Point(0, 0)); + return false; + } else { + try { + foo(new Point(0, 0), new Point(0, 0)); + } catch (IllegalArgumentException e) { + System.err.println("asdsad"); + } + return true; + } + } } From f3dd60d72b9819bb08c9886a836f4bce8ddc62a0 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Wed, 29 Nov 2023 09:51:03 +0100 Subject: [PATCH 2/9] first experiments --- .../asm/manager/ClassInstantiationManager.kt | 12 + .../kex/trace/symbolic/SymbolicState.kt | 4 + .../analysis/concolic/ConcolicPathSelector.kt | 2 +- .../concolic/InstructionConcolicChecker.kt | 11 +- .../analysis/concolic/bfs/BfsPathSelector.kt | 5 +- .../concolic/cgs/ContextGuidedSelector.kt | 14 +- .../coverage/CoverageGuidedSelector.kt | 56 ++++ .../concolic/coverage/ExecutionGraph.kt | 295 ++++++++++++++++++ .../analysis/concolic/gui/GUIProxySelector.kt | 5 +- .../research/kex/test/javadebug/JavaTest.java | 14 +- kex.ini | 2 +- 11 files changed, 401 insertions(+), 19 deletions(-) create mode 100644 kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt create mode 100644 kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt index 8023c03b9..ec27a729e 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/manager/ClassInstantiationManager.kt @@ -39,6 +39,18 @@ interface ClassInstantiationManager { else -> type } + fun getAll(type: Type, accessLevel: AccessModifier, excludes: Set): Set = + when (type) { + is ClassType -> getAllConcreteSubtypes(type.klass, accessLevel) + .filter { it !in excludes } + .mapTo(mutableSetOf()) { it.asType } + + is ArrayType -> getAll(type.component, accessLevel, excludes) + .mapTo(mutableSetOf()) { it.asArray } + + else -> setOf(type) + } + fun getAllConcreteSubtypes(klass: Class, accessLevel: AccessModifier): Set fun getConcreteClass(klass: KexClass, cm: ClassManager, accessLevel: AccessModifier, random: Random): KexClass = diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt index 86e54eefb..3c9e917ae 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt @@ -179,6 +179,8 @@ data class PersistentClauseList( override fun plus(other: ClauseList): PersistentClauseList = PersistentClauseList(state.addAll(other.state)) override fun plus(other: Clause): PersistentClauseList = PersistentClauseList(state.add(other)) + + fun dropLast(n: Int): PersistentClauseList = subState(0, maxOf(0, size - n)) } @Serializable @@ -268,6 +270,8 @@ data class PersistentPathCondition( override fun plus(other: PathCondition): PersistentPathCondition = PersistentPathCondition(path.addAll(other.path)) override fun plus(other: PathClause): PersistentPathCondition = PersistentPathCondition(path.add(other)) + + fun dropLast(n: Int): PersistentPathCondition = subPath(0, maxOf(0, size - n)) } @Serializable diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt index 88e4b01af..ef0943edf 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt @@ -13,7 +13,7 @@ interface ConcolicPathSelectorManager { fun createPathSelectorFor(target: Method): ConcolicPathSelector } -interface ConcolicPathSelector : SuspendableIterator { +interface ConcolicPathSelector : SuspendableIterator> { val ctx: ExecutionContext suspend fun isEmpty(): Boolean diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt index 84cd3b9a9..a2e56d49f 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt @@ -30,6 +30,7 @@ import org.vorpal.research.kex.trace.symbolic.SymbolicState import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionResult import org.vorpal.research.kex.util.newFixedThreadPoolContextWithMDC +import org.vorpal.research.kex.util.view import org.vorpal.research.kfg.ClassManager import org.vorpal.research.kfg.ir.Method import org.vorpal.research.kthelper.assert.unreachable @@ -104,6 +105,14 @@ class InstructionConcolicChecker( }.awaitAll() } } + + val graph = when (selectorManager) { + is ContextGuidedSelectorManager -> selectorManager.graph + is CoverageGuidedSelectorManager -> selectorManager.executionGraph + else -> TODO() + } + graph.view() + val a = 10 } } @@ -176,7 +185,7 @@ class InstructionConcolicChecker( yield() while (pathSelector.hasNext()) { - val state = pathSelector.next() + val (method, state) = pathSelector.next() log.debug { "Checking state: $state" } log.debug { "Path:\n${state.path.asState()}" } yield() diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt index b23194316..d60eab08a 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt @@ -31,11 +31,12 @@ class BfsPathSelectorManager( override val targets: Set ) : ConcolicPathSelectorManager { override fun createPathSelectorFor(target: Method): ConcolicPathSelector = - BfsPathSelectorImpl(ctx) + BfsPathSelectorImpl(ctx, target) } class BfsPathSelectorImpl( override val ctx: ExecutionContext, + val method: Method ) : ConcolicPathSelector { private val coveredPaths = mutableSetOf() private val candidates = mutableSetOf() @@ -51,7 +52,7 @@ class BfsPathSelectorImpl( addCandidates(persistentResult) } - override suspend fun next(): PersistentSymbolicState = deque.pollFirst() + override suspend fun next(): Pair = method to deque.pollFirst() override fun reverse(pathClause: PathClause): PathClause? = pathClause.reversed() diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt index 9c799f59b..c4a8be412 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt @@ -4,6 +4,7 @@ import kotlinx.coroutines.yield import org.vorpal.research.kex.ExecutionContext import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelector import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelectorManager +import org.vorpal.research.kex.asm.analysis.concolic.coverage.ExecutionGraph import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException import org.vorpal.research.kex.asm.manager.instantiationManager import org.vorpal.research.kex.ktype.kexType @@ -43,12 +44,16 @@ class ContextGuidedSelectorManager( override val ctx: ExecutionContext, override val targets: Set ) : ConcolicPathSelectorManager { + val graph = ExecutionGraph(ctx) + override fun createPathSelectorFor(target: Method): ConcolicPathSelector = - ContextGuidedSelector(ctx) + ContextGuidedSelector(ctx, target, graph) } class ContextGuidedSelector( - override val ctx: ExecutionContext + override val ctx: ExecutionContext, + val method: Method, + val graph: ExecutionGraph ) : ConcolicPathSelector { private val executionTree = ExecutionTree(ctx) private var currentDepth = 0 @@ -87,7 +92,7 @@ class ContextGuidedSelector( false }.getOrElse { false } - override suspend fun next(): PersistentSymbolicState { + override suspend fun next(): Pair { val currentState = states.pollFirst()!! visitedContexts += currentState.context @@ -95,7 +100,7 @@ class ContextGuidedSelector( val stateSize = currentStateState.clauses.indexOf(currentState.activeClause) val state = currentStateState.clauses.subState(0, stateSize) - return persistentSymbolicState( + return method to persistentSymbolicState( state, currentState.path + currentState.revertedClause, currentStateState.concreteTypes, @@ -127,6 +132,7 @@ class ContextGuidedSelector( override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { executionTree.addTrace(result.symbolicState.toPersistentState()) + graph.addTrace(method, result) } override fun reverse(pathClause: PathClause): PathClause? = pathClause.reversed() diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt new file mode 100644 index 000000000..75d3d48d5 --- /dev/null +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt @@ -0,0 +1,56 @@ +package org.vorpal.research.kex.asm.analysis.concolic.coverage + +import org.vorpal.research.kex.ExecutionContext +import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelector +import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelectorManager +import org.vorpal.research.kex.trace.symbolic.PathClause +import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState +import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult +import org.vorpal.research.kfg.ir.Method +import org.vorpal.research.kfg.ir.value.instruction.Instruction + +class CoverageGuidedSelectorManager( + override val ctx: ExecutionContext, + override val targets: Set +) : ConcolicPathSelectorManager { + val executionGraph = ExecutionGraph(ctx) + + override fun createPathSelectorFor(target: Method): ConcolicPathSelector = + CoverageGuidedSelector(this) + + private val targetInstructions = targets.flatMapTo(mutableSetOf()) { it.body.flatten() } + private val coveredInstructions = mutableSetOf() + + fun addCoverage(trace: List) { + coveredInstructions += trace + } + + fun isCovered(): Boolean = coveredInstructions.containsAll(targetInstructions) +} + +class CoverageGuidedSelector( + private val manager: CoverageGuidedSelectorManager +) : ConcolicPathSelector { + override val ctx: ExecutionContext + get() = manager.ctx + private val executionGraph get() = manager.executionGraph + + override suspend fun isEmpty(): Boolean = manager.isCovered() || executionGraph.candidates.isEmpty() + + override suspend fun hasNext(): Boolean = !isEmpty() + + override suspend fun next(): Pair { + val candidate = executionGraph.candidates.keys.randomOrNull(ctx.random)!! + val method = executionGraph.candidates[candidate]!! + executionGraph.candidates.remove(candidate) + return method to candidate + } + + override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { + manager.addCoverage(result.trace) + executionGraph.addTrace(method, result) + } + + override fun reverse(pathClause: PathClause): PathClause = TODO() //pathClause.reversed() + +} diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt new file mode 100644 index 000000000..b6645aac2 --- /dev/null +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt @@ -0,0 +1,295 @@ +package org.vorpal.research.kex.asm.analysis.concolic.coverage + +import com.jetbrains.rd.util.concurrentMapOf +import org.vorpal.research.kex.ExecutionContext +import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException +import org.vorpal.research.kex.asm.manager.instantiationManager +import org.vorpal.research.kex.ktype.kexType +import org.vorpal.research.kex.state.predicate.DefaultSwitchPredicate +import org.vorpal.research.kex.state.predicate.EqualityPredicate +import org.vorpal.research.kex.state.predicate.InequalityPredicate +import org.vorpal.research.kex.state.predicate.Predicate +import org.vorpal.research.kex.state.predicate.path +import org.vorpal.research.kex.state.predicate.predicate +import org.vorpal.research.kex.state.term.ConstBoolTerm +import org.vorpal.research.kex.state.term.InstanceOfTerm +import org.vorpal.research.kex.state.term.numericValue +import org.vorpal.research.kex.state.transformer.TermCollector +import org.vorpal.research.kex.trace.symbolic.PathClause +import org.vorpal.research.kex.trace.symbolic.PathClauseType +import org.vorpal.research.kex.trace.symbolic.PersistentPathCondition +import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState +import org.vorpal.research.kex.trace.symbolic.persistentSymbolicState +import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult +import org.vorpal.research.kex.trace.symbolic.toPersistentState +import org.vorpal.research.kfg.ir.BasicBlock +import org.vorpal.research.kfg.ir.Method +import org.vorpal.research.kfg.ir.value.EmptyUsageContext +import org.vorpal.research.kfg.ir.value.IntConstant +import org.vorpal.research.kfg.ir.value.Value +import org.vorpal.research.kfg.ir.value.instruction.BranchInst +import org.vorpal.research.kfg.ir.value.instruction.Instruction +import org.vorpal.research.kfg.ir.value.instruction.SwitchInst +import org.vorpal.research.kfg.ir.value.instruction.TableSwitchInst +import org.vorpal.research.kfg.type.ClassType +import org.vorpal.research.kthelper.assert.unreachable +import org.vorpal.research.kthelper.graph.GraphView +import org.vorpal.research.kthelper.graph.PredecessorGraph +import org.vorpal.research.kthelper.graph.Viewable +import org.vorpal.research.kthelper.logging.log +import java.util.* + +private fun Predicate.reverseBoolCond() = when (this) { + is EqualityPredicate -> predicate(this.type, this.location) { + lhv equality !(rhv as ConstBoolTerm).value + } + + is InequalityPredicate -> predicate(this.type, this.location) { + lhv inequality !(rhv as ConstBoolTerm).value + } + + else -> unreachable { log.error("Unexpected predicate in bool cond: $this") } +} + +private fun Predicate.reverseSwitchCond( + predecessors: Set, + branches: Map +): List = when (this) { + is DefaultSwitchPredicate -> branches.keys + .mapTo(mutableSetOf()) { (it as IntConstant).value } + .map { + predicate(this.type, this.location) { + cond equality it + } + } + + + is EqualityPredicate -> { + val outgoingPaths = branches.toList() + .groupBy({ it.second }, { it.first }) + .map { it.value.mapTo(mutableSetOf()) { const -> (const as IntConstant).value } } + + val equivalencePaths = mutableMapOf>() + for (set in outgoingPaths) { + for (value in set) { + equivalencePaths[value] = set + } + } + + val visitedCandidates = predecessors + .map { it.path.last().predicate } + .filterIsInstance() + .mapTo(mutableSetOf()) { it.rhv.numericValue } + + val candidates = run { + val currentRange = branches.keys.map { (it as IntConstant).value }.toMutableSet() + for (candidate in visitedCandidates) { + currentRange.removeAll(equivalencePaths[candidate]!!) + } + currentRange + } + + candidates.map { + predicate(type, location) { + lhv equality it + } + } + } + + else -> unreachable { log.error("Unexpected predicate in switch clause: $this") } +} + + +sealed class Vertex( + val type: String, + val instruction: Instruction +) : PredecessorGraph.PredecessorVertex { + companion object { + const val STATE = "STATE" + } + + private val _predecessors = mutableSetOf() + private val _successors = mutableSetOf() + + override val predecessors: Set + get() = _predecessors + override val successors: Set + get() = _successors + + fun linkDown(other: Vertex) { + _successors += other + other._predecessors += this + } + + fun linkUp(other: Vertex) { + _predecessors += other + other._successors += this + } + + override fun toString(): String { + return "Vertex($type, ${instruction.print()})" + } +} + +class StateVertex( + instruction: Instruction +) : Vertex(STATE, instruction) + +class PathVertex( + val pathType: PathClauseType, + instruction: Instruction +) : Vertex(pathType.name, instruction) { + val states = concurrentMapOf>() + private val visitedPrefixes = Collections.newSetFromMap(concurrentMapOf()) + + fun addStateAndProduceCandidates( + ctx: ExecutionContext, + state: PersistentSymbolicState + ): List { + val prefix = state.path.dropLast(1) + val condition = state.path.last() + val prefixStates = states.getOrPut(prefix, ::mutableSetOf).also { + it += state + } + return when (prefix) { + in visitedPrefixes -> emptyList() + else -> { + visitedPrefixes += prefix + val reversedConditions = when (condition.type) { + PathClauseType.NULL_CHECK -> listOf(condition.copy(predicate = condition.predicate.reverseBoolCond())) + PathClauseType.TYPE_CHECK -> listOf(condition.copy(predicate = condition.predicate.reverseBoolCond())) + PathClauseType.BOUNDS_CHECK -> listOf(condition.copy(predicate = condition.predicate.reverseBoolCond())) + PathClauseType.CONDITION_CHECK -> when (val inst = condition.instruction) { + is BranchInst -> listOf(condition.copy(predicate = condition.predicate.reverseBoolCond())) + is SwitchInst -> condition.predicate.reverseSwitchCond(prefixStates, inst.branches).map { + condition.copy(predicate = it) + } + + is TableSwitchInst -> { + val branches = inst.range.let { range -> + range.associateWith { inst.branches[it - range.first] } + .mapKeys { ctx.values.getInt(it.key) } + } + condition.predicate.reverseSwitchCond(prefixStates, branches).map { + condition.copy(predicate = it) + } + } + + else -> unreachable { log.error("Unexpected predicate in clause $inst") } + } + + PathClauseType.OVERLOAD_CHECK -> { + val excludeClasses = prefixStates + .map { it.path.last().predicate } + .flatMap { TermCollector.getFullTermSet(it).filterIsInstance() } + .map { it.checkedType.getKfgType(ctx.types) } + .filterIsInstance() + .mapTo(mutableSetOf()) { it.klass } + + try { + val lhv = condition.predicate.operands[0] as InstanceOfTerm + val termType = lhv.operand.type.getKfgType(ctx.types) + instantiationManager.getAll(termType, ctx.accessLevel, excludeClasses).map { + condition.copy(predicate = path(instruction.location) { + (lhv.operand `is` it.kexType) equality true + }) + } + } catch (e: NoConcreteInstanceException) { + emptyList() + } + } + } + reversedConditions.map { + persistentSymbolicState( + state.clauses.dropLast(1), + prefix + it, + state.concreteTypes, + state.concreteValues, + state.termMap + ) + } + } + } + } +} + + +class ExecutionGraph(val ctx: ExecutionContext) : PredecessorGraph, Viewable { + private val root: Vertex = StateVertex(ctx.cm.instruction.getUnreachable(EmptyUsageContext)) + private val innerNodes = concurrentMapOf, Vertex>().also { + it["STATE" to root.instruction] = root + } + + val candidates = concurrentMapOf() + + override val entry: Vertex + get() = root + + override val nodes: Set + get() = innerNodes.values.toSet() + + fun addTrace(method: Method, executionResult: ExecutionCompletedResult) = synchronized(this) { + var prevVertex = root + var clauseIndex = 0 + var pathIndex = 0 + val symbolicState = executionResult.symbolicState.toPersistentState() + var totalNewCandidates = 0 + for (clause in symbolicState.clauses) { + ++clauseIndex + if (clause is PathClause) ++pathIndex + + val type = when (clause) { + is PathClause -> clause.type.toString() + else -> Vertex.STATE + } + val currentVertex = innerNodes.getOrPut(type to clause.instruction) { + when (clause) { + is PathClause -> PathVertex(clause.type, clause.instruction) + else -> StateVertex(clause.instruction) + } + } + + if (clause is PathClause) { + currentVertex as PathVertex + val newCands = currentVertex.addStateAndProduceCandidates( + ctx, persistentSymbolicState( + symbolicState.clauses.subState(0, clauseIndex), + symbolicState.path.subPath(0, pathIndex), + symbolicState.concreteTypes, + symbolicState.concreteValues, + symbolicState.termMap + ) + ) + totalNewCandidates += newCands.size + candidates += newCands.map { it to method } + } + + prevVertex.linkDown(currentVertex) + prevVertex = currentVertex + } + if (totalNewCandidates == 0) { + val a= 10 + } + } + + override val graphView: List + get() { + val graphNodes = mutableMapOf() + + var i = 0 + for (vertex in nodes) { + graphNodes[vertex] = GraphView("${i++}", "$vertex".replace("\"", "\\\"")) { + it.setColor(info.leadinglight.jdot.enums.Color.X11.black) + } + } + + for (vertex in nodes) { + val current = graphNodes.getValue(vertex) + for (child in vertex.successors) { + current.addSuccessor(graphNodes.getValue(child)) + } + } + + return graphNodes.values.toList() + } +} diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt index 4ffa3a7e6..74b240a24 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt @@ -49,7 +49,7 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) : concolicPathSelector.addExecutionTrace(method, result) } - override suspend fun next(): PersistentSymbolicState { + override suspend fun next(): Pair { log.debug("Waiting for client decision") val received = client.receive() @@ -61,7 +61,8 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) : val vertex: Vertex = Json.decodeFromString(received) log.debug("Received vertex: {}", vertex) - return interactiveNext(vertex) ?: concolicPathSelector.next() + return interactiveNext(vertex)?.let { it.clauses.first().instruction.parent.method to it } + ?: concolicPathSelector.next() } private fun interactiveNext(vertex: Vertex): PersistentSymbolicState? { diff --git a/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java b/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java index ed6177f46..29215ff6b 100644 --- a/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java +++ b/kex-test/src/main/kotlin/org/vorpal/research/kex/test/javadebug/JavaTest.java @@ -2,8 +2,6 @@ import org.vorpal.research.kex.test.concolic.Point; -import java.util.ArrayList; - @SuppressWarnings("ALL") public class JavaTest { public int foo(Point a, Point b) { @@ -27,12 +25,12 @@ public int foo(Point a, Point b) { return res; } - public int testWrapper(ArrayList b) { - if (b.get(0) < 0) { - throw new IllegalArgumentException(); - } - return b.size(); - } +// public int testWrapper(ArrayList b) { +// if (b.get(0) < 0) { +// throw new IllegalArgumentException(); +// } +// return b.size(); +// } public boolean testFoo(boolean b) { if (b) { diff --git a/kex.ini b/kex.ini index 852d015f7..d49450ac9 100644 --- a/kex.ini +++ b/kex.ini @@ -77,7 +77,7 @@ numberOfConcreteMethods = 3 [concolic] timeLimit = 120 numberOfExecutors = 1 -searchStrategy = cgs +searchStrategy = coverage [crash] timeLimit = 600 From 7b97082eadff6c8a67d1cfe6911855ca3d7cf468 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Thu, 14 Dec 2023 13:57:40 +0100 Subject: [PATCH 3/9] m --- .../research/kex/descriptor/converter.kt | 2 +- .../kex/trace/symbolic/SymbolicState.kt | 45 +++ .../concolic/InstructionConcolicChecker.kt | 9 - .../concolic/cgs/ContextGuidedSelector.kt | 9 +- .../coverage/CoverageGuidedSelector.kt | 9 +- .../concolic/coverage/ExecutionGraph.kt | 259 ++++++++++++++++-- .../vorpal/research/kex/smt/AsyncChecker.kt | 9 +- kex.ini | 2 + 8 files changed, 295 insertions(+), 49 deletions(-) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt index d66453854..11c599144 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/converter.kt @@ -64,7 +64,7 @@ class Object2DescriptorConverter : DescriptorBuilder() { is LongArray -> KexLong.asArray() is FloatArray -> KexFloat.asArray() is DoubleArray -> KexDouble.asArray() - is Array<*> -> any.javaClass.componentType.kex + is Array<*> -> any.javaClass.componentType.kex.asArray() is String -> KexString() else -> any.javaClass.kex } diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt index 3c9e917ae..62a2b86b2 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt @@ -18,7 +18,11 @@ import org.vorpal.research.kex.state.predicate.Predicate import org.vorpal.research.kex.state.term.Term import org.vorpal.research.kfg.ir.Method import org.vorpal.research.kfg.ir.value.Value +import org.vorpal.research.kfg.ir.value.instruction.CallInst +import org.vorpal.research.kfg.ir.value.instruction.CatchInst import org.vorpal.research.kfg.ir.value.instruction.Instruction +import org.vorpal.research.kfg.ir.value.instruction.ReturnInst +import org.vorpal.research.kthelper.assert.ktassert enum class PathClauseType { NULL_CHECK, @@ -333,15 +337,19 @@ internal class SymbolicStateImpl( concreteValues = concreteValues + other.concreteValues, termMap = termMap + other.termMap ) + override fun plus(other: StateClause): SymbolicState = copy( clauses = clauses + other ) + override fun plus(other: PathClause): SymbolicState = copy( path = path + other, ) + override fun plus(other: ClauseList): SymbolicState = copy( clauses = clauses + other ) + override fun plus(other: PathCondition): SymbolicState = copy( path = path + other, ) @@ -370,6 +378,39 @@ class PersistentSymbolicState( override val concreteValues: @Contextual PersistentMap, override val termMap: @Contextual PersistentMap, ) : SymbolicState() { + + val stackTrace: List> by lazy { + buildList> { + var previousInstruction: Instruction? = null + for (clause in clauses) { + val currentInstruction = clause.instruction + val currentMethod = currentInstruction.parent.method + when (currentInstruction) { + currentMethod.body.entry.first() -> { + add(previousInstruction to currentMethod) + } + + is CallInst -> { + previousInstruction = currentInstruction + } + + is ReturnInst -> { + ktassert(last().second == currentMethod) + removeLast() + } + + is CatchInst -> { + ktassert(isNotEmpty()) + while (last().second != currentMethod) { + removeLast() + ktassert(isNotEmpty()) + } + } + } + } + }.reversed() + } + override fun toString() = clauses.joinToString("\n") { it.predicate.toString() } override fun plus(other: SymbolicState): PersistentSymbolicState = PersistentSymbolicState( @@ -379,15 +420,19 @@ class PersistentSymbolicState( concreteValues = concreteValues.putAll(other.concreteValues), termMap = termMap.putAll(other.termMap) ) + override fun plus(other: StateClause): PersistentSymbolicState = copy( clauses = clauses + other ) + override fun plus(other: PathClause): PersistentSymbolicState = copy( path = path + other, ) + override fun plus(other: ClauseList): PersistentSymbolicState = copy( clauses = clauses + other ) + override fun plus(other: PathCondition): PersistentSymbolicState = copy( path = path + other, ) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt index a2e56d49f..f734b4ae2 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt @@ -30,7 +30,6 @@ import org.vorpal.research.kex.trace.symbolic.SymbolicState import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionResult import org.vorpal.research.kex.util.newFixedThreadPoolContextWithMDC -import org.vorpal.research.kex.util.view import org.vorpal.research.kfg.ClassManager import org.vorpal.research.kfg.ir.Method import org.vorpal.research.kthelper.assert.unreachable @@ -105,14 +104,6 @@ class InstructionConcolicChecker( }.awaitAll() } } - - val graph = when (selectorManager) { - is ContextGuidedSelectorManager -> selectorManager.graph - is CoverageGuidedSelectorManager -> selectorManager.executionGraph - else -> TODO() - } - graph.view() - val a = 10 } } diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt index c4a8be412..72546e0ff 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt @@ -4,7 +4,6 @@ import kotlinx.coroutines.yield import org.vorpal.research.kex.ExecutionContext import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelector import org.vorpal.research.kex.asm.analysis.concolic.ConcolicPathSelectorManager -import org.vorpal.research.kex.asm.analysis.concolic.coverage.ExecutionGraph import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException import org.vorpal.research.kex.asm.manager.instantiationManager import org.vorpal.research.kex.ktype.kexType @@ -44,16 +43,13 @@ class ContextGuidedSelectorManager( override val ctx: ExecutionContext, override val targets: Set ) : ConcolicPathSelectorManager { - val graph = ExecutionGraph(ctx) - override fun createPathSelectorFor(target: Method): ConcolicPathSelector = - ContextGuidedSelector(ctx, target, graph) + ContextGuidedSelector(ctx, target) } class ContextGuidedSelector( override val ctx: ExecutionContext, - val method: Method, - val graph: ExecutionGraph + val method: Method ) : ConcolicPathSelector { private val executionTree = ExecutionTree(ctx) private var currentDepth = 0 @@ -132,7 +128,6 @@ class ContextGuidedSelector( override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { executionTree.addTrace(result.symbolicState.toPersistentState()) - graph.addTrace(method, result) } override fun reverse(pathClause: PathClause): PathClause? = pathClause.reversed() diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt index 75d3d48d5..15018df56 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt @@ -13,7 +13,7 @@ class CoverageGuidedSelectorManager( override val ctx: ExecutionContext, override val targets: Set ) : ConcolicPathSelectorManager { - val executionGraph = ExecutionGraph(ctx) + val executionGraph = ExecutionGraph(ctx, targets) { isCovered(it) } override fun createPathSelectorFor(target: Method): ConcolicPathSelector = CoverageGuidedSelector(this) @@ -26,6 +26,7 @@ class CoverageGuidedSelectorManager( } fun isCovered(): Boolean = coveredInstructions.containsAll(targetInstructions) + fun isCovered(instruction: Instruction): Boolean = instruction in coveredInstructions } class CoverageGuidedSelector( @@ -40,10 +41,8 @@ class CoverageGuidedSelector( override suspend fun hasNext(): Boolean = !isEmpty() override suspend fun next(): Pair { - val candidate = executionGraph.candidates.keys.randomOrNull(ctx.random)!! - val method = executionGraph.candidates[candidate]!! - executionGraph.candidates.remove(candidate) - return method to candidate + val candidate = executionGraph.candidates.nextCandidate() + return candidate.method to candidate.state } override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt index b6645aac2..8fc83b24f 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt @@ -4,6 +4,7 @@ import com.jetbrains.rd.util.concurrentMapOf import org.vorpal.research.kex.ExecutionContext import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException import org.vorpal.research.kex.asm.manager.instantiationManager +import org.vorpal.research.kex.ktype.KexRtManager.isKexRt import org.vorpal.research.kex.ktype.kexType import org.vorpal.research.kex.state.predicate.DefaultSwitchPredicate import org.vorpal.research.kex.state.predicate.EqualityPredicate @@ -13,25 +14,34 @@ import org.vorpal.research.kex.state.predicate.path import org.vorpal.research.kex.state.predicate.predicate import org.vorpal.research.kex.state.term.ConstBoolTerm import org.vorpal.research.kex.state.term.InstanceOfTerm +import org.vorpal.research.kex.state.term.boolValue import org.vorpal.research.kex.state.term.numericValue import org.vorpal.research.kex.state.transformer.TermCollector import org.vorpal.research.kex.trace.symbolic.PathClause import org.vorpal.research.kex.trace.symbolic.PathClauseType -import org.vorpal.research.kex.trace.symbolic.PersistentPathCondition +import org.vorpal.research.kex.trace.symbolic.PersistentClauseList import org.vorpal.research.kex.trace.symbolic.PersistentSymbolicState import org.vorpal.research.kex.trace.symbolic.persistentSymbolicState import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult import org.vorpal.research.kex.trace.symbolic.toPersistentState +import org.vorpal.research.kex.util.isSubtypeOfCached +import org.vorpal.research.kex.util.next +import org.vorpal.research.kfg.arrayIndexOOBClass +import org.vorpal.research.kfg.classCastClass import org.vorpal.research.kfg.ir.BasicBlock import org.vorpal.research.kfg.ir.Method import org.vorpal.research.kfg.ir.value.EmptyUsageContext import org.vorpal.research.kfg.ir.value.IntConstant import org.vorpal.research.kfg.ir.value.Value import org.vorpal.research.kfg.ir.value.instruction.BranchInst +import org.vorpal.research.kfg.ir.value.instruction.CallInst import org.vorpal.research.kfg.ir.value.instruction.Instruction import org.vorpal.research.kfg.ir.value.instruction.SwitchInst import org.vorpal.research.kfg.ir.value.instruction.TableSwitchInst +import org.vorpal.research.kfg.nullptrClass +import org.vorpal.research.kfg.type.ArrayType import org.vorpal.research.kfg.type.ClassType +import org.vorpal.research.kfg.type.Type import org.vorpal.research.kthelper.assert.unreachable import org.vorpal.research.kthelper.graph.GraphView import org.vorpal.research.kthelper.graph.PredecessorGraph @@ -84,7 +94,8 @@ private fun Predicate.reverseSwitchCond( val candidates = run { val currentRange = branches.keys.map { (it as IntConstant).value }.toMutableSet() for (candidate in visitedCandidates) { - currentRange.removeAll(equivalencePaths[candidate]!!) + val visited: Set = equivalencePaths[candidate] ?: emptySet() + currentRange.removeAll(visited) } currentRange } @@ -139,14 +150,14 @@ class PathVertex( val pathType: PathClauseType, instruction: Instruction ) : Vertex(pathType.name, instruction) { - val states = concurrentMapOf>() - private val visitedPrefixes = Collections.newSetFromMap(concurrentMapOf()) + val states = concurrentMapOf>() + private val visitedPrefixes = Collections.newSetFromMap(concurrentMapOf()) fun addStateAndProduceCandidates( ctx: ExecutionContext, state: PersistentSymbolicState ): List { - val prefix = state.path.dropLast(1) + val prefix = state.clauses.dropLast(1) val condition = state.path.last() val prefixStates = states.getOrPut(prefix, ::mutableSetOf).also { it += state @@ -189,7 +200,14 @@ class PathVertex( try { val lhv = condition.predicate.operands[0] as InstanceOfTerm val termType = lhv.operand.type.getKfgType(ctx.types) - instantiationManager.getAll(termType, ctx.accessLevel, excludeClasses).map { + val allCandidates = instantiationManager.getAll(termType, ctx.accessLevel, excludeClasses) + .filterNot { it.isKexRt } + // TODO: add proper prioritization + val prioritizedCandidates = allCandidates.shuffled(ctx.random).take(5) + prioritizedCandidates.map { + if (it is ArrayType) { + val a = 10 + } condition.copy(predicate = path(instruction.location) { (lhv.operand `is` it.kexType) equality true }) @@ -201,8 +219,8 @@ class PathVertex( } reversedConditions.map { persistentSymbolicState( - state.clauses.dropLast(1), - prefix + it, + prefix, + state.path.dropLast(1) + it, state.concreteTypes, state.concreteValues, state.termMap @@ -213,14 +231,137 @@ class PathVertex( } } +private fun PersistentSymbolicState.findExceptionHandlerInst(type: Type): Instruction? { + val currentClause = path.last() + val stackTrace = listOf(currentClause.instruction) + stackTrace.mapNotNull { it.first } + var result: Instruction? = null + stackTrace@ for (inst in stackTrace) { + for (handler in inst.parent.handlers) { + if (type.isSubtypeOfCached(handler.exception)) { + result = handler.first() + break@stackTrace + } + } + } + return result +} + +class CandidateState( + val method: Method, + val state: PersistentSymbolicState +) { + val nextInstruction: Instruction? + + init { + val cm = method.cm + val currentClause = state.path.last() + nextInstruction = when (currentClause.type) { + PathClauseType.NULL_CHECK -> when (currentClause.predicate.operands[1].boolValue) { + true -> state.findExceptionHandlerInst(cm.nullptrClass.asType) + false -> currentClause.instruction.next + } + + PathClauseType.TYPE_CHECK -> when (currentClause.predicate.operands[1].boolValue) { + true -> currentClause.instruction.next + false -> state.findExceptionHandlerInst(cm.classCastClass.asType) + } + + PathClauseType.BOUNDS_CHECK -> when (currentClause.predicate.operands[1].boolValue) { + true -> currentClause.instruction.next + false -> state.findExceptionHandlerInst(cm.arrayIndexOOBClass.asType) + } + + PathClauseType.OVERLOAD_CHECK -> { + val checkedType = + (currentClause.predicate.operands[0] as InstanceOfTerm).checkedType.getKfgType(cm.type) + val callInst = currentClause.instruction as CallInst + when (checkedType) { + is ClassType -> { + val calledMethod = checkedType.klass.getMethod( + callInst.method.name, + callInst.method.returnType, + *callInst.method.argTypes.toTypedArray() + ) + when { + calledMethod.hasBody -> calledMethod.body.entry.first() + else -> callInst.next + } + } + + else -> callInst.next + } + } + + PathClauseType.CONDITION_CHECK -> when (val inst = currentClause.instruction) { + is BranchInst -> when (currentClause.predicate.operands[1].boolValue) { + true -> inst.trueSuccessor.first() + false -> inst.falseSuccessor.first() + } + + is SwitchInst -> { + val numericValue = currentClause.predicate.operands[1].numericValue + var result: Instruction? = null + for ((key, branch) in inst.branches) { + if (numericValue == (key as IntConstant).value) { + result = branch.first() + } + } + if (result == null) { + result = inst.default.first() + } + result + } + + is TableSwitchInst -> { + val numericValue = currentClause.predicate.operands[1].numericValue + var result: Instruction? = null + for (key in inst.range) { + if (numericValue == key) { + result = inst.branches[key - inst.range.first].first() + } + } + if (result == null) { + result = inst.default.first() + } + result + } + + else -> unreachable { log.error("Unexpected instruction in condition check: $inst") } + } + } + } + + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (javaClass != other?.javaClass) return false + + other as CandidateState + + return state == other.state + } + + override fun hashCode(): Int { + return state.hashCode() + } +} + + +class ExecutionGraph( + val ctx: ExecutionContext, + val targets: Set, + val isCovered: (Instruction) -> Boolean +) : PredecessorGraph, Viewable { + + companion object { + const val DEFAULT_SCORE = 10_000L + } -class ExecutionGraph(val ctx: ExecutionContext) : PredecessorGraph, Viewable { private val root: Vertex = StateVertex(ctx.cm.instruction.getUnreachable(EmptyUsageContext)) private val innerNodes = concurrentMapOf, Vertex>().also { it["STATE" to root.instruction] = root } - val candidates = concurrentMapOf() + val candidates = CandidateSet(ctx) override val entry: Vertex get() = root @@ -228,12 +369,84 @@ class ExecutionGraph(val ctx: ExecutionContext) : PredecessorGraph, View override val nodes: Set get() = innerNodes.values.toSet() + inner class CandidateSet(val ctx: ExecutionContext) : Iterable { + private var isValid = true + private var totalScore: Long = 0L + private val candidates = Collections.newSetFromMap(concurrentMapOf()) +// private val queue = PriorityQueue(compareBy { -it.score() }) + + override fun iterator(): Iterator = candidates.iterator() + + fun isEmpty() = candidates.isEmpty() + + fun addAll(newCandidates: Collection) { + candidates.addAll(newCandidates) + newCandidates.forEach { totalScore += it.score() } +// queue.addAll(newCandidates) + } + + private fun remove(candidateState: CandidateState) { + if (candidates.remove(candidateState)) { + totalScore -= candidateState.score() + } + } + + fun invalidate() { + isValid = false + } + + private fun recomputeScores() { + totalScore = 0L + candidates.forEach { totalScore += it.score() } +// queue.clear() +// queue.addAll(candidates) + isValid = true + } + + fun nextCandidate(): CandidateState { + if (!isValid) recomputeScores() + +// return queue.poll()!!.also { remove(it) } +// + val random = ctx.random.nextLong(totalScore) + var current = 0L + for (state in candidates) { + current += state.score() + if (random < current) { + remove(state) + return state + } + } + return unreachable { log.error("Unexpected error") } + } + } + + private fun CandidateState.score(): Long { + var score = 1L + val stackTrace = this.state.stackTrace + if (nextInstruction != null) { + score += DEFAULT_SCORE + if (nextInstruction.parent.method in targets) { + score += DEFAULT_SCORE + } + if (!isCovered(nextInstruction)) { + score += DEFAULT_SCORE + } +// val distanceToTarget = stackTrace.size - ((stackTrace.withIndex().firstOrNull { it.value.second in targets }?.index ?: 0) + 1) +// val distanceToTargetScore = (DEFAULT_SCORE.toDouble() / 2.0.pow(distanceToTarget)).toLong() +// score += distanceToTargetScore +// if (!isCovered(nextInstruction)) { +// score += distanceToTargetScore +// } + } + return score + } + fun addTrace(method: Method, executionResult: ExecutionCompletedResult) = synchronized(this) { var prevVertex = root var clauseIndex = 0 var pathIndex = 0 val symbolicState = executionResult.symbolicState.toPersistentState() - var totalNewCandidates = 0 for (clause in symbolicState.clauses) { ++clauseIndex if (clause is PathClause) ++pathIndex @@ -243,6 +456,7 @@ class ExecutionGraph(val ctx: ExecutionContext) : PredecessorGraph, View else -> Vertex.STATE } val currentVertex = innerNodes.getOrPut(type to clause.instruction) { + candidates.invalidate() when (clause) { is PathClause -> PathVertex(clause.type, clause.instruction) else -> StateVertex(clause.instruction) @@ -251,25 +465,22 @@ class ExecutionGraph(val ctx: ExecutionContext) : PredecessorGraph, View if (clause is PathClause) { currentVertex as PathVertex - val newCands = currentVertex.addStateAndProduceCandidates( - ctx, persistentSymbolicState( - symbolicState.clauses.subState(0, clauseIndex), - symbolicState.path.subPath(0, pathIndex), - symbolicState.concreteTypes, - symbolicState.concreteValues, - symbolicState.termMap - ) + candidates.addAll( + currentVertex.addStateAndProduceCandidates( + ctx, persistentSymbolicState( + symbolicState.clauses.subState(0, clauseIndex), + symbolicState.path.subPath(0, pathIndex), + symbolicState.concreteTypes, + symbolicState.concreteValues, + symbolicState.termMap + ) + ).mapTo(mutableSetOf()) { CandidateState(method, it) } ) - totalNewCandidates += newCands.size - candidates += newCands.map { it to method } } prevVertex.linkDown(currentVertex) prevVertex = currentVertex } - if (totalNewCandidates == 0) { - val a= 10 - } } override val graphView: List diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt index c5faf9224..5445f440a 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt @@ -52,6 +52,7 @@ class AsyncChecker( ) { private val isSlicingEnabled = kexConfig.getBooleanValue("smt", "slicing", false) private val logQuery = kexConfig.getBooleanValue("smt", "logQuery", false) + private val useADSolver = kexConfig.getBooleanValue("smt", "useADSolver", false) private val psa = PredicateStateAnalysis(ctx.cm) lateinit var state: PredicateState @@ -158,9 +159,11 @@ class AsyncChecker( log.debug("Query size: {}", query.size) } - tryAbstractDomainSolve(ctx, state, query)?.let { - log.debug("Constant solver acquired {}", it) - return it + if (useADSolver) { + tryAbstractDomainSolve(ctx, state, query)?.let { + log.debug("Constant solver acquired {}", it) + return it + } } val result = AsyncSMTProxySolver(ctx).use { diff --git a/kex.ini b/kex.ini index d49450ac9..e78d66463 100644 --- a/kex.ini +++ b/kex.ini @@ -121,6 +121,8 @@ logSMTLib = false simplifyFormulae = false +useADSolver = false + [ksmt] solver = z3 solver = cvc5 From 0ffb4751be5ee463d2ad0c170084d2e82fe64b88 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Wed, 27 Dec 2023 15:37:37 +0100 Subject: [PATCH 4/9] m --- .../kex/trace/symbolic/SymbolicState.kt | 4 +- .../research/kex/smt/ksmt/KSMTSolver.kt | 12 +- .../analysis/concolic/ConcolicPathSelector.kt | 2 +- .../concolic/InstructionConcolicChecker.kt | 40 ++-- .../analysis/concolic/bfs/BfsPathSelector.kt | 18 +- .../concolic/cgs/ContextGuidedSelector.kt | 6 +- .../coverage/CoverageGuidedSelector.kt | 12 +- .../concolic/coverage/ExecutionGraph.kt | 175 +++++++++------ .../concolic/coverage/InstructionGraph.kt | 207 ++++++++++++++++++ .../analysis/concolic/gui/GUIProxySelector.kt | 8 +- 10 files changed, 384 insertions(+), 100 deletions(-) create mode 100644 kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt index 62a2b86b2..9877a88ed 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt @@ -379,7 +379,7 @@ class PersistentSymbolicState( override val termMap: @Contextual PersistentMap, ) : SymbolicState() { - val stackTrace: List> by lazy { + val stackTrace: PersistentList> by lazy { buildList> { var previousInstruction: Instruction? = null for (clause in clauses) { @@ -408,7 +408,7 @@ class PersistentSymbolicState( } } } - }.reversed() + }.reversed().toPersistentList() } override fun toString() = clauses.joinToString("\n") { it.predicate.toString() } diff --git a/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt b/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt index f49c36eac..b6067bf68 100644 --- a/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt +++ b/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt @@ -431,6 +431,7 @@ class KSMTSolver( } val indices = hashSetOf() + val coveredArrays = hashSetOf() for (ptr in ptrs) { val memspace = ptr.memspace @@ -550,10 +551,13 @@ class KSMTSolver( val maxLen = maxOf(initialLength, finalLength) properties[memspace]!!["length"]!!.first[modelPtr] = term { const(initialLength) } properties[memspace]!!["length"]!!.second[modelPtr] = term { const(finalLength) } - for (i in 0 until maxLen) { - val indexTerm = term { ptr[i] } - if (indexTerm !in ptrs) - indices += indexTerm + if (modelPtr !in coveredArrays) { + coveredArrays += modelPtr + for (i in 0 until maxLen) { + val indexTerm = term { ptr[i] } + if (indexTerm !in ptrs) + indices += indexTerm + } } } else if (ptr is ConstClassTerm || ptr is ClassAccessTerm) { properties.recoverBitvectorProperty( diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt index ef0943edf..a9ccc7533 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/ConcolicPathSelector.kt @@ -17,6 +17,6 @@ interface ConcolicPathSelector : SuspendableIterator pathIterator.addExecutionTrace(method, it) - else -> log.warn("Failed to generate random trace: $it") + val initialExecution = when (val randomTrace = getRandomTrace(method)) { + is ExecutionCompletedResult -> randomTrace + else -> getDefaultTrace(method) + } + when (initialExecution) { + is ExecutionCompletedResult -> { + pathIterator.addExecutionTrace(method, persistentSymbolicState(), initialExecution) + } + + else -> { + log.warn("Failed to generate random trace for method $method: $initialExecution") } } } - private suspend fun processMethod(method: Method) { - handleStartingTrace(method, pathSelector, getRandomTrace(method)) - if (pathSelector.isEmpty()) { - handleStartingTrace(method, pathSelector, getDefaultTrace(method)) - } + private suspend fun processMethod(startingMethod: Method) { + initializeExecutionGraph(startingMethod, pathSelector) yield() while (pathSelector.hasNext()) { @@ -185,7 +191,7 @@ class InstructionConcolicChecker( when (newState) { is ExecutionCompletedResult -> when { newState.trace.isEmpty() -> log.warn { "Collected empty state from $state" } - else -> pathSelector.addExecutionTrace(method, newState) + else -> pathSelector.addExecutionTrace(method, state, newState) } else -> log.warn("Failure during execution: $newState") diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt index d60eab08a..e0a76427f 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt @@ -45,7 +45,11 @@ class BfsPathSelectorImpl( override suspend fun isEmpty(): Boolean = deque.isEmpty() override suspend fun hasNext(): Boolean = deque.isNotEmpty() - override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { + override suspend fun addExecutionTrace( + method: Method, + checkedState: PersistentSymbolicState, + result: ExecutionCompletedResult + ) { val persistentResult = result.symbolicState.toPersistentState() if (persistentResult.path in coveredPaths) return coveredPaths += persistentResult.path @@ -94,6 +98,7 @@ class BfsPathSelectorImpl( if (coveredPaths.any { reversed in it }) null else reversed } + is SwitchInst -> when (predicate) { is DefaultSwitchPredicate -> { val defaultSwitch = predicate as DefaultSwitchPredicate @@ -109,6 +114,7 @@ class BfsPathSelectorImpl( } result } + is EqualityPredicate -> { val equalityPredicate = predicate as EqualityPredicate val switchInst = instruction as SwitchInst @@ -129,8 +135,10 @@ class BfsPathSelectorImpl( if (coveredPaths.any { mutated in it }) mutated else null } } + else -> unreachable { log.error("Unexpected predicate in switch clause: $predicate") } } + is TableSwitchInst -> when (predicate) { is DefaultSwitchPredicate -> { val defaultSwitch = predicate as DefaultSwitchPredicate @@ -146,6 +154,7 @@ class BfsPathSelectorImpl( } result } + is EqualityPredicate -> { val equalityPredicate = predicate as EqualityPredicate val switchInst = instruction as TableSwitchInst @@ -166,8 +175,10 @@ class BfsPathSelectorImpl( if (coveredPaths.any { mutated in it }) null else mutated } } + else -> unreachable { log.error("Unexpected predicate in switch clause: $predicate") } } + else -> when (val pred = predicate) { is EqualityPredicate -> { val (lhv, rhv) = pred.lhv to pred.rhv @@ -175,21 +186,26 @@ class BfsPathSelectorImpl( is NullTerm -> copy(predicate = path(instruction.location) { lhv inequality null }) + is ConstBoolTerm -> copy(predicate = path(instruction.location) { lhv equality !rhv.value }) + else -> log.warn("Unknown clause $this").let { null } } } + is InequalityPredicate -> { val (lhv, rhv) = pred.lhv to pred.rhv when (rhv) { is NullTerm -> copy(predicate = path(instruction.location) { lhv equality null }) + else -> log.warn("Unknown clause $this").let { null } } } + else -> null } } diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt index 72546e0ff..9af59e619 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt @@ -126,7 +126,11 @@ class ContextGuidedSelector( branchIterator = executionTree.getBranches(currentDepth).shuffled(ctx.random).iterator() } - override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { + override suspend fun addExecutionTrace( + method: Method, + checkedState: PersistentSymbolicState, + result: ExecutionCompletedResult + ) { executionTree.addTrace(result.symbolicState.toPersistentState()) } diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt index 15018df56..92525a1c5 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/CoverageGuidedSelector.kt @@ -13,7 +13,7 @@ class CoverageGuidedSelectorManager( override val ctx: ExecutionContext, override val targets: Set ) : ConcolicPathSelectorManager { - val executionGraph = ExecutionGraph(ctx, targets) { isCovered(it) } + val executionGraph = ExecutionGraph(ctx, targets) override fun createPathSelectorFor(target: Method): ConcolicPathSelector = CoverageGuidedSelector(this) @@ -35,6 +35,7 @@ class CoverageGuidedSelector( override val ctx: ExecutionContext get() = manager.ctx private val executionGraph get() = manager.executionGraph + private val candidates = mutableMapOf() override suspend fun isEmpty(): Boolean = manager.isCovered() || executionGraph.candidates.isEmpty() @@ -42,12 +43,17 @@ class CoverageGuidedSelector( override suspend fun next(): Pair { val candidate = executionGraph.candidates.nextCandidate() + candidates[candidate.state] = candidate return candidate.method to candidate.state } - override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { + override suspend fun addExecutionTrace( + method: Method, + checkedState: PersistentSymbolicState, + result: ExecutionCompletedResult + ) { manager.addCoverage(result.trace) - executionGraph.addTrace(method, result) + executionGraph.addTrace(method, candidates[checkedState], result) } override fun reverse(pathClause: PathClause): PathClause = TODO() //pathClause.reversed() diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt index 8fc83b24f..398bfc352 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt @@ -39,7 +39,6 @@ import org.vorpal.research.kfg.ir.value.instruction.Instruction import org.vorpal.research.kfg.ir.value.instruction.SwitchInst import org.vorpal.research.kfg.ir.value.instruction.TableSwitchInst import org.vorpal.research.kfg.nullptrClass -import org.vorpal.research.kfg.type.ArrayType import org.vorpal.research.kfg.type.ClassType import org.vorpal.research.kfg.type.Type import org.vorpal.research.kthelper.assert.unreachable @@ -48,6 +47,8 @@ import org.vorpal.research.kthelper.graph.PredecessorGraph import org.vorpal.research.kthelper.graph.Viewable import org.vorpal.research.kthelper.logging.log import java.util.* +import kotlin.math.exp +import kotlin.math.pow private fun Predicate.reverseBoolCond() = when (this) { is EqualityPredicate -> predicate(this.type, this.location) { @@ -73,7 +74,6 @@ private fun Predicate.reverseSwitchCond( } } - is EqualityPredicate -> { val outgoingPaths = branches.toList() .groupBy({ it.second }, { it.first }) @@ -132,11 +132,6 @@ sealed class Vertex( other._predecessors += this } - fun linkUp(other: Vertex) { - _predecessors += other - other._successors += this - } - override fun toString(): String { return "Vertex($type, ${instruction.print()})" } @@ -191,6 +186,7 @@ class PathVertex( PathClauseType.OVERLOAD_CHECK -> { val excludeClasses = prefixStates + .asSequence() .map { it.path.last().predicate } .flatMap { TermCollector.getFullTermSet(it).filterIsInstance() } .map { it.checkedType.getKfgType(ctx.types) } @@ -205,9 +201,6 @@ class PathVertex( // TODO: add proper prioritization val prioritizedCandidates = allCandidates.shuffled(ctx.random).take(5) prioritizedCandidates.map { - if (it is ArrayType) { - val a = 10 - } condition.copy(predicate = path(instruction.location) { (lhv.operand `is` it.kexType) equality true }) @@ -348,12 +341,12 @@ class CandidateState( class ExecutionGraph( val ctx: ExecutionContext, - val targets: Set, - val isCovered: (Instruction) -> Boolean + val targets: Set ) : PredecessorGraph, Viewable { companion object { const val DEFAULT_SCORE = 10_000L + const val SIGMA = 10.0 } private val root: Vertex = StateVertex(ctx.cm.instruction.getUnreachable(EmptyUsageContext)) @@ -369,11 +362,12 @@ class ExecutionGraph( override val nodes: Set get() = innerNodes.values.toSet() + val instructionGraph = InstructionGraph() + inner class CandidateSet(val ctx: ExecutionContext) : Iterable { private var isValid = true private var totalScore: Long = 0L private val candidates = Collections.newSetFromMap(concurrentMapOf()) -// private val queue = PriorityQueue(compareBy { -it.score() }) override fun iterator(): Iterator = candidates.iterator() @@ -382,7 +376,6 @@ class ExecutionGraph( fun addAll(newCandidates: Collection) { candidates.addAll(newCandidates) newCandidates.forEach { totalScore += it.score() } -// queue.addAll(newCandidates) } private fun remove(candidateState: CandidateState) { @@ -398,16 +391,12 @@ class ExecutionGraph( private fun recomputeScores() { totalScore = 0L candidates.forEach { totalScore += it.score() } -// queue.clear() -// queue.addAll(candidates) isValid = true } fun nextCandidate(): CandidateState { if (!isValid) recomputeScores() -// return queue.poll()!!.also { remove(it) } -// val random = ctx.random.nextLong(totalScore) var current = 0L for (state in candidates) { @@ -421,67 +410,115 @@ class ExecutionGraph( } } + val coverageAll = mutableSetOf() + + private val distances = mutableMapOf() + private val scaledDistances = mutableMapOf() + private val scores = mutableMapOf() + private val coverage = mutableMapOf>() + private fun CandidateState.score(): Long { - var score = 1L - val stackTrace = this.state.stackTrace + var score = 0L if (nextInstruction != null) { - score += DEFAULT_SCORE - if (nextInstruction.parent.method in targets) { - score += DEFAULT_SCORE - } - if (!isCovered(nextInstruction)) { - score += DEFAULT_SCORE - } -// val distanceToTarget = stackTrace.size - ((stackTrace.withIndex().firstOrNull { it.value.second in targets }?.index ?: 0) + 1) -// val distanceToTargetScore = (DEFAULT_SCORE.toDouble() / 2.0.pow(distanceToTarget)).toLong() -// score += distanceToTargetScore -// if (!isCovered(nextInstruction)) { -// score += distanceToTargetScore -// } + score += 1L + val distance = instructionGraph.getVertex(nextInstruction).distanceToUncovered(targets, state.stackTrace) + val normalizedDistance = exp(-0.5 * (distance.toDouble() / SIGMA).pow(2)) + val scaledDistance = (normalizedDistance * DEFAULT_SCORE).toLong() + score += scaledDistance + + distances[this] = distance + scaledDistances[this] = scaledDistance + scores[this] = score + coverage[this] = coverageAll.toSet() } return score } - fun addTrace(method: Method, executionResult: ExecutionCompletedResult) = synchronized(this) { - var prevVertex = root - var clauseIndex = 0 - var pathIndex = 0 - val symbolicState = executionResult.symbolicState.toPersistentState() - for (clause in symbolicState.clauses) { - ++clauseIndex - if (clause is PathClause) ++pathIndex - - val type = when (clause) { - is PathClause -> clause.type.toString() - else -> Vertex.STATE - } - val currentVertex = innerNodes.getOrPut(type to clause.instruction) { - candidates.invalidate() - when (clause) { - is PathClause -> PathVertex(clause.type, clause.instruction) - else -> StateVertex(clause.instruction) + fun evaluatePerformance(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) = synchronized(instructionGraph) { + val overallCoverageIncrease = executionResult.trace.count { !instructionGraph.getVertex(it).covered } + val targetCoverageIncrease = executionResult.trace.filter { it.parent.method in targets } + .count { !instructionGraph.getVertex(it).covered } + + val oldCoverage = coverage[candidate] ?: emptySet() + val oldCoverageIncrease = executionResult.trace.count { it !in oldCoverage } + val nextInstWasCovered = candidate?.nextInstruction?.let { it in oldCoverage } ?: false + val nextInstNowCovered = candidate?.nextInstruction?.let { it in executionResult.trace } ?: false + + + val relativeOverallCoverageIncrease = overallCoverageIncrease.toDouble() / instructionGraph.covered + val relativeTargetCoverageIncrease = + targetCoverageIncrease.toDouble() / targets.flatMap { it.body.bodyBlocks.flatMap { it.instructions } } + .count { instructionGraph.getVertex(it).covered } + + val inLoop = candidate?.nextInstruction?.let { inst -> + val loopInfo = inst.parent.method.getLoopInfo() + loopInfo.count { inst.parent in it.body } + } ?: 0 + + log.debug( + "COVERAGE STATS *" + + "${method}\t" + + "${candidate?.state?.path?.lastOrNull()}\t" + + "${distances[candidate] ?: Int.MAX_VALUE}\t" + + "${scaledDistances[candidate] ?: DEFAULT_SCORE}\t" + + "${scores[candidate] ?: 0.0}\t" + + "${candidate?.state?.path?.last()?.type}\t" + + "${candidate?.nextInstruction?.javaClass}\t" + + "${inLoop}\t" + + "${overallCoverageIncrease}\t" + + "${targetCoverageIncrease}\t" + + "${relativeOverallCoverageIncrease}\t" + + "${relativeTargetCoverageIncrease}\t" + + "${oldCoverageIncrease}\t" + + "${nextInstWasCovered}\t" + + "${nextInstNowCovered}\t" + ) + } + + fun addTrace(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) = + synchronized(instructionGraph) { +// evaluatePerformance(method, candidate, executionResult) + coverageAll += executionResult.trace + instructionGraph.addTrace(executionResult.trace) + var prevVertex = root + var clauseIndex = 0 + var pathIndex = 0 + val symbolicState = executionResult.symbolicState.toPersistentState() + for (clause in symbolicState.clauses) { + ++clauseIndex + if (clause is PathClause) ++pathIndex + + val type = when (clause) { + is PathClause -> clause.type.toString() + else -> Vertex.STATE + } + val currentVertex = innerNodes.getOrPut(type to clause.instruction) { + candidates.invalidate() + when (clause) { + is PathClause -> PathVertex(clause.type, clause.instruction) + else -> StateVertex(clause.instruction) + } } - } - if (clause is PathClause) { - currentVertex as PathVertex - candidates.addAll( - currentVertex.addStateAndProduceCandidates( - ctx, persistentSymbolicState( - symbolicState.clauses.subState(0, clauseIndex), - symbolicState.path.subPath(0, pathIndex), - symbolicState.concreteTypes, - symbolicState.concreteValues, - symbolicState.termMap - ) - ).mapTo(mutableSetOf()) { CandidateState(method, it) } - ) - } + if (clause is PathClause) { + currentVertex as PathVertex + candidates.addAll( + currentVertex.addStateAndProduceCandidates( + ctx, persistentSymbolicState( + symbolicState.clauses.subState(0, clauseIndex), + symbolicState.path.subPath(0, pathIndex), + symbolicState.concreteTypes, + symbolicState.concreteValues, + symbolicState.termMap + ) + ).mapTo(mutableSetOf()) { CandidateState(method, it) } + ) + } - prevVertex.linkDown(currentVertex) - prevVertex = currentVertex + prevVertex.linkDown(currentVertex) + prevVertex = currentVertex + } } - } override val graphView: List get() { diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt new file mode 100644 index 000000000..82be419d0 --- /dev/null +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt @@ -0,0 +1,207 @@ +package org.vorpal.research.kex.asm.analysis.concolic.coverage + +import info.leadinglight.jdot.enums.Color +import kotlinx.collections.immutable.PersistentList +import org.vorpal.research.kfg.ir.BasicBlock +import org.vorpal.research.kfg.ir.Method +import org.vorpal.research.kfg.ir.value.instruction.ArrayLoadInst +import org.vorpal.research.kfg.ir.value.instruction.ArrayStoreInst +import org.vorpal.research.kfg.ir.value.instruction.BranchInst +import org.vorpal.research.kfg.ir.value.instruction.CallInst +import org.vorpal.research.kfg.ir.value.instruction.FieldLoadInst +import org.vorpal.research.kfg.ir.value.instruction.FieldStoreInst +import org.vorpal.research.kfg.ir.value.instruction.Instruction +import org.vorpal.research.kfg.ir.value.instruction.ReturnInst +import org.vorpal.research.kthelper.assert.ktassert +import org.vorpal.research.kthelper.collection.queueOf +import org.vorpal.research.kthelper.graph.GraphView +import org.vorpal.research.kthelper.graph.Viewable + + +class InstructionGraph : Viewable { + private val nodes = mutableMapOf() + + var covered = 0 + + inner class Vertex(val instruction: Instruction) { + var covered = false + val upEdges = mutableSetOf() + val downEdges = mutableSetOf() + + override fun toString(): String = instruction.print() + + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (javaClass != other?.javaClass) return false + + other as Vertex + + return instruction == other.instruction + } + + override fun hashCode(): Int { + return instruction.hashCode() + } + + fun linkDown(other: Vertex) { + downEdges += other + other.upEdges += this + } + + fun distanceToUncovered( + targets: Set, + initialStackTrace: PersistentList> + ): Int { + var minDistance = Int.MAX_VALUE + + val distances = mutableMapOf() + distances[this] = 0 + val queue = queueOf(this to initialStackTrace) + while (queue.isNotEmpty()) { + val (current, stackTrace) = queue.poll() + val currentDistance = distances[current]!! + + if (!current.covered && current.instruction.parent.method in targets) { + if (currentDistance < minDistance) { + minDistance = currentDistance + } + continue + } + + val edges = when (current.instruction) { + is ReturnInst -> { + val newStackTrace = stackTrace.removeAt(stackTrace.size - 1) + if (newStackTrace.isEmpty()) continue + current.downEdges.filter { it.instruction.parent.method == newStackTrace.last().second } + .map { it to newStackTrace } + } + + is CallInst -> { + current.downEdges.map { + if (it.instruction.parent.method != current.instruction.parent.method) { + it to stackTrace.add(it.instruction to it.instruction.parent.method) + } else { + it to stackTrace + } + } + } + + else -> current.downEdges.map { it to stackTrace } + } + + for ((edge, edgeStackTrace) in edges) { + val distance = distances.getOrDefault(edge, Int.MAX_VALUE) + val stepValue = when (current.instruction) { + is CallInst -> 2 + is FieldLoadInst, is FieldStoreInst -> 1 + is ArrayLoadInst, is ArrayStoreInst -> 1 + is BranchInst -> 1 + else -> 0 + } + if (distance > (currentDistance + stepValue)) { + distances[edge] = currentDistance + stepValue + queue += edge to edgeStackTrace + } + } + } +// object : Viewable { +// override val graphView: List +// get() { +// val graphNodes = mutableMapOf() +// +// var i = 0 +// for (vertex in nodes.values) { +// graphNodes[vertex] = GraphView("${i++}", "$vertex".replace("\"", "\\\"")) { +// val color = when { +// vertex == this@Vertex -> Color.X11.blue +// vertex.instruction.parent.method in targets -> when { +// vertex.covered -> Color.X11.green +// else -> Color.X11.red +// } +// else -> Color.X11.black +// } +// it.setColor(color) +// } +// } +// +// for (vertex in nodes.values) { +// val current = graphNodes.getValue(vertex) +// for (child in vertex.downEdges) { +// current.addSuccessor(graphNodes.getValue(child)) { +// it.setLabel(distances[child]?.toString() ?: "") +// } +// } +// } +// +// return graphNodes.values.toList() +// } +// }.view() + return minDistance + } + } + + fun getVertex(instruction: Instruction): Vertex { + if (instruction in nodes) { + return nodes[instruction]!! + } else { + val method = instruction.parent.method + ktassert(instruction == method.body.entry.first()) + + val queue = queueOf>() + queue += null to method.body.entry + queue.addAll(method.body.catchEntries.map { null to it }) + val visited = mutableSetOf>() + while (queue.isNotEmpty()) { + var (prev, block) = queue.poll() + if (prev?.instruction to block in visited) continue + visited += prev?.instruction to block + + for (inst in block) { + val vertex = nodes.getOrPut(inst) { Vertex(inst) } + prev?.linkDown(vertex) + prev = vertex + } + + queue.addAll(block.successors.map { prev to it }) + } + return nodes.getOrPut(instruction) { Vertex(instruction) } + } + } + + fun addTrace(trace: List) { + var prev: Vertex? = null + for (inst in trace) { + val current = getVertex(inst) + if (!current.covered) ++covered + + current.covered = true + prev?.linkDown(current) + prev = current + } + } + + override val graphView: List + get() { + val graphNodes = mutableMapOf() + + var i = 0 + for (vertex in nodes.values) { + graphNodes[vertex] = GraphView("${i++}", "$vertex".replace("\"", "\\\"")) { + val color = when { + vertex.covered -> Color.X11.green + else -> Color.X11.red + } + it.setColor(color) + } + } + + for (vertex in nodes.values) { + val current = graphNodes.getValue(vertex) + for (child in vertex.downEdges) { + current.addSuccessor(graphNodes.getValue(child)) + } + } + + return graphNodes.values.toList() + } +} diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt index 74b240a24..5f02557d8 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt @@ -40,13 +40,17 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) : override suspend fun isEmpty(): Boolean = concolicPathSelector.isEmpty() - override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { + override suspend fun addExecutionTrace( + method: Method, + checkedState: PersistentSymbolicState, + result: ExecutionCompletedResult + ) { val vertices = graph.addTrace(result.symbolicState.toPersistentState()) val json = Json.encodeToString(vertices) log.debug("Vertices trace: $json") log.debug(graph) client.send(json) - concolicPathSelector.addExecutionTrace(method, result) + concolicPathSelector.addExecutionTrace(method, checkedState, result) } override suspend fun next(): Pair { From ccb48ecebd476a1723c997c54d47e0419ba63741 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Wed, 3 Jan 2024 15:37:34 +0100 Subject: [PATCH 5/9] small optimizations --- .../src/main/resources/SMTExpr.vm | 2 +- .../kex/trace/symbolic/SymbolicState.kt | 36 ---- .../concolic/InstructionConcolicChecker.kt | 2 - .../concolic/coverage/ExecutionGraph.kt | 178 ++++++++++++------ .../concolic/coverage/InstructionGraph.kt | 16 +- 5 files changed, 128 insertions(+), 106 deletions(-) diff --git a/kex-annotation-processor/src/main/resources/SMTExpr.vm b/kex-annotation-processor/src/main/resources/SMTExpr.vm index fd8858687..4d804906c 100644 --- a/kex-annotation-processor/src/main/resources/SMTExpr.vm +++ b/kex-annotation-processor/src/main/resources/SMTExpr.vm @@ -573,7 +573,7 @@ class Ifer { inline fun < reified T : $valexpr > `else`(`false`: T): T { val ctx = cond.ctx val expr = engine().ite(ctx, cond.expr, `true`.expr, `false`.expr) - val axiom = spliceAxioms(ctx, `true`.axiom, `false`.axiom) + val axiom = spliceAxioms(ctx, cond.axiom, `true`.axiom, `false`.axiom) return ${valexpr}.forceCast< T >($valexpr(ctx, expr, axiom)) } inline fun < reified T : $valexpr > else_(`false`: () -> T) = `else`(`false`()) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt index 9877a88ed..9ef3975b2 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/SymbolicState.kt @@ -18,11 +18,7 @@ import org.vorpal.research.kex.state.predicate.Predicate import org.vorpal.research.kex.state.term.Term import org.vorpal.research.kfg.ir.Method import org.vorpal.research.kfg.ir.value.Value -import org.vorpal.research.kfg.ir.value.instruction.CallInst -import org.vorpal.research.kfg.ir.value.instruction.CatchInst import org.vorpal.research.kfg.ir.value.instruction.Instruction -import org.vorpal.research.kfg.ir.value.instruction.ReturnInst -import org.vorpal.research.kthelper.assert.ktassert enum class PathClauseType { NULL_CHECK, @@ -379,38 +375,6 @@ class PersistentSymbolicState( override val termMap: @Contextual PersistentMap, ) : SymbolicState() { - val stackTrace: PersistentList> by lazy { - buildList> { - var previousInstruction: Instruction? = null - for (clause in clauses) { - val currentInstruction = clause.instruction - val currentMethod = currentInstruction.parent.method - when (currentInstruction) { - currentMethod.body.entry.first() -> { - add(previousInstruction to currentMethod) - } - - is CallInst -> { - previousInstruction = currentInstruction - } - - is ReturnInst -> { - ktassert(last().second == currentMethod) - removeLast() - } - - is CatchInst -> { - ktassert(isNotEmpty()) - while (last().second != currentMethod) { - removeLast() - ktassert(isNotEmpty()) - } - } - } - } - }.reversed().toPersistentList() - } - override fun toString() = clauses.joinToString("\n") { it.predicate.toString() } override fun plus(other: SymbolicState): PersistentSymbolicState = PersistentSymbolicState( diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt index 4cb9a92e3..055096dde 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/InstructionConcolicChecker.kt @@ -31,7 +31,6 @@ import org.vorpal.research.kex.trace.symbolic.persistentSymbolicState import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionCompletedResult import org.vorpal.research.kex.trace.symbolic.protocol.ExecutionResult import org.vorpal.research.kex.util.newFixedThreadPoolContextWithMDC -import org.vorpal.research.kex.util.view import org.vorpal.research.kfg.ClassManager import org.vorpal.research.kfg.ir.Method import org.vorpal.research.kthelper.assert.unreachable @@ -106,7 +105,6 @@ class InstructionConcolicChecker( }.awaitAll() } } - (selectorManager as CoverageGuidedSelectorManager).executionGraph.instructionGraph.view() } } diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt index 398bfc352..d0dedd5b6 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt @@ -1,6 +1,8 @@ package org.vorpal.research.kex.asm.analysis.concolic.coverage import com.jetbrains.rd.util.concurrentMapOf +import kotlinx.collections.immutable.PersistentList +import kotlinx.collections.immutable.toPersistentList import org.vorpal.research.kex.ExecutionContext import org.vorpal.research.kex.asm.manager.NoConcreteInstanceException import org.vorpal.research.kex.asm.manager.instantiationManager @@ -35,7 +37,9 @@ import org.vorpal.research.kfg.ir.value.IntConstant import org.vorpal.research.kfg.ir.value.Value import org.vorpal.research.kfg.ir.value.instruction.BranchInst import org.vorpal.research.kfg.ir.value.instruction.CallInst +import org.vorpal.research.kfg.ir.value.instruction.CatchInst import org.vorpal.research.kfg.ir.value.instruction.Instruction +import org.vorpal.research.kfg.ir.value.instruction.ReturnInst import org.vorpal.research.kfg.ir.value.instruction.SwitchInst import org.vorpal.research.kfg.ir.value.instruction.TableSwitchInst import org.vorpal.research.kfg.nullptrClass @@ -145,8 +149,9 @@ class PathVertex( val pathType: PathClauseType, instruction: Instruction ) : Vertex(pathType.name, instruction) { - val states = concurrentMapOf>() - private val visitedPrefixes = Collections.newSetFromMap(concurrentMapOf()) + val states = hashMapOf>() + private val visitedPrefixes = + hashSetOf()//Collections.newSetFromMap(concurrentMapOf()) fun addStateAndProduceCandidates( ctx: ExecutionContext, @@ -154,7 +159,7 @@ class PathVertex( ): List { val prefix = state.clauses.dropLast(1) val condition = state.path.last() - val prefixStates = states.getOrPut(prefix, ::mutableSetOf).also { + val prefixStates = states.getOrPut(prefix, ::hashSetOf).also { it += state } return when (prefix) { @@ -224,9 +229,12 @@ class PathVertex( } } -private fun PersistentSymbolicState.findExceptionHandlerInst(type: Type): Instruction? { +private fun PersistentSymbolicState.findExceptionHandlerInst( + type: Type, + stateStackTrace: PersistentList> +): Instruction? { val currentClause = path.last() - val stackTrace = listOf(currentClause.instruction) + stackTrace.mapNotNull { it.first } + val stackTrace = listOf(currentClause.instruction) + stateStackTrace.mapNotNull { it.first } var result: Instruction? = null stackTrace@ for (inst in stackTrace) { for (handler in inst.parent.handlers) { @@ -241,7 +249,8 @@ private fun PersistentSymbolicState.findExceptionHandlerInst(type: Type): Instru class CandidateState( val method: Method, - val state: PersistentSymbolicState + val state: PersistentSymbolicState, + val stackTrace: PersistentList> ) { val nextInstruction: Instruction? @@ -250,18 +259,18 @@ class CandidateState( val currentClause = state.path.last() nextInstruction = when (currentClause.type) { PathClauseType.NULL_CHECK -> when (currentClause.predicate.operands[1].boolValue) { - true -> state.findExceptionHandlerInst(cm.nullptrClass.asType) + true -> state.findExceptionHandlerInst(cm.nullptrClass.asType, stackTrace) false -> currentClause.instruction.next } PathClauseType.TYPE_CHECK -> when (currentClause.predicate.operands[1].boolValue) { true -> currentClause.instruction.next - false -> state.findExceptionHandlerInst(cm.classCastClass.asType) + false -> state.findExceptionHandlerInst(cm.classCastClass.asType, stackTrace) } PathClauseType.BOUNDS_CHECK -> when (currentClause.predicate.operands[1].boolValue) { true -> currentClause.instruction.next - false -> state.findExceptionHandlerInst(cm.arrayIndexOOBClass.asType) + false -> state.findExceptionHandlerInst(cm.arrayIndexOOBClass.asType, stackTrace) } PathClauseType.OVERLOAD_CHECK -> { @@ -396,6 +405,9 @@ class ExecutionGraph( fun nextCandidate(): CandidateState { if (!isValid) recomputeScores() + if (totalScore == 0L) { + return candidates.first().also { remove(it) } + } val random = ctx.random.nextLong(totalScore) var current = 0L @@ -412,8 +424,11 @@ class ExecutionGraph( val coverageAll = mutableSetOf() - private val distances = mutableMapOf() - private val scaledDistances = mutableMapOf() + private val targetDistances = mutableMapOf() + private val scaledTargetDistances = mutableMapOf() + + private val uncoveredDistances = mutableMapOf() + private val scaledUncoveredDistances = mutableMapOf() private val scores = mutableMapOf() private val coverage = mutableMapOf>() @@ -421,20 +436,28 @@ class ExecutionGraph( var score = 0L if (nextInstruction != null) { score += 1L - val distance = instructionGraph.getVertex(nextInstruction).distanceToUncovered(targets, state.stackTrace) - val normalizedDistance = exp(-0.5 * (distance.toDouble() / SIGMA).pow(2)) - val scaledDistance = (normalizedDistance * DEFAULT_SCORE).toLong() - score += scaledDistance - - distances[this] = distance - scaledDistances[this] = scaledDistance - scores[this] = score - coverage[this] = coverageAll.toSet() + + val scaleDistance = { distance: Int -> + val normalizedDistance = exp(-0.5 * (distance.toDouble() / SIGMA).pow(2)) + (normalizedDistance * DEFAULT_SCORE).toLong() + } + + val (targetDistance, uncoveredDistance) = instructionGraph.getVertex(nextInstruction) + .distanceToUncovered(targets, stackTrace) + score += scaleDistance(targetDistance) + score += scaleDistance(uncoveredDistance) / 10L + +// targetDistances[this] = targetDistance +// scaledTargetDistances[this] = scaleDistance(targetDistance) +// uncoveredDistances[this] = uncoveredDistance +// scaledUncoveredDistances[this] = scaleDistance(uncoveredDistance) / 10L +// scores[this] = score +// coverage[this] = coverageAll.toSet() } return score } - fun evaluatePerformance(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) = synchronized(instructionGraph) { + fun evaluatePerformance(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) { val overallCoverageIncrease = executionResult.trace.count { !instructionGraph.getVertex(it).covered } val targetCoverageIncrease = executionResult.trace.filter { it.parent.method in targets } .count { !instructionGraph.getVertex(it).covered } @@ -455,12 +478,19 @@ class ExecutionGraph( loopInfo.count { inst.parent in it.body } } ?: 0 + if (candidate?.state?.path?.lastOrNull()?.type != null + && targetDistances[candidate] == 0 && overallCoverageIncrease == 0) { + val a = 10 + } + log.debug( "COVERAGE STATS *" + - "${method}\t" + + "${method}\t" + "${candidate?.state?.path?.lastOrNull()}\t" + - "${distances[candidate] ?: Int.MAX_VALUE}\t" + - "${scaledDistances[candidate] ?: DEFAULT_SCORE}\t" + + "${targetDistances[candidate] ?: Int.MAX_VALUE}\t" + + "${scaledTargetDistances[candidate] ?: DEFAULT_SCORE}\t" + + "${uncoveredDistances[candidate] ?: Int.MAX_VALUE}\t" + + "${scaledUncoveredDistances[candidate] ?: DEFAULT_SCORE}\t" + "${scores[candidate] ?: 0.0}\t" + "${candidate?.state?.path?.last()?.type}\t" + "${candidate?.nextInstruction?.javaClass}\t" + @@ -475,50 +505,76 @@ class ExecutionGraph( ) } - fun addTrace(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) = - synchronized(instructionGraph) { -// evaluatePerformance(method, candidate, executionResult) - coverageAll += executionResult.trace - instructionGraph.addTrace(executionResult.trace) - var prevVertex = root - var clauseIndex = 0 - var pathIndex = 0 - val symbolicState = executionResult.symbolicState.toPersistentState() - for (clause in symbolicState.clauses) { - ++clauseIndex - if (clause is PathClause) ++pathIndex - - val type = when (clause) { - is PathClause -> clause.type.toString() - else -> Vertex.STATE + fun addTrace(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) { +// evaluatePerformance(method, candidate, executionResult) +// coverageAll += executionResult.trace + instructionGraph.addTrace(executionResult.trace) + var prevVertex = root + var clauseIndex = 0 + var pathIndex = 0 + val symbolicState = executionResult.symbolicState.toPersistentState() + + var previousInstruction: Instruction? = null + val stackTrace = mutableListOf>() + + for (clause in symbolicState.clauses) { + // stack trace building part + val currentInstruction = clause.instruction + val currentMethod = currentInstruction.parent.method + when (currentInstruction) { + currentMethod.body.entry.first() -> { + stackTrace += previousInstruction to currentMethod } - val currentVertex = innerNodes.getOrPut(type to clause.instruction) { - candidates.invalidate() - when (clause) { - is PathClause -> PathVertex(clause.type, clause.instruction) - else -> StateVertex(clause.instruction) - } + + is CallInst -> { + previousInstruction = currentInstruction } - if (clause is PathClause) { - currentVertex as PathVertex - candidates.addAll( - currentVertex.addStateAndProduceCandidates( - ctx, persistentSymbolicState( - symbolicState.clauses.subState(0, clauseIndex), - symbolicState.path.subPath(0, pathIndex), - symbolicState.concreteTypes, - symbolicState.concreteValues, - symbolicState.termMap - ) - ).mapTo(mutableSetOf()) { CandidateState(method, it) } - ) + is ReturnInst -> stackTrace.removeLast() + is CatchInst -> while (stackTrace.last().second != currentMethod) { + stackTrace.removeLast() } + } + + // candidate states calculation part + ++clauseIndex + // TODO: limit number of states +// if (clauseIndex > 10_000) break + if (clause is PathClause) ++pathIndex - prevVertex.linkDown(currentVertex) - prevVertex = currentVertex + val type = when (clause) { + is PathClause -> clause.type.toString() + else -> Vertex.STATE } + val currentVertex = innerNodes.getOrPut(type to clause.instruction) { + candidates.invalidate() + when (clause) { + is PathClause -> PathVertex(clause.type, clause.instruction) + else -> StateVertex(clause.instruction) + } + } + + if (clause is PathClause) { + currentVertex as PathVertex + val currentStackTrace = stackTrace.reversed().toPersistentList() + + candidates.addAll( + currentVertex.addStateAndProduceCandidates( + ctx, persistentSymbolicState( + symbolicState.clauses.subState(0, clauseIndex), + symbolicState.path.subPath(0, pathIndex), + symbolicState.concreteTypes, + symbolicState.concreteValues, + symbolicState.termMap + ) + ).mapTo(mutableSetOf()) { CandidateState(method, it, currentStackTrace) } + ) + } + + prevVertex.linkDown(currentVertex) + prevVertex = currentVertex } + } override val graphView: List get() { diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt index 82be419d0..9de79b4ed 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt @@ -51,8 +51,9 @@ class InstructionGraph : Viewable { fun distanceToUncovered( targets: Set, initialStackTrace: PersistentList> - ): Int { - var minDistance = Int.MAX_VALUE + ): Pair { + var minTargetDistance = Int.MAX_VALUE + var minUncoveredDistance = Int.MAX_VALUE val distances = mutableMapOf() distances[this] = 0 @@ -61,9 +62,12 @@ class InstructionGraph : Viewable { val (current, stackTrace) = queue.poll() val currentDistance = distances[current]!! - if (!current.covered && current.instruction.parent.method in targets) { - if (currentDistance < minDistance) { - minDistance = currentDistance + if (!current.covered) { + if (currentDistance < minUncoveredDistance) { + minUncoveredDistance = currentDistance + } + if (current.instruction.parent.method in targets && currentDistance < minTargetDistance) { + minTargetDistance = currentDistance } continue } @@ -136,7 +140,7 @@ class InstructionGraph : Viewable { // return graphNodes.values.toList() // } // }.view() - return minDistance + return minTargetDistance to minUncoveredDistance } } From 23efd62e749a3853019d131a13c582d4b85515df Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Wed, 3 Jan 2024 15:59:40 +0100 Subject: [PATCH 6/9] small optimizations 2 --- .../concolic/coverage/ExecutionGraph.kt | 29 ++++++++++++------- 1 file changed, 18 insertions(+), 11 deletions(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt index d0dedd5b6..b026b3326 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt @@ -253,6 +253,7 @@ class CandidateState( val stackTrace: PersistentList> ) { val nextInstruction: Instruction? + var score: Long = 0L init { val cm = method.cm @@ -374,7 +375,7 @@ class ExecutionGraph( val instructionGraph = InstructionGraph() inner class CandidateSet(val ctx: ExecutionContext) : Iterable { - private var isValid = true + private var isValid = false private var totalScore: Long = 0L private val candidates = Collections.newSetFromMap(concurrentMapOf()) @@ -384,12 +385,15 @@ class ExecutionGraph( fun addAll(newCandidates: Collection) { candidates.addAll(newCandidates) - newCandidates.forEach { totalScore += it.score() } + newCandidates.forEach { totalScore += it.score } } private fun remove(candidateState: CandidateState) { if (candidates.remove(candidateState)) { - totalScore -= candidateState.score() + totalScore -= candidateState.score + if (totalScore < 0L) { + val a = 10 + } } } @@ -399,7 +403,10 @@ class ExecutionGraph( private fun recomputeScores() { totalScore = 0L - candidates.forEach { totalScore += it.score() } + candidates.forEach { + it.recomputeScore() + totalScore += it.score + } isValid = true } @@ -412,7 +419,7 @@ class ExecutionGraph( val random = ctx.random.nextLong(totalScore) var current = 0L for (state in candidates) { - current += state.score() + current += state.score if (random < current) { remove(state) return state @@ -432,10 +439,10 @@ class ExecutionGraph( private val scores = mutableMapOf() private val coverage = mutableMapOf>() - private fun CandidateState.score(): Long { - var score = 0L + private fun CandidateState.recomputeScore() { + var newScore = 0L if (nextInstruction != null) { - score += 1L + newScore += 1L val scaleDistance = { distance: Int -> val normalizedDistance = exp(-0.5 * (distance.toDouble() / SIGMA).pow(2)) @@ -444,8 +451,8 @@ class ExecutionGraph( val (targetDistance, uncoveredDistance) = instructionGraph.getVertex(nextInstruction) .distanceToUncovered(targets, stackTrace) - score += scaleDistance(targetDistance) - score += scaleDistance(uncoveredDistance) / 10L + newScore += scaleDistance(targetDistance) + newScore += scaleDistance(uncoveredDistance) / 10L // targetDistances[this] = targetDistance // scaledTargetDistances[this] = scaleDistance(targetDistance) @@ -454,7 +461,7 @@ class ExecutionGraph( // scores[this] = score // coverage[this] = coverageAll.toSet() } - return score + score = newScore } fun evaluatePerformance(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) { From d29859c7dfc4e7bafdc6cc2d8de1095c236fadb7 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Wed, 3 Jan 2024 16:54:42 +0100 Subject: [PATCH 7/9] proper static field inlining --- .../research/kex/descriptor/descriptor.kt | 61 ++++++++++++++++ .../vorpal/research/kex/smt/AsyncChecker.kt | 2 + .../kex/smt/AsyncIncrementalChecker.kt | 2 + .../state/transformer/StaticFieldInliner.kt | 71 +++++++++++++++++++ 4 files changed, 136 insertions(+) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt index f2569e4d8..8e7eaef9d 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/descriptor/descriptor.kt @@ -54,6 +54,7 @@ sealed class Descriptor(term: Term, type: KexType) { } val query: PredicateState get() = collectQuery(mutableSetOf()) + val initializerState: PredicateState get() = collectInitializerState(mutableSetOf()) val depth: Int get() = countDepth(setOf(), mutableMapOf()) val typeInfo: PredicateState get() = generateTypeInfo(mutableSetOf()) @@ -67,6 +68,7 @@ sealed class Descriptor(term: Term, type: KexType) { abstract fun print(map: MutableMap): String abstract fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean abstract fun collectQuery(set: MutableSet): PredicateState + abstract fun collectInitializerState(set: MutableSet): PredicateState abstract fun countDepth(visited: Set, cache: MutableMap): Int abstract fun concretize( @@ -105,6 +107,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality null } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality null } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>) = other is Null } @@ -116,6 +122,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality value } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality value } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean { if (other !is Bool) return false return this.value == other.value @@ -129,6 +139,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality value } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality value } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean { if (other !is Byte) return false return this.value == other.value @@ -142,6 +156,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality value } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality value } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean { if (other !is Char) return false return this.value == other.value @@ -155,6 +173,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality value } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality value } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean { if (other !is Short) return false return this.value == other.value @@ -168,6 +190,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality value } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality value } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean { if (other !is Int) return false return this.value == other.value @@ -181,6 +207,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality value } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality value } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean { if (other !is Long) return false return this.value == other.value @@ -194,6 +224,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality value } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality value } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean { if (other !is Float) return false return this.value == other.value @@ -207,6 +241,10 @@ sealed class ConstantDescriptor(term: Term, type: KexType) : Descriptor(term, ty require { term equality value } } + override fun collectInitializerState(set: MutableSet): PredicateState = basic { + state { term equality value } + } + override fun structuralEquality(other: Descriptor, map: MutableSet>): Boolean { if (other !is Double) return false return this.value == other.value @@ -283,6 +321,19 @@ sealed class FieldContainingDescriptor>( } } + override fun collectInitializerState(set: MutableSet): PredicateState { + if (this in set) return emptyState() + set += this + return basic { + state { term.initializeNew() } + for ((field, value) in fields) { + val fieldTerm = term.field(field.second, field.first) + append(value.collectInitializerState(set)) + state { fieldTerm.initialize(value.term) } + } + } + } + override fun concretize( cm: ClassManager, accessLevel: AccessModifier, @@ -483,6 +534,16 @@ class ArrayDescriptor(val elementType: KexType, val length: Int) : } } + override fun collectInitializerState(set: MutableSet): PredicateState { + if (this in set) return emptyState() + set += this + return basic { + val fullElements = (0 until length).map { elements[it] ?: descriptor { default(elementType) } } + fullElements.forEach { append(it.collectInitializerState(set)) } + state { term.initializeNew(length, fullElements.map { it.term }) } + } + } + override fun concretize( cm: ClassManager, diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt index 5445f440a..cc75aba54 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncChecker.kt @@ -31,6 +31,7 @@ import org.vorpal.research.kex.state.transformer.Optimizer import org.vorpal.research.kex.state.transformer.RecursiveInliner import org.vorpal.research.kex.state.transformer.ReflectionInfoAdapter import org.vorpal.research.kex.state.transformer.Slicer +import org.vorpal.research.kex.state.transformer.StaticFieldWDescriptorInliner import org.vorpal.research.kex.state.transformer.StensgaardAA import org.vorpal.research.kex.state.transformer.StringMethodAdapter import org.vorpal.research.kex.state.transformer.TermCollector @@ -101,6 +102,7 @@ class AsyncChecker( +BoolTypeAdapter(method.cm.type) +ClassMethodAdapter(method.cm) +ConstEnumAdapter(ctx) + +StaticFieldWDescriptorInliner(ctx) +ConstStringAdapter(method.cm.type) +StringMethodAdapter(ctx.cm) +ConcolicArrayLengthAdapter() diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt index cd7b68a51..70b475c2d 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/AsyncIncrementalChecker.kt @@ -24,6 +24,7 @@ import org.vorpal.research.kex.state.transformer.KexRtAdapter import org.vorpal.research.kex.state.transformer.NewFieldInitializer import org.vorpal.research.kex.state.transformer.Optimizer import org.vorpal.research.kex.state.transformer.RecursiveInliner +import org.vorpal.research.kex.state.transformer.StaticFieldWDescriptorInliner import org.vorpal.research.kex.state.transformer.StringMethodAdapter import org.vorpal.research.kex.state.transformer.TypeInfoMap import org.vorpal.research.kex.state.transformer.TypeNameAdapter @@ -84,6 +85,7 @@ class AsyncIncrementalChecker( +BoolTypeAdapter(method.cm.type) +ClassMethodAdapter(method.cm) +ConstEnumAdapter(ctx) + +StaticFieldWDescriptorInliner(ctx) +ConstStringAdapter(method.cm.type) +StringMethodAdapter(ctx.cm) +ConcolicArrayLengthAdapter() diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt index 8abb5570e..ef0e4f82b 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt @@ -6,16 +6,23 @@ import org.vorpal.research.kex.asm.state.PredicateStateAnalysis import org.vorpal.research.kex.config.kexConfig import org.vorpal.research.kex.descriptor.ClassDescriptor import org.vorpal.research.kex.descriptor.Descriptor +import org.vorpal.research.kex.descriptor.Object2DescriptorConverter import org.vorpal.research.kex.descriptor.descriptor import org.vorpal.research.kex.ktype.kexType import org.vorpal.research.kex.smt.Checker import org.vorpal.research.kex.smt.Result +import org.vorpal.research.kex.state.IncrementalPredicateState import org.vorpal.research.kex.state.PredicateState import org.vorpal.research.kex.state.StateBuilder +import org.vorpal.research.kex.state.predicate.state import org.vorpal.research.kex.state.term.FieldLoadTerm import org.vorpal.research.kex.state.term.FieldTerm import org.vorpal.research.kex.state.term.Term import org.vorpal.research.kex.util.KfgTargetFilter +import org.vorpal.research.kex.util.allFields +import org.vorpal.research.kex.util.isFinal +import org.vorpal.research.kex.util.isStatic +import org.vorpal.research.kex.util.loadClass import org.vorpal.research.kfg.ir.Class import org.vorpal.research.kfg.ir.Field import org.vorpal.research.kfg.ir.Method @@ -160,3 +167,67 @@ class StaticFieldInliner( ps } } + + +class StaticFieldWDescriptorInliner( + val ctx: ExecutionContext +) : RecollectingTransformer, IncrementalTransformer { + override val builders = dequeOf(StateBuilder()) + + companion object { + private val objectConverter = Object2DescriptorConverter() + private val staticFields = mutableMapOf>() + + private fun getStaticField(ctx: ExecutionContext, field: Field): Descriptor? = when (field.klass) { + in staticFields -> staticFields[field.klass]!![field.name] + else -> { + val loadedKlass = ctx.loader.loadClass(field.klass) + val fields = mutableMapOf() + staticFields[field.klass] = fields + for (fieldReflection in loadedKlass.allFields) { + if (fieldReflection.isStatic && fieldReflection.isFinal) { + fields[fieldReflection.name] = tryOrNull { + objectConverter.convert(fieldReflection.get(null)) + } ?: continue + } + } + fields[field.name] + } + } + } + + override fun apply(ps: PredicateState): PredicateState = `try` { + val staticFields = TermCollector.getFullTermSet(ps) + .asSequence() + .filterIsInstance() + .mapNotNullTo(mutableSetOf()) { + val field = it.field as FieldTerm + tryOrNull { field.unmappedKfgField(ctx.cm) }?.let { kfgField -> + if (kfgField.isStatic && kfgField.isFinal) { + kfgField + } else { + null + } + } + } + .filterNotTo(mutableSetOf()) { field -> ignores.any { filter -> filter.matches(field.klass) } } + for (field in staticFields) { + val descriptor = getStaticField(ctx, field) ?: continue + currentBuilder += descriptor.initializerState + currentBuilder += state { + staticRef(field.klass).field(field.type.kexType, field.name).initialize(descriptor.term) + } + } + super.apply(ps) + }.getOrElse { + log.error("Failed to inline static fields in $ps") + ps + } + + override fun apply(state: IncrementalPredicateState): IncrementalPredicateState { + return IncrementalPredicateState( + apply(state.state), + state.queries + ) + } +} From 4769325c77f003acc2baafe8c3b649b9749b5973 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Wed, 3 Jan 2024 16:55:55 +0100 Subject: [PATCH 8/9] m --- .../research/kex/state/transformer/StaticFieldInliner.kt | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt index ef0e4f82b..380f6887c 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/state/transformer/StaticFieldInliner.kt @@ -26,6 +26,7 @@ import org.vorpal.research.kex.util.loadClass import org.vorpal.research.kfg.ir.Class import org.vorpal.research.kfg.ir.Field import org.vorpal.research.kfg.ir.Method +import org.vorpal.research.kfg.type.ClassType import org.vorpal.research.kthelper.collection.dequeOf import org.vorpal.research.kthelper.logging.log import org.vorpal.research.kthelper.`try` @@ -196,6 +197,8 @@ class StaticFieldWDescriptorInliner( } } + private val Term.isEnum get() = (this.type.getKfgType(ctx.cm.type) as? ClassType)?.klass?.isEnum ?: false + override fun apply(ps: PredicateState): PredicateState = `try` { val staticFields = TermCollector.getFullTermSet(ps) .asSequence() @@ -203,7 +206,7 @@ class StaticFieldWDescriptorInliner( .mapNotNullTo(mutableSetOf()) { val field = it.field as FieldTerm tryOrNull { field.unmappedKfgField(ctx.cm) }?.let { kfgField -> - if (kfgField.isStatic && kfgField.isFinal) { + if (kfgField.isStatic && kfgField.isFinal && !field.isEnum) { kfgField } else { null From 206ce3c506bae0995ed6b17b5c003730061af974 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Tue, 9 Jan 2024 09:27:28 +0100 Subject: [PATCH 9/9] working version of coverage guided selector --- .../concolic/coverage/ExecutionGraph.kt | 106 +++------------ .../concolic/coverage/InstructionGraph.kt | 127 +++++++++++------- kex-test.ini | 2 +- 3 files changed, 98 insertions(+), 137 deletions(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt index b026b3326..fccde853b 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/ExecutionGraph.kt @@ -1,6 +1,5 @@ package org.vorpal.research.kex.asm.analysis.concolic.coverage -import com.jetbrains.rd.util.concurrentMapOf import kotlinx.collections.immutable.PersistentList import kotlinx.collections.immutable.toPersistentList import org.vorpal.research.kex.ExecutionContext @@ -50,11 +49,10 @@ import org.vorpal.research.kthelper.graph.GraphView import org.vorpal.research.kthelper.graph.PredecessorGraph import org.vorpal.research.kthelper.graph.Viewable import org.vorpal.research.kthelper.logging.log -import java.util.* import kotlin.math.exp import kotlin.math.pow -private fun Predicate.reverseBoolCond() = when (this) { +fun Predicate.reverseBoolCond() = when (this) { is EqualityPredicate -> predicate(this.type, this.location) { lhv equality !(rhv as ConstBoolTerm).value } @@ -66,7 +64,7 @@ private fun Predicate.reverseBoolCond() = when (this) { else -> unreachable { log.error("Unexpected predicate in bool cond: $this") } } -private fun Predicate.reverseSwitchCond( +fun Predicate.reverseSwitchCond( predecessors: Set, branches: Map ): List = when (this) { @@ -146,12 +144,11 @@ class StateVertex( ) : Vertex(STATE, instruction) class PathVertex( - val pathType: PathClauseType, + pathType: PathClauseType, instruction: Instruction ) : Vertex(pathType.name, instruction) { - val states = hashMapOf>() - private val visitedPrefixes = - hashSetOf()//Collections.newSetFromMap(concurrentMapOf()) + private val states = hashMapOf>() + private val visitedPrefixes = hashSetOf() fun addStateAndProduceCandidates( ctx: ExecutionContext, @@ -234,9 +231,10 @@ private fun PersistentSymbolicState.findExceptionHandlerInst( stateStackTrace: PersistentList> ): Instruction? { val currentClause = path.last() - val stackTrace = listOf(currentClause.instruction) + stateStackTrace.mapNotNull { it.first } + val stackTrace = stateStackTrace.mapNotNullTo(mutableListOf()) { it.first } + stackTrace.add(currentClause.instruction) var result: Instruction? = null - stackTrace@ for (inst in stackTrace) { + stackTrace@ for (inst in stackTrace.asReversed()) { for (handler in inst.parent.handlers) { if (type.isSubtypeOfCached(handler.exception)) { result = handler.first() @@ -349,9 +347,10 @@ class CandidateState( } +// TODO: add concurrency support class ExecutionGraph( val ctx: ExecutionContext, - val targets: Set + private val targets: Set ) : PredecessorGraph, Viewable { companion object { @@ -360,10 +359,10 @@ class ExecutionGraph( } private val root: Vertex = StateVertex(ctx.cm.instruction.getUnreachable(EmptyUsageContext)) - private val innerNodes = concurrentMapOf, Vertex>().also { + private val innerNodes = hashMapOf, Vertex>().also { it["STATE" to root.instruction] = root } - + private val instructionGraph = InstructionGraph(targets) val candidates = CandidateSet(ctx) override val entry: Vertex @@ -372,12 +371,10 @@ class ExecutionGraph( override val nodes: Set get() = innerNodes.values.toSet() - val instructionGraph = InstructionGraph() - inner class CandidateSet(val ctx: ExecutionContext) : Iterable { private var isValid = false private var totalScore: Long = 0L - private val candidates = Collections.newSetFromMap(concurrentMapOf()) + private val candidates = hashSetOf() override fun iterator(): Iterator = candidates.iterator() @@ -391,9 +388,6 @@ class ExecutionGraph( private fun remove(candidateState: CandidateState) { if (candidates.remove(candidateState)) { totalScore -= candidateState.score - if (totalScore < 0L) { - val a = 10 - } } } @@ -429,16 +423,6 @@ class ExecutionGraph( } } - val coverageAll = mutableSetOf() - - private val targetDistances = mutableMapOf() - private val scaledTargetDistances = mutableMapOf() - - private val uncoveredDistances = mutableMapOf() - private val scaledUncoveredDistances = mutableMapOf() - private val scores = mutableMapOf() - private val coverage = mutableMapOf>() - private fun CandidateState.recomputeScore() { var newScore = 0L if (nextInstruction != null) { @@ -449,72 +433,16 @@ class ExecutionGraph( (normalizedDistance * DEFAULT_SCORE).toLong() } - val (targetDistance, uncoveredDistance) = instructionGraph.getVertex(nextInstruction) + val (targetDistance, _) = instructionGraph.getVertex(nextInstruction) .distanceToUncovered(targets, stackTrace) newScore += scaleDistance(targetDistance) - newScore += scaleDistance(uncoveredDistance) / 10L - -// targetDistances[this] = targetDistance -// scaledTargetDistances[this] = scaleDistance(targetDistance) -// uncoveredDistances[this] = uncoveredDistance -// scaledUncoveredDistances[this] = scaleDistance(uncoveredDistance) / 10L -// scores[this] = score -// coverage[this] = coverageAll.toSet() +// newScore += scaleDistance(uncoveredDistance) / 10L } score = newScore } - fun evaluatePerformance(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) { - val overallCoverageIncrease = executionResult.trace.count { !instructionGraph.getVertex(it).covered } - val targetCoverageIncrease = executionResult.trace.filter { it.parent.method in targets } - .count { !instructionGraph.getVertex(it).covered } - - val oldCoverage = coverage[candidate] ?: emptySet() - val oldCoverageIncrease = executionResult.trace.count { it !in oldCoverage } - val nextInstWasCovered = candidate?.nextInstruction?.let { it in oldCoverage } ?: false - val nextInstNowCovered = candidate?.nextInstruction?.let { it in executionResult.trace } ?: false - - - val relativeOverallCoverageIncrease = overallCoverageIncrease.toDouble() / instructionGraph.covered - val relativeTargetCoverageIncrease = - targetCoverageIncrease.toDouble() / targets.flatMap { it.body.bodyBlocks.flatMap { it.instructions } } - .count { instructionGraph.getVertex(it).covered } - - val inLoop = candidate?.nextInstruction?.let { inst -> - val loopInfo = inst.parent.method.getLoopInfo() - loopInfo.count { inst.parent in it.body } - } ?: 0 - - if (candidate?.state?.path?.lastOrNull()?.type != null - && targetDistances[candidate] == 0 && overallCoverageIncrease == 0) { - val a = 10 - } - - log.debug( - "COVERAGE STATS *" + - "${method}\t" + - "${candidate?.state?.path?.lastOrNull()}\t" + - "${targetDistances[candidate] ?: Int.MAX_VALUE}\t" + - "${scaledTargetDistances[candidate] ?: DEFAULT_SCORE}\t" + - "${uncoveredDistances[candidate] ?: Int.MAX_VALUE}\t" + - "${scaledUncoveredDistances[candidate] ?: DEFAULT_SCORE}\t" + - "${scores[candidate] ?: 0.0}\t" + - "${candidate?.state?.path?.last()?.type}\t" + - "${candidate?.nextInstruction?.javaClass}\t" + - "${inLoop}\t" + - "${overallCoverageIncrease}\t" + - "${targetCoverageIncrease}\t" + - "${relativeOverallCoverageIncrease}\t" + - "${relativeTargetCoverageIncrease}\t" + - "${oldCoverageIncrease}\t" + - "${nextInstWasCovered}\t" + - "${nextInstNowCovered}\t" - ) - } - + @Suppress("UNUSED_PARAMETER") fun addTrace(method: Method, candidate: CandidateState?, executionResult: ExecutionCompletedResult) { -// evaluatePerformance(method, candidate, executionResult) -// coverageAll += executionResult.trace instructionGraph.addTrace(executionResult.trace) var prevVertex = root var clauseIndex = 0 @@ -563,7 +491,7 @@ class ExecutionGraph( if (clause is PathClause) { currentVertex as PathVertex - val currentStackTrace = stackTrace.reversed().toPersistentList() + val currentStackTrace = stackTrace.toPersistentList() candidates.addAll( currentVertex.addStateAndProduceCandidates( diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt index 9de79b4ed..52e5be1b8 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/coverage/InstructionGraph.kt @@ -2,23 +2,35 @@ package org.vorpal.research.kex.asm.analysis.concolic.coverage import info.leadinglight.jdot.enums.Color import kotlinx.collections.immutable.PersistentList +import org.vorpal.research.kex.asm.manager.instantiationManager +import org.vorpal.research.kex.asm.util.AccessModifier +import org.vorpal.research.kex.ktype.KexRtManager.isKexRt +import org.vorpal.research.kex.ktype.KexRtManager.rtMapped +import org.vorpal.research.kex.ktype.KexRtManager.rtUnmapped import org.vorpal.research.kfg.ir.BasicBlock import org.vorpal.research.kfg.ir.Method import org.vorpal.research.kfg.ir.value.instruction.ArrayLoadInst import org.vorpal.research.kfg.ir.value.instruction.ArrayStoreInst import org.vorpal.research.kfg.ir.value.instruction.BranchInst import org.vorpal.research.kfg.ir.value.instruction.CallInst +import org.vorpal.research.kfg.ir.value.instruction.CallOpcode import org.vorpal.research.kfg.ir.value.instruction.FieldLoadInst import org.vorpal.research.kfg.ir.value.instruction.FieldStoreInst import org.vorpal.research.kfg.ir.value.instruction.Instruction import org.vorpal.research.kfg.ir.value.instruction.ReturnInst +import org.vorpal.research.kfg.ir.value.instruction.TerminateInst import org.vorpal.research.kthelper.assert.ktassert +import org.vorpal.research.kthelper.collection.mapToArray import org.vorpal.research.kthelper.collection.queueOf import org.vorpal.research.kthelper.graph.GraphView import org.vorpal.research.kthelper.graph.Viewable +import org.vorpal.research.kthelper.tryOrNull -class InstructionGraph : Viewable { +@Suppress("MemberVisibilityCanBePrivate") +class InstructionGraph( + val targets: Set +) : Viewable { private val nodes = mutableMapOf() var covered = 0 @@ -108,38 +120,6 @@ class InstructionGraph : Viewable { } } } -// object : Viewable { -// override val graphView: List -// get() { -// val graphNodes = mutableMapOf() -// -// var i = 0 -// for (vertex in nodes.values) { -// graphNodes[vertex] = GraphView("${i++}", "$vertex".replace("\"", "\\\"")) { -// val color = when { -// vertex == this@Vertex -> Color.X11.blue -// vertex.instruction.parent.method in targets -> when { -// vertex.covered -> Color.X11.green -// else -> Color.X11.red -// } -// else -> Color.X11.black -// } -// it.setColor(color) -// } -// } -// -// for (vertex in nodes.values) { -// val current = graphNodes.getValue(vertex) -// for (child in vertex.downEdges) { -// current.addSuccessor(graphNodes.getValue(child)) { -// it.setLabel(distances[child]?.toString() ?: "") -// } -// } -// } -// -// return graphNodes.values.toList() -// } -// }.view() return minTargetDistance to minUncoveredDistance } } @@ -151,23 +131,76 @@ class InstructionGraph : Viewable { val method = instruction.parent.method ktassert(instruction == method.body.entry.first()) - val queue = queueOf>() - queue += null to method.body.entry - queue.addAll(method.body.catchEntries.map { null to it }) - val visited = mutableSetOf>() + val queue = queueOf>() + queue += Triple(null, method.body.entry, 0) + queue.addAll(method.body.catchEntries.map { Triple(null, it, 0) }) + val visited = mutableSetOf>() + val resolves = mutableMapOf>() + while (queue.isNotEmpty()) { - var (prev, block) = queue.poll() - if (prev?.instruction to block in visited) continue - visited += prev?.instruction to block - - for (inst in block) { - val vertex = nodes.getOrPut(inst) { Vertex(inst) } - prev?.linkDown(vertex) - prev = vertex - } + val (prev, block, index) = queue.poll() + val current = block.instructions[index] + if (prev?.instruction to current in visited) continue + visited += prev?.instruction to current + + val vertex = nodes.getOrPut(current) { Vertex(current) } + prev?.linkDown(vertex) + + when (current) { + is CallInst -> { + val resolvedMethods = resolves.getOrPut(current) { + when (current.opcode) { + CallOpcode.STATIC -> listOf(current.method) + CallOpcode.SPECIAL -> listOf(current.method) + CallOpcode.INTERFACE, CallOpcode.VIRTUAL -> { + val currentMethod = current.method + + val targetPackages = targets.map { it.klass.pkg }.toSet() + + val retTypeMapped = currentMethod.returnType.rtMapped + val argTypesMapped = currentMethod.argTypes.mapToArray { it.rtMapped } + val retTypeUnmapped = currentMethod.returnType.rtUnmapped + val argTypesUnmapped = currentMethod.argTypes.mapToArray { it.rtUnmapped } + instantiationManager.getAllConcreteSubtypes( + currentMethod.klass, + AccessModifier.Private + ) + .filter { klass -> targetPackages.any { it.isParent(klass.pkg) } } + .mapNotNullTo(mutableSetOf()) { + tryOrNull { + if (it.isKexRt) { + it.getMethod(currentMethod.name, retTypeMapped, *argTypesMapped) + } else { + it.getMethod(currentMethod.name, retTypeUnmapped, *argTypesUnmapped) + } + } + } + .filter { it.hasBody } + } + }.filter { it.hasBody } + } + for (candidate in resolvedMethods) { + queue += Triple(vertex, candidate.body.entry, 0) + queue.addAll(candidate.body.catchEntries.map { Triple(null, it, 0) }) - queue.addAll(block.successors.map { prev to it }) + candidate.body.flatten().filterIsInstance().forEach { + val returnVertex = nodes.getOrPut(it) { Vertex(it) } + queue += Triple(returnVertex, block, index + 1) + } + } + if (resolvedMethods.isEmpty()) { + queue += Triple(vertex, block, index + 1) + } + } + + is TerminateInst -> current.successors.forEach { + queue += Triple(vertex, it, 0) + } + + else -> queue += Triple(vertex, block, index + 1) + } } + return nodes.getOrPut(instruction) { Vertex(instruction) } } } diff --git a/kex-test.ini b/kex-test.ini index 33efafbe2..131d89212 100644 --- a/kex-test.ini +++ b/kex-test.ini @@ -63,7 +63,7 @@ numberOfConcreteMethods = 5 [concolic] timeLimit = 300 numberOfExecutors = 1 -searchStrategy = cgs +searchStrategy = coverage [crash] timeLimit = 100