Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

New path selectors infrastructure #29

Merged
merged 9 commits into from
Jun 30, 2023
Merged

New path selectors infrastructure #29

merged 9 commits into from
Jun 30, 2023

Conversation

mxprshn
Copy link
Collaborator

@mxprshn mxprshn commented Jun 28, 2023 •
edited
Loading

What's new

  • New path selectors
    • Random path (like random path in KLEE)
    • Depth (shorter path lengths is better)
    • Fork depth (less forks is better)
    • Closest to uncovered (closer to uncovered instructions is better)
  • Common weighted path selectors infrastructure (including discrete PDF structure)
  • Statistics pipeline refactoring
  • New statistics collectors:
    • Coverage statistics
    • Symbolic execution tree statistics
  • Little refactoring (not final yet) of Machine
  • UsvmTest attribute to run tests parametrized with various symbolic machine options

Further work:

  • Guided path selector
  • Fair path selector
  • More tests for path selectors efficiency

@mxprshn mxprshn requested review from dvvrd and sergeypospelov and removed request for dvvrd and sergeypospelov June 28, 2023 13:18
@mxprshn mxprshn changed the base branch from sergey/jvm to main June 30, 2023 09:29
@mxprshn mxprshn changed the title WIP: Path selectors New path selectors infrastructure Jun 30, 2023
@mxprshn mxprshn force-pushed the mxprshn/path-selectors branch 4 times, most recently from 10f1c5c to 01c1833 Compare June 30, 2023 11:45
dvvrd
dvvrd reviewed Jun 30, 2023
View reviewed changes
usvm-core/src/test/kotlin/org/usvm/TestUtil.kt
}

internal fun pseudoRandom(i: Int): Int {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please write comment why this can't be replaced by Random with fixed seed

usvm-core/src/main/kotlin/org/usvm/Context.kt Outdated
import org.usvm.memory.UInputArrayRegion
import org.usvm.memory.UInputFieldRegion
import org.usvm.memory.splitUHeapRef
import org.usvm.memory.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's not use * in imports

usvm-core/src/main/kotlin/org/usvm/Context.kt Outdated
* Generates new deterministic id of state in this context.
*/
fun getNextStateId(): UInt {
val result = currentStateId
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

return currentStateId++

usvm-core/src/main/kotlin/org/usvm/Machine.kt Outdated
interpreter: UInterpreter<State>,
pathSelector: UPathSelector<State>,
onState: (State) -> Unit,
observer: UMachineObserver<State>,
continueAnalyzing: (State) -> Boolean,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe rename it to isStateTerminated? @sergeypospelov

usvm-core/src/main/kotlin/org/usvm/Machine.kt Outdated
pathSelector.remove(state)
observer.onStateTerminated(state)
}
pathSelector.add(aliveForkedStates)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we really want to add empty list of states?

usvm-core/src/main/kotlin/org/usvm/stopstrategies/StepLimitStopStrategy.kt Outdated
private var counter = 0UL

override fun shouldStop(): Boolean {
val currentCounter = counter
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

return counter++ < limit

usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt Outdated
import org.usvm.UContext
import org.usvm.UIndexedMocker
import org.usvm.URegisterLValue
import org.usvm.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

please no stars

usvm-jvm/src/samples/java/org/usvm/samples/psbenchmarks/CreditRequest.java Outdated
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's merge this file into LoanExam.java

usvm-util/src/main/kotlin/org/usvm/util/DiscretePdf.kt Outdated
* @param comparator comparator for elements to arrange them in tree. It doesn't affect the priorities.
* @param unitIntervalRandom function returning a random value in [[0..1]] interval which is used to peek the element.
*/
class DiscretePdf<T>(comparator: Comparator<T>, private val unitIntervalRandom: () -> Float) : UPriorityCollection<T, Float> {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's rename it to RandomizedPriorityCollection

usvm-util/src/main/kotlin/org/usvm/util/VanillaPriorityQueue.kt Outdated
* [UPriorityCollection] implementation based on [java.util.PriorityQueue].
*/
// TODO: what to do if elements have same priority?
class VanillaPriorityQueue<T, Priority>(comparator: Comparator<Priority>) : UPriorityCollection<T, Priority> {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's rename it to DeterministicPriorityCollection

dvvrd
dvvrd reviewed Jun 30, 2023
View reviewed changes
usvm-util/src/main/kotlin/org/usvm/util/VanillaPriorityQueue.kt Outdated
* [UPriorityCollection] implementation based on [java.util.PriorityQueue].
*/
// TODO: what to do if elements have same priority?
class VanillaPriorityQueue<T, Priority>(comparator: Comparator<Priority>) : UPriorityCollection<T, Priority> {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's rename it to DeterministicPriorityCollection

dvvrd
dvvrd reviewed Jun 30, 2023
View reviewed changes
usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleApplicationGraph.kt Outdated
import org.usvm.language.SetLabel
import org.usvm.language.SetValue
import org.usvm.language.Stmt
import org.usvm.language.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

star

usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt Outdated
import org.usvm.UExpr
import org.usvm.USort
import org.usvm.UState
import org.usvm.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

star

usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt Outdated
import org.usvm.language.Stmt
import org.usvm.language.argumentCount
import org.usvm.language.localsCount
import org.usvm.language.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

star

usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt Outdated
import org.usvm.language.SampleType
import org.usvm.ps.DfsPathSelector
import org.usvm.ps.stopstrategies.CollectedStatesLimitStrategy
import org.usvm.language.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

star

usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt Outdated
import org.usvm.ps.stopstrategies.CollectedStatesLimitStrategy
import org.usvm.language.*
import org.usvm.ps.createPathSelector
import org.usvm.statistics.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

star

usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt Outdated
import kotlin.reflect.KFunction2
import kotlin.reflect.KFunction3
import kotlin.reflect.KFunction4
import kotlin.reflect.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nope

@dvvrd dvvrd merged commit 5ed0379 into main Jun 30, 2023
CaelmBleidd
CaelmBleidd reviewed Jul 3, 2023
View reviewed changes
usvm-core/src/main/kotlin/org/usvm/Machine.kt

val originalStateAlive = stateAlive && continueAnalyzing(state)
observer.onState(state, forkedStates)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

onState won't be called on the first state, will it? Is it fine?

korifey pushed a commit that referenced this pull request Jul 12, 2023
@mxprshn @korifey
New path selectors infrastructure (#29)
9516343 
* Add general framework for weighted searchers

* Add tests for AA-tree and discrete PDF

* Little typo fix in tests

* Add shortest distance to targets weighter

* Add random tree path selector

* Add fork depth path selector

* Fix interleaved path selector

* Add comments and some new java tests, infrastructure fixes

* PR comments fixes, add solver type and timeout options
korifey pushed a commit that referenced this pull request Jul 12, 2023
@mxprshn @korifey
New path selectors infrastructure (#29)
4f73478 
* Add general framework for weighted searchers

* Add tests for AA-tree and discrete PDF

* Little typo fix in tests

* Add shortest distance to targets weighter

* Add random tree path selector

* Add fork depth path selector

* Fix interleaved path selector

* Add comments and some new java tests, infrastructure fixes

* PR comments fixes, add solver type and timeout options
korifey added a commit that referenced this pull request Jul 13, 2023
@korifey @sergeypospelov
@CaelmBleidd @mxprshn
First version of logging in USVM (#38)
c09f086 
* First version of logging for usvm

* Implementation of the JacoDB interpreter (#18)

Co-authored-by: Alexey Menshutin <alex.menshutin99@gmail.com>

* New path selectors infrastructure (#29)

* Add general framework for weighted searchers

* Add tests for AA-tree and discrete PDF

* Little typo fix in tests

* Add shortest distance to targets weighter

* Add random tree path selector

* Add fork depth path selector

* Fix interleaved path selector

* Add comments and some new java tests, infrastructure fixes

* PR comments fixes, add solver type and timeout options

* First version of logging for usvm

* synchronize with master

---------

Co-authored-by: Sergey Pospelov <sergeypospelov59@gmail.com>
Co-authored-by: Alexey Menshutin <alex.menshutin99@gmail.com>
Co-authored-by: Maksim Parshin <mxprshn@gmail.com>
@Saloed Saloed deleted the mxprshn/path-selectors branch December 11, 2023 13:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CaelmBleidd CaelmBleidd CaelmBleidd left review comments

@dvvrd dvvrd dvvrd left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@mxprshn @dvvrd @CaelmBleidd