refactoring

vorpal-research · Jan 15, 2024 · 53863aa · 53863aa
1 parent c8ac9e1
commit 53863aa
Show file tree

Hide file tree

Showing 199 changed files with 7,783 additions and 7,211 deletions.
diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -11,12 +11,12 @@ assignees: AbdullinAM
 A clear and concise description of what the bug is.
 
 **To Reproduce**
+
 1. Steps to reproduce the behavior.
 2. Class, method (if applicable) and project where unexpected behavior occurs.
 
 **Expected behavior**
 A clear and concise description of what is expected.
 
-
 **Additional context**
 Add any other context about the problem here.
diff --git a/README.md b/README.md
@@ -1,6 +1,6 @@
 # Kex
 
-Kex is a platform for analysis of Java  bytecode.
+Kex is a platform for analysis of Java bytecode.
 
 # Build
 
@@ -13,13 +13,14 @@ Kex is a platform for analysis of Java  bytecode.
     ```
     mvn clean package -Psolver
     ```
-    where `solver` can be:
-  * `z3`
-  * `boolector` (supported only on linux)
-  * `ksmt` &mdash; used by default
-  * `full-smt` &mdash; build with z3, boolector and KSMT
+  where `solver` can be:
+    * `z3`
+    * `boolector` (supported only on linux)
+    * `ksmt` &mdash; used by default
+    * `full-smt` &mdash; build with z3, boolector and KSMT
 
 Run all the tests:
+
 ```
 mvn clean verify [-Psolver]
 ```
@@ -61,6 +62,7 @@ docker run -v ~/myproject:/home/myproject -v ~/kex-output:/home/kex-output \
 # Example
 
 Consider an example class:
+
 ```kotlin
 class TestClass {
     class Point(val x: Int, val y: Int)
@@ -78,6 +80,7 @@ class TestClass {
 ```
 
 Compile that class into the jar file and run Kex on it using following command:
+
 ```bash
 python ./kex.py --classpath test.jar --target TestClass --output test --mode concolic
 ```

diff --git a/kex-annotation-processor/src/main/kotlin/org/vorpal/research/kex/InheritanceInfo.kt b/kex-annotation-processor/src/main/kotlin/org/vorpal/research/kex/InheritanceInfo.kt
@@ -1,14 +1,13 @@
 package org.vorpal.research.kex
 
 import kotlinx.serialization.Serializable
