Refactoring

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

@@ -58,9 +58,8 @@ open class UContext<USizeSort : USort>(
 
     private val solver by lazy { components.mkSolver(this) }
     private val typeSystem by lazy { components.mkTypeSystem(this) }
-    private val softConstraintsProvider: USoftConstraintsProvider<Nothing, USizeSort> by lazy {
-        USoftConstraintsProvider(this)
-    }
+    private val softConstraintsProvider by lazy { USoftConstraintsProvider<Nothing, USizeSort>(this) }
+
     val sizeExprs by lazy { components.mkSizeExprProvider(this) }
     val statesForkProvider by lazy { components.mkStatesForkProvider() }
 

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

@@ -126,16 +126,9 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
 
 @Suppress("MoveVariableDeclarationIntoWhen")
 fun <T : UState<Type, *, *, *, *, T>, Type> T.applySoftConstraints() {
-    val softConstraints = hashSetOf<UBoolExpr>()
-
-    // TODO perhaps move it to the provider code?
-    val softConstraintSources = pathConstraints.logicalConstraints.asSequence() + pathConstraints.numericConstraints.constraints()
-    softConstraintSources.flatMapTo(softConstraints) {
-        ctx.softConstraintsProvider<Type>()
-            .provide(it)
-            .filterNot(UBoolExpr::isFalse)
-    }
+    val softConstraints = ctx.softConstraintsProvider<Type>().makeSoftConstraints(pathConstraints)
 
+    // Before running the solver, check the models for satisfying soft constraints
     val trueModels = models.filter { model ->
         softConstraints.all { model.eval(it).isTrue }
     }
@@ -152,7 +145,7 @@ fun <T : UState<Type, *, *, *, *, T>, Type> T.applySoftConstraints() {
         is USatResult -> {
             models = listOf(solverResult.model)
         }
-        is UUnsatResult -> error("Unexpected $solverResult for sat state $this")
+        is UUnsatResult -> error("Unexpected $solverResult for the state $this supposed to be sat")
         is UUnknownResult -> {
             // This state is supposed to be sat without soft constraints, so we just keep old models
         }

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

@@ -93,7 +93,7 @@ open class UModelBase<Type>(
 fun modelEnsureConcreteInputRef(ref: UHeapRef): UConcreteHeapRef {
     // All the expressions in the model are interpreted, therefore, they must
     // have concrete addresses. Moreover, the model knows only about input values
-    // which have addresses less or equal than INITIAL_INPUT_ADDRESS
+    // which have addresses less or equal than INITIAL_INPUT_ADDRESS (or NULL_ADDRESS for null values)
     require(ref is UConcreteHeapRef && (ref.address <= INITIAL_INPUT_ADDRESS || ref.address == NULL_ADDRESS)) {
         "Unexpected ref: $ref"
     }

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

@@ -109,7 +109,7 @@ open class USolverBase<Type>(
     }
 
     override fun check(query: UPathConstraints<Type>): USolverResult<UModelBase<Type>> =
-        internalCheck(query, emptyList())
+        internalCheck(query, softConstraints = emptyList())
 
     fun checkWithSoftConstraints(
         pc: UPathConstraints<Type>,

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

@@ -50,7 +50,9 @@ import org.usvm.collection.set.primitive.UInputSetReading
 import org.usvm.collection.set.ref.UAllocatedRefSetWithInputElementsReading
 import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
 import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
+import org.usvm.constraints.UPathConstraints
 import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.isFalse
 import org.usvm.isStaticHeapRef
 import org.usvm.mkSizeExpr
 import org.usvm.mkSizeLeExpr
@@ -65,6 +67,20 @@ class USoftConstraintsProvider<Type, USizeSort : USort>(
     private val caches = hashMapOf<UExpr<*>, Set<UBoolExpr>>()
     private val sortPreferredValuesProvider = SortPreferredValuesProvider()
 
+    fun makeSoftConstraints(pathConstraints: UPathConstraints<Type>): Set<UBoolExpr> {
+        val softConstraints = hashSetOf<UBoolExpr>()
+
+        val softConstraintSources = pathConstraints.logicalConstraints.asSequence() +
+                pathConstraints.numericConstraints.constraints()
+        softConstraintSources.flatMapTo(softConstraints) {
+            ctx.softConstraintsProvider<Type>()
+                .provide(it)
+                .filterNot(UBoolExpr::isFalse)
+        }
+
+        return softConstraints
+    }
+
     fun provide(initialExpr: UExpr<*>): Set<UBoolExpr> =
         caches.getOrElse(initialExpr) {
             apply(initialExpr)
@@ -307,7 +323,6 @@ private class SortPreferredValuesProvider : KSortVisitor<(KExpr<*>) -> KExpr<KBo
     ): (KExpr<*>) -> KExpr<KBoolSort> = sort.range.accept(this)
 
     override fun visit(sort: KBoolSort): (KExpr<*>) -> KExpr<KBoolSort> = { it.asExpr(sort) }
-//    override fun visit(sort: KBoolSort): (KExpr<*>) -> KExpr<KBoolSort> = { sort.ctx.falseExpr }
 
     override fun visit(sort: KFpRoundingModeSort): (KExpr<*>) -> KExpr<KBoolSort> =
         caches.getOrPut(sort) {

usvm-core/src/main/kotlin/org/usvm/statistics/constraints/SoftConstraintsObserver.kt

@@ -7,7 +7,9 @@ import org.usvm.statistics.UMachineObserver
 class SoftConstraintsObserver<Type, State : UState<Type, *, *, *, *, State>> : UMachineObserver<State> {
     override fun onStateTerminated(state: State, stateReachable: Boolean) {
         if (stateReachable) {
-            // TODO actually, only states presented in CoveredNewStatesCollector should be here
+            // TODO actually, only states presented in CoveredNewStatesCollector should be here,
+            //  so for now soft constraints are applied for more states than required. Rewrite it after refactoring
+            //  path selector factory, observers, collectors, etc.
             state.applySoftConstraints()
         }
     }

usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt

@@ -21,7 +21,6 @@ import kotlin.test.assertSame
 
 private typealias Type = SingleTypeSystem.SingleType
 
-/*
 open class SoftConstraintsTest {
     private lateinit var ctx: UContext<USizeSort>
     private lateinit var softConstraintsProvider: USoftConstraintsProvider<Type, *>
@@ -42,7 +41,7 @@ open class SoftConstraintsTest {
         decoder = ULazyModelDecoder(translator)
 
         val typeSolver = UTypeSolver(SingleTypeSystem)
-        solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, softConstraintsProvider)
+        solver = USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder)
     }
 
     @Test
@@ -54,7 +53,8 @@ open class SoftConstraintsTest {
         val pc = UPathConstraints<Type>(ctx)
         pc += expr
 
-        val result = solver.checkWithSoftConstraints(pc) as USatResult
+        val softConstraints = softConstraintsProvider.makeSoftConstraints(pc)
+        val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult
         val model = result.model
 
         val fstRegisterValue = model.eval(fstRegister)
@@ -85,9 +85,10 @@ open class SoftConstraintsTest {
 
         val typeSolver = UTypeSolver<Type>(mockk())
         val solver: USolverBase<Type> =
-            USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder, softConstraintsProvider)
+            USolverBase(ctx, KZ3Solver(ctx), typeSolver, translator, decoder)
 
-        val result = solver.checkWithSoftConstraints(pc) as USatResult
+        val softConstraints = softConstraintsProvider.makeSoftConstraints(pc)
+        val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult
         val model = result.model
 
         verify(exactly = 1) {
@@ -131,7 +132,8 @@ open class SoftConstraintsTest {
         pc += inputRef eq secondInputRef
         pc += (inputRef eq nullRef).not()
 
-        val result = (solver.checkWithSoftConstraints(pc)) as USatResult
+        val softConstraints = softConstraintsProvider.makeSoftConstraints(pc)
+        val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult
 
         val model = result.model
         val value = model.eval(mkInputArrayLengthReading(region, inputRef))
@@ -149,7 +151,9 @@ open class SoftConstraintsTest {
 
         val pc = UPathConstraints<Type>(ctx)
         pc += (inputRef eq nullRef).not()
-        val result = (solver.checkWithSoftConstraints(pc)) as USatResult
+
+        val softConstraints = softConstraintsProvider.makeSoftConstraints(pc)
+        val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult
 
         val model = result.model
         val value = model.eval(mkInputArrayLengthReading(region, inputRef))
@@ -165,10 +169,11 @@ open class SoftConstraintsTest {
 
         val pc = UPathConstraints<Type>(ctx)
         pc += expression
-        val result = (solver.checkWithSoftConstraints(pc)) as USatResult
+
+        val softConstraints = softConstraintsProvider.makeSoftConstraints(pc)
+        val result = solver.checkWithSoftConstraints(pc, softConstraints) as USatResult
 
         val model = result.model
         model.eval(expression)
     }
 }
-*/

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

@@ -20,7 +20,6 @@ import org.usvm.solver.UTypeSolver
 
 class JcComponents(
     private val typeSystem: JcTypeSystem,
-    // TODO group all parameters below to the one class
     private val solverType: SolverType,
     override val useSolverForForks: Boolean,
     private val runSolverInAnotherProcess: Boolean,
@@ -52,7 +51,7 @@ class JcComponents(
 
 }
 
-interface SolverFactory : AutoCloseable {
+private interface SolverFactory : AutoCloseable {
     fun <Context : UContext<USizeSort>> mkSolver(
         ctx: Context,
         solverType: SolverType

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

@@ -147,7 +147,6 @@ class JcMachine(
             interpreter.forkBlackList = UForkBlackList.createDefault()
         }
 
-        // TODO extract common code
         if (options.useSoftConstraints) {
             observers.add(SoftConstraintsObserver())
         }

usvm-jvm/src/samples/java/org/usvm/samples/algorithms/Sort.java

@@ -20,8 +20,7 @@ public void swap(long[] array, int i, int j) {
     }
 
     public int partition(long[] array, int begin, int end) {
-//        int index = begin + new Random().nextInt(end - begin + 1);
-        int index = begin + new java.util.Random().nextInt(end - begin + 1);
+        int index = begin + new Random().nextInt(end - begin + 1);
         long pivot = array[index];
         int firstIndex = begin;
         int lastIndex = end;

usvm-jvm/src/test/kotlin/org/usvm/samples/algorithms/SortTest.kt

@@ -9,10 +9,12 @@ import org.usvm.util.isException
 
 internal class SortTest : JavaMethodTestRunner() {
     @Test
+    @Disabled("TODO discover why there are no meaningful non-exceptional executions")
     fun testQuickSort() {
-        checkDiscoveredProperties(
+        checkDiscoveredPropertiesWithExceptions(
             Sort::quickSort,
             ignoreNumberOfAnalysisResults,
+            { _, _, begin, end, r -> end > begin && r.isSuccess } // check that we have found at least one meaningful non-exceptional execution
             // TODO coverage or properties
         )
     }

usvm-jvm/src/test/kotlin/org/usvm/samples/arrays/PrimitiveArraysTest.kt

@@ -2,7 +2,6 @@ package org.usvm.samples.arrays
 
 
 import org.junit.jupiter.api.Disabled
-import org.junit.jupiter.api.RepeatedTest
 import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq

usvm-jvm/src/test/kotlin/org/usvm/samples/types/CastExamplesTest.kt

@@ -54,7 +54,7 @@ internal class CastExamplesTest : JavaMethodTestRunner() {
 
     @Test
     fun testFloatToInt() {
-        // TODO remove after fixing Z3 model detach in ksmt
+        // TODO remove after fixing Z3 model detach in ksmt https://github.com/UnitTestBot/ksmt/issues/139
         withOptions(options.copy(solverType = SolverType.YICES)) {
             checkDiscoveredProperties(
                 CastExamples::floatToInt,

usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt

@@ -85,7 +85,6 @@ class SampleMachine(
         observers.add(TerminatedStateRemover())
         observers.add(statesCollector)
 
-        // TODO extract common code
         if (options.useSoftConstraints) {
             observers.add(SoftConstraintsObserver())
         }