From 3aded92e451009e742f66bacdd2743108192c714 Mon Sep 17 00:00:00 2001
From: tochilinak <tochilina.2002@yandex.ru>
Date: Fri, 1 Aug 2025 15:42:26 +0300
Subject: [PATCH] Added option `throwExceptionOnStepFailure`

---
 usvm-core/src/main/kotlin/org/usvm/Machine.kt               | 6 ++++++
 usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt      | 2 +-
 .../src/main/kotlin/org/usvm/machine/PyMachine.kt           | 3 +++
 .../src/main/kotlin/org/usvm/machine/SampleMachine.kt       | 2 +-
 usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt       | 2 +-
 usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt       | 4 ++++
 6 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/Machine.kt b/usvm-core/src/main/kotlin/org/usvm/Machine.kt
index da43d71e42..775fd5b989 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Machine.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Machine.kt
@@ -15,6 +15,8 @@ val logger = object : KLogging() {}.logger
  * @see [run]
  */
 abstract class UMachine<State : UState<*, *, *, *, *, State>> : AutoCloseable {
+    abstract val options: UMachineOptions
+
     /**
      * Runs symbolic execution loop.
      *
@@ -44,6 +46,10 @@ abstract class UMachine<State : UState<*, *, *, *, *, State>> : AutoCloseable {
                     val (forkedStates, stateAlive) = try {
                         interpreter.step(state)
                     } catch (e: Throwable) {
+                        if (options.throwExceptionOnStepFailure) {
+                            throw e
+                        }
+
                         logger.error(e) { "Step failed" }
                         observer.onState(state, forks = emptySequence())
                         pathSelector.remove(state)
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 6138db8534..a3ea7395bc 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt
@@ -42,7 +42,7 @@ val logger = object : KLogging() {}.logger
 
 class JcMachine(
     cp: JcClasspath,
-    private val options: UMachineOptions,
+    override val options: UMachineOptions,
     private val jcMachineOptions: JcMachineOptions = JcMachineOptions(),
     private val interpreterObserver: JcInterpreterObserver? = null,
 ) : UMachine<JcState>() {
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt
index ed520ba387..b08db03a68 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt
@@ -2,6 +2,7 @@ package org.usvm.machine
 
 import mu.KLogging
 import org.usvm.UMachine
+import org.usvm.UMachineOptions
 import org.usvm.UPathSelector
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.language.PyCallable
@@ -44,6 +45,8 @@ class PyMachine(
     private val random = Random(0)
     val statistics = PyMachineStatistics()
 
+    override val options: UMachineOptions = UMachineOptions()
+
     private fun <PyObjectRepr> getInterpreter(
         pinnedTarget: PyPinnedCallable,
         saver: PyMachineResultsReceiver<PyObjectRepr>,
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt
index 3741d29245..0b46a57cb2 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt
@@ -31,7 +31,7 @@ import org.usvm.targets.UTargetsSet
  */
 class SampleMachine(
     program: Program,
-    private val options: UMachineOptions
+    override val options: UMachineOptions
 ) : UMachine<SampleState>() {
     private val applicationGraph = SampleApplicationGraph(program)
     private val typeSystem = SampleTypeSystem(options.typeOperationsTimeout)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
index b3d05421a7..cd7d487192 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -36,7 +36,7 @@ private val logger = KotlinLogging.logger {}
 
 class TsMachine(
     private val scene: EtsScene,
-    private val options: UMachineOptions,
+    override val options: UMachineOptions,
     private val tsOptions: TsOptions,
     private val machineObserver: UMachineObserver<TsState>? = null,
     observer: TsInterpreterObserver? = null,
diff --git a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt
index b2989d2685..9964f00aef 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,
+    /**
+     * If set to false, exception will be suppressed and the failed state will be killed.
+     * */
+    val throwExceptionOnStepFailure: Boolean = false,
 )