-import kotlinx.serialization.decodeFromString
 import kotlinx.serialization.encodeToString
 import kotlinx.serialization.json.Json
 
 @Serializable
 data class InheritanceInfo(
-        val base: String,
-        val inheritors: Set<Inheritor>
+    val base: String,
+    val inheritors: Set<Inheritor>
 ) {
     fun toJson() = Json.encodeToString(this)
 
@@ -21,8 +20,8 @@ data class InheritanceInfo(
 
 @Serializable
 data class Inheritor(
-        val name: String,
-        val inheritorClass: String
+    val name: String,
+    val inheritorClass: String
 )
 
 
diff --git a/kex-annotation-processor/src/main/kotlin/org/vorpal/research/kex/KexProcessor.kt b/kex-annotation-processor/src/main/kotlin/org/vorpal/research/kex/KexProcessor.kt
@@ -20,8 +20,8 @@ abstract class KexProcessor : AbstractProcessor() {
         val parameters = mutableMapOf<String, Any>()
 
         for (property in klass.declaredMemberProperties) {
-            parameters[property.name] = instance.getProperty(property.name) ?:
-                    unreachable { error("Could not get property $property of annotation $instance") }
+            parameters[property.name] = instance.getProperty(property.name)
+                ?: unreachable { error("Could not get property $property of annotation $instance") }
         }
 
         return parameters

diff --git a/kex-annotation-processor/src/main/kotlin/org/vorpal/research/kex/smt/SMTProcessor.kt b/kex-annotation-processor/src/main/kotlin/org/vorpal/research/kex/smt/SMTProcessor.kt
@@ -12,11 +12,12 @@ import javax.lang.model.element.TypeElement
 import kotlin.reflect.KClass
 
 @SupportedAnnotationTypes(
-        "org.vorpal.research.kex.smt.SMTExpr",
-        "org.vorpal.research.kex.smt.SMTMemory",
-        "org.vorpal.research.kex.smt.SMTExprFactory",
-        "org.vorpal.research.kex.smt.SMTContext",
-        "org.vorpal.research.kex.smt.SMTConverter")
+    "org.vorpal.research.kex.smt.SMTExpr",
+    "org.vorpal.research.kex.smt.SMTMemory",
+    "org.vorpal.research.kex.smt.SMTExprFactory",
+    "org.vorpal.research.kex.smt.SMTContext",
+    "org.vorpal.research.kex.smt.SMTConverter"
+)
 @SupportedOptions(SMTProcessor.KAPT_GENERATED_SOURCES)
 class SMTProcessor : KexProcessor() {
     companion object {
@@ -52,7 +53,7 @@ class SMTProcessor : KexProcessor() {
     private fun <T : Annotation> processAnnotation(element: Element, annotationClass: KClass<T>, nameTemplate: String) {
         val `package` = processingEnv.elementUtils.getPackageOf(element).toString()
         val annotation = element.getAnnotation(annotationClass.java)
-                ?: unreachable { error("Element $element have no annotation $annotationClass") }
+            ?: unreachable { error("Element $element have no annotation $annotationClass") }
 
         val parameters = getAnnotationProperties(annotation, annotationClass).toMutableMap()
         val solver = parameters.getValue("solver") as String

diff --git a/kex-annotation-processor/src/main/kotlin/org/vorpal/research/kex/smt/annotations.kt b/kex-annotation-processor/src/main/kotlin/org/vorpal/research/kex/smt/annotations.kt
@@ -3,64 +3,64 @@
 package org.vorpal.research.kex.smt
 
 annotation class SMTExpr(
-        val solver: String,
-        val importPackages: Array<String>,
-        val context: String,
-        val expr: String,
-        val sort: String,
-        val function: String,
-        val generateString: Boolean = false
+    val solver: String,
+    val importPackages: Array<String>,
+    val context: String,
+    val expr: String,
+    val sort: String,
+    val function: String,
+    val generateString: Boolean = false
 )
 
 annotation class SMTMemory(
-        val solver: String,
-        val importPackages: Array<String>,
-        val context: String,
-        val byteSize: Int,
-        val generateString: Boolean = false
+    val solver: String,
+    val importPackages: Array<String>,
+    val context: String,
+    val byteSize: Int,
+    val generateString: Boolean = false
 )
 
 annotation class SMTExprFactory(
-        val solver: String,
-        val importPackages: Array<String>,
-        val context: String,
-        val contextInitializer: String = "",
-        val generateString: Boolean = false
+    val solver: String,
+    val importPackages: Array<String>,
+    val context: String,
+    val contextInitializer: String = "",
+    val generateString: Boolean = false
 )
 
 annotation class SMTContext(
-        val solver: String,
-        val importPackages: Array<String>,
-        val context: String,
-        val generateString: Boolean = false
+    val solver: String,
+    val importPackages: Array<String>,
+    val context: String,
+    val generateString: Boolean = false
 )
 
 annotation class SMTConverter(
-        val solver: String,
-        val importPackages: Array<String>,
-        val generateString: Boolean = false
+    val solver: String,
+    val importPackages: Array<String>,
+    val generateString: Boolean = false
 )
 
 annotation class AbstractSolver
 
 annotation class Solver(
-        val name: String
+    val name: String
 )
 
 annotation class AbstractAsyncSolver
 
 annotation class AsyncSolver(
-        val name: String
+    val name: String
 )
 
 annotation class AbstractIncrementalSolver
 
 annotation class IncrementalSolver(
-        val name: String
+    val name: String
 )
 
 annotation class AbstractAsyncIncrementalSolver
 
 annotation class AsyncIncrementalSolver(
-        val name: String
+    val name: String
 )
diff --git a/kex-boolector/src/main/kotlin/org/vorpal/research/kex/smt/boolector/BoolectorEngine.kt b/kex-boolector/src/main/kotlin/org/vorpal/research/kex/smt/boolector/BoolectorEngine.kt
@@ -239,24 +239,30 @@ object BoolectorEngine :
                     else
                         and(lhv.toBitvecNode(rhv.width), rhv.toBitvecNode())
                 }
+
                 else -> unreachable { log.error("Unexpected and arguments: $lhv and $rhv") }
             }
+
             Opcode.OR -> when {
                 (lhv.isBoolNode && rhv.isBoolNode) -> or(lhv.toBoolNode(), rhv.toBoolNode())
                 !(lhv.isArrayNode && rhv.isArrayNode) -> {
                     if (lhv.width >= rhv.width) or(lhv.toBitvecNode(), rhv.toBitvecNode(lhv.width))
                     else or(lhv.toBitvecNode(rhv.width), rhv.toBitvecNode())
                 }
+
                 else -> unreachable { log.error("Unexpected or arguments: $lhv or $rhv") }
             }
+
             Opcode.XOR -> when {
                 (lhv.isBoolNode && rhv.isBoolNode) -> xor(lhv.toBoolNode(), rhv.toBoolNode())
                 !(lhv.isArrayNode && rhv.isArrayNode) -> {
                     if (lhv.width >= rhv.width) xor(lhv.toBitvecNode(), rhv.toBitvecNode(lhv.width))
                     else xor(lhv.toBitvecNode(rhv.width), rhv.toBitvecNode())
                 }
+
                 else -> unreachable { log.error("Unexpected xor arguments: $lhv xor $rhv") }
             }
+
             Opcode.IMPLIES -> implies(lhv.toBoolNode(), rhv.toBoolNode())
             Opcode.IFF -> iff(lhv.toBoolNode(), rhv.toBoolNode())
             Opcode.CONCAT -> concat(lhv.toBitvecNode(), rhv.toBitvecNode())

diff --git a/kex-boolector/src/main/kotlin/org/vorpal/research/kex/smt/boolector/BoolectorNativeLoader.kt b/kex-boolector/src/main/kotlin/org/vorpal/research/kex/smt/boolector/BoolectorNativeLoader.kt
@@ -24,6 +24,7 @@ abstract class BoolectorNativeLoader {
                 osProperty.startsWith("linux") -> {
                     "boolector-$BOOLECTOR_VERSION-linux64-native.zip" to libraries.map { "$it.so" }
                 }
+
                 else -> unreachable { log.error("Unknown OS: $osProperty") }
             }
 

diff --git a/kex-boolector/src/test/kotlin/org/vorpal/research/kex/smt/boolector/BoolectorSolverTest.kt b/kex-boolector/src/test/kotlin/org/vorpal/research/kex/smt/boolector/BoolectorSolverTest.kt
@@ -72,10 +72,12 @@ class BoolectorSolverTest : KexTest("boolector-solver") {
         memA.writeWordMemory(ptr, 0, a)
         memB.writeWordMemory(ptr, 0, b)
 
-        val merged = BoolectorContext.mergeContexts("merged", default, mapOf(
+        val merged = BoolectorContext.mergeContexts(
+            "merged", default, mapOf(
                 condA to memA,
                 condB to memB
-        ))
+            )
+        )
 
         val c = merged.readWordMemory(ptr, 0)
 

diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/state/PredicateStateBuilder.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/state/PredicateStateBuilder.kt
@@ -38,6 +38,7 @@ class PredicateStateBuilder(val method: Method) {
             return when {
                 insts.any { it is ReturnInst } -> insts.firstOrNull { it is ReturnInst }
                     ?.run { getInstructionState(this) }
+
                 method.isConstructor -> insts.lastOrNull()?.run { getInstructionState(this) }
                 method.isStaticInitializer -> insts.lastOrNull()?.run { getInstructionState(this) }
                 else -> null

diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/state/TermExpressionBuilder.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/state/TermExpressionBuilder.kt
@@ -133,15 +133,17 @@ class TermExpressionBuilder(override val cm: ClassManager) : TermBuilder, Method
         type: Type,
         index: Int,
         incomings: List<Pair<BasicBlock, Value>>,
-        default: Term): Term = when {
-            index < incomings.size -> ite(
-                type.kexType,
-                incomings[index].first.condition,
-                incomings[index].second.term,
-                mkIte(type, index + 1, incomings, default)
-            )
-            else -> default
-        }
+        default: Term
+    ): Term = when {
+        index < incomings.size -> ite(
+            type.kexType,
+            incomings[index].first.condition,
+            incomings[index].second.term,
+            mkIte(type, index + 1, incomings, default)
+        )
+
+        else -> default
+    }
 
     override fun visitPhiInst(inst: PhiInst) {
         termMap[inst] = mkIte(inst.type, 0, inst.incomings.toList(), default(inst.type.kexType))

diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/LoopDeroller.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/transform/LoopDeroller.kt
@@ -378,8 +378,8 @@ class LoopDeroller(override val cm: ClassManager) : LoopOptimizer(cm) {
 
             val users = inst.users.filterIsInstance<Instruction>()
             if (users.any {
-                it.hasParent && it.parent !in state.blockMappings && it.parent in method.body && it !is PhiInst
-            }) {
+                    it.hasParent && it.parent !in state.blockMappings && it.parent in method.body && it !is PhiInst
+                }) {
                 for (exit in state.exits) {
                     val mappings = exit.predecessors
                         .filter { it in state.exitingBlocks }

diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/util/AccessModifier.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/asm/util/AccessModifier.kt
@@ -116,6 +116,7 @@ fun Method.getAccessModifier(cm: ClassManager): AccessModifier = when {
     this.isProtected -> (this.declaringClass.toKfgType(cm.type) as ClassType).klass.let {
         AccessModifier.Protected(it)
     }
+
     else -> (this.declaringClass.toKfgType(cm.type) as ClassType).klass.let {
         AccessModifier.Package(it.pkg)
     }
@@ -127,6 +128,7 @@ fun Field.getAccessModifier(cm: ClassManager): AccessModifier = when {
     this.isProtected -> (this.declaringClass.toKfgType(cm.type) as ClassType).klass.let {
         AccessModifier.Protected(it)
     }
+
     else -> (this.declaringClass.toKfgType(cm.type) as ClassType).klass.let {
         AccessModifier.Package(it.pkg)
     }

diff --git a/kex-core/src/main/kotlin/org/vorpal/research/kex/config/AbstractCmdConfig.kt b/kex-core/src/main/kotlin/org/vorpal/research/kex/config/AbstractCmdConfig.kt
@@ -22,6 +22,7 @@ abstract class AbstractCmdConfig(
     protected val options = Options()
     protected val commandLineOptions = hashMapOf<String, MutableMap<String, String>>()
     protected val cmd: CommandLine
+
     @Suppress("unused")
     val argList: List<String> get() = cmd.argList
-Original file line number
+Diff line change
@@ Expand Up / @@ -24,6 +24,7 @@ abstract class BoolectorNativeLoader { @@
                     osProperty.startsWith("linux") -> {
                         "boolector-$BOOLECTOR_VERSION-linux64-native.zip" to libraries.map { "$it.so" }
                     }
                     else -> unreachable { log.error("Unknown OS: $osProperty") }
                 }
@@ Expand Down @@