Migration from SWAT-Research

.dockerignore

@@ -0,0 +1,9 @@
+.git
+.github
+.gradle
+build
+**/*.iml
+*.log
+*.swp
+.DS_Store
+docker-compose.yml

.gitattributes

@@ -0,0 +1 @@
+*.sh text eol=lf

.github/workflows/run_svcomp_with_docker.yml

@@ -0,0 +1,45 @@
+name: Run SV-COMP Targets
+
+on:
+  push:
+    branches: [ "development" , "nico/ci-test"]
+
+jobs:
+  build-and-run:
+    name: Build & Run Container
+    runs-on: self-hosted
+
+    steps:
+      - name: Checkout this repo
+        uses: actions/checkout@v4
+
+      - name: Checkout SV-Benchmarks
+        uses: actions/checkout@v4
+        with:
+          repository: 'SWAT-project/SV-Benchmarks'
+          ssh-key: '${{ secrets.SWAT_PROJECT_SV_BENCHMARKS }}'
+          path: ./targets/sv-comp/sv-benchmarks
+
+      - name: Build Docker Image
+        run: |
+          docker build --no-cache -f ./docker/Dockerfile -t swat-svcomp-image:ci .
+
+      - name: Run SV-COMP Target Tests
+        run: |
+          summary_dir=$(dirname "$GITHUB_STEP_SUMMARY")
+          summary_file=$(basename "$GITHUB_STEP_SUMMARY")
+          docker run --rm \
+            -w /app/targets/sv-comp/scripts \
+            -v "$summary_dir:/gh-summary" \
+            -e GITHUB_STEP_SUMMARY="/gh-summary/$summary_file" \
+            swat-svcomp-image:ci ./ci_run.sh
+
+      - name: Remove Docker Image
+        if: always()
+        run: |
+          docker rmi -f swat-svcomp-image:ci || true
+
+      - name: Cleanup Work Directory
+        if: always()
+        run: |
+          rm -rf ./targets/sv-comp/sv-benchmarks || true

.gitignore

@@ -2,12 +2,31 @@
 .gradle
 /symbolic-executor/build/
 /symbolic-executor/lib/
+/symbolic-executor/bin/
 /symbolic-executor/logs/
 /symbolic-explorer/venv/
 **/*.log
 targets/**/bin/
 targets/**/build/
+targets/applications/openolat/libs/z3/
 /logs/
 **/logs/
+**/logs-debug/
+**/results/
+**/*.class
 /build/
-/libs/java-library-path/*
+**/build/
+/libs/java-library-path/*
+libs/jacoco/report
+targets/applications/openhospital/oh_build/restler_working_dir/Compile
+targets/applications/openhospital/oh_build/restler_working_dir/RestlerResults
+targets/sv-comp/sv-benchmarks/*
+**/__pycache__
+**/.venv/*
+/.vscode/
+**/smt_files/
+**/witness/
+**/sv-comp/results/
+**/analysis/
+!targets/sv-comp/scripts/lib/analysis
+libs/cfg-extractor/cfg-extractor-1.0-SNAPSHOT.jar

.gitmodules

@@ -0,0 +1,24 @@
+[submodule "targets/applications/petclinic-test/petclinic"]
+	path = targets/applications/petclinic-test/petclinic
+	url = https://github.com/spring-projects/spring-petclinic.git
+[submodule "targets/applications/petclinic-rest/spring-petclinic-rest"]
+	path = targets/applications/petclinic-rest/spring-petclinic-rest
+	url = https://github.com/spring-petclinic/spring-petclinic-rest.git
+[submodule "targets/applications/openolat/openolat"]
+	path = targets/applications/openolat/openolat
+	url = https://github.com/OpenOLAT/OpenOLAT.git
+[submodule "targets/applications/genomenexus/genomenexus"]
+	path = targets/applications/genomenexus/genomenexus
+	url = https://github.com/genome-nexus/genome-nexus.git
+[submodule "targets/applications/genomenexus/genomenexus-importer"]
+	path = targets/applications/genomenexus/genomenexus-importer
+	url = https://github.com/genome-nexus/genome-nexus-importer.git
+[submodule "targets/applications/oss-fuzz/gson/gson"]
+	path = targets/applications/oss-fuzz/gson/gson
+	url = https://github.com/google/gson.git
+[submodule "targets/applications/oss-fuzz/java-diff-utils/java-diff-utils"]
+	path = targets/applications/oss-fuzz/java-diff-utils/java-diff-utils
+	url = https://github.com/java-diff-utils/java-diff-utils.git
+[submodule "targets/applications/oss-fuzz/spatial4j/spatial4j"]
+	path = targets/applications/oss-fuzz/spatial4j/spatial4j
+	url = https://github.com/locationtech/spatial4j.git

.run/ModelMapper.run.xml

@@ -0,0 +1,10 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="ModelMapper" type="JarApplication">
+    <option name="JAR_PATH" value="$PROJECT_DIR$/targets/applications/modelmapper-test-app/build/libs/modelmapper-test-app-0.0.1-SNAPSHOT.jar" />
+    <option name="VM_PARAMETERS" value="-Xmx16g -Dconfig.path=./targets/applications/modelmapper-test-app/swat.cfg -Djava.library.path=./libs/java-library-path -javaagent:./symbolic-executor/lib/symbolic-executor.jar" />
+    <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$" />
+    <option name="ALTERNATIVE_JRE_PATH_ENABLED" value="true" />
+    <option name="ALTERNATIVE_JRE_PATH" value="17" />
+    <method v="2" />
+  </configuration>
+</component>

README.md

@@ -1,4 +1,4 @@
 # SWAT
-A dynamic symbolic execution engine for Java Applications that uses on-the-fly instrumentation to facilitate symbolic tracking. 
+A dynamic symbolic execution engine for Java Applications that uses on-the-fly instrumentation to facilitate symbolic tracking.
 The documentation is available at [https://swat-project.github.io/docs/](https://swat-project.github.io/docs/).
 The repository is also still under construction.

annotations/build.gradle

@@ -0,0 +1,6 @@
+plugins {
+    id 'java'
+}
+
+group = 'de.uzl.its.swat'
+version = '1.0'

annotations/src/main/java/de/uzl/its/swat/annotations/Symbolic.java

@@ -0,0 +1,11 @@
+package de.uzl.its.swat.annotations;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.FIELD, ElementType.PARAMETER, ElementType.LOCAL_VARIABLE, ElementType.METHOD, ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
+public @interface Symbolic {
+}

build.gradle

@@ -6,18 +6,22 @@ plugins {
 
 tasks.register('copyNativeLibs', Copy) { // copies correct native z3 files to libs/
         def osArchMap = [
-                'windows-x64': 'z3-4.12.5-x64-win',
-                'windows-x86': 'z3-4.12.5-x86-win',
-                'osx-x64'    : 'z3-4.12.5-x64-osx-11.7.10',
-                'osx-arm64'  : 'z3-4.12.5-arm64-osx-11.0',
-                'linux-x64'  : 'z3-4.12.5-x64-glibc-2.31',
-                'linux-arm64': 'z3-4.12.5-arm64-glibc-2.35'
+                'windows-x64': 'z3-4.15.4-x64-win',
+                'windows-x86': 'z3-4.15.4-x86-win',
+                'osx-x64'    : 'z3-4.15.4-x64-osx-13.7.6',
+                'osx-arm64'  : 'z3-4.15.4-arm64-osx-13.7.6',
+                'linux-x64'  : 'z3-4.15.4-x64-glibc-2.39',
+                'linux-arm64': 'z3-4.15.4-arm64-glibc-2.34'
         ]
 
         def os = OperatingSystem.current()
         println("Operating system: $os")
-        def arch = os.getArch()
-        def osKey = ''
+
+        def arch = System.getProperty("os.arch") // Use Java system property to get architecture
+        println("Architecture: $arch")
+
+
+    def osKey = ''
         switch (os) {
             case OperatingSystem.LINUX:
                 osKey = arch == "aarch64" ? "linux-arm64" : "linux-x64"
@@ -50,13 +54,84 @@ tasks.register('copyNativeLibs', Copy) { // copies correct native z3 files to li
             includeEmptyDirs false
 
     }
+tasks.register('downloadJacoco') {
+    description = 'Downloads JaCoCo agent jar for coverage collection'
+    def jacocoVersion = '0.8.13'
+    def jacocoUrl = "https://repo1.maven.org/maven2/org/jacoco/org.jacoco.agent/${jacocoVersion}/org.jacoco.agent-${jacocoVersion}-runtime.jar"
+    def jacocoCliUrl = "https://repo1.maven.org/maven2/org/jacoco/org.jacoco.cli/${jacocoVersion}/org.jacoco.cli-${jacocoVersion}-nodeps.jar"
+    def jacocoDir = file('libs/jacoco')
+    def jacocoAgent = file("${jacocoDir}/jacocoagent.jar")
+    def jacocoCli = file("${jacocoDir}/jacococli.jar")
+
+    outputs.files(jacocoAgent, jacocoCli)
+
+    doLast {
+        jacocoDir.mkdirs()
+
+        // Download JaCoCo agent
+        if (!jacocoAgent.exists()) {
+            println "Downloading JaCoCo agent from ${jacocoUrl}"
+            new URL(jacocoUrl).withInputStream{ i -> jacocoAgent.withOutputStream{ it << i }}
+        }
+
+        // Download JaCoCo CLI for report generation
+        if (!jacocoCli.exists()) {
+            println "Downloading JaCoCo CLI from ${jacocoCliUrl}"
+            new URL(jacocoCliUrl).withInputStream{ i -> jacocoCli.withOutputStream{ it << i }}
+        }
+
+        println "JaCoCo agent downloaded to: ${jacocoAgent.absolutePath}"
+        println "JaCoCo CLI downloaded to: ${jacocoCli.absolutePath}"
+    }
+}
+
+configurations {
+    cfgExtractor
+}
+
+dependencies {
+    cfgExtractor 'de.uzl.its:cfg-extractor:1.0-SNAPSHOT'
+}
+
+tasks.register('downloadCfgExtractor', Copy) {
+    description = 'Downloads cfg-extractor fat JAR from GitHub Packages'
+    from configurations.cfgExtractor
+    into 'libs/cfg-extractor'
+    duplicatesStrategy = DuplicatesStrategy.EXCLUDE
+
+    doLast {
+        def jarFile = fileTree('libs/cfg-extractor').matching { include '*.jar' }.singleFile
+        println "cfg-extractor fat JAR downloaded to: ${jarFile.absolutePath}"
+        println "Usage: java -jar ${jarFile.name} <input-path> <output-dir> [entry-class] [entry-method] [analysis-type]"
+    }
+}
 
 
 allprojects {
     apply plugin: 'com.diffplug.spotless'
     apply plugin: 'java'
     repositories {
         mavenCentral()
+
+        // GitHub Packages repository for cfg-extractor
+        maven {
+            name = "GitHubPackages"
+            url = uri("https://maven.pkg.github.com/SWAT-project/SWAT-Research")
+            credentials {
+                username = project.findProperty("gpr.user") ?: System.getenv("GITHUB_USERNAME")
+                password = project.findProperty("gpr.token") ?: System.getenv("GITHUB_TOKEN")
+            }
+        }
+
+        // JitPack for SootUp dependencies (dex-tools)
+        maven {
+            url = uri("https://jitpack.io")
+        }
+
+        // Google's Maven repository for Android tools (R8)
+        maven {
+            url = uri("https://maven.google.com")
+        }
     }
     java {
         toolchain {