feat: Add agent, first version

usvm-core/build.gradle.kts

@@ -1,13 +1,14 @@
 plugins {
     id("usvm.kotlin-conventions")
-}
+    kotlin("plugin.serialization") version "1.9.22" }
 
 dependencies {
     api(project(":usvm-util"))
     api(Libs.ksmt_core)
     api(Libs.ksmt_z3)
     api(Libs.kotlinx_collections)
-
+    implementation("org.jetbrains.kotlinx:kotlinx-serialization-json:1.6.2")
+    implementation("org.jetbrains.kotlinx:atomicfu:0.23.2")
     testImplementation(Libs.mockk)
     testImplementation(Libs.junit_jupiter_params)
     testImplementation(Libs.ksmt_yices)

usvm-core/src/main/kotlin/org/usvm/statistics/Agent.kt

@@ -0,0 +1,177 @@
+package org.usvm.statistics
+
+import kotlinx.serialization.Serializable
+import kotlinx.serialization.json.Json
+import org.usvm.UState
+import kotlinx.serialization.encodeToString
+import java.io.InputStreamReader
+import java.io.OutputStreamWriter
+import java.net.HttpURLConnection
+import java.net.URL
+import kotlinx.atomicfu.atomic
+
+@Serializable
+data class Params(val funName: String, val type: String, val value: String, val transitive: Boolean)
+
+@Serializable
+data class Metric(val guid: String, val name: String, val params: Params)
+
+class Agent<Method, Statement, State : UState<*, Method, Statement, *, *, State>>   (
+    private val timeStatistics: TimeStatistics<Method, State>,
+    private val stepsStatistics: StepsStatistics<Method, State>,
+    private val coverage: CoverageStatistics<Method, Statement, State>
+) : UMachineObserver<State> {
+
+    private val shouldStop = atomic(false)
+    private val serverConnection = ServerConnection(CONFIG.getUidUrl, CONFIG.saveMetricUrl)
+    private var methodUnderMonitoring = mutableListOf<Method>()
+
+    init {
+        getCurrentMethods()
+    }
+
+    /**
+     * The class responsible for sending data to the server
+     */
+
+    inner class ServerConnection(private var getUidUrl: String, private var saveMetricUrl: String) {
+
+        /**
+         * Personal uid of a separate session
+         */
+
+        var uid = "NotConnection"
+
+        private fun connection(url: String, type: String): HttpURLConnection {
+            val httpUrlConnection = URL(url).openConnection() as HttpURLConnection
+            httpUrlConnection.requestMethod = type
+            if (type == "POST") {
+                httpUrlConnection.doOutput = true
+                httpUrlConnection.setRequestProperty("Content-Type", "application/json")
+            }
+
+            return httpUrlConnection
+        }
+
+        fun getUID() {
+            val httpUrlConnection = connection(getUidUrl, "GET")
+            val streamReader = InputStreamReader(httpUrlConnection.inputStream)
+            streamReader.use { uid = it.readText() }
+            httpUrlConnection.disconnect()
+        }
+
+        fun saveMetrics(metrics: String) {
+            val httpUrlConnection = connection(saveMetricUrl, "POST")
+            OutputStreamWriter(httpUrlConnection.outputStream).use { it.write(metrics) }
+            httpUrlConnection.disconnect()
+        }
+
+    }
+
+    /**
+     * A function that starts collecting statistics, serializing them and sending them to the server
+     */
+
+    override fun onMachineStarted() {
+        startCollectionStatistics()
+    }
+
+    private fun startCollectionStatistics() {
+        Thread {
+            try {
+                serverConnection.getUID()
+            } catch (e: Exception) {
+                println("Failed to get session uid, perhaps the server is not active")
+                return@Thread
+            }
+
+
+            if (serverConnection.uid == "NotConnection") return@Thread
+
+            while (!shouldStop.value) {
+                try {
+                    serverConnection.saveMetrics(serialize(getStatistic()))
+                } catch (e: Exception) {
+                    println("Failed to send metrics, check the server")
+                    return@Thread
+                }
+                Thread.sleep(CONFIG.deltaTime)
+            }
+        }.start()
+    }
+
+    override fun onMachineStopped() {
+        try {
+            serverConnection.saveMetrics(serialize(getStatistic()))
+        } catch (e: Exception) {
+            println("Failed to send metrics, check the server")
+        }
+        shouldStop.value = true
+    }
+
+    override fun onStateTerminated(state: State, stateReachable: Boolean) {
+        getCurrentMethods()
+    }
+
+    private fun getCurrentMethods() {
+        methodUnderMonitoring = coverage.getCoverageMethods().toMutableList()
+    }
+
+    /**
+     * Function to get statistics
+     */
+
+    private fun getStatistic() : Map<Method, Map<String, Comparable<*>>>{
+        val statsMap = mutableMapOf<Method, Map<String, Comparable<*>>>()
+
+        for (method in methodUnderMonitoring) {
+            statsMap[method] = mapOf(
+                "Steps" to stepsStatistics.getMethodSteps(method),
+                "Time" to timeStatistics.getTimeSpentOnMethod(method)
+            )
+        }
+
+        return statsMap
+    }
+
+    /**
+     * A function that is responsible for serializing statistics
+     */
+
+    private fun serialize(currentStatistic: Map<Method, Map<String, Comparable<*>>>): String {
+
+        val metricsList = mutableListOf<Metric>()
+
+        for ((method, statMap) in currentStatistic) {
+            for ((name, count) in statMap) {
+                val metric = Metric(
+                    guid = serverConnection.uid,
+                    name = name,
+                    params = Params(
+                        funName = method.toString(),
+                        type = "int",
+                        value = count.toString(),
+                        transitive = false
+                    )
+                )
+                metricsList += metric
+            }
+        }
+
+        val json = Json { prettyPrint = true }
+        val jsonString = json.encodeToString(metricsList)
+
+        return jsonString
+    }
+
+}
+
+/**
+ * Configurations necessary for the agent to work correctly
+ */
+
+object CONFIG {
+    var getUidUrl: String = "http://localhost:8080/new-session"
+    var saveMetricUrl: String = "http://localhost:8080/metrics"
+    var deltaTime: Long = 1000L
+}

usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt

@@ -65,6 +65,8 @@ class CoverageStatistics<Method, Statement, State : UState<*, Method, Statement,
         return covered.toFloat() / ((covered + uncovered).toFloat()) * 100f
     }
 
+    fun getCoverageMethods() = uncoveredStatements.keys.toList()
+
     /**
      * Returns current total coverage of all methods in coverage zone (in percents).
      */

usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt

@@ -18,13 +18,7 @@ import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.lastStmt
 import org.usvm.ps.createPathSelector
-import org.usvm.statistics.CompositeUMachineObserver
-import org.usvm.statistics.CoverageStatistics
-import org.usvm.statistics.StatisticsByMethodPrinter
-import org.usvm.statistics.StepsStatistics
-import org.usvm.statistics.TimeStatistics
-import org.usvm.statistics.TransitiveCoverageZoneObserver
-import org.usvm.statistics.UMachineObserver
+import org.usvm.statistics.*
 import org.usvm.statistics.collectors.AllStatesCollector
 import org.usvm.statistics.collectors.CoveredNewStatesCollector
 import org.usvm.statistics.collectors.TargetsReachedStatesCollector
@@ -131,7 +125,7 @@ class JcMachine(
         val observers = mutableListOf<UMachineObserver<JcState>>(coverageStatistics)
         observers.add(timeStatistics)
         observers.add(stepsStatistics)
-
+        if (options.monitoringIsEnable) observers.add(Agent(timeStatistics, stepsStatistics, coverageStatistics))
         if (interpreterObserver is UMachineObserver<*>) {
             @Suppress("UNCHECKED_CAST")
             observers.add(interpreterObserver as UMachineObserver<JcState>)

usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt

@@ -259,4 +259,8 @@ data class UMachineOptions(
      * Limit loop iterations.
      * */
     val loopIterationLimit: Int? = null,
+    /**
+     * Whether to run the statistics monitoring function
+     */
+    val monitoringIsEnable: Boolean = true
 )