From c09f086f29cd3376caca970a70aa238bcc05bbe0 Mon Sep 17 00:00:00 2001 From: Dmitry Ivanov Date: Thu, 13 Jul 2023 17:55:54 +0300 Subject: [PATCH] First version of logging in USVM (#38) * First version of logging for usvm * Implementation of the JacoDB interpreter (#18) Co-authored-by: Alexey Menshutin * New path selectors infrastructure (#29) * Add general framework for weighted searchers * Add tests for AA-tree and discrete PDF * Little typo fix in tests * Add shortest distance to targets weighter * Add random tree path selector * Add fork depth path selector * Fix interleaved path selector * Add comments and some new java tests, infrastructure fixes * PR comments fixes, add solver type and timeout options * First version of logging for usvm * synchronize with master --------- Co-authored-by: Sergey Pospelov Co-authored-by: Alexey Menshutin Co-authored-by: Maksim Parshin --- buildSrc/src/main/kotlin/Versions.kt | 3 + usvm-core/build.gradle.kts | 1 + .../src/main/kotlin/org/usvm/Interpreter.kt | 2 + usvm-core/src/main/kotlin/org/usvm/Machine.kt | 54 +++++++------ usvm-jvm/build.gradle.kts | 1 + .../kotlin/org/usvm/machine/JcInterpreter.kt | 9 +++ .../main/kotlin/org/usvm/machine/JcMachine.kt | 4 + usvm-jvm/src/test/resources/logback.xml | 12 +++ usvm-sample-language/build.gradle.kts | 2 + .../main/kotlin/org/usvm/language/Domain.kt | 6 +- .../org/usvm/machine/SampleInterpreter.kt | 7 +- .../src/test/resources/logback.xml | 12 +++ usvm-util/build.gradle.kts | 1 + .../src/main/kotlin/org/usvm/util/Logging.kt | 78 +++++++++++++++++++ .../src/main/kotlin/org/usvm/util/Maybe.kt | 23 ++++++ 15 files changed, 191 insertions(+), 24 deletions(-) create mode 100644 usvm-jvm/src/test/resources/logback.xml create mode 100644 usvm-sample-language/src/test/resources/logback.xml create mode 100644 usvm-util/src/main/kotlin/org/usvm/util/Logging.kt create mode 100644 usvm-util/src/main/kotlin/org/usvm/util/Maybe.kt diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt index 46be8c841..626560b1c 100644 --- a/buildSrc/src/main/kotlin/Versions.kt +++ b/buildSrc/src/main/kotlin/Versions.kt @@ -1,10 +1,13 @@ object Versions { + const val klogging = "1.8.3" + const val slf4j = "1.6.1" const val ksmt = "0.5.3" const val collections = "0.3.5" const val coroutines = "1.6.4" const val jcdb = "1.1.3" const val mockk = "1.13.4" const val junitParams = "5.9.3" + const val logback = "1.4.8" // versions for jvm samples const val samplesLombok = "1.18.20" diff --git a/usvm-core/build.gradle.kts b/usvm-core/build.gradle.kts index 7d4ff0b8b..ef0f4b763 100644 --- a/usvm-core/build.gradle.kts +++ b/usvm-core/build.gradle.kts @@ -7,6 +7,7 @@ dependencies { api("io.ksmt:ksmt-core:${Versions.ksmt}") api("io.ksmt:ksmt-z3:${Versions.ksmt}") + api("io.github.microutils:kotlin-logging:${Versions.klogging}") implementation("org.jetbrains.kotlinx:kotlinx-collections-immutable-jvm:${Versions.collections}") testImplementation("io.mockk:mockk:${Versions.mockk}") diff --git a/usvm-core/src/main/kotlin/org/usvm/Interpreter.kt b/usvm-core/src/main/kotlin/org/usvm/Interpreter.kt index 80824b298..4b42c8b9b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Interpreter.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Interpreter.kt @@ -10,4 +10,6 @@ abstract class UInterpreter { * @return next states. */ abstract fun step(state: State): StepResult + + override fun toString(): String = this::class.simpleName?:"" } \ No newline at end of file diff --git a/usvm-core/src/main/kotlin/org/usvm/Machine.kt b/usvm-core/src/main/kotlin/org/usvm/Machine.kt index aaff135f7..679f65bde 100644 --- a/usvm-core/src/main/kotlin/org/usvm/Machine.kt +++ b/usvm-core/src/main/kotlin/org/usvm/Machine.kt @@ -1,13 +1,19 @@ package org.usvm +import mu.KLogging import org.usvm.statistics.UMachineObserver import org.usvm.stopstrategies.StopStrategy +import org.usvm.util.bracket +import org.usvm.util.debug /** * An abstract symbolic machine. * * @see [run] */ + +val logger = object : KLogging() {}.logger + abstract class UMachine : AutoCloseable { /** * Runs symbolic execution loop. @@ -28,34 +34,38 @@ abstract class UMachine : AutoCloseable { isStateTerminated: (State) -> Boolean, stopStrategy: StopStrategy = StopStrategy { false } ) { - while (!pathSelector.isEmpty() && !stopStrategy.shouldStop()) { - val state = pathSelector.peek() - val (forkedStates, stateAlive) = interpreter.step(state) + logger.debug().bracket("$this.run($interpreter, ${pathSelector::class.simpleName})") { + while (!pathSelector.isEmpty() && !stopStrategy.shouldStop()) { + val state = pathSelector.peek() + val (forkedStates, stateAlive) = interpreter.step(state) - observer.onState(state, forkedStates) + observer.onState(state, forkedStates) - val originalStateAlive = stateAlive && !isStateTerminated(state) - val aliveForkedStates = mutableListOf() - for (forkedState in forkedStates) { - if (!isStateTerminated(forkedState)) { - aliveForkedStates.add(forkedState) - } else { - // TODO: distinguish between states terminated by exception (runtime or user) and - // those which just exited - observer.onStateTerminated(forkedState) + val originalStateAlive = stateAlive && !isStateTerminated(state) + val aliveForkedStates = mutableListOf() + for (forkedState in forkedStates) { + if (!isStateTerminated(forkedState)) { + aliveForkedStates.add(forkedState) + } else { + // TODO: distinguish between states terminated by exception (runtime or user) and + // those which just exited + observer.onStateTerminated(forkedState) + } } - } - if (originalStateAlive) { - pathSelector.update(state) - } else { - pathSelector.remove(state) - observer.onStateTerminated(state) - } + if (originalStateAlive) { + pathSelector.update(state) + } else { + pathSelector.remove(state) + observer.onStateTerminated(state) + } - if (aliveForkedStates.isNotEmpty()) { - pathSelector.add(aliveForkedStates) + if (aliveForkedStates.isNotEmpty()) { + pathSelector.add(aliveForkedStates) + } } } } + + override fun toString(): String = this::class.simpleName?:"" } diff --git a/usvm-jvm/build.gradle.kts b/usvm-jvm/build.gradle.kts index c2ded10de..e597ac2b5 100644 --- a/usvm-jvm/build.gradle.kts +++ b/usvm-jvm/build.gradle.kts @@ -13,6 +13,7 @@ dependencies { testImplementation("io.mockk:mockk:${Versions.mockk}") testImplementation("org.junit.jupiter:junit-jupiter-params:${Versions.junitParams}") + testImplementation("ch.qos.logback:logback-classic:${Versions.logback}") // https://mvnrepository.com/artifact/org.burningwave/core // Use it to export all modules to all diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt index 4417db0b2..cf79ab9b2 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt @@ -1,6 +1,7 @@ package org.usvm.machine import io.ksmt.utils.asExpr +import mu.KLogging import org.jacodb.api.JcField import org.jacodb.api.JcMethod import org.jacodb.api.JcRefType @@ -43,6 +44,11 @@ class JcInterpreter( private val ctx: JcContext, private val applicationGraph: JcApplicationGraph, ) : UInterpreter() { + + companion object { + val logger = object : KLogging() {}.logger + } + fun getInitialState(method: JcMethod): JcState { val state = JcState(ctx) state.addEntryMethodCall(applicationGraph, method) @@ -79,6 +85,9 @@ class JcInterpreter( override fun step(state: JcState): StepResult { val stmt = state.lastStmt + + logger.debug("Step: {}", stmt) + val scope = StepScope(state) // handle exception firstly diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt index eec62a9af..9a7c11a76 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt @@ -1,5 +1,6 @@ package org.usvm.machine +import mu.KLogging import org.jacodb.api.JcClasspath import org.jacodb.api.JcMethod import org.jacodb.api.cfg.JcInst @@ -19,6 +20,8 @@ import org.usvm.statistics.PathsTreeStatistics import org.usvm.statistics.UMachineObserver import org.usvm.stopstrategies.createStopStrategy +val logger = object : KLogging() {}.logger + class JcMachine( cp: JcClasspath, private val options: UMachineOptions @@ -36,6 +39,7 @@ class JcMachine( fun analyze( method: JcMethod ): List { + logger.debug("$this.analyze($method)") val initialState = interpreter.getInitialState(method) // TODO: now paths tree doesn't support parallel execution processes. It should be replaced with forest diff --git a/usvm-jvm/src/test/resources/logback.xml b/usvm-jvm/src/test/resources/logback.xml new file mode 100644 index 000000000..cf11c9cba --- /dev/null +++ b/usvm-jvm/src/test/resources/logback.xml @@ -0,0 +1,12 @@ + + + + + %d{HH:mm:ss.SSS} |%.-1level| %replace(%c{0}){'(\$Companion)?\$logger\$1',''} - %msg%n + + + + + + + \ No newline at end of file diff --git a/usvm-sample-language/build.gradle.kts b/usvm-sample-language/build.gradle.kts index 2c4e4515a..6e78313d9 100644 --- a/usvm-sample-language/build.gradle.kts +++ b/usvm-sample-language/build.gradle.kts @@ -10,5 +10,7 @@ dependencies { // implementation("io.ksmt:ksmt-cvc5:${Versions.ksmt}") // implementation("io.ksmt:ksmt-bitwuzla:${Versions.ksmt}") + implementation(group = "org.slf4j", name = "slf4j-simple", version = Versions.slf4j) implementation("org.jetbrains.kotlinx:kotlinx-collections-immutable-jvm:${Versions.collections}") + testImplementation("ch.qos.logback:logback-classic:${Versions.logback}") } \ No newline at end of file diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/language/Domain.kt b/usvm-sample-language/src/main/kotlin/org/usvm/language/Domain.kt index 7123848a8..6491d2fe7 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/language/Domain.kt +++ b/usvm-sample-language/src/main/kotlin/org/usvm/language/Domain.kt @@ -11,7 +11,11 @@ class Method( val argumentsTypes: List, val returnType: R, val body: Body?, -) +) { + override fun toString(): String { + return "$name(${argumentsTypes.joinToString()}): $returnType" + } +} class Body( var registersCount: Int, diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleInterpreter.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleInterpreter.kt index c0780d595..5ac9a2000 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleInterpreter.kt +++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleInterpreter.kt @@ -1,5 +1,6 @@ package org.usvm.machine +import mu.KLogging import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UContext @@ -15,6 +16,8 @@ import org.usvm.language.SetValue typealias SampleStepScope = StepScope> + +val logger = object : KLogging() {}.logger /** * Symbolic interpreter for a sample language. */ @@ -30,7 +33,9 @@ class SampleInterpreter( */ override fun step(state: SampleState): StepResult { val scope = StepScope(state) - when (val stmt = state.lastStmt) { + val stmt = state.lastStmt + logger.debug { "step: $stmt" } + when (stmt) { is Call -> visitCall(scope, stmt) is Goto -> visitGoto(scope, stmt) is If -> visitIf(scope, stmt) diff --git a/usvm-sample-language/src/test/resources/logback.xml b/usvm-sample-language/src/test/resources/logback.xml new file mode 100644 index 000000000..cf11c9cba --- /dev/null +++ b/usvm-sample-language/src/test/resources/logback.xml @@ -0,0 +1,12 @@ + + + + + %d{HH:mm:ss.SSS} |%.-1level| %replace(%c{0}){'(\$Companion)?\$logger\$1',''} - %msg%n + + + + + + + \ No newline at end of file diff --git a/usvm-util/build.gradle.kts b/usvm-util/build.gradle.kts index 4a454300c..320c83e0d 100644 --- a/usvm-util/build.gradle.kts +++ b/usvm-util/build.gradle.kts @@ -3,6 +3,7 @@ plugins { } dependencies { + implementation(group = "io.github.microutils", name = "kotlin-logging", version = Versions.klogging) implementation("org.jetbrains.kotlinx:kotlinx-collections-immutable-jvm:${Versions.collections}") testImplementation("io.mockk:mockk:${Versions.mockk}") testImplementation("org.junit.jupiter:junit-jupiter-params:${Versions.junitParams}") diff --git a/usvm-util/src/main/kotlin/org/usvm/util/Logging.kt b/usvm-util/src/main/kotlin/org/usvm/util/Logging.kt new file mode 100644 index 000000000..cd7432232 --- /dev/null +++ b/usvm-util/src/main/kotlin/org/usvm/util/Logging.kt @@ -0,0 +1,78 @@ +package org.usvm.util + +import mu.KLogger + +class LoggerWithLogMethod(val logger: KLogger, val logMethod: (() -> Any?) -> Unit) + +fun KLogger.info(): LoggerWithLogMethod = LoggerWithLogMethod(this, this::info) +fun KLogger.debug(): LoggerWithLogMethod = LoggerWithLogMethod(this, this::debug) +fun KLogger.trace(): LoggerWithLogMethod = LoggerWithLogMethod(this, this::trace) + +fun elapsedSecFrom(startNano: Long): String { + val elapsedNano = System.nanoTime() - startNano + val elapsedS = elapsedNano.toDouble() / 1_000_000_000 + return String.format("%.3f", elapsedS) + " sec" +} + +/** + * Structured logging. + * + * Usage: `logger.info().bracket("message") { ... block_of_code ...}` + * + * Results in + * + * ``` + * Started: message + * -- other messages inside block of code + * Finished (in xxx.xxx sec): message + * ``` + * + * Method can handle exceptions and nonlocal returns from inline lambda + * You can use [closingComment] to add some result-depending comment to "Finished:" message. Special "" comment + * is added if nonlocal return happened in [block] + */ +inline fun LoggerWithLogMethod.bracket( + msg: String, + crossinline closingComment: (Result) -> Any? = { "" }, + block: () -> T +): T { + logMethod { "Started: $msg" } + val startNano = System.nanoTime() + var alreadyLogged = false + + var res : Maybe = Maybe.empty() + try { + // Note: don't replace this one with runCatching, otherwise return from lambda breaks "finished" logging. + res = Maybe(block()) + return res.getOrThrow() + } catch (t: Throwable) { + logMethod { "Finished (in ${elapsedSecFrom(startNano)}): $msg :: EXCEPTION :: ${closingComment(Result.failure(t))}" } + alreadyLogged = true + throw t + } finally { + if (!alreadyLogged) { + if (res.hasValue) + logMethod { "Finished (in ${elapsedSecFrom(startNano)}): $msg ${closingComment(Result.success(res.getOrThrow()))}" } + else + logMethod { "Finished (in ${elapsedSecFrom(startNano)}): $msg " } + } + } +} + +inline fun KLogger.catchException(block: () -> T): T? { + return try { + block() + } catch (e: Throwable) { + this.error(e) { "Isolated" } + null + } +} + +inline fun KLogger.logException(block: () -> T): T { + return try { + block() + } catch (e: Throwable) { + this.error("Exception occurred", e) + throw e + } +} \ No newline at end of file diff --git a/usvm-util/src/main/kotlin/org/usvm/util/Maybe.kt b/usvm-util/src/main/kotlin/org/usvm/util/Maybe.kt new file mode 100644 index 000000000..c630f4d4d --- /dev/null +++ b/usvm-util/src/main/kotlin/org/usvm/util/Maybe.kt @@ -0,0 +1,23 @@ +package org.usvm.util + +/** + * Analogue of java's [java.util.Optional] + */ +class Maybe private constructor(val hasValue: Boolean, val value:T? ) { + constructor(v: T) : this(true, v) + companion object { + fun empty() = Maybe(false, null) + } + + /** + * Returns [value] if [hasValue]. Otherwise, throws exception + */ + @Suppress("UNCHECKED_CAST") + fun getOrThrow() : T = if (!hasValue) { + error("Maybe hasn't value") + } else { + value as T + } + + override fun toString(): String = if (hasValue) "Maybe($value)" else "" +} \ No newline at end of file