From df857162bfa8921ae580ab4809561871e32fb0e4 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Thu, 11 Jan 2024 17:49:52 +0100 Subject: [PATCH] small optimizations + add filter to remove number of candidate states --- .../vorpal/research/kex/ktype/KexInteger.kt | 8 +---- .../org/vorpal/research/kex/ktype/KexReal.kt | 12 ------- .../org/vorpal/research/kex/ktype/KexType.kt | 6 ---- .../kex/trace/symbolic/SymbolicState.kt | 31 ++++++++++++++++--- .../concolic/cgs/ContextGuidedSelector.kt | 2 +- .../concolic/coverage/ExecutionGraph.kt | 29 ++++++++++++++--- .../analysis/concolic/gui/GUIProxySelector.kt | 5 +-- 7 files changed, 56 insertions(+), 37 deletions(-) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexInteger.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexInteger.kt index 5761899c7..9a20d670e 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexInteger.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexInteger.kt @@ -7,13 +7,7 @@ import org.vorpal.research.kfg.type.TypeFactory @InheritorOf("KexType") @Serializable -sealed class KexInteger : KexType() { - override fun hashCode() = name.hashCode() - override fun equals(other: Any?): Boolean { - if (this === other) return true - return other?.javaClass == this.javaClass - } -} +sealed class KexInteger : KexType() @InheritorOf("KexType") @Serializable diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexReal.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexReal.kt index d1c9156ca..65bb8bd84 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexReal.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexReal.kt @@ -19,12 +19,6 @@ object KexFloat : KexReal() { get() = WORD override fun getKfgType(types: TypeFactory): Type = types.floatType - - override fun hashCode() = name.hashCode() - override fun equals(other: Any?): Boolean { - if (this === other) return true - return other is KexFloat - } } @InheritorOf("KexType") @@ -37,10 +31,4 @@ object KexDouble : KexReal() { get() = DWORD override fun getKfgType(types: TypeFactory): Type = types.doubleType - - override fun hashCode() = name.hashCode() - override fun equals(other: Any?): Boolean { - if (this === other) return true - return other is KexDouble - } } diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexType.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexType.kt index 33d715072..2893e6aa4 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexType.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/ktype/KexType.kt @@ -307,12 +307,6 @@ object KexVoid : KexType() { get() = throw IllegalAccessError("Trying to get bit size of void") override fun getKfgType(types: TypeFactory): Type = types.voidType - - override fun hashCode() = name.hashCode() - override fun equals(other: Any?): Boolean { - if (this === other) return true - return other is KexVoid - } } fun KexType.unMemspaced() = when (this) { 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 7ee5c8231..592f4ba59 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 @@ -100,6 +100,8 @@ sealed class ClauseList : Iterable { abstract fun subState(startInclusive: Int, endExclusive: Int): ClauseList + open fun subState(endExclusive: Int): ClauseList = subState(0, endExclusive) + abstract operator fun plus(other: ClauseList): ClauseList abstract operator fun plus(other: Clause): ClauseList override fun toString(): String { @@ -171,8 +173,19 @@ data class PersistentClauseList( override fun lastIndexOf(element: Clause): Int = state.lastIndexOf(element) - override fun subState(startInclusive: Int, endExclusive: Int): PersistentClauseList = - PersistentClauseList(state.subList(startInclusive, endExclusive).toPersistentList()) + override fun subState(startInclusive: Int, endExclusive: Int): PersistentClauseList = when (startInclusive) { + 0 -> subState(endExclusive) + else -> PersistentClauseList(state.subList(startInclusive, endExclusive).toPersistentList()) + } + + override fun subState(endExclusive: Int): PersistentClauseList { + var newClauses = state + var index = size - 1 + repeat(size - endExclusive) { + newClauses = newClauses.removeAt(index--) + } + return PersistentClauseList(newClauses) + } override fun subList(fromIndex: Int, toIndex: Int): PersistentList = state.subList(fromIndex, toIndex).toPersistentList() @@ -180,7 +193,7 @@ 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)) + fun dropLast(n: Int): PersistentClauseList = subState(maxOf(0, size - n)) } @Serializable @@ -188,6 +201,7 @@ sealed class PathCondition : Iterable { abstract val path: List override fun iterator(): Iterator = path.iterator() abstract fun subPath(startInclusive: Int, endExclusive: Int): PathCondition + open fun subPath(endExclusive: Int): PathCondition = subPath(0, endExclusive) fun asState() = BasicState(path.map { it.predicate }) abstract operator fun plus(other: PathCondition): PathCondition @@ -265,13 +279,22 @@ data class PersistentPathCondition( subList(startInclusive, endExclusive).toPersistentList() ) + override fun subPath(endExclusive: Int): PersistentPathCondition { + var newPath = path + var index = size - 1 + repeat(size - endExclusive) { + newPath = newPath.removeAt(index--) + } + return PersistentPathCondition(newPath) + } + override fun subList(fromIndex: Int, toIndex: Int): PersistentList = path.subList(fromIndex, toIndex).toPersistentList() 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)) + fun dropLast(n: Int): PersistentPathCondition = subPath(maxOf(0, size - n)) } @Serializable 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 9af59e619..4b67a7e68 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 @@ -94,7 +94,7 @@ class ContextGuidedSelector( val currentStateState = currentState.context.symbolicState val stateSize = currentStateState.clauses.indexOf(currentState.activeClause) - val state = currentStateState.clauses.subState(0, stateSize) + val state = currentStateState.clauses.subState(stateSize) return method to persistentSymbolicState( state, 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 fccde853b..3e24af298 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 @@ -5,6 +5,7 @@ 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 +import org.vorpal.research.kex.config.kexConfig import org.vorpal.research.kex.ktype.KexRtManager.isKexRt import org.vorpal.research.kex.ktype.kexType import org.vorpal.research.kex.state.predicate.DefaultSwitchPredicate @@ -253,6 +254,8 @@ class CandidateState( val nextInstruction: Instruction? var score: Long = 0L + private val hashCode = state.hashCode() + init { val cm = method.cm val currentClause = state.path.last() @@ -342,7 +345,7 @@ class CandidateState( } override fun hashCode(): Int { - return state.hashCode() + return hashCode } } @@ -363,6 +366,8 @@ class ExecutionGraph( it["STATE" to root.instruction] = root } private val instructionGraph = InstructionGraph(targets) + private val maximalCandidateCapacity = kexConfig.getLongValue("concolic", "maximalCandidateCapacity", 50_000L) + val candidates = CandidateSet(ctx) override val entry: Vertex @@ -376,6 +381,8 @@ class ExecutionGraph( private var totalScore: Long = 0L private val candidates = hashSetOf() + val size get() = candidates.size + override fun iterator(): Iterator = candidates.iterator() fun isEmpty() = candidates.isEmpty() @@ -421,6 +428,13 @@ class ExecutionGraph( } return unreachable { log.error("Unexpected error") } } + + fun cleanUnreachables(): Boolean { + if (!isValid) recomputeScores() + return candidates.removeAll { it.score <= 1 }.also { + totalScore = candidates.sumOf { it.score } + } + } } private fun CandidateState.recomputeScore() { @@ -473,8 +487,13 @@ class ExecutionGraph( // candidate states calculation part ++clauseIndex - // TODO: limit number of states -// if (clauseIndex > 10_000) break + + // limit maximum number of states in candidate set + if (candidates.size > maximalCandidateCapacity) { + val cleanupSuccessful = candidates.cleanUnreachables() + if (!cleanupSuccessful) break + } + if (clause is PathClause) ++pathIndex val type = when (clause) { @@ -496,8 +515,8 @@ class ExecutionGraph( candidates.addAll( currentVertex.addStateAndProduceCandidates( ctx, persistentSymbolicState( - symbolicState.clauses.subState(0, clauseIndex), - symbolicState.path.subPath(0, pathIndex), + symbolicState.clauses.subState(clauseIndex), + symbolicState.path.subPath(pathIndex), symbolicState.concreteTypes, symbolicState.concreteValues, symbolicState.termMap 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 5f02557d8..9a242b6b0 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 @@ -16,6 +16,7 @@ import org.vorpal.research.kthelper.logging.log import org.vorpal.research.kthelper.`try` import java.net.ServerSocket +@Suppress("unused") class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) : ConcolicPathSelector { override val ctx = concolicPathSelector.ctx @@ -74,8 +75,8 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) : val state = graph.findStateByPathClause(pathClause) ?: return null val revertedClause = reverse(pathClause) ?: return null - val clauses = state.clauses.subState(0, state.clauses.indexOf(pathClause)) - val path = state.path.subPath(0, state.path.indexOf(pathClause)) + val clauses = state.clauses.subState(state.clauses.indexOf(pathClause)) + val path = state.path.subPath(state.path.indexOf(pathClause)) return persistentSymbolicState( clauses,