Checkers API

usvm-core/src/main/kotlin/org/usvm/State.kt

@@ -156,7 +156,7 @@ private fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext<*>>
     } else {
         newConstraintToOriginalState
     }
-    val solver = newConstraintToForkedState.uctx.solver<Type>()
+    val solver = state.ctx.solver<Type>()
     val satResult = solver.checkWithSoftConstraints(constraintsToCheck)
 
     return when (satResult) {
@@ -214,7 +214,7 @@ fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext<*>> fork(
         holdsInModel.isTrue
     }
 
-    val notCondition = condition.uctx.mkNot(condition)
+    val notCondition = state.ctx.mkNot(condition)
     val (posState, negState) = when {
 
         trueModels.isNotEmpty() && falseModels.isNotEmpty() -> {

usvm-core/src/main/kotlin/org/usvm/StepScope.kt

@@ -207,6 +207,19 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
         return forkMulti(filteredConditionsWithBlockOnStates)
     }
 
+    /**
+     * [assert]s the [condition] on the scope with the cloned [originalState]. Returns this cloned state, if this [condition]
+     * is satisfiable, and returns `null` otherwise.
+     */
+    fun checkSat(condition: UBoolExpr): T? {
+        val conditionalState = originalState.clone()
+        val conditionalScope = StepScope(conditionalState, forkBlackList)
+
+        return conditionalScope.assert(condition)?.let {
+            conditionalState
+        }
+    }
+
     /**
      * Represents the current state of this [StepScope].
      */

usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcChecker.kt

@@ -0,0 +1,50 @@
+package org.usvm.api.checkers
+
+import org.jacodb.api.JcClasspath
+import org.jacodb.api.JcMethod
+import org.jacodb.api.JcType
+import org.jacodb.api.cfg.JcInstVisitor
+import org.jacodb.api.cfg.JcValue
+import org.usvm.UBoolExpr
+import org.usvm.UExpr
+import org.usvm.UMachineOptions
+import org.usvm.api.targets.JcTarget
+import org.usvm.machine.JcContext
+import org.usvm.machine.JcMachine
+import org.usvm.memory.UReadOnlyMemory
+
+sealed interface JcCheckerResult {
+    // Has no data for now
+}
+
+interface JcCheckerSatResult : JcCheckerResult
+interface JcCheckerUnsatResult : JcCheckerResult
+interface JcCheckerUnknownResult : JcCheckerResult
+
+interface JcCheckerApi {
+    val ctx: JcContext
+    val memory: UReadOnlyMemory<JcType>
+
+    fun resolveValue(value: JcValue): UExpr<*>
+    fun checkSat(condition: UBoolExpr): JcCheckerResult
+}
+
+class JcCheckerRunner(val cp: JcClasspath) {
+    private val apiImpl = JcCheckerApiImpl()
+
+    val api: JcCheckerApi
+        get() = apiImpl
+
+    fun <T> runChecker(
+        entryPoint: JcMethod,
+        checkersVisitor: JcInstVisitor<T>,
+        targets: List<JcTarget> = emptyList(),
+        options: UMachineOptions = UMachineOptions(),
+    ) {
+        val checkersObserver = JcCheckerObserver(checkersVisitor, apiImpl)
+
+        JcMachine(cp, options, checkersObserver).use { machine ->
+            machine.analyze(entryPoint, targets)
+        }
+    }
+}

usvm-jvm/src/main/kotlin/org/usvm/api/checkers/JcCheckerImpl.kt

@@ -0,0 +1,183 @@
+package org.usvm.api.checkers
+
+import org.jacodb.api.JcType
+import org.jacodb.api.cfg.JcAssignInst
+import org.jacodb.api.cfg.JcCallExpr
+import org.jacodb.api.cfg.JcCallInst
+import org.jacodb.api.cfg.JcCatchInst
+import org.jacodb.api.cfg.JcEnterMonitorInst
+import org.jacodb.api.cfg.JcExitMonitorInst
+import org.jacodb.api.cfg.JcGotoInst
+import org.jacodb.api.cfg.JcIfInst
+import org.jacodb.api.cfg.JcInstVisitor
+import org.jacodb.api.cfg.JcReturnInst
+import org.jacodb.api.cfg.JcSwitchInst
+import org.jacodb.api.cfg.JcThrowInst
+import org.jacodb.api.cfg.JcValue
+import org.usvm.UBoolExpr
+import org.usvm.UExpr
+import org.usvm.machine.JcContext
+import org.usvm.machine.JcInterpreterObserver
+import org.usvm.machine.JcMethodCallBaseInst
+import org.usvm.machine.JcMethodEntrypointInst
+import org.usvm.machine.interpreter.JcSimpleValueResolver
+import org.usvm.machine.interpreter.JcStepScope
+import org.usvm.memory.UReadOnlyMemory
+
+internal class JcCheckerApiImpl : JcCheckerApi {
+    // TODO How to retrieve it properly?
+    private var internalStepScope: JcStepScope? = null
+    private var internalExprResolver: JcSimpleValueResolver? = null
+
+    private val stepScope: JcStepScope
+        get() = ensureProcessing(internalStepScope)
+
+    private val exprResolver: JcSimpleValueResolver
+        get() = ensureProcessing(internalExprResolver)
+
+    private fun <T> ensureProcessing(e: T?): T =
+        e ?: error("Checker API can be used during instruction processing only")
+
+    override val ctx: JcContext
+        get() = stepScope.calcOnState { ctx }
+
+    override val memory: UReadOnlyMemory<JcType>
+        get() = stepScope.calcOnState { memory }
+
+    override fun resolveValue(value: JcValue): UExpr<*> = value.accept(exprResolver)
+
+    override fun checkSat(condition: UBoolExpr): JcCheckerResult =
+        stepScope.checkSat(condition)?.let {
+            JcCheckerSatResultImpl
+        } ?: JcCheckerUnsatResultImpl
+
+    internal fun setResolverAndScope(simpleValueResolver: JcSimpleValueResolver, stepScope: JcStepScope) {
+        internalExprResolver = simpleValueResolver
+        internalStepScope = stepScope
+    }
+
+    internal fun resetResolverAndScope() {
+        internalStepScope = null
+        internalExprResolver = null
+    }
+}
+
+internal object JcCheckerSatResultImpl : JcCheckerSatResult
+internal object JcCheckerUnsatResultImpl : JcCheckerUnsatResult
+internal object JcCheckerUnknownSatResultImpl : JcCheckerUnknownResult
+
+internal class JcCheckerObserver<T>(
+    private val visitor: JcInstVisitor<T>,
+    private val jcCheckerApi: JcCheckerApiImpl,
+) : JcInterpreterObserver {
+    override fun onAssignStatement(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcAssignInst,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcAssignInst(stmt) }
+    }
+
+    override fun onEntryPoint(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcMethodEntrypointInst,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) {
+            // Looks like we do not need this signal in the ast-based checker
+        }
+    }
+
+    override fun onMethodCallWithUnresolvedArguments(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcCallExpr,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) {
+            // Looks like we do not need this signal in the ast-based checker
+        }
+    }
+
+    override fun onMethodCallWithResolvedArguments(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcMethodCallBaseInst,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) {
+            // Looks like we do not need this signal in the ast-based checker
+        }
+    }
+
+    override fun onIfStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcIfInst, stepScope: JcStepScope) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcIfInst(stmt) }
+    }
+
+    override fun onReturnStatement(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcReturnInst,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcReturnInst(stmt) }
+    }
+
+    override fun onGotoStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcGotoInst, stepScope: JcStepScope) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcGotoInst(stmt) }
+    }
+
+    override fun onCatchStatement(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcCatchInst,
+        stepScope: JcStepScope
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcCatchInst(stmt) }
+    }
+
+    override fun onSwitchStatement(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcSwitchInst,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcSwitchInst(stmt) }
+    }
+
+    override fun onThrowStatement(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcThrowInst,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcThrowInst(stmt) }
+    }
+
+    override fun onCallStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallInst, stepScope: JcStepScope) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcCallInst(stmt) }
+    }
+
+    override fun onEnterMonitorStatement(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcEnterMonitorInst,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcEnterMonitorInst(stmt) }
+    }
+
+    override fun onExitMonitorStatement(
+        simpleValueResolver: JcSimpleValueResolver,
+        stmt: JcExitMonitorInst,
+        stepScope: JcStepScope,
+    ) {
+        withScopeAndResolver(simpleValueResolver, stepScope) { visitor.visitJcExitMonitorInst(stmt) }
+    }
+
+    // TODO it's very dirty way to get required fields, rewrite
+    private inline fun withScopeAndResolver(
+        simpleValueResolver: JcSimpleValueResolver,
+        stepScope: JcStepScope,
+        blockOnStmt: () -> Unit
+    ) = try {
+        jcCheckerApi.setResolverAndScope(simpleValueResolver, stepScope)
+
+        blockOnStmt()
+    } finally {
+        jcCheckerApi.resetResolverAndScope()
+    }
+}

usvm-jvm/src/main/kotlin/org/usvm/api/targets/TaintAnalysis.kt

@@ -96,10 +96,10 @@ class TaintAnalysis(
             state.targets.filter { it in targets }
         }.orEmpty().toList().uncheckedCast()
 
-    override fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {
+    override fun onAssignStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {
         // Sinks are already processed at this moment since we resolved it on a call statement
 
-        stmt.callExpr?.let { processTaintConfiguration(it, stepScope, exprResolver) }
+        stmt.callExpr?.let { processTaintConfiguration(it, stepScope, simpleValueResolver) }
 
         // TODO add fields processing
     }
@@ -241,15 +241,10 @@ class TaintAnalysis(
 
         val resolvedCondition = stepScope.ctx.mkAnd(resolvedConfigCondition, resolvedSinkCondition)
 
-        val (originalStateCopy, taintedStepScope) = stepScope.calcOnState {
-            val originalStateCopy = clone()
-            originalStateCopy to JcStepScope(originalStateCopy, UForkBlackList.createDefault())
-        }
-
-        taintedStepScope.assert(resolvedCondition)?.let {
+        stepScope.checkSat(resolvedCondition)?.let { taintedState ->
             // TODO remove corresponding target
-            collectedStates += originalStateCopy
-            target?.propagate(taintedStepScope.state)
+            collectedStates += taintedState
+            target?.propagate(taintedState)
         }
     }
 

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

@@ -3,6 +3,7 @@ package org.usvm.machine
 import org.jacodb.api.cfg.JcAssignInst
 import org.jacodb.api.cfg.JcCallExpr
 import org.jacodb.api.cfg.JcCallInst
+import org.jacodb.api.cfg.JcCatchInst
 import org.jacodb.api.cfg.JcEnterMonitorInst
 import org.jacodb.api.cfg.JcExitMonitorInst
 import org.jacodb.api.cfg.JcGotoInst
@@ -15,14 +16,14 @@ import org.usvm.machine.interpreter.JcStepScope
 import org.usvm.statistics.UInterpreterObserver
 
 interface JcInterpreterObserver : UInterpreterObserver {
-    fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {}
+    fun onAssignStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {}
     fun onEntryPoint(simpleValueResolver: JcSimpleValueResolver, stmt: JcMethodEntrypointInst, stepScope: JcStepScope)
     fun onMethodCallWithUnresolvedArguments(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallExpr, stepScope: JcStepScope) {}
     fun onMethodCallWithResolvedArguments(simpleValueResolver: JcSimpleValueResolver, stmt: JcMethodCallBaseInst, stepScope: JcStepScope) {}
     fun onIfStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcIfInst, stepScope: JcStepScope) {}
     fun onReturnStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcReturnInst, stepScope: JcStepScope) {}
     fun onGotoStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcGotoInst, stepScope: JcStepScope) {}
-    fun onCatchStatement(simpleValueResolver: JcSimpleValueResolver, stepScope: JcStepScope) {}
+    fun onCatchStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCatchInst, stepScope: JcStepScope) {}
     fun onSwitchStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcSwitchInst, stepScope: JcStepScope) {}
     fun onThrowStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcThrowInst, stepScope: JcStepScope) {}
     fun onCallStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallInst, stepScope: JcStepScope) {}

usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt

@@ -278,7 +278,7 @@ class JcInterpreter(
                 is JcMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
                 is JcMethodResult.JcException -> error("Exceptions must be processed earlier")
             }
-        }
+        } ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
 
         val lvalue = exprResolver.resolveLValue(stmt.lhv) ?: return
         val expr = exprResolver.resolveJcExpr(stmt.rhv, stmt.lhv.type) ?: return