Merge pull request #97 from vorpal-research/small-fixes

Small fixes
vorpal-research · Nov 20, 2023 · 464a27f · 464a27f
2 parents b158e75 + 17dab3f
commit 464a27f
Show file tree

Hide file tree

Showing 13 changed files with 48 additions and 18 deletions.
diff --git 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)
     }
 

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
@@ -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<Instruction>
     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
@@ -118,6 +118,9 @@ class SymbolicTraceBuilder(
     override val termMap: Map<Term, WrappedValue>
         get() = terms.toMap()
 
+    override val instructionTrace: List<Instruction>
+        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
@@ -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<Instruction>()
     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
@@ -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<Instruction>
 }
 @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
@@ -64,7 +64,13 @@ class KexExecutor(args: Array<String>) {
             }
         }
         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<String>) {
             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
@@ -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/...nner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/bfs/BfsPathSelector.kt b/...nner/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/...rc/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/cgs/ContextGuidedSelector.kt b/...rc/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/...ner/src/main/kotlin/org/vorpal/research/kex/asm/analysis/concolic/gui/GUIProxySelector.kt b/...ner/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/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)
+            }
         }
     }
 

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
@@ -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/...ner/src/main/kotlin/org/vorpal/research/kex/trace/runner/SymbolicExternalTracingRunner.kt b/...ner/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)