-
Notifications
You must be signed in to change notification settings - Fork 22
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Added WeightedByNumberOfVirtualPathSelector; changed baseline probabi…
…lities
- Loading branch information
1 parent
7f9bfe7
commit 086702c
Showing
10 changed files
with
140 additions
and
73 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
17 changes: 9 additions & 8 deletions
17
usvm-python/usvm-python-commons/src/main/kotlin/org/usvm/python/ps/PyPathSelectorType.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
68 changes: 68 additions & 0 deletions
68
...-python-main/src/main/kotlin/org/usvm/machine/ps/WeightedByNumberOfVirtualPathSelector.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<PyState> | ||
| ): UPathSelector<PyState> { | ||
| private val selectors = mutableMapOf<Int, UPathSelector<PyState>>() | ||
| private val selectorOfState = mutableMapOf<PyState, UPathSelector<PyState>?>() | ||
|
|
||
| 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<PyState>) { | ||
| 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) | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters