Merge remote-tracking branch 'origin/symbolic_path_selector' into sym…

…bolic_path_selector # Conflicts: # kex.ini
vorpal-research · Apr 4, 2024 · d90eb1d · d90eb1d
2 parents 55bfaf8 + be3fcfa
commit d90eb1d
Show file tree

Hide file tree

Showing 269 changed files with 10,151 additions and 7,828 deletions.
diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -0,0 +1,22 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: "[BUG]"
+labels: bug
+assignees: AbdullinAM
+
+---
+
+**Describe the bug**
+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/.github/ISSUE_TEMPLATE/feature_request.md b/.github/ISSUE_TEMPLATE/feature_request.md
@@ -0,0 +1,20 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: "[FEATURE]"
+labels: enhancement
+assignees: AbdullinAM
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.
diff --git a/.github/workflows/jdk11-ci.yml b/.github/workflows/jdk11-ci.yml
@@ -13,11 +13,21 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v1
+      - uses: actions/checkout@v4
       - name: Set up JDK 11
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v4
         with:
-          java-version: 11
+          distribution: 'zulu'
+          java-version: '11'
+
+      - name: Cache local Maven repository
+        uses: actions/cache@v4
+        with:
+          path: ~/.m2/repository
+          key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}
+          restore-keys: |
+            ${{ runner.os }}-maven-
+
       - name: Build with Maven
         run: mvn verify -Pfull-smt --file pom.xml -s .github/github-settings.xml
         env:

diff --git a/.github/workflows/jdk17-ci.yml b/.github/workflows/jdk17-ci.yml
@@ -0,0 +1,35 @@
+name: JDK 17 CI
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - name: Set up JDK 17
+        uses: actions/setup-java@v4
+        with:
+          distribution: 'zulu'
+          java-version: '17'
+
+      - name: Cache local Maven repository
+        uses: actions/cache@v4
+        with:
+          path: ~/.m2/repository
+          key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}
+          restore-keys: |
+            ${{ runner.os }}-maven-
+
+      - name: Build with Maven
+        run: mvn verify -Pfull-smt --file pom.xml -s .github/github-settings.xml
+        env:
+          GITHUB_ACTOR: vorpal-reseacher
+          GITHUB_TOKEN: ${{ secrets.ORG_GITHUB_TOKEN }}
diff --git a/.github/workflows/jdk8-cd.yml b/.github/workflows/jdk8-cd.yml
@@ -10,11 +10,21 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v1
+      - uses: actions/checkout@v4
       - name: Set up JDK 1.8
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v4
         with:
-          java-version: 1.8
+          distribution: 'zulu'
+          java-version: '8'
+
+      - name: Cache local Maven repository
+        uses: actions/cache@v4
+        with:
+          path: ~/.m2/repository
+          key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}
+          restore-keys: |
+            ${{ runner.os }}-maven-
+
       - name: Build sources
         id: build
         run: |

diff --git a/.github/workflows/jdk8-ci.yml b/.github/workflows/jdk8-ci.yml
@@ -13,11 +13,21 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v1
+      - uses: actions/checkout@v4
       - name: Set up JDK 1.8
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v4
         with:
-          java-version: 1.8
+          distribution: 'zulu'
+          java-version: '8'
+
+      - name: Cache local Maven repository
+        uses: actions/cache@v4
+        with:
+          path: ~/.m2/repository
+          key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}
+          restore-keys: |
+            ${{ runner.os }}-maven-
+
       - name: Build with Maven
         run: mvn verify -Pfull-smt --file pom.xml -s .github/github-settings.xml
         env:

diff --git a/LICENSE b/LICENSE
@@ -175,18 +175,7 @@
 
    END OF TERMS AND CONDITIONS
 
-   APPENDIX: How to apply the Apache License to your work.
-
-      To apply the Apache License to your work, attach the following
-      boilerplate notice, with the fields enclosed by brackets "[]"
-      replaced with your own identifying information. (Don't include
-      the brackets!)  The text should be enclosed in the appropriate
-      comment syntax for the file format. We also recommend that a
-      file or class name and description of purpose be included on the
-      same "printed page" as the copyright notice for easier
-      identification within third-party archives.
-
-   Copyright [yyyy] [name of copyright owner]
+   Copyright 2024 Azat Abdullin
 
    Licensed under the Apache License, Version 2.0 (the "License");
    you may not use this file except in compliance with the License.

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]
 ```
@@ -54,13 +55,14 @@ Docker images with the latest version installed. Example:
 
 ```bash
 docker run -v ~/myproject:/home/myproject -v ~/kex-output:/home/kex-output \
- abdullin/kex-standalone:run --classpath /home/myproject/target/myproject.jar \
+ abdullin/kex-standalone:0.0.1 --classpath /home/myproject/target/myproject.jar \
  --target myproject.\* --output /home/kex-output --mode concolic
 ```
 
 # 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-annotation-processor/src/main/resources/SMTExpr.vm b/kex-annotation-processor/src/main/resources/SMTExpr.vm
@@ -573,7 +573,7 @@ class Ifer {
             inline fun < reified T : $valexpr > `else`(`false`: T): T {
                 val ctx = cond.ctx
                 val expr = engine().ite(ctx, cond.expr, `true`.expr, `false`.expr)
-                val axiom = spliceAxioms(ctx, `true`.axiom, `false`.axiom)
+                val axiom = spliceAxioms(ctx, cond.axiom, `true`.axiom, `false`.axiom)
                 return ${valexpr}.forceCast< T >($valexpr(ctx, expr, axiom))
             }
             inline fun < reified T : $valexpr > else_(`false`: () -> T) = `else`(`false`())