From 16d7ae40d1428491b1aad88f902d53e1b6ce7cf9 Mon Sep 17 00:00:00 2001 From: YazoonDinalt Date: Tue, 7 Jan 2025 08:23:53 +0300 Subject: [PATCH] feat: Add agent, first version --- usvm-core/build.gradle.kts | 5 +- .../main/kotlin/org/usvm/statistics/Agent.kt | 177 ++++++++++++++++++ .../org/usvm/statistics/CoverageStatistics.kt | 2 + .../main/kotlin/org/usvm/machine/JcMachine.kt | 10 +- .../main/kotlin/org/usvm/UMachineOptions.kt | 4 + 5 files changed, 188 insertions(+), 10 deletions(-) create mode 100644 usvm-core/src/main/kotlin/org/usvm/statistics/Agent.kt diff --git a/usvm-core/build.gradle.kts b/usvm-core/build.gradle.kts index d1181e3b8c..af1ba5b2bd 100644 --- a/usvm-core/build.gradle.kts +++ b/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) diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/Agent.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/Agent.kt new file mode 100644 index 0000000000..c7d3c6644d --- /dev/null +++ b/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> ( + private val timeStatistics: TimeStatistics, + private val stepsStatistics: StepsStatistics, + private val coverage: CoverageStatistics +) : UMachineObserver { + + private val shouldStop = atomic(false) + private val serverConnection = ServerConnection(CONFIG.getUidUrl, CONFIG.saveMetricUrl) + private var methodUnderMonitoring = mutableListOf() + + 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>>{ + val statsMap = mutableMapOf>>() + + 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>>): String { + + val metricsList = mutableListOf() + + 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 +} diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt index df263e6ac1..bd3f65c50c 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt @@ -65,6 +65,8 @@ class CoverageStatistics>(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) diff --git a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt index b2989d2685..5f4bd6ccbd 100644 --- a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt +++ b/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 )