First version of logging in USVM (#38)

* First version of logging for usvm * Implementation of the JacoDB interpreter (#18) Co-authored-by: Alexey Menshutin <[email protected]> * 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 <[email protected]> Co-authored-by: Alexey Menshutin <[email protected]> Co-authored-by: Maksim Parshin <[email protected]>
UnitTestBot · Jul 13, 2023 · c09f086 · c09f086
1 parent 34e6503
commit c09f086
Show file tree

Hide file tree

Showing 15 changed files with 191 additions and 24 deletions.
diff --git 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
@@ -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
@@ -10,4 +10,6 @@ abstract class UInterpreter<State> {
      * @return next states.
      */
     abstract fun step(state: State): StepResult<State>
+
+    override fun toString(): String = this::class.simpleName?:"<empty>"
 }
diff --git 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<State> : AutoCloseable {
     /**
      * Runs symbolic execution loop.
@@ -28,34 +34,38 @@ abstract class UMachine<State> : 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<State>()
-            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<State>()
+                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?:"<empty>"
 }
diff --git 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
@@ -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<JcState>() {
+
+    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<JcState> {
         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
@@ -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<JcState> {
+        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
@@ -0,0 +1,12 @@
+<configuration>
+    <appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
+        <encoder>
+<!--        Refer to this to choose your pattern: https://logback.qos.ch/manual/layouts.html -->
+            <pattern>%d{HH:mm:ss.SSS} |%.-1level| %replace(%c{0}){'(\$Companion)?\$logger\$1',''} - %msg%n</pattern>
+        </encoder>
+    </appender>
+
+    <root level="debug">
+        <appender-ref ref="STDOUT" />
+    </root>
+</configuration>
diff --git 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}")
 }
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
@@ -11,7 +11,11 @@ class Method<out R : SampleType?>(
     val argumentsTypes: List<SampleType>,
     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
@@ -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<SampleState, SampleType, Field<*>>
 
+
+val logger = object : KLogging() {}.logger
 /**
  * Symbolic interpreter for a sample language.
  */
@@ -30,7 +33,9 @@ class SampleInterpreter(
      */
     override fun step(state: SampleState): StepResult<SampleState> {
         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
@@ -0,0 +1,12 @@
+<configuration>
+    <appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
+        <encoder>
+<!--        Refer to this to choose your pattern: https://logback.qos.ch/manual/layouts.html -->
+            <pattern>%d{HH:mm:ss.SSS} |%.-1level| %replace(%c{0}){'(\$Companion)?\$logger\$1',''} - %msg%n</pattern>
+        </encoder>
+    </appender>
+
+    <root level="debug">
+        <appender-ref ref="STDOUT" />
+    </root>
+</configuration>
diff --git 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
@@ -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 "<Nothing>" comment
+ * is added if nonlocal return happened in [block]
+ */
+inline fun <T> LoggerWithLogMethod.bracket(
+    msg: String,
+    crossinline closingComment: (Result<T>) -> Any? = { "" },
+    block: () -> T
+): T {
+    logMethod { "Started: $msg" }
+    val startNano = System.nanoTime()
+    var alreadyLogged = false
+
+    var res : Maybe<T> = 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 <Nothing>" }
+        }
+    }
+}
+
+inline fun <T> KLogger.catchException(block: () -> T): T? {
+    return try {
+        block()
+    } catch (e: Throwable) {
+        this.error(e) { "Isolated" }
+        null
+    }
+}
+
+inline fun <T> KLogger.logException(block: () -> T): T {
+    return try {
+        block()
+    } catch (e: Throwable) {
+        this.error("Exception occurred", e)
+        throw e
+    }
+}
diff --git a/usvm-util/src/main/kotlin/org/usvm/util/Maybe.kt 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<out T> 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 "<empty>"
+}