m

vorpal-research · Jun 22, 2023 · 28fd524 · 28fd524
1 parent b21a1fa
commit 28fd524
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 16 deletions.
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
@@ -410,14 +410,13 @@ class KSMTSolver(
         val typeMap = hashMapOf<Term, KexType>()
 
         for ((type, value) in ef.typeMap) {
-            val index =
-                when (val actualValue = KSMTUnlogic.undo(value.expr.asExpr(kCtx), kCtx, model)) {
-                    is ConstStringTerm -> term {
-                        const(actualValue.value.length - actualValue.value.indexOf('1') - 1)
-                    }
-
-                    else -> term { const(log2(actualValue.numericValue.toDouble()).toInt()) }
+            val index = when (val actualValue = KSMTUnlogic.undo(value.expr.asExpr(kCtx), kCtx, model)) {
+                is ConstStringTerm -> term {
+                    const(actualValue.value.length - actualValue.value.indexOf('1') - 1)
                 }
+
+                else -> term { const(log2(actualValue.numericValue.toDouble()).toInt()) }
+            }
             typeMap[index] = type.kexType
         }
 
@@ -428,10 +427,12 @@ class KSMTSolver(
             when (ptr) {
                 is ArrayLoadTerm -> {}
                 is ArrayIndexTerm -> {
-                    val arrayPtrExpr = KSMTConverter(executionContext, noAxioms = true).convert(ptr.arrayRef, ef, ctx) as? Ptr_
-                        ?: unreachable { log.error("Non-ptr expr for pointer $ptr") }
-                    val indexExpr = KSMTConverter(executionContext, noAxioms = true).convert(ptr.index, ef, ctx) as? Int_
-                        ?: unreachable { log.error("Non integer expr for index in $ptr") }
+                    val arrayPtrExpr =
+                        KSMTConverter(executionContext, noAxioms = true).convert(ptr.arrayRef, ef, ctx) as? Ptr_
+                            ?: unreachable { log.error("Non-ptr expr for pointer $ptr") }
+                    val indexExpr =
+                        KSMTConverter(executionContext, noAxioms = true).convert(ptr.index, ef, ctx) as? Int_
+                            ?: unreachable { log.error("Non integer expr for index in $ptr") }
 
                     val modelPtr = KSMTUnlogic.undo(
                         model.eval(arrayPtrExpr.expr.asExpr(kCtx), true),

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/launcher/KexAnalysisLauncher.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/launcher/KexAnalysisLauncher.kt
@@ -114,9 +114,9 @@ abstract class KexAnalysisLauncher(classPaths: List<String>, targetName: String)
         cm.initialize(analysisJars)
 
         analysisLevel = AnalysisLevel.parse(cm, targetName)
-        log.debug("Target: $analysisLevel")
+        log.debug("Target: {}", analysisLevel)
         accessLevel = analysisLevel.accessLevel
-        log.debug("Access level: $accessLevel")
+        log.debug("Access level: {}", accessLevel)
 
         val classLoader = URLClassLoader(arrayOf(instrumentedCodeDir.toUri().toURL()))
         val klassPath = containers.map { it.path }

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/launcher/LibraryCheckLauncher.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/launcher/LibraryCheckLauncher.kt
@@ -23,7 +23,7 @@ class LibraryCheckLauncher(
         runPipeline(context, analysisLevel) {
             +CallCiteChecker(context, callCitePackage, psa)
         }
-        log.debug("Analysis finished, emitting results info ${DefectManager.defectFile}")
+        log.debug("Analysis finished, emitting results info {}", DefectManager.defectFile)
         DefectManager.emit()
     }
 

diff --git a/kex-runner/src/main/kotlin/org/vorpal/research/kex/main.kt b/kex-runner/src/main/kotlin/org/vorpal/research/kex/main.kt
@@ -10,7 +10,6 @@ import org.vorpal.research.kex.config.kexConfig
 import org.vorpal.research.kex.launcher.ConcolicLauncher
 import org.vorpal.research.kex.launcher.CrashReproductionLauncher
 import org.vorpal.research.kex.launcher.DefectCheckerLauncher
-import org.vorpal.research.kex.launcher.KexLauncher
 import org.vorpal.research.kex.launcher.LaunchMode
 import org.vorpal.research.kex.launcher.LauncherException
 import org.vorpal.research.kex.launcher.LibraryCheckLauncher
@@ -45,7 +44,7 @@ fun main(args: Array<String>) {
     require(classPaths != null, cmd::printHelp)
 
     try {
-        val launcher: KexLauncher = when (val mode = cmd.getEnumValue("mode", LaunchMode.Concolic, ignoreCase = true)) {
+        val launcher = when (val mode = cmd.getEnumValue("mode", LaunchMode.Concolic, ignoreCase = true)) {
             LaunchMode.Crash -> {
                 val traceFile = cmd.getCmdValue("trace")
                 require(traceFile != null) {
@@ -61,6 +60,7 @@ fun main(args: Array<String>) {
 
                 CrashReproductionLauncher(classPaths, traceFile, traceDepth!!.toUInt())
             }
+
             else -> {
                 val targetName = cmd.getCmdValue("target")
                 require(targetName != null) {
@@ -78,6 +78,7 @@ fun main(args: Array<String>) {
 
                         LibraryCheckLauncher(classPaths, targetName, libraryTarget)
                     }
+
                     LaunchMode.Symbolic -> SymbolicLauncher(classPaths, targetName)
                     LaunchMode.Concolic -> ConcolicLauncher(classPaths, targetName)
                     LaunchMode.DefectChecker -> DefectCheckerLauncher(classPaths, targetName)