diff --git a/usvm-python/src/test/kotlin/org/usvm/samples/EnumerateTest.kt b/usvm-python/src/test/kotlin/org/usvm/samples/EnumerateTest.kt index 8d5af23a38..a59bc1abba 100644 --- a/usvm-python/src/test/kotlin/org/usvm/samples/EnumerateTest.kt +++ b/usvm-python/src/test/kotlin/org/usvm/samples/EnumerateTest.kt @@ -9,7 +9,7 @@ import kotlin.time.Duration.Companion.seconds class EnumerateTest: PythonTestRunnerForPrimitiveProgram( "Enumerate", - UMachineOptions(stepLimit = 15U, timeout = 20.seconds), + UMachineOptions(stepLimit = 25U, timeout = 20.seconds), // allowPathDiversions = true ) { @Test diff --git a/usvm-python/src/test/kotlin/org/usvm/samples/ListsTest.kt b/usvm-python/src/test/kotlin/org/usvm/samples/ListsTest.kt index 7571618ca4..3df7efd928 100644 --- a/usvm-python/src/test/kotlin/org/usvm/samples/ListsTest.kt +++ b/usvm-python/src/test/kotlin/org/usvm/samples/ListsTest.kt @@ -201,7 +201,7 @@ class ListsTest : PythonTestRunnerForPrimitiveProgram( private fun richcompareCheck(function: PyUnpinnedCallable) { val oldOptions = options - options = UMachineOptions(stepLimit = 10U) + options = UMachineOptions(stepLimit = 15U) allowPathDiversions = true check2WithConcreteRun( function, @@ -262,7 +262,7 @@ class ListsTest : PythonTestRunnerForPrimitiveProgram( @Test fun testDoubleSubscriptAndCompare() { val oldOptions = options - options = UMachineOptions(stepLimit = 20U, timeout = 20.seconds) + options = UMachineOptions(stepLimit = 30U, timeout = 20.seconds) allowPathDiversions = true check2WithConcreteRun( constructFunction("double_subscript_and_compare", listOf(typeSystem.pythonList, typeSystem.pythonList)), diff --git a/usvm-python/src/test/kotlin/org/usvm/samples/MethodsTest.kt b/usvm-python/src/test/kotlin/org/usvm/samples/MethodsTest.kt index 6c3a79435a..d34283b3b4 100644 --- a/usvm-python/src/test/kotlin/org/usvm/samples/MethodsTest.kt +++ b/usvm-python/src/test/kotlin/org/usvm/samples/MethodsTest.kt @@ -116,10 +116,10 @@ class MethodsTest: PythonTestRunnerForStructuredProgram("Methods", UMachineOptio @Test fun testPoint2Inference() { val oldOptions = options - options = UMachineOptions(stepLimit = 2U) + options = UMachineOptions(stepLimit = 4U) check1WithConcreteRun( constructFunction("point2_inference", List(1) { PythonAnyType }), - eq(1), + ignoreNumberOfAnalysisResults, standardConcolicAndConcreteChecks, /* invariants = */ emptyList(), /* propertiesToDiscover = */ listOf { x, _ -> x.typeName == "Point2" } diff --git a/usvm-python/src/test/kotlin/org/usvm/samples/SimpleCustomClassesTest.kt b/usvm-python/src/test/kotlin/org/usvm/samples/SimpleCustomClassesTest.kt index 13b0162a6d..6674f48735 100644 --- a/usvm-python/src/test/kotlin/org/usvm/samples/SimpleCustomClassesTest.kt +++ b/usvm-python/src/test/kotlin/org/usvm/samples/SimpleCustomClassesTest.kt @@ -7,7 +7,7 @@ import org.usvm.runner.PythonTestRunnerForStructuredProgram import org.usvm.test.util.checkers.eq import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults -class SimpleCustomClassesTest: PythonTestRunnerForStructuredProgram("SimpleCustomClasses", UMachineOptions(stepLimit = 20U)) { +class SimpleCustomClassesTest: PythonTestRunnerForStructuredProgram("SimpleCustomClasses", UMachineOptions(stepLimit = 25U)) { @Test fun testMatmulUsage() { check1WithConcreteRun( @@ -25,10 +25,10 @@ class SimpleCustomClassesTest: PythonTestRunnerForStructuredProgram("SimpleCusto @Test fun testMatmulAndAdd() { val oldOptions = options - options = UMachineOptions(stepLimit = 2U) + options = UMachineOptions(stepLimit = 4U) check1WithConcreteRun( constructFunction("matmul_and_add", List(1) { PythonAnyType }), - eq(1), + ignoreNumberOfAnalysisResults, compareConcolicAndConcreteTypes, /* invariants = */ emptyList(), /* propertiesToDiscover = */ listOf { x, res -> @@ -41,7 +41,7 @@ class SimpleCustomClassesTest: PythonTestRunnerForStructuredProgram("SimpleCusto @Test fun testMatmulAddAndSub() { val oldOptions = options - options = UMachineOptions(stepLimit = 6U) + options = UMachineOptions(stepLimit = 10U) check1WithConcreteRun( constructFunction("matmul_add_and_sub", List(1) { PythonAnyType }), ignoreNumberOfAnalysisResults, diff --git a/usvm-python/src/test/kotlin/org/usvm/samples/SimpleTypeInferenceTest.kt b/usvm-python/src/test/kotlin/org/usvm/samples/SimpleTypeInferenceTest.kt index 9fc3455545..aa517bbbe1 100644 --- a/usvm-python/src/test/kotlin/org/usvm/samples/SimpleTypeInferenceTest.kt +++ b/usvm-python/src/test/kotlin/org/usvm/samples/SimpleTypeInferenceTest.kt @@ -126,7 +126,7 @@ class SimpleTypeInferenceTest: PythonTestRunnerForPrimitiveProgram("SimpleTypeIn fun testAddAndCompare() { val oldOptions = options allowPathDiversions = true - options = UMachineOptions(stepLimit = 100U) + options = UMachineOptions(stepLimit = 120U) timeoutPerRunMs = 2000 check2WithConcreteRun( constructFunction("add_and_compare", List(2) { PythonAnyType }), diff --git a/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/ps/PyPathSelectorType.kt b/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/ps/PyPathSelectorType.kt index c22e635b69..ae0b96d79e 100644 --- a/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/ps/PyPathSelectorType.kt +++ b/usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/ps/PyPathSelectorType.kt @@ -1,12 +1,13 @@ package org.usvm.python.ps enum class PyPathSelectorType { - BaselinePriorityDfs, - BaselineWeightedDfs, - BaselinePriorityRandomTree, - BaselinePriorityWeightedByNumberOfVirtual, - BaselinePriorityPlusTypeRatingByHintsDfs, - DelayedForkByInstructionPriorityDfs, - DelayedForkByInstructionWeightedDfs, - DelayedForkByInstructionWeightedRandomTree + BaselinePriorityDfs, // passes tests + BaselineWeightedDfs, // passes tests + BaselinePriorityNumberOfVirtualDfs, // passes tests + BaselinePriorityPlusTypeRatingByHintsDfs, // passes tests + DelayedForkByInstructionPriorityDfs, // fails tests + DelayedForkByInstructionWeightedDfs, // passes tests + DelayedForkByInstructionWeightedRandomTree, // passes tests + DelayedForkByInstructionPriorityNumberOfVirtualDfs, // passes tests + DelayedForkByInstructionWeightedNumberOfVirtualDfs, // fails test MultiplyAndCompare } \ No newline at end of file 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 d97df5cbb4..6137b2cbf2 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 @@ -27,7 +27,7 @@ import kotlin.random.Random class PyMachine( private val program: PyProgram, private val typeSystem: PythonTypeSystem, - private val pathSelectorType: PyPathSelectorType = PyPathSelectorType.DelayedForkByInstructionWeightedRandomTree, + private val pathSelectorType: PyPathSelectorType = PyPathSelectorType.BaselinePriorityDfs, private val printErrorMsg: Boolean = false ): UMachine() { private val ctx = PyContext(typeSystem) diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/PyPathSelectorFactory.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/PyPathSelectorFactory.kt index e74f196190..6519ce700d 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/PyPathSelectorFactory.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/PyPathSelectorFactory.kt @@ -1,24 +1,14 @@ package org.usvm.machine.ps -import mu.KLogging -import org.usvm.algorithms.RandomizedPriorityCollection import org.usvm.machine.PyContext import org.usvm.machine.PyState -import org.usvm.machine.model.PyModelHolder import org.usvm.machine.ps.strategies.impls.* import org.usvm.machine.results.observers.NewStateObserver -import org.usvm.machine.symbolicobjects.interpretSymbolicPythonObject -import org.usvm.machine.symbolicobjects.rendering.PyObjectModelBuilder import org.usvm.ps.DfsPathSelector import org.usvm.ps.RandomTreePathSelector -import org.usvm.ps.WeightedPathSelector -import org.usvm.python.model.PyTupleObject -import org.usvm.python.model.calculateNumberOfMocks import org.usvm.python.ps.PyPathSelectorType -import kotlin.math.max import kotlin.random.Random -private val logger = object : KLogging() {}.logger fun createPyPathSelector( initialState: PyState, @@ -34,11 +24,8 @@ fun createPyPathSelector( PyPathSelectorType.BaselineWeightedDfs -> createBaselineWeightedDfsPyPathSelector(ctx, random, newStateObserver) - PyPathSelectorType.BaselinePriorityRandomTree -> - createBaselinePriorityRandomTreePyPathSelector(initialState, ctx, random, newStateObserver) - - PyPathSelectorType.BaselinePriorityWeightedByNumberOfVirtual -> - createBaselineWeightedByNumberOfVirtualPyPathSelector(ctx, random, newStateObserver) + PyPathSelectorType.BaselinePriorityNumberOfVirtualDfs -> + createBaselinePriorityNumberOfVirtualDfsPyPathSelector(ctx, random, newStateObserver) PyPathSelectorType.BaselinePriorityPlusTypeRatingByHintsDfs -> createTypeRatingByHintsDfsPyPathSelector(ctx, random, newStateObserver) @@ -51,6 +38,12 @@ fun createPyPathSelector( PyPathSelectorType.DelayedForkByInstructionWeightedRandomTree -> createDelayedForkByInstructionWeightedRandomTreePyPathSelector(initialState, ctx, random, newStateObserver) + + PyPathSelectorType.DelayedForkByInstructionPriorityNumberOfVirtualDfs -> + createDelayedForkByInstructionPriorityNumberOfVirtualDfsPyPathSelector(ctx, random, newStateObserver) + + PyPathSelectorType.DelayedForkByInstructionWeightedNumberOfVirtualDfs -> + createDelayedForkByInstructionWeightedNumberOfVirtualDfsPyPathSelector(ctx, random, newStateObserver) } selector.add(listOf(initialState)) return selector @@ -69,25 +62,6 @@ fun createBaselinePriorityDfsPyPathSelector( newStateObserver ) -fun createBaselinePriorityRandomTreePyPathSelector( - initialState: PyState, - ctx: PyContext, - random: Random, - newStateObserver: NewStateObserver -): PyVirtualPathSelector<*, *> = - PyVirtualPathSelector( - ctx, - makeBaselinePriorityActionStrategy(random), - BaselineDelayedForkStrategy(), - BaselineDFGraphCreation { - RandomTreePathSelector.fromRoot( - initialState.pathNode, - randomNonNegativeInt = { random.nextInt(0, it) } - ) - }, - newStateObserver - ) - fun createBaselineWeightedDfsPyPathSelector( ctx: PyContext, random: Random, @@ -101,7 +75,7 @@ fun createBaselineWeightedDfsPyPathSelector( newStateObserver ) -fun createBaselineWeightedByNumberOfVirtualPyPathSelector( +fun createBaselinePriorityNumberOfVirtualDfsPyPathSelector( ctx: PyContext, random: Random, newStateObserver: NewStateObserver @@ -111,23 +85,9 @@ fun createBaselineWeightedByNumberOfVirtualPyPathSelector( makeBaselinePriorityActionStrategy(random), BaselineDelayedForkStrategy(), BaselineDFGraphCreation { - WeightedPathSelector( - priorityCollectionFactory = { - RandomizedPriorityCollection(compareBy { it.id }) { random.nextDouble() } - }, - weighter = { - val modelHolder = PyModelHolder(it.pyModel) - val builder = PyObjectModelBuilder(it, modelHolder) - val models = it.inputSymbols.map { symbol -> - val interpreted = interpretSymbolicPythonObject(modelHolder, it.memory, symbol) - builder.convert(interpreted) - } - val tupleOfModels = PyTupleObject(models) - val mocks = calculateNumberOfMocks(tupleOfModels) - logger.debug { "Mocks of state $it: $mocks" } - 1.0 / max(1, 10 * mocks) - } - ) + WeightedByNumberOfVirtualPathSelector(random) { + DfsPathSelector() + } }, newStateObserver ) @@ -177,6 +137,40 @@ fun createDelayedForkByInstructionWeightedRandomTreePyPathSelector( newStateObserver ) +fun createDelayedForkByInstructionPriorityNumberOfVirtualDfsPyPathSelector( + ctx: PyContext, + random: Random, + newStateObserver: NewStateObserver +): PyVirtualPathSelector<*, *> = + PyVirtualPathSelector( + ctx, + makeDelayedForkByInstructionPriorityStrategy(random), + BaselineDelayedForkStrategy(), + DelayedForkByInstructionGraphCreation { + WeightedByNumberOfVirtualPathSelector(random) { + DfsPathSelector() + } + }, + newStateObserver + ) + +fun createDelayedForkByInstructionWeightedNumberOfVirtualDfsPyPathSelector( + ctx: PyContext, + random: Random, + newStateObserver: NewStateObserver +): PyVirtualPathSelector<*, *> = + PyVirtualPathSelector( + ctx, + makeDelayedForkByInstructionWeightedStrategy(random), + BaselineDelayedForkStrategy(), + DelayedForkByInstructionGraphCreation { + WeightedByNumberOfVirtualPathSelector(random) { + DfsPathSelector() + } + }, + newStateObserver + ) + fun createTypeRatingByHintsDfsPyPathSelector( ctx: PyContext, random: Random, diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/WeightedByNumberOfVirtualPathSelector.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/WeightedByNumberOfVirtualPathSelector.kt new file mode 100644 index 0000000000..8dfa9c6dd8 --- /dev/null +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/WeightedByNumberOfVirtualPathSelector.kt @@ -0,0 +1,68 @@ +package org.usvm.machine.ps + +import org.usvm.UPathSelector +import org.usvm.machine.PyState +import org.usvm.machine.model.PyModelHolder +import org.usvm.machine.symbolicobjects.interpretSymbolicPythonObject +import org.usvm.machine.symbolicobjects.rendering.PyObjectModelBuilder +import org.usvm.python.model.PyTupleObject +import org.usvm.python.model.calculateNumberOfMocks +import kotlin.math.max +import kotlin.random.Random + + +class WeightedByNumberOfVirtualPathSelector( + private val random: Random, + private val baseBaseSelectorCreation: () -> UPathSelector +): UPathSelector { + private val selectors = mutableMapOf>() + private val selectorOfState = mutableMapOf?>() + + override fun isEmpty(): Boolean { + return selectors.all { it.value.isEmpty() } + } + + override fun peek(): PyState { + val availableNumbers = selectors.mapNotNull { (number, selector) -> + if (selector.isEmpty()) null else number + } + val chosenNumber = weightedRandom(random, availableNumbers) { mocks -> 1.0 / max(1, 10 * mocks) } + val selector = selectors[chosenNumber]!! + return selector.peek() + } + + override fun update(state: PyState) { + remove(state) + add(state) + } + + override fun add(states: Collection) { + states.forEach { add(it) } + } + + private fun add(state: PyState) { + val numberOfVirtual = calculateNumberOfVirtual(state) + if (selectors[numberOfVirtual] == null) + selectors[numberOfVirtual] = baseBaseSelectorCreation() + val selector = selectors[numberOfVirtual]!! + selector.add(listOf(state)) + selectorOfState[state] = selector + } + + override fun remove(state: PyState) { + val selector = selectorOfState[state] ?: error("State was not in path selector") + selector.remove(state) + selectorOfState[state] = null + } + + private fun calculateNumberOfVirtual(state: PyState): Int { + val modelHolder = PyModelHolder(state.pyModel) + val builder = PyObjectModelBuilder(state, modelHolder) + val models = state.inputSymbols.map { symbol -> + val interpreted = interpretSymbolicPythonObject(modelHolder, state.memory, symbol) + builder.convert(interpreted) + } + val tupleOfModels = PyTupleObject(models) + return calculateNumberOfMocks(tupleOfModels) + } +} \ No newline at end of file diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/BaselineStrategy.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/BaselineStrategy.kt index e47b07e306..0586686add 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/BaselineStrategy.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/ps/strategies/impls/BaselineStrategy.kt @@ -7,8 +7,12 @@ import org.usvm.machine.PyState import org.usvm.machine.ps.strategies.* import kotlin.random.Random -val baselineProbabilities = listOf(1.0, 0.6, 0.9, 0.7, 1.0) -val baselineWeights = listOf(100.0, 0.6, 0.35, 0.04, 0.01) +val baselineProbabilities = listOf(1.0, 0.6, 0.875, 0.8, 1.0) +private val probNegations = baselineProbabilities + .drop(1) + .runningFold(1.0) { acc, p -> acc * (1 - p) } +val baselineWeights = //listOf(100.0, 0.6, 0.35, 0.04, 0.01) + listOf(100.0) + (baselineProbabilities.drop(1) zip probNegations.dropLast(1)).map { (a, b) -> a * b } fun makeBaselinePriorityActionStrategy( random: Random