From 76e6a76dd02bd16aaefb48c1aeb6a9a529df2a67 Mon Sep 17 00:00:00 2001 From: ravsemirnov Date: Thu, 4 Jan 2024 11:47:51 +0100 Subject: [PATCH 1/5] implemented n-subpaths path selector for symbolic executor --- .../symbolic/InstructionSymbolicChecker.kt | 3 +- .../analysis/symbolic/SymbolicPathSelector.kt | 40 +++++++++++++++++++ 2 files changed, 42 insertions(+), 1 deletion(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt index 634a0b8ad..83f703d5e 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt @@ -17,7 +17,8 @@ class InstructionSymbolicChecker( ctx: ExecutionContext, rootMethod: Method, ) : SymbolicTraverser(ctx, rootMethod) { - override val pathSelector: SymbolicPathSelector = DequePathSelector() + override val pathSelector: SymbolicPathSelector = NSubpathPathSelector(2) +// override val pathSelector: SymbolicPathSelector = DequePathSelector() override val callResolver: SymbolicCallResolver = DefaultCallResolver(ctx) override val invokeDynamicResolver: SymbolicInvokeDynamicResolver = DefaultCallResolver(ctx) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt index 80a31ace0..dd166d8a6 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt @@ -3,6 +3,7 @@ package org.vorpal.research.kex.asm.analysis.symbolic import org.vorpal.research.kex.asm.analysis.util.SuspendableIterator import org.vorpal.research.kfg.ir.BasicBlock import org.vorpal.research.kthelper.collection.queueOf +import kotlin.math.min interface SymbolicPathSelector : SuspendableIterator> { suspend fun add(state: TraverserState, block: BasicBlock) @@ -21,3 +22,42 @@ class DequePathSelector : SymbolicPathSelector { override suspend fun next(): Pair = queue.poll() } + +class NSubpathPathSelector(val n: Int = 2) : SymbolicPathSelector { + private val eSVector = mutableSetOf() + private val p = mutableMapOf, Int>() + + override suspend fun add(state: TraverserState, block: BasicBlock) { + val newState = ExecutionState(state to block, n) + eSVector.add(newState) + if (p[newState.path] == null) { + p[newState.path] = 0 + } + } + + override suspend fun hasNext(): Boolean = eSVector.isNotEmpty() + + override suspend fun next(): Pair { + var minPath = Int.MAX_VALUE + eSVector.forEach { minPath = min(minPath, p[it.path]!!) } + val selectSet = mutableSetOf() + + for (elem in eSVector) { + if (p[elem.path] == minPath) { + selectSet.add(elem) + } + } + + val result = selectSet.random() + p[result.path] = p[result.path]!! + 1 + eSVector.remove(result) + return result.node + } + + class ExecutionState( + val node: Pair, + pathLength: Int + ) { + val path: List = node.first.blockPath.takeLast(pathLength) + } +} From 76f9e0dee60a9816d87633144841917e6a554798 Mon Sep 17 00:00:00 2001 From: ravsemirnov Date: Mon, 11 Mar 2024 10:07:15 +0100 Subject: [PATCH 2/5] new Path Selectors and add of path selector choice in kek.ini. --- .../symbolic/InstructionSymbolicChecker.kt | 15 +++- .../analysis/symbolic/SymbolicPathSelector.kt | 84 +++++++++++++++++-- kex.ini | 5 +- 3 files changed, 94 insertions(+), 10 deletions(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt index 83f703d5e..9fea4da11 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt @@ -17,11 +17,22 @@ class InstructionSymbolicChecker( ctx: ExecutionContext, rootMethod: Method, ) : SymbolicTraverser(ctx, rootMethod) { - override val pathSelector: SymbolicPathSelector = NSubpathPathSelector(2) -// override val pathSelector: SymbolicPathSelector = DequePathSelector() + override val pathSelector: SymbolicPathSelector override val callResolver: SymbolicCallResolver = DefaultCallResolver(ctx) override val invokeDynamicResolver: SymbolicInvokeDynamicResolver = DefaultCallResolver(ctx) + init { + val pathSelectorName: String = kexConfig.getStringValue("kex", "pathSelector", "NSubpathPathSelector") + val n: Int = kexConfig.getIntValue("kex", "nPathSelectorArg", 2) + pathSelector = when (pathSelectorName) { + "DequePathSelector" -> DequePathSelector() + "NSubpathPathSelector" -> NSubpathPathSelector(n) + "PriorityDequePathSelector" -> PriorityDequePathSelector(n) + else -> throw IllegalArgumentException("PathSelector '$pathSelectorName' doesn't exist. " + + "Check InstructionSymbolicChecker to see available path selectors") + } + } + companion object { @ExperimentalTime @DelicateCoroutinesApi diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt index dd166d8a6..d7bae993f 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt @@ -1,8 +1,11 @@ package org.vorpal.research.kex.asm.analysis.symbolic +import kotlinx.coroutines.Dispatchers +import kotlinx.coroutines.withContext import org.vorpal.research.kex.asm.analysis.util.SuspendableIterator import org.vorpal.research.kfg.ir.BasicBlock import org.vorpal.research.kthelper.collection.queueOf +import java.io.File import kotlin.math.min interface SymbolicPathSelector : SuspendableIterator> { @@ -11,11 +14,25 @@ interface SymbolicPathSelector : SuspendableIterator) = add(data.first, data.second) } +/** + * Implements bfs algorithm + */ class DequePathSelector : SymbolicPathSelector { private val queue = queueOf>() + init { + val file = File("/Users/ravsemirnov/Desktop/JetBrains/projects/kex/checkPathSelector.txt") + val writer = file.bufferedWriter() + writer.write("I USE DequePathSelector") + } + override suspend fun add(state: TraverserState, block: BasicBlock) { queue += state to block + val file = File("/Users/ravsemirnov/Desktop/JetBrains/projects/kex/checkPathSelector.txt") + val writer = file.bufferedWriter() + withContext(Dispatchers.IO) { + writer.write("I USE DequePathSelector") + } } override suspend fun hasNext(): Boolean = queue.isNotEmpty() @@ -23,15 +40,24 @@ class DequePathSelector : SymbolicPathSelector { override suspend fun next(): Pair = queue.poll() } +/** + * Implements n-subpath algorithm, which makes path decisions based on the frequency of visits to paths of length n + */ class NSubpathPathSelector(val n: Int = 2) : SymbolicPathSelector { private val eSVector = mutableSetOf() - private val p = mutableMapOf, Int>() + private val pathVisits = mutableMapOf, Int>() + + init { + val file = File("/Users/ravsemirnov/Desktop/JetBrains/projects/kex/checkPathSelector.txt") + val writer = file.bufferedWriter() + writer.write("I USE NSubpathPathSelector") + } override suspend fun add(state: TraverserState, block: BasicBlock) { val newState = ExecutionState(state to block, n) eSVector.add(newState) - if (p[newState.path] == null) { - p[newState.path] = 0 + if (pathVisits[newState.path] == null) { + pathVisits[newState.path] = 0 } } @@ -39,17 +65,17 @@ class NSubpathPathSelector(val n: Int = 2) : SymbolicPathSelector { override suspend fun next(): Pair { var minPath = Int.MAX_VALUE - eSVector.forEach { minPath = min(minPath, p[it.path]!!) } + eSVector.forEach { minPath = min(minPath, pathVisits[it.path]!!) } val selectSet = mutableSetOf() for (elem in eSVector) { - if (p[elem.path] == minPath) { + if (pathVisits[elem.path] == minPath) { selectSet.add(elem) } } val result = selectSet.random() - p[result.path] = p[result.path]!! + 1 + pathVisits[result.path] = pathVisits[result.path]!! + 1 eSVector.remove(result) return result.node } @@ -61,3 +87,49 @@ class NSubpathPathSelector(val n: Int = 2) : SymbolicPathSelector { val path: List = node.first.blockPath.takeLast(pathLength) } } + +/** + * Implements bfs algorithm, which takes into account frequency of visits to paths of length n from n-subpath + */ +class PriorityDequePathSelector(val n: Int = 2) : SymbolicPathSelector { + private val eSVector = mutableSetOf() + private val p = mutableMapOf, Int>() + + init { + val file = File("/Users/ravsemirnov/Desktop/JetBrains/projects/kex/checkPathSelector.txt") + val writer = file.bufferedWriter() + writer.write("I USE PriorityDequePathSelector") + } + + override suspend fun add(state: TraverserState, block: BasicBlock) { + val newState = ExecutionState(state to block, n) + eSVector.add(newState) + if (p[newState.path] == null) { + p[newState.path] = 0 + } + } + + override suspend fun hasNext(): Boolean = eSVector.isNotEmpty() + + override suspend fun next(): Pair { + val minLen = eSVector.minOf { it.path.size } + val filteredESVector = eSVector.filter { it.path.size == minLen } + + var minPath = Int.MAX_VALUE + filteredESVector.forEach { minPath = min(minPath, p[it.path]!!) } + val filteredESVector2 = filteredESVector.filter { p[it.path] == minPath } + + val result = filteredESVector2.random() + + p[result.path] = p[result.path]!! + 1 + eSVector.remove(result) + return result.node + } + + class ExecutionState( + val node: Pair, + pathLength: Int + ) { + val path: List = node.first.blockPath.takeLast(pathLength) + } +} \ No newline at end of file diff --git a/kex.ini b/kex.ini index 852d015f7..9dc53912b 100644 --- a/kex.ini +++ b/kex.ini @@ -13,6 +13,7 @@ computeCoverage = true computeSaturationCoverage = false printDetailedCoverage = true useReflectionInfo = false +pathSelector = NSubpathPathSelector [compile] enabled = true @@ -123,8 +124,8 @@ simplifyFormulae = false [ksmt] solver = z3 -solver = cvc5 -solver = bitwuzla +; solver = cvc5 +; solver = bitwuzla ; solver = yices runners = 1 seed = 42 From 029c7202523f7a52dfce58f1d53e3bb228a183f6 Mon Sep 17 00:00:00 2001 From: ravsemirnov Date: Mon, 11 Mar 2024 10:30:16 +0100 Subject: [PATCH 3/5] small fixes / delete of redundant code --- .../analysis/symbolic/SymbolicPathSelector.kt | 26 ------------------- 1 file changed, 26 deletions(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt index d7bae993f..24dbd081d 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt @@ -1,11 +1,8 @@ package org.vorpal.research.kex.asm.analysis.symbolic -import kotlinx.coroutines.Dispatchers -import kotlinx.coroutines.withContext import org.vorpal.research.kex.asm.analysis.util.SuspendableIterator import org.vorpal.research.kfg.ir.BasicBlock import org.vorpal.research.kthelper.collection.queueOf -import java.io.File import kotlin.math.min interface SymbolicPathSelector : SuspendableIterator> { @@ -20,19 +17,8 @@ interface SymbolicPathSelector : SuspendableIterator>() - init { - val file = File("/Users/ravsemirnov/Desktop/JetBrains/projects/kex/checkPathSelector.txt") - val writer = file.bufferedWriter() - writer.write("I USE DequePathSelector") - } - override suspend fun add(state: TraverserState, block: BasicBlock) { queue += state to block - val file = File("/Users/ravsemirnov/Desktop/JetBrains/projects/kex/checkPathSelector.txt") - val writer = file.bufferedWriter() - withContext(Dispatchers.IO) { - writer.write("I USE DequePathSelector") - } } override suspend fun hasNext(): Boolean = queue.isNotEmpty() @@ -47,12 +33,6 @@ class NSubpathPathSelector(val n: Int = 2) : SymbolicPathSelector { private val eSVector = mutableSetOf() private val pathVisits = mutableMapOf, Int>() - init { - val file = File("/Users/ravsemirnov/Desktop/JetBrains/projects/kex/checkPathSelector.txt") - val writer = file.bufferedWriter() - writer.write("I USE NSubpathPathSelector") - } - override suspend fun add(state: TraverserState, block: BasicBlock) { val newState = ExecutionState(state to block, n) eSVector.add(newState) @@ -95,12 +75,6 @@ class PriorityDequePathSelector(val n: Int = 2) : SymbolicPathSelector { private val eSVector = mutableSetOf() private val p = mutableMapOf, Int>() - init { - val file = File("/Users/ravsemirnov/Desktop/JetBrains/projects/kex/checkPathSelector.txt") - val writer = file.bufferedWriter() - writer.write("I USE PriorityDequePathSelector") - } - override suspend fun add(state: TraverserState, block: BasicBlock) { val newState = ExecutionState(state to block, n) eSVector.add(newState) From 55bfaf8cd8a17c25e51dc9a292e095e51780e8ac Mon Sep 17 00:00:00 2001 From: ravsemirnov Date: Thu, 4 Apr 2024 15:43:23 +0200 Subject: [PATCH 4/5] style fixes, renaming --- .../symbolic/InstructionSymbolicChecker.kt | 10 +++++----- .../asm/analysis/symbolic/SymbolicPathSelector.kt | 14 ++++++-------- kex.ini | 2 +- 3 files changed, 12 insertions(+), 14 deletions(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt index 9fea4da11..7e29b6e93 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt @@ -22,12 +22,12 @@ class InstructionSymbolicChecker( override val invokeDynamicResolver: SymbolicInvokeDynamicResolver = DefaultCallResolver(ctx) init { - val pathSelectorName: String = kexConfig.getStringValue("kex", "pathSelector", "NSubpathPathSelector") - val n: Int = kexConfig.getIntValue("kex", "nPathSelectorArg", 2) + val pathSelectorName = kexConfig.getStringValue("symbolic", "pathSelector", "sgs") + val n = kexConfig.getIntValue("symbolic", "n", 2) pathSelector = when (pathSelectorName) { - "DequePathSelector" -> DequePathSelector() - "NSubpathPathSelector" -> NSubpathPathSelector(n) - "PriorityDequePathSelector" -> PriorityDequePathSelector(n) + "bfs" -> BFS() + "sgs" -> SGS(n) + "priority-bfs" -> PriorityBFS(n) else -> throw IllegalArgumentException("PathSelector '$pathSelectorName' doesn't exist. " + "Check InstructionSymbolicChecker to see available path selectors") } diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt index 24dbd081d..328921635 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/SymbolicPathSelector.kt @@ -3,7 +3,6 @@ package org.vorpal.research.kex.asm.analysis.symbolic import org.vorpal.research.kex.asm.analysis.util.SuspendableIterator import org.vorpal.research.kfg.ir.BasicBlock import org.vorpal.research.kthelper.collection.queueOf -import kotlin.math.min interface SymbolicPathSelector : SuspendableIterator> { suspend fun add(state: TraverserState, block: BasicBlock) @@ -14,7 +13,7 @@ interface SymbolicPathSelector : SuspendableIterator>() override suspend fun add(state: TraverserState, block: BasicBlock) { @@ -29,7 +28,7 @@ class DequePathSelector : SymbolicPathSelector { /** * Implements n-subpath algorithm, which makes path decisions based on the frequency of visits to paths of length n */ -class NSubpathPathSelector(val n: Int = 2) : SymbolicPathSelector { +class SGS(val n: Int = 2) : SymbolicPathSelector { private val eSVector = mutableSetOf() private val pathVisits = mutableMapOf, Int>() @@ -44,8 +43,8 @@ class NSubpathPathSelector(val n: Int = 2) : SymbolicPathSelector { override suspend fun hasNext(): Boolean = eSVector.isNotEmpty() override suspend fun next(): Pair { - var minPath = Int.MAX_VALUE - eSVector.forEach { minPath = min(minPath, pathVisits[it.path]!!) } + val minPath = eSVector.minOf { pathVisits[it.path]!! } + val selectSet = mutableSetOf() for (elem in eSVector) { @@ -71,7 +70,7 @@ class NSubpathPathSelector(val n: Int = 2) : SymbolicPathSelector { /** * Implements bfs algorithm, which takes into account frequency of visits to paths of length n from n-subpath */ -class PriorityDequePathSelector(val n: Int = 2) : SymbolicPathSelector { +class PriorityBFS(val n: Int = 2) : SymbolicPathSelector { private val eSVector = mutableSetOf() private val p = mutableMapOf, Int>() @@ -89,8 +88,7 @@ class PriorityDequePathSelector(val n: Int = 2) : SymbolicPathSelector { val minLen = eSVector.minOf { it.path.size } val filteredESVector = eSVector.filter { it.path.size == minLen } - var minPath = Int.MAX_VALUE - filteredESVector.forEach { minPath = min(minPath, p[it.path]!!) } + val minPath = filteredESVector.minOf { p[it.path]!! } val filteredESVector2 = filteredESVector.filter { p[it.path] == minPath } val result = filteredESVector2.random() diff --git a/kex.ini b/kex.ini index 9dc53912b..5120239bf 100644 --- a/kex.ini +++ b/kex.ini @@ -13,7 +13,6 @@ computeCoverage = true computeSaturationCoverage = false printDetailedCoverage = true useReflectionInfo = false -pathSelector = NSubpathPathSelector [compile] enabled = true @@ -74,6 +73,7 @@ exclude = class io.netty.buffer.ByteBuf timeLimit = 120 numberOfExecutors = 8 numberOfConcreteMethods = 3 +pathSelector = sgs [concolic] timeLimit = 120 From 6f055c3871ba9ef11ab92d71c923ae765eb04180 Mon Sep 17 00:00:00 2001 From: ravsemirnov Date: Fri, 26 Apr 2024 13:29:24 +0200 Subject: [PATCH 5/5] set n = 8 as basic, renaming --- .../asm/analysis/symbolic/InstructionSymbolicChecker.kt | 2 +- kex.ini | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt index 7e29b6e93..f78bd7d64 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/symbolic/InstructionSymbolicChecker.kt @@ -22,7 +22,7 @@ class InstructionSymbolicChecker( override val invokeDynamicResolver: SymbolicInvokeDynamicResolver = DefaultCallResolver(ctx) init { - val pathSelectorName = kexConfig.getStringValue("symbolic", "pathSelector", "sgs") + val pathSelectorName = kexConfig.getStringValue("symbolic", "searchStrategy", "sgs") val n = kexConfig.getIntValue("symbolic", "n", 2) pathSelector = when (pathSelectorName) { "bfs" -> BFS() diff --git a/kex.ini b/kex.ini index 2f8efa77a..94ffbfb09 100644 --- a/kex.ini +++ b/kex.ini @@ -74,7 +74,8 @@ exclude = class io.netty.buffer.ByteBuf timeLimit = 120 numberOfExecutors = 8 numberOfConcreteMethods = 3 -pathSelector = sgs +searchStrategy = sgs +n = 8 [concolic] timeLimit = 120 @@ -127,8 +128,8 @@ useADSolver = false [ksmt] solver = z3 -; solver = cvc5 -; solver = bitwuzla +solver = cvc5 +solver = bitwuzla ; solver = yices runners = 1 seed = 42