Remove redundant code

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

@@ -8,7 +8,7 @@ import org.usvm.types.UTypeSystem
 
 /**
  * Provides core USVM components tuned for specific language.
- * Instatiated once per [UContext].
+ * Instantiated once per [UContext].
  */
 interface UComponents<Type> {
     fun mkSolver(ctx: UContext): USolverBase<Type>

usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt

@@ -44,8 +44,6 @@ fun <ArrayType, Sort : USort> UWritableMemory<*>.writeArrayIndex(
     ref: UHeapRef, index: USizeExpr, type: ArrayType, sort: Sort, value: UExpr<Sort>, guard: UBoolExpr
 ) = write(UArrayIndexLValue(sort, ref, index, type), value, guard)
 
-// TODO move it here
-
 fun <ArrayType> UWritableMemory<*>.writeArrayLength(
     ref: UHeapRef, size: USizeExpr, arrayType: ArrayType
 ) = write(UArrayLengthLValue(ref, arrayType), size, ref.uctx.trueExpr)

usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt

@@ -7,17 +7,12 @@ import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UHeapRef
-import org.usvm.UMockEvaluator
 import org.usvm.constraints.UEqualityConstraints
 import org.usvm.constraints.UPathConstraints
 import org.usvm.isFalse
 import org.usvm.isTrue
-import org.usvm.memory.UMemoryRegionId
-import org.usvm.memory.UReadOnlyMemoryRegion
-import org.usvm.memory.UReadOnlyRegistersStack
 import org.usvm.model.UModelBase
 import org.usvm.model.UModelDecoder
-import org.usvm.model.UTypeModel
 
 sealed interface USolverResult<out T>
 
@@ -41,17 +36,6 @@ open class USolverBase<Type>(
     protected val decoder: UModelDecoder<UModelBase<Type>>,
     protected val softConstraintsProvider: USoftConstraintsProvider<Type>,
 ) : USolver<UPathConstraints<Type>, UModelBase<Type>>(), AutoCloseable {
-    // TODO remove it
-    protected open val modelBuilder: (
-        ctx: UContext,
-        UReadOnlyRegistersStack,
-        UTypeModel<Type>,
-        UMockEvaluator,
-        Map<UMemoryRegionId<*, *>, UReadOnlyMemoryRegion<*, *>>,
-        UConcreteHeapRef,
-    ) -> UModelBase<Type> = { ctx, stack, types, mocker, regions, nullRef ->
-        UModelBase(ctx, stack, types, mocker, regions, nullRef)
-    }
 
     protected fun translateLogicalConstraints(constraints: Iterable<UBoolExpr>) {
         for (constraint in constraints) {
@@ -179,7 +163,7 @@ open class USolverBase<Type>(
                 // fourth, check it satisfies typeConstraints
                 when (val typeResult = typeSolver.check(typeSolverQuery)) {
                     is USatResult -> return USatResult(
-                        modelBuilder(
+                        UModelBase(
                             ctx,
                             uModel.stack,
                             typeResult.model,

usvm-core/src/main/kotlin/org/usvm/statistics/UInterpreterObserver.kt

@@ -1,5 +1,5 @@
 package org.usvm.statistics
 
 interface UInterpreterObserver {
-
+    // Empty
 }

usvm-core/src/main/kotlin/org/usvm/targets/UTargetController.kt

@@ -1,6 +1,5 @@
 package org.usvm.targets
 
-// TODO add self generic for the controller
 interface UTargetController {
     val targets: MutableCollection<out UTarget<*, *, *>>
 }

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

@@ -24,9 +24,8 @@ import org.usvm.machine.state.JcState
 import org.usvm.statistics.UMachineObserver
 import org.usvm.targets.UTargetController
 
-// TODO do we need a context here?
 class TaintAnalysis(
-    private val configuration: TaintConfiguration,// TODO how to pass initial targets????
+    private val configuration: TaintConfiguration,
     override val targets: MutableCollection<TaintTarget> = mutableListOf(),
 ) : UTargetController, JcInterpreterObserver, UMachineObserver<JcState> {
     private val taintTargets: MutableMap<JcInst, MutableSet<TaintTarget>> = mutableMapOf()
@@ -37,9 +36,6 @@ class TaintAnalysis(
         }
     }
 
-    // TODO recursively add children here???????????????????????????????????????
-    // TODO add recursively children at the beginning????????????????????????????????????????????????????????????????
-
     // TODO save mapping between initial targets and the states that reach them
     //      Replace with the corresponding observer-collector?
     val collectedStates: MutableList<JcState> = mutableListOf()
@@ -98,7 +94,7 @@ class TaintAnalysis(
         }.orEmpty().toList().uncheckedCast()
 
     override fun onAssignStatement(exprResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {
-        // Sinks are already processed at this moment since we resolved it on call statement
+        // Sinks are already processed at this moment since we resolved it on a call statement
 
         stmt.callExpr?.let { processTaintConfiguration(it, stepScope, exprResolver) }
 
@@ -114,7 +110,9 @@ class TaintAnalysis(
         val methodResult = stepScope.calcOnState { methodResult }
         val method = callExpr.method.method
 
-        require(methodResult is JcMethodResult.Success) { "TODO message" }
+        require(methodResult is JcMethodResult.Success) {
+            "Other result statuses must be processed in `onMethodCallWithUnresolvedArguments`"
+        }
 
         val callPositionResolver = createCallPositionResolver(ctx, callExpr, simpleValueResolver, methodResult)
 
@@ -138,34 +136,32 @@ class TaintAnalysis(
         sourceConfigurations?.forEach {
             val target = sourceTargets[it]
 
-            val (condition, action) = it.conditionWithAction
-            val resolvedCondition = conditionResolver.visit(condition, simpleValueResolver, stepScope) ?: ctx.trueExpr
+            val resolvedCondition =
+                conditionResolver.visit(it.condition, simpleValueResolver, stepScope) ?: ctx.trueExpr
 
             val targetCondition = target?.condition ?: ConstantTrue
             val resolvedTargetCondition =
                 conditionResolver.visit(targetCondition, simpleValueResolver, stepScope) ?: ctx.trueExpr
 
             val combinedCondition = ctx.mkAnd(resolvedTargetCondition, resolvedCondition)
 
-            action.accept(actionResolver, stepScope, combinedCondition)
+            it.action.accept(actionResolver, stepScope, combinedCondition)
 
             target?.propagate(stepScope.state)
         }
 
         val cleanerConfigurations = configuration.cleaners[method]
         cleanerConfigurations?.forEach {
-            val (condition, action) = it.conditionWithAction
-            val resolvedCondition = conditionResolver.visit(condition, simpleValueResolver, stepScope)
+            val resolvedCondition = conditionResolver.visit(it.condition, simpleValueResolver, stepScope)
 
-            action.accept(actionResolver, stepScope, resolvedCondition)
+            it.action.accept(actionResolver, stepScope, resolvedCondition)
         }
 
         val passThroughConfigurations = configuration.passThrough[method]
         passThroughConfigurations?.forEach {
-            val (condition, action) = it.conditionWithAction
-            val resolvedCondition = conditionResolver.visit(condition, simpleValueResolver, stepScope)
+            val resolvedCondition = conditionResolver.visit(it.condition, simpleValueResolver, stepScope)
 
-            action.accept(actionResolver, stepScope, resolvedCondition)
+            it.action.accept(actionResolver, stepScope, resolvedCondition)
         }
     }
 
@@ -190,19 +186,15 @@ class TaintAnalysis(
         // TODO entry point configuration
     }
 
-    // TODO documentation, but looks like sinks should be processed here since
-    //      otherwise some extra conditions might be added during the parameters resolving (e.g., non-null
-    //      constraint in virtual invokes
     override fun onMethodCallWithUnresolvedArguments(
         simpleValueResolver: JcSimpleValueResolver,
         stmt: JcCallExpr,
         stepScope: JcStepScope,
     ) {
-        // TODO add comment about absence of configuration
         val method = stmt.method.method
 
         val methodResult = stepScope.calcOnState { methodResult }
-        require(methodResult is JcMethodResult.NoCall) { "TODO" }
+        require(methodResult is JcMethodResult.NoCall) { "This signal must be sent before the method call" }
 
         val ctx = stepScope.ctx
 
@@ -213,10 +205,11 @@ class TaintAnalysis(
             val currentStatement = stepScope.calcOnState { currentStatement }
             val targets = findTaintTargets(currentStatement, stepScope.state)
 
-            val sinks = targets.filterIsInstance<TaintMethodSinkTarget>()
-            sinks.forEach {
-                processSink(it.configRule, it.condition, conditionResolver, simpleValueResolver, stepScope, it)
-            }
+            targets
+                .filterIsInstance<TaintMethodSinkTarget>()
+                .forEach {
+                    processSink(it.configRule, it.condition, conditionResolver, simpleValueResolver, stepScope, it)
+                }
         } else {
             val methodSinks = configuration.methodSinks[method] ?: return
             methodSinks.forEach {
@@ -252,7 +245,6 @@ class TaintAnalysis(
 
         taintedStepScope.assert(resolvedCondition)?.let {
             // TODO remove corresponding target
-            // TODO probably, we should terminate this state? Yes, we should
             collectedStates += originalStateCopy
             target?.propagate(taintedStepScope.state)
         }
@@ -263,32 +255,23 @@ class TaintAnalysis(
         stmt: JcMethodCallBaseInst,
         stepScope: JcStepScope,
     ) {
-        // TODO message, it is a redundant signal
+        // It is a redundant signal
     }
 
     override fun onCallStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallInst, stepScope: JcStepScope) {
         processTaintConfiguration(stmt.callExpr, stepScope, simpleValueResolver)
     }
 
-    override fun onStateProcessed(
-        simpleValueResolver: () -> JcSimpleValueResolver,
-        stmt: JcInst,
-        stepScope: JcStepScope,
-    ) {
-        // TODO for now, we might process each target several times if we have a transition with the same instruction
-        //      and different path constraints
-
-    }
-
     override fun onState(parent: JcState, forks: Sequence<JcState>) {
         propagateIntermediateTarget(parent)
 
         forks.forEach { propagateIntermediateTarget(it) }
     }
 
     private fun propagateIntermediateTarget(state: JcState) {
-        // TODO add comment why is it safe
-        val targets = findTaintTargets(state.pathLocation.parent!!.statement, state)
+        val parent = state.pathLocation.parent ?: error("This is impossible by construction")
+        val targets = findTaintTargets(parent.statement, state)
+
         targets.forEach {
             when (it) {
                 is TaintIntermediateTarget -> it.propagate(state)
@@ -297,31 +280,26 @@ class TaintAnalysis(
         }
     }
 
-    sealed class TaintTarget(
-        location: JcInst,
-    ) : JcTarget<TaintAnalysis>(location)
+    private fun resolveCallInstance(
+        callExpr: JcCallExpr,
+    ) = if (callExpr is JcInstanceCallExpr) callExpr.instance else null
+
+    sealed class TaintTarget(location: JcInst) : JcTarget<TaintAnalysis>(location)
 
     class TaintMethodSourceTarget(
         location: JcInst,
         val condition: Condition,
         val configurationRule: TaintMethodSource,
     ) : TaintTarget(location)
-    // TODO add field source targets
-
-    class TaintIntermediateTarget(location: JcInst) : TaintTarget(location) {
+    // TODO add field sources and sinks targets
 
-    }
+    class TaintIntermediateTarget(location: JcInst) : TaintTarget(location)
 
-    // TODO is it important? Or we track every possible mark?
     class TaintMethodSinkTarget(
         location: JcInst,
         val condition: Condition,
         val configRule: TaintMethodSink,
     ) : TaintTarget(location)
-
-    private fun resolveCallInstance(
-        callExpr: JcCallExpr,
-    ) = if (callExpr is JcInstanceCallExpr) callExpr.instance else null
 }
 
 

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

@@ -3,6 +3,7 @@ package org.usvm.api.targets
 import org.jacodb.api.JcField
 import org.jacodb.api.JcMethod
 
+// TODO separate cleaning actions from the ones who can taint data
 data class TaintConfiguration(
     val entryPoints: Map<JcMethod, List<TaintEntryPointSource>>,
     val methodSources: Map<JcMethod, List<TaintMethodSource>>,
@@ -17,19 +18,20 @@ sealed interface TaintConfigurationItem
 
 class TaintEntryPointSource(
     val method: JcMethod,
-    val conditionWithAction: Pair<Condition, Action>,
+    val condition: Condition,
+    val action: Action,
 ) : TaintConfigurationItem
 
-// TODO probably conditions should be stored in some other way
-// source is it either a method call or a field reading
 class TaintMethodSource(
     val method: JcMethod,
-    val conditionWithAction: Pair<Condition, Action>, // TODO replace with a specific class
+    val condition: Condition,
+    val action: Action,
 ) : TaintConfigurationItem
 
 class TaintFieldSource(
     val field: JcField,
-    val conditionWithAction: Pair<Condition, Action>,
+    val condition: Condition,
+    val action: Action,
 ) : TaintConfigurationItem
 
 class TaintMethodSink(
@@ -44,11 +46,13 @@ class TaintFieldSink(
 
 class TaintPassThrough(
     val methodInfo: JcMethod,
-    val conditionWithAction: Pair<Condition, Action>,
+    val condition: Condition,
+    val action: Action,
 ) : TaintConfigurationItem
 
 class TaintCleaner(
     val methodInfo: JcMethod,
-    val conditionWithAction: Pair<Condition, Action>,
+    val condition: Condition,
+    val action: Action,
 ) : TaintConfigurationItem