Add a series of tests for the concolic execution engine (#8)

* Add a series of tests for the concolic execution engine

* Add tests with float to int conversion instructions

* Add some additional assertions on the values found + between test for floats

* Parameterize floats in between test

* Add a few additional tests

* Make test more strict

(Will fail on an older warduino version)

* Give a slightly more informative error message when finding more or less paths

* Add CI actions to run the mio setup process and execute the concolic tests

* Make checkout in action recursive

* Add wabt to dependencies

* Update gradle settings to include full stacktrace on failure

* Log standard streams for tests

* Update symbolic warduino version

Author: MaartenS11

.github/workflows/gradle.yml

@@ -18,6 +18,8 @@ jobs:
 
     steps:
     - uses: actions/checkout@v4
+      with:
+        submodules: recursive
     - name: Set up JDK 22
       uses: actions/setup-java@v4
       with:
@@ -49,6 +51,15 @@ jobs:
         name: MIO fatJar
         path: build/libs/mio.jar
 
+    - name: Install dependencies
+      run: sudo apt install -y libz3-dev wabt
+
+    - name: Setup MIO
+      run: ./gradlew setup
+
+    - name: Test concolic execution engine
+      run: ./gradlew test --tests concolic.ConcolicTests
+
   dependency-submission:
 
     runs-on: ubuntu-latest

WARDuino-symbolic

@@ -1,7 +1,7 @@
 import java.util.*
 
 plugins {
-    kotlin("jvm") version "2.0.0"
+    kotlin("jvm") version "2.2.0"
     application
 }
 
@@ -33,6 +33,12 @@ dependencies {
 
 tasks.test {
     useJUnitPlatform()
+
+    testLogging {
+        events("failed")
+        exceptionFormat = org.gradle.api.tasks.testing.logging.TestExceptionFormat.FULL
+        showStandardStreams = true
+    }
 }
 
 kotlin {

build.gradle.kts

@@ -14,16 +14,36 @@ data class SymbolicValueMapping(val primitive: String, val arg: Int, val value:
     }
 }
 
-data class ConcolicAnalysisResult(val paths: List<SymbolicValueMapping>)
+data class ConcolicAnalysisResult(val paths: List<SymbolicValueMapping>) {
+    fun getPathCount(): Int {
+        return getPathCount(paths)
+    }
+    private fun getPathCount(paths: List<SymbolicValueMapping>): Int {
+        if (paths.isEmpty()) {
+            return 1
+        }
+
+        var count = 0
+        for (path in paths) {
+            count += getPathCount(path.paths)
+        }
+        return count
+    }
+}
 
-fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String, maxInstructions: Int = 50, maxSymbolicVariables: Int = -1, maxIterations: Int = -1, stopPc: Int = -1): ConcolicAnalysisResult {
-    val woodState = WOODState.fromLine(jsonSnapshot)
-    val messages = woodState.toBinary(io = false, overrides = false).map { it.trim('\n', ' ') }
-    for (msg in messages) {
-        println("\"$msg\"")
+fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String?, maxInstructions: Int = 50, maxSymbolicVariables: Int = -1, maxIterations: Int = -1, stopPc: Int = -1): ConcolicAnalysisResult {
+    val command = if (jsonSnapshot != null) {
+        val woodState = WOODState.fromLine(jsonSnapshot)
+        val messages = woodState.toBinary(io = false, overrides = false).map { it.trim('\n', ' ') }
+        for (msg in messages) {
+            println("\"$msg\"")
+        }
+        listOf(wdcliPath, wasmFile, "--no-socket", "--mode", "concolic", "--snapshot", *messages.toTypedArray(), "end", "--max-instructions", "$maxInstructions", "--max-symbolic-variables", "$maxSymbolicVariables", "--max-iterations", "$maxIterations", "--stop-at-pc", "$stopPc")
+    }
+    else {
+        listOf(wdcliPath, wasmFile, "--no-socket", "--mode", "concolic", "--max-instructions", "$maxInstructions", "--max-symbolic-variables", "$maxSymbolicVariables", "--max-iterations", "$maxIterations", "--stop-at-pc", "$stopPc")
     }
 
-    val command = listOf(wdcliPath, wasmFile, "--no-socket", "--mode", "concolic", "--snapshot", *messages.toTypedArray(), "end", "--max-instructions", "$maxInstructions", "--max-symbolic-variables", "$maxSymbolicVariables", "--max-iterations", "$maxIterations", "--stop-at-pc", "$stopPc")
     println("Running command: ${command.joinToString(" ") }")
     val process = ProcessBuilder(command).redirectErrorStream(true).start()
     val lineScanner = Scanner(process.inputStream)
@@ -40,6 +60,9 @@ fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String, maxInstru
             //process(result)
             return ConcolicAnalysisResult(result.paths.sortedBy { it.value })
         }
+        if (currentLine.startsWith("Trap:")) {
+            throw Exception("Execution resulted in a trap!")
+        }
     }
     process.destroy()
     println("Output:")