From a75f1138948122494831b5ac5c93749522659170 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Mon, 13 Nov 2023 17:20:23 +0100 Subject: [PATCH 1/3] call terms are fresh vars in smt --- kex-annotation-processor/src/main/resources/SMTConverter.vm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kex-annotation-processor/src/main/resources/SMTConverter.vm b/kex-annotation-processor/src/main/resources/SMTConverter.vm index bf29acb48..ead51792d 100644 --- a/kex-annotation-processor/src/main/resources/SMTConverter.vm +++ b/kex-annotation-processor/src/main/resources/SMTConverter.vm @@ -627,7 +627,7 @@ class ${solver}Converter( } fun convert(call: CallTerm, ef: Factory_, ctx: Context_): Dynamic_ { - val expr = ef.getVarByTypeAndName(call.type, call.name) + val expr = ef.getVarByTypeAndName(call.type, call.name, true) return call.withAxioms(expr, ef, ctx) } From fc08d628aef16c9ac76ccebf8a034fc65164b4cf Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Thu, 16 Nov 2023 14:39:31 +0100 Subject: [PATCH 2/3] full instruction trace --- .../trace/symbolic/InstructionTraceCollector.kt | 3 +++ .../kex/trace/symbolic/SymbolicTraceBuilder.kt | 3 +++ .../kex/trace/symbolic/TraceCollectorProxy.kt | 2 ++ .../kex/trace/symbolic/protocol/responce.kt | 10 +++++++--- .../org/vorpal/research/kex/KexExecutor.kt | 17 ++++++++++++++--- .../vorpal/research/kex/worker/TestExecutor.kt | 9 +++++++-- .../analysis/concolic/bfs/BfsPathSelector.kt | 2 +- .../concolic/cgs/ContextGuidedSelector.kt | 3 +-- .../analysis/concolic/gui/GUIProxySelector.kt | 2 +- .../vorpal/research/kex/smt/ModelReanimator.kt | 6 +++--- .../runner/SymbolicExternalTracingRunner.kt | 2 +- 11 files changed, 43 insertions(+), 16 deletions(-) diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/InstructionTraceCollector.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/InstructionTraceCollector.kt index 3bba8c568..46435482e 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/InstructionTraceCollector.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/InstructionTraceCollector.kt @@ -1,6 +1,9 @@ package org.vorpal.research.kex.trace.symbolic +import org.vorpal.research.kfg.ir.value.instruction.Instruction + interface InstructionTraceCollector { + val instructionTrace: List val symbolicState: SymbolicState fun track(value: String, concreteValue: Any?) 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 e7b5f4880..4f89afd34 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 @@ -118,6 +118,9 @@ class SymbolicTraceBuilder( override val termMap: Map get() = terms.toMap() + override val instructionTrace: List + get() = traceBuilder + override val symbolicState: SymbolicState get() { checkCall() diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/TraceCollectorProxy.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/TraceCollectorProxy.kt index 4f890c8c0..dac7e0f55 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/TraceCollectorProxy.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/TraceCollectorProxy.kt @@ -8,6 +8,7 @@ import org.vorpal.research.kex.ktype.KexType import org.vorpal.research.kex.serialization.KexSerializer import org.vorpal.research.kex.state.term.Term import org.vorpal.research.kfg.ir.value.NameMapperContext +import org.vorpal.research.kfg.ir.value.instruction.Instruction import java.nio.file.Path private class EmptyTraceCollector : InstructionTraceCollector { @@ -26,6 +27,7 @@ private class EmptyTraceCollector : InstructionTraceCollector { override fun plus(other: PathCondition): SymbolicState = this } + override val instructionTrace = emptyList() override val symbolicState = EmptyState() override fun track(value: String, concreteValue: Any?) {} diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/protocol/responce.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/protocol/responce.kt index 9b3bf7ddb..131027bec 100644 --- a/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/protocol/responce.kt +++ b/kex-core/src/main/kotlin/org/vorpal/research/kex/trace/symbolic/protocol/responce.kt @@ -4,6 +4,7 @@ import kotlinx.serialization.Contextual import kotlinx.serialization.Serializable import org.vorpal.research.kex.descriptor.Descriptor import org.vorpal.research.kex.trace.symbolic.SymbolicState +import org.vorpal.research.kfg.ir.value.instruction.Instruction @Serializable sealed class ExecutionResult @@ -26,15 +27,18 @@ data class ExecutionTimedOutResult( @Serializable sealed class ExecutionCompletedResult : ExecutionResult() { - abstract val trace: SymbolicState + abstract val symbolicState: SymbolicState + abstract val trace: List } @Serializable data class ExceptionResult( val cause: @Contextual Descriptor, - override val trace: @Contextual SymbolicState + override val trace: List<@Contextual Instruction>, + override val symbolicState: @Contextual SymbolicState ) : ExecutionCompletedResult() @Serializable data class SuccessResult( - override val trace: @Contextual SymbolicState + override val trace: List<@Contextual Instruction>, + override val symbolicState: @Contextual SymbolicState ) : ExecutionCompletedResult() diff --git a/kex-executor/src/main/kotlin/org/vorpal/research/kex/KexExecutor.kt b/kex-executor/src/main/kotlin/org/vorpal/research/kex/KexExecutor.kt index cb47f81b9..dfdaa16b6 100644 --- a/kex-executor/src/main/kotlin/org/vorpal/research/kex/KexExecutor.kt +++ b/kex-executor/src/main/kotlin/org/vorpal/research/kex/KexExecutor.kt @@ -64,7 +64,13 @@ class KexExecutor(args: Array) { } } classManager = ClassManager(KfgConfig(flags = Flags.readAll, failOnError = false, verifyIR = false)) - classManager.initialize(*listOfNotNull(*containers.toTypedArray(), getRuntime(), getIntrinsics()).toTypedArray()) + classManager.initialize( + *listOfNotNull( + *containers.toTypedArray(), + getRuntime(), + getIntrinsics() + ).toTypedArray() + ) } @ExperimentalSerializationApi @@ -105,8 +111,13 @@ class KexExecutor(args: Array) { TraceCollectorProxy.disableCollector() log.debug("Collected state: {}", collector.symbolicState) val result = when { - exception != null -> ExceptionResult(convertToDescriptor(exception), collector.symbolicState) - else -> SuccessResult(collector.symbolicState) + exception != null -> ExceptionResult( + convertToDescriptor(exception), + collector.instructionTrace, + collector.symbolicState + ) + + else -> SuccessResult(collector.instructionTrace, collector.symbolicState) } val jsonString = serializer.toJson(result) output.toFile().writeText(jsonString) diff --git a/kex-executor/src/main/kotlin/org/vorpal/research/kex/worker/TestExecutor.kt b/kex-executor/src/main/kotlin/org/vorpal/research/kex/worker/TestExecutor.kt index 853368b3c..742c4ed2b 100644 --- a/kex-executor/src/main/kotlin/org/vorpal/research/kex/worker/TestExecutor.kt +++ b/kex-executor/src/main/kotlin/org/vorpal/research/kex/worker/TestExecutor.kt @@ -43,8 +43,13 @@ class TestExecutor( TraceCollectorProxy.disableCollector() log.debug("Collected state: {}", collector.symbolicState) return when { - exception != null -> ExceptionResult(convertToDescriptor(exception), collector.symbolicState) - else -> SuccessResult(collector.symbolicState) + exception != null -> ExceptionResult( + convertToDescriptor(exception), + collector.instructionTrace, + collector.symbolicState + ) + + else -> SuccessResult(collector.instructionTrace, collector.symbolicState) } } 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 34cda0c9e..b58be5a80 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 @@ -37,7 +37,7 @@ class BfsPathSelectorImpl( override suspend fun hasNext(): Boolean = deque.isNotEmpty() override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { - val persistentResult = result.trace.toPersistentState() + val persistentResult = result.symbolicState.toPersistentState() if (persistentResult.path in coveredPaths) return coveredPaths += persistentResult.path addCandidates(persistentResult) 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 b4b733b48..c3f134b7b 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 @@ -116,8 +116,7 @@ class ContextGuidedSelector( } override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { - executionTree.addTrace(result.trace.toPersistentState()) -// executionTree.view() + executionTree.addTrace(result.symbolicState.toPersistentState()) } override fun reverse(pathClause: PathClause): PathClause? = pathClause.reversed() 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 49ebf1a7c..4ffa3a7e6 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 @@ -41,7 +41,7 @@ class GUIProxySelector(private val concolicPathSelector: ConcolicPathSelector) : override suspend fun isEmpty(): Boolean = concolicPathSelector.isEmpty() override suspend fun addExecutionTrace(method: Method, result: ExecutionCompletedResult) { - val vertices = graph.addTrace(result.trace.toPersistentState()) + val vertices = graph.addTrace(result.symbolicState.toPersistentState()) val json = Json.encodeToString(vertices) log.debug("Vertices trace: $json") log.debug(graph) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/ModelReanimator.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/ModelReanimator.kt index 16094495a..5f2f7b729 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/ModelReanimator.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/smt/ModelReanimator.kt @@ -141,7 +141,7 @@ class ObjectReanimator( return when (type) { is KexBool -> (value as ConstBoolTerm).value is KexByte -> value.numericValue.toByte() - is KexChar -> value.numericValue.toChar() + is KexChar -> value.numericValue.toInt().toChar() is KexShort -> value.numericValue.toShort() is KexInt -> value.numericValue.toInt() is KexLong -> value.numericValue.toLong() @@ -379,7 +379,7 @@ abstract class DescriptorReanimator( else when (term.type) { is KexBool -> const((value as ConstBoolTerm).value) is KexByte -> const(value.numericValue.toByte()) - is KexChar -> const(value.numericValue.toChar()) + is KexChar -> const(value.numericValue.toInt().toChar()) is KexShort -> const(value.numericValue.toShort()) is KexInt -> const(value.numericValue.toInt()) is KexLong -> const(value.numericValue.toLong()) @@ -579,7 +579,7 @@ abstract class DescriptorReanimator( is KexPointer -> reanimateReferencePointer(term, value) is KexBool -> const(intVal.toBoolean()) is KexByte -> const(intVal.toByte()) - is KexChar -> const(intVal.toChar()) + is KexChar -> const(intVal.toInt().toChar()) is KexShort -> const(intVal.toShort()) is KexInt -> const(intVal) is KexLong -> const(intVal.toLong()) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/trace/runner/SymbolicExternalTracingRunner.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/trace/runner/SymbolicExternalTracingRunner.kt index 6913d2010..48f253d6f 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/trace/runner/SymbolicExternalTracingRunner.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/trace/runner/SymbolicExternalTracingRunner.kt @@ -106,7 +106,7 @@ class SymbolicExternalTracingRunner(val ctx: ExecutionContext) { val result = it.receive() when (result) { null -> log.debug("Connection timeout") - is ExecutionCompletedResult -> log.debug("Execution result: {}", result.trace) + is ExecutionCompletedResult -> log.debug("Execution result: {}", result.symbolicState) else -> log.debug("Execution result: {}", result) } //log.debug("Test {} executed with result {}", klass, result) From 17dab3f98a36ee43887d55cef7d84016da019af7 Mon Sep 17 00:00:00 2001 From: Azat Abdullin Date: Thu, 16 Nov 2023 17:49:28 +0100 Subject: [PATCH 3/3] fix string formatting in tests --- .../research/kex/reanimator/codegen/javagen/JavaBuilder.kt | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/reanimator/codegen/javagen/JavaBuilder.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/reanimator/codegen/javagen/JavaBuilder.kt index 77e8e7648..1d017b694 100644 --- a/kex-runner/src/main/kotlin/org/vorpal/research/kex/reanimator/codegen/javagen/JavaBuilder.kt +++ b/kex-runner/src/main/kotlin/org/vorpal/research/kex/reanimator/codegen/javagen/JavaBuilder.kt @@ -24,7 +24,10 @@ class JavaBuilder(val pkg: String = "") { '\'' -> "\\'" '\"' -> "\\\"" '\\' -> "\\\\" - else -> char + else -> when { + char.code in 32..126 -> char + else -> String.format("\\u%04X", char.code) + } } }