Add support for taint analysis

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

@@ -26,9 +26,6 @@ open class UComposer<Type>(
 ) : UExprTransformer<Type>(ctx) {
     open fun <Sort : USort> compose(expr: UExpr<Sort>): UExpr<Sort> = apply(expr)
 
-    override fun <Sort : USort> transform(expr: USymbol<Sort>): UExpr<Sort> =
-        error("You must override `transform` function in org.usvm.UComposer for ${expr::class}")
-
     override fun <T : USort> transform(expr: UIteExpr<T>): UExpr<T> =
         transformExprAfterTransformed(expr, expr.condition) { condition ->
             when {
@@ -42,12 +39,6 @@ open class UComposer<Type>(
         expr: URegisterReading<Sort>,
     ): UExpr<Sort> = with(expr) { memory.stack.readRegister(idx, sort) }
 
-    override fun <Sort : USort> transform(expr: UCollectionReading<*, *, *>): UExpr<Sort> =
-        error("You must override `transform` function in org.usvm.UComposer for ${expr::class}")
-
-    override fun <Sort : USort> transform(expr: UMockSymbol<Sort>): UExpr<Sort> =
-        error("You must override `transform` function in org.usvm.UComposer for ${expr::class}")
-
     override fun <Method, Sort : USort> transform(
         expr: UIndexedMethodReturnValue<Method, Sort>,
     ): UExpr<Sort> = memory.mocker.eval(expr)

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

@@ -43,9 +43,9 @@ import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
 import org.usvm.collection.set.ref.UInputRefSetWithInputElements
 import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
 import org.usvm.memory.splitUHeapRef
+import org.usvm.regions.Region
 import org.usvm.solver.USolverBase
 import org.usvm.types.UTypeSystem
-import org.usvm.regions.Region
 
 @Suppress("LeakingThis")
 open class UContext(
@@ -67,9 +67,7 @@ open class UContext(
         return currentStateId++
     }
 
-    @Suppress("UNCHECKED_CAST")
-    fun <Type, Context : UContext> solver(): USolverBase<Type, Context> =
-        this.solver as USolverBase<Type, Context>
+    fun <Type> solver(): USolverBase<Type> = this.solver.uncheckedCast()
 
     @Suppress("UNCHECKED_CAST")
     fun <Type> typeSystem(): UTypeSystem<Type> =

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

@@ -20,12 +20,8 @@ import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
 import org.usvm.regions.Region
 
 interface UTransformer<Type> : KTransformer {
-    fun <Sort : USort> transform(expr: USymbol<Sort>): UExpr<Sort>
-
     fun <Sort : USort> transform(expr: URegisterReading<Sort>): UExpr<Sort>
 
-    fun <Sort : USort> transform(expr: UCollectionReading<*, *, *>): UExpr<Sort>
-
     fun <Field, Sort : USort> transform(expr: UInputFieldReading<Field, Sort>): UExpr<Sort>
 
     fun <Sort : USort> transform(expr: UAllocatedArrayReading<Type, Sort>): UExpr<Sort>
@@ -60,8 +56,6 @@ interface UTransformer<Type> : KTransformer {
 
     fun transform(expr: UInputRefSetWithInputElementsReading<Type>): UBoolExpr
 
-    fun <Sort : USort> transform(expr: UMockSymbol<Sort>): UExpr<Sort>
-
     fun <Method, Sort : USort> transform(expr: UIndexedMethodReturnValue<Method, Sort>): UExpr<Sort>
 
     fun transform(expr: UIsSubtypeExpr<Type>): UBoolExpr

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

@@ -9,20 +9,21 @@ import org.usvm.model.UModelBase
 import org.usvm.solver.USatResult
 import org.usvm.solver.UUnknownResult
 import org.usvm.solver.UUnsatResult
+import org.usvm.targets.UTarget
 
 typealias StateId = UInt
 
 abstract class UState<Type, Method, Statement, Context, Target, State>(
     // TODO: add interpreter-specific information
-    ctx: UContext,
+    val ctx: Context,
     open val callStack: UCallStack<Method, Statement>,
-    open val pathConstraints: UPathConstraints<Type, Context>,
+    open val pathConstraints: UPathConstraints<Type>,
     open val memory: UMemory<Type, Method>,
     open var models: List<UModelBase<Type>>,
     open var pathLocation: PathsTrieNode<State, Statement>,
     targets: List<Target> = emptyList(),
 ) where Context : UContext,
-        Target : UTarget<Statement, Target, State>,
+        Target : UTarget<Statement, Target, *>,
         State : UState<Type, Method, Statement, Context, Target, State> {
     /**
      * Deterministic state id.
@@ -53,7 +54,7 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
      * Creates new state structurally identical to this.
      * If [newConstraints] is null, clones [pathConstraints]. Otherwise, uses [newConstraints] in cloned state.
      */
-    abstract fun clone(newConstraints: UPathConstraints<Type, Context>? = null): State
+    abstract fun clone(newConstraints: UPathConstraints<Type>? = null): State
 
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
@@ -105,7 +106,7 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
         val previousTargetCount = targetsImpl.size
         targetsImpl = targetsImpl.remove(target)
 
-        if (previousTargetCount == targetsImpl.size || !target.isRemoved) {
+        if (previousTargetCount == targetsImpl.size || target.isRemoved) {
             return false
         }
 
@@ -155,7 +156,7 @@ private fun <T : UState<Type, *, *, Context, *, T>, Type, Context : UContext> fo
     } else {
         newConstraintToOriginalState
     }
-    val solver = newConstraintToForkedState.uctx.solver<Type, Context>()
+    val solver = newConstraintToForkedState.uctx.solver<Type>()
     val satResult = solver.checkWithSoftConstraints(constraintsToCheck)
 
     return when (satResult) {

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

@@ -1,13 +1,29 @@
 package org.usvm
 
+import org.usvm.model.ULazyModelDecoder
+import org.usvm.model.UModelDecoder
+import org.usvm.solver.UExprTranslator
 import org.usvm.solver.USolverBase
 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 <Context : UContext> mkSolver(ctx: Context): USolverBase<Type, Context>
+    fun mkSolver(ctx: UContext): USolverBase<Type>
     fun mkTypeSystem(ctx: UContext): UTypeSystem<Type>
+
+    /**
+     * Initializes [UExprTranslator] and [UModelDecoder] and returns them. We can safely reuse them while [UContext] is
+     * alive.
+     */
+    fun buildTranslatorAndLazyDecoder(
+        ctx: UContext,
+    ): Pair<UExprTranslator<Type>, ULazyModelDecoder<Type>> {
+        val translator = UExprTranslator<Type>(ctx)
+        val decoder = ULazyModelDecoder(translator)
+
+        return translator to decoder
+    }
 }

usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt

@@ -21,8 +21,8 @@ import org.usvm.uctx
 /**
  * Mutable representation of path constraints.
  */
-open class UPathConstraints<Type, Context : UContext> private constructor(
-    val ctx: Context,
+open class UPathConstraints<Type> private constructor(
+    private val ctx: UContext,
     logicalConstraints: PersistentSet<UBoolExpr> = persistentSetOf(),
     /**
      * Specially represented equalities and disequalities between objects, used in various part of constraints management.
@@ -51,7 +51,7 @@ open class UPathConstraints<Type, Context : UContext> private constructor(
     var logicalConstraints: PersistentSet<UBoolExpr> = logicalConstraints
         private set
 
-    constructor(ctx: Context) : this(ctx, persistentSetOf())
+    constructor(ctx: UContext) : this(ctx, persistentSetOf())
 
     open val isFalse: Boolean
         get() = equalityConstraints.isContradicting ||
@@ -128,7 +128,7 @@ open class UPathConstraints<Type, Context : UContext> private constructor(
             }
         }
 
-    open fun clone(): UPathConstraints<Type, Context> {
+    open fun clone(): UPathConstraints<Type> {
         val clonedEqualityConstraints = equalityConstraints.clone()
         val clonedTypeConstraints = typeConstraints.clone(clonedEqualityConstraints)
         val clonedNumericConstraints = numericConstraints.clone()

usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt

@@ -3,8 +3,8 @@ package org.usvm.model
 import io.ksmt.expr.KExpr
 import io.ksmt.solver.KModel
 import io.ksmt.sort.KUninterpretedSort
-import org.usvm.INITIAL_STATIC_ADDRESS
 import org.usvm.INITIAL_INPUT_ADDRESS
+import org.usvm.INITIAL_STATIC_ADDRESS
 import org.usvm.NULL_ADDRESS
 import org.usvm.UAddressSort
 import org.usvm.UConcreteHeapRef
@@ -19,18 +19,6 @@ interface UModelDecoder<Model> {
     fun decode(model: KModel): Model
 }
 
-/**
- * Initializes [UExprTranslator] and [UModelDecoder] and returns them. We can safely reuse them while [UContext] is
- * alive.
- */
-fun <Type> buildTranslatorAndLazyDecoder(
-    ctx: UContext,
-): Pair<UExprTranslator<Type>, ULazyModelDecoder<Type>> {
-    val translator = UExprTranslator<Type>(ctx)
-    val decoder = ULazyModelDecoder(translator)
-
-    return translator to decoder
-}
 
 typealias AddressesMapping = Map<UExpr<UAddressSort>, UConcreteHeapRef>
 
@@ -53,18 +41,18 @@ open class ULazyModelDecoder<Type>(
      * equivalence classes of addresses and work with their number in the future.
      */
     private fun buildMapping(model: KModel, nullRef: UConcreteHeapRef): AddressesMapping {
-        val interpreterdNullRef = model.eval(translatedNullRef, isComplete = true)
+        val interpretedNullRef = model.eval(translatedNullRef, isComplete = true)
 
         val result = mutableMapOf<KExpr<KUninterpretedSort>, UConcreteHeapRef>()
         // The null value has the NULL_ADDRESS
-        result[interpreterdNullRef] = nullRef
+        result[interpretedNullRef] = nullRef
 
         val universe = model.uninterpretedSortUniverse(ctx.addressSort) ?: return result
         // All the numbers are enumerated from the INITIAL_INPUT_ADDRESS to the Int.MIN_VALUE
         var counter = INITIAL_INPUT_ADDRESS
 
         for (interpretedAddress in universe) {
-            if (interpretedAddress == interpreterdNullRef) {
+            if (interpretedAddress == interpretedNullRef) {
                 continue
             }
 

usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt

@@ -5,7 +5,6 @@ import org.usvm.PathSelectorCombinationStrategy
 import org.usvm.UMachineOptions
 import org.usvm.UPathSelector
 import org.usvm.UState
-import org.usvm.UTarget
 import org.usvm.algorithms.DeterministicPriorityCollection
 import org.usvm.algorithms.RandomizedPriorityCollection
 import org.usvm.statistics.ApplicationGraph
@@ -17,18 +16,23 @@ import org.usvm.statistics.distances.InterprocDistance
 import org.usvm.statistics.distances.InterprocDistanceCalculator
 import org.usvm.statistics.distances.MultiTargetDistanceCalculator
 import org.usvm.statistics.distances.ReachabilityKind
+import org.usvm.targets.UTarget
+import org.usvm.targets.UTargetController
 import org.usvm.util.log2
 import kotlin.math.max
 import kotlin.random.Random
 
-fun <Method, Statement, Target : UTarget<Statement, Target, State>, State : UState<*, Method, Statement, *, Target, State>> createPathSelector(
+fun <Method, Statement, Target, State> createPathSelector(
     initialState: State,
     options: UMachineOptions,
     applicationGraph: ApplicationGraph<Method, Statement>,
     coverageStatistics: () -> CoverageStatistics<Method, Statement, State>? = { null },
     cfgStatistics: () -> CfgStatistics<Method, Statement>? = { null },
-    callGraphStatistics: () -> CallGraphStatistics<Method>? = { null }
-): UPathSelector<State> {
+    callGraphStatistics: () -> CallGraphStatistics<Method>? = { null },
+): UPathSelector<State>
+        where Target : UTarget<Statement, Target, *>,
+              State : UState<*, Method, Statement, *, Target, State> {
+
     val strategies = options.pathSelectionStrategies
     require(strategies.isNotEmpty()) { "At least one path selector strategy should be specified" }
 
@@ -56,6 +60,7 @@ fun <Method, Statement, Target : UTarget<Statement, Target, State>, State : USta
                 requireNotNull(cfgStatistics()) { "CFG statistics is required for closest to uncovered path selector" },
                 applicationGraph
             )
+
             PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM -> createClosestToUncoveredPathSelector(
                 requireNotNull(coverageStatistics()) { "Coverage statistics is required for closest to uncovered path selector" },
                 requireNotNull(cfgStatistics()) { "CFG statistics is required for closest to uncovered path selector" },
@@ -68,6 +73,7 @@ fun <Method, Statement, Target : UTarget<Statement, Target, State>, State : USta
                 requireNotNull(callGraphStatistics()) { "Call graph statistics is required for targeted path selector" },
                 applicationGraph
             )
+
             PathSelectionStrategy.TARGETED_RANDOM -> createTargetedPathSelector<Method, Statement, Target, State>(
                 requireNotNull(cfgStatistics()) { "CFG statistics is required for targeted path selector" },
                 requireNotNull(callGraphStatistics()) { "Call graph statistics is required for targeted path selector" },
@@ -79,6 +85,7 @@ fun <Method, Statement, Target : UTarget<Statement, Target, State>, State : USta
                 requireNotNull(cfgStatistics()) { "CFG statistics is required for targeted call stack local path selector" },
                 applicationGraph
             )
+
             PathSelectionStrategy.TARGETED_CALL_STACK_LOCAL_RANDOM -> createTargetedPathSelector<Method, Statement, Target, State>(
                 requireNotNull(cfgStatistics()) { "CFG statistics is required for targeted call stack local path selector" },
                 applicationGraph,
@@ -160,7 +167,12 @@ private fun <Method, Statement, State : UState<*, Method, Statement, *, *, State
         applicationGraph
     )
 
-    coverageStatistics.addOnCoveredObserver { _, method, statement -> distanceCalculator.removeTarget(method, statement) }
+    coverageStatistics.addOnCoveredObserver { _, method, statement ->
+        distanceCalculator.removeTarget(
+            method,
+            statement
+        )
+    }
 
     if (random == null) {
         return WeightedPathSelector(
@@ -171,7 +183,12 @@ private fun <Method, Statement, State : UState<*, Method, Statement, *, *, State
 
     return WeightedPathSelector(
         priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } },
-        weighter = { 1.0 / max(distanceCalculator.calculateDistance(it.currentStatement, it.callStack).toDouble(), 1.0) }
+        weighter = {
+            1.0 / max(
+                distanceCalculator.calculateDistance(it.currentStatement, it.callStack).toDouble(),
+                1.0
+            )
+        }
     )
 }
 
@@ -191,11 +208,14 @@ private fun <Method, Statement, State : UState<*, Method, Statement, *, *, State
     )
 }
 
-internal fun <Method, Statement, Target : UTarget<Statement, Target, State>, State : UState<*, Method, Statement, *, Target, State>> createTargetedPathSelector(
+internal fun <Method, Statement, Target, State> createTargetedPathSelector(
     cfgStatistics: CfgStatistics<Method, Statement>,
     applicationGraph: ApplicationGraph<Method, Statement>,
     random: Random? = null,
-): UPathSelector<State> {
+): UPathSelector<State>
+        where Target : UTarget<Statement, Target, *>,
+              State : UState<*, Method, Statement, *, Target, State> {
+
     val distanceCalculator = MultiTargetDistanceCalculator<Method, Statement, _> { loc ->
         CallStackDistanceCalculator(
             targets = listOf(loc),
@@ -249,12 +269,15 @@ private fun InterprocDistance.logWeight(): UInt {
     return weight
 }
 
-internal fun <Method, Statement, Target : UTarget<Statement, Target, State>, State : UState<*, Method, Statement, *, Target, State>> createTargetedPathSelector(
+internal fun <Method, Statement, Target, State> createTargetedPathSelector(
     cfgStatistics: CfgStatistics<Method, Statement>,
     callGraphStatistics: CallGraphStatistics<Method>,
     applicationGraph: ApplicationGraph<Method, Statement>,
     random: Random? = null,
-): UPathSelector<State> {
+): UPathSelector<State>
+        where Target : UTarget<Statement, Target, out UTargetController>,
+              State : UState<*, Method, Statement, *, Target, State> {
+
     val distanceCalculator = MultiTargetDistanceCalculator<Method, Statement, _> { stmt ->
         InterprocDistanceCalculator(
             targetLocation = stmt,

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

@@ -8,7 +8,6 @@ import io.ksmt.utils.uncheckedCast
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
-import org.usvm.UCollectionReading
 import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UExpr
@@ -18,12 +17,10 @@ import org.usvm.UIndexedMethodReturnValue
 import org.usvm.UIsExpr
 import org.usvm.UIsSubtypeExpr
 import org.usvm.UIsSupertypeExpr
-import org.usvm.UMockSymbol
 import org.usvm.UNullRef
 import org.usvm.URegisterReading
 import org.usvm.USizeSort
 import org.usvm.USort
-import org.usvm.USymbol
 import org.usvm.USymbolicHeapRef
 import org.usvm.collection.array.UAllocatedArrayReading
 import org.usvm.collection.array.UArrayRegionDecoder
@@ -78,20 +75,11 @@ open class UExprTranslator<Type>(
 ) : UExprTransformer<Type>(ctx) {
     open fun <Sort : USort> translate(expr: UExpr<Sort>): KExpr<Sort> = apply(expr)
 
-    override fun <Sort : USort> transform(expr: USymbol<Sort>): KExpr<Sort> =
-        error("You must override `transform` function in UExprTranslator for ${expr::class}")
-
     override fun <Sort : USort> transform(expr: URegisterReading<Sort>): KExpr<Sort> {
         val registerConst = expr.sort.mkConst("r${expr.idx}_${expr.sort}")
         return registerConst
     }
 
-    override fun <Sort : USort> transform(expr: UCollectionReading<*, *, *>): KExpr<Sort> =
-        error("You must override `transform` function in UExprTranslator for ${expr::class}")
-
-    override fun <Sort : USort> transform(expr: UMockSymbol<Sort>): KExpr<Sort> =
-        error("You must override `transform` function in UExprTranslator for ${expr::class}")
-
     override fun <Method, Sort : USort> transform(expr: UIndexedMethodReturnValue<Method, Sort>): KExpr<Sort> {
         val const = expr.sort.mkConst("m${expr.method}_${expr.callIndex}_${expr.sort}")
         return const