Skip to content

Commit 5ec4a76

Browse files
committed
Create ApplicationBlockGraph interface, jvm impl
1 parent 3a975ab commit 5ec4a76

File tree

15 files changed

+1327
-18
lines changed

15 files changed

+1327
-18
lines changed

.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,6 @@ buildSrc/.gradle
88

99
# Ignore Idea directory
1010
.idea
11+
12+
# Ignore MacOS-specific files
13+
/**/.DS_Store

usvm-core/src/main/kotlin/org/usvm/statistics/CoverageStatistics.kt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,10 @@ class CoverageStatistics<Method, Statement, State : UState<*, Method, Statement,
8989
return uncoveredStatements.values.flatten()
9090
}
9191

92+
fun isCovered(statement: Statement) = statement in coveredStatements.values.flatten()
93+
94+
fun inCoverageZone(method: Method) = coveredStatements.containsKey(method) || uncoveredStatements.containsKey(method)
95+
9296
/**
9397
* Adds a listener triggered when a new statement is covered.
9498
*/

usvm-path-selection/build.gradle

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,5 @@ dependencies {
77
implementation(project(":usvm-jvm"))
88

99
implementation("org.jacodb:jacodb-analysis:${Versions.jcdb}")
10-
}
10+
implementation("org.jacodb:jacodb-approximations:${Versions.jcdb}")
11+
}

usvm-path-selection/src/main/kotlin/org/usvm/ApplicationBlockGraph.kt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ package org.usvm
33
import org.usvm.statistics.ApplicationGraph
44

55
interface ApplicationBlockGraph<Method, BasicBlock, Statement> : ApplicationGraph<Method, BasicBlock> {
6-
fun block(stmt: Statement): BasicBlock
6+
fun blockOf(stmt: Statement): BasicBlock
77
fun instructions(block: BasicBlock): Sequence<Statement>
88
fun blocks(): Sequence<BasicBlock>
99
}
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
package org.usvm
2+
3+
enum class MLPathSelectionStrategy {
4+
/**
5+
* Collects features according to states selected by any other path selector.
6+
*/
7+
FEATURES_LOGGING,
8+
9+
/**
10+
* Collects features and feeds them to the ML model to select states.
11+
* Extends FEATURE_LOGGING path selector.
12+
*/
13+
MACHINE_LEARNING,
14+
15+
/**
16+
* Selects states with best Graph Neural Network state score
17+
*/
18+
GNN,
19+
}
20+
21+
data class MLMachineOptions(
22+
val basicOptions: UMachineOptions,
23+
val pathSelectionStrategy: MLPathSelectionStrategy,
24+
val heteroGNNModelPath: String = ""
25+
)
Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
package org.usvm
2+
3+
import org.usvm.ps.ExceptionPropagationPathSelector
4+
import org.usvm.ps.GNNPathSelector
5+
import org.usvm.statistics.CoverageStatistics
6+
import org.usvm.statistics.StateVisitsStatistics
7+
8+
fun <Method, Statement, BasicBlock, State : UState<*, Method, Statement, *, *, State>> createPathSelector(
9+
initialState: State,
10+
options: MLMachineOptions,
11+
applicationGraph: ApplicationBlockGraph<Method, BasicBlock, Statement>,
12+
stateVisitsStatistics: StateVisitsStatistics<Method, Statement, State>,
13+
coverageStatistics: CoverageStatistics<Method, Statement, State>,
14+
): UPathSelector<State> {
15+
val selector = when (options.pathSelectionStrategy) {
16+
MLPathSelectionStrategy.GNN -> createGNNPathSelector(
17+
stateVisitsStatistics,
18+
coverageStatistics, applicationGraph, options.heteroGNNModelPath
19+
)
20+
21+
else -> {
22+
throw NotImplementedError()
23+
}
24+
}
25+
26+
val propagateExceptions = options.basicOptions.exceptionsPropagation
27+
28+
val resultSelector = selector.wrapIfRequired(propagateExceptions)
29+
resultSelector.add(listOf(initialState))
30+
31+
return selector
32+
}
33+
34+
private fun <State : UState<*, *, *, *, *, State>> UPathSelector<State>.wrapIfRequired(propagateExceptions: Boolean) =
35+
if (propagateExceptions && this !is ExceptionPropagationPathSelector<State>) {
36+
ExceptionPropagationPathSelector(this)
37+
} else {
38+
this
39+
}
40+
41+
private fun <Method, Statement, BasicBlock, State : UState<*, Method, Statement, *, *, State>> createGNNPathSelector(
42+
stateVisitsStatistics: StateVisitsStatistics<Method, Statement, State>,
43+
coverageStatistics: CoverageStatistics<Method, Statement, State>,
44+
applicationGraph: ApplicationBlockGraph<Method, BasicBlock, Statement>,
45+
heteroGNNModelPath: String,
46+
): UPathSelector<State> {
47+
return GNNPathSelector(
48+
coverageStatistics,
49+
stateVisitsStatistics,
50+
applicationGraph,
51+
heteroGNNModelPath
52+
)
53+
}
Lines changed: 61 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,42 @@
11
package org.usvm.jvm
22

3+
import org.jacodb.api.JcClasspath
34
import org.jacodb.api.JcMethod
5+
import org.jacodb.api.JcTypedMethod
46
import org.jacodb.api.cfg.JcBasicBlock
57
import org.jacodb.api.cfg.JcBlockGraph
6-
import org.jacodb.api.cfg.JcGraph
78
import org.jacodb.api.cfg.JcInst
8-
import org.jacodb.impl.cfg.JcBlockGraphImpl
9+
import org.jacodb.api.ext.toType
910
import org.usvm.ApplicationBlockGraph
1011
import org.usvm.machine.JcApplicationGraph
12+
import java.util.concurrent.ConcurrentHashMap
1113

12-
class JcApplicationBlockGraph(jcGraph: JcGraph) :
14+
class JcApplicationBlockGraph(cp: JcClasspath) :
1315
ApplicationBlockGraph<JcMethod, JcBasicBlock, JcInst> {
14-
private val jcBlockGraphImpl: JcBlockGraph = JcBlockGraphImpl(jcGraph)
15-
private val jcApplicationGraph: JcApplicationGraph = JcApplicationGraph(jcGraph.classpath)
16-
override fun predecessors(node: JcBasicBlock): Sequence<JcBasicBlock> =
17-
jcBlockGraphImpl.predecessors(node).asSequence()
16+
val jcApplicationGraph: JcApplicationGraph = JcApplicationGraph(cp)
17+
var initialStatement: JcInst? = null
18+
private fun getInitialStatement(): JcInst {
19+
if (initialStatement == null) {
20+
throw RuntimeException("initial statement not set")
21+
}
22+
return initialStatement!!
23+
}
24+
25+
private fun getBlockGraph() = getInitialStatement().location.method.flowGraph().blockGraph()
1826

19-
override fun successors(node: JcBasicBlock): Sequence<JcBasicBlock> = jcBlockGraphImpl.successors(node).asSequence()
27+
override fun predecessors(node: JcBasicBlock): Sequence<JcBasicBlock> {
28+
val jcBlockGraphImpl: JcBlockGraph = getBlockGraph()
29+
return jcBlockGraphImpl.predecessors(node).asSequence()
30+
}
31+
32+
override fun successors(node: JcBasicBlock): Sequence<JcBasicBlock> {
33+
val jcBlockGraphImpl: JcBlockGraph = getBlockGraph()
34+
return jcBlockGraphImpl.successors(node).asSequence()
35+
}
2036

2137
override fun callees(node: JcBasicBlock): Sequence<JcMethod> {
38+
val jcBlockGraphImpl: JcBlockGraph = getBlockGraph()
39+
2240
return jcBlockGraphImpl.instructions(node)
2341
.map { jcApplicationGraph.callees(it) }
2442
.reduce { acc, sequence -> acc + sequence }
@@ -29,26 +47,53 @@ class JcApplicationBlockGraph(jcGraph: JcGraph) :
2947
override fun callers(method: JcMethod): Sequence<JcBasicBlock> {
3048
return jcApplicationGraph
3149
.callers(method)
32-
.map { stmt -> block(stmt) }
50+
.map { stmt -> blockOf(stmt) }
3351
.toSet()
3452
.asSequence()
3553
}
3654

37-
override fun entryPoints(method: JcMethod): Sequence<JcBasicBlock> = jcBlockGraphImpl.entries.asSequence()
55+
override fun entryPoints(method: JcMethod): Sequence<JcBasicBlock> =
56+
method.flowGraph().blockGraph().entries.asSequence()
57+
58+
override fun exitPoints(method: JcMethod): Sequence<JcBasicBlock> =
59+
method.flowGraph().blockGraph().exits.asSequence()
3860

39-
override fun exitPoints(method: JcMethod): Sequence<JcBasicBlock> = jcBlockGraphImpl.exits.asSequence()
61+
override fun methodOf(node: JcBasicBlock): JcMethod {
62+
val firstInstruction = getBlockGraph().instructions(node).first()
63+
return jcApplicationGraph.methodOf(firstInstruction)
64+
}
4065

41-
override fun methodOf(node: JcBasicBlock): JcMethod = jcBlockGraphImpl.instructions(node).first().location.method
66+
override fun instructions(block: JcBasicBlock): Sequence<JcInst> {
67+
return getBlockGraph().instructions(block).asSequence()
68+
}
4269

4370
override fun statementsOf(method: JcMethod): Sequence<JcBasicBlock> {
4471
return jcApplicationGraph
4572
.statementsOf(method)
46-
.map { stmt -> block(stmt) }
73+
.map { stmt -> blockOf(stmt) }
4774
.toSet()
4875
.asSequence()
4976
}
5077

51-
override fun block(stmt: JcInst): JcBasicBlock = jcBlockGraphImpl.block(stmt)
52-
override fun instructions(block: JcBasicBlock): Sequence<JcInst> = jcBlockGraphImpl.instructions(block).asSequence()
53-
override fun blocks(): Sequence<JcBasicBlock> = jcBlockGraphImpl.asSequence()
78+
override fun blockOf(stmt: JcInst): JcBasicBlock {
79+
val jcBlockGraphImpl: JcBlockGraph = stmt.location.method.flowGraph().blockGraph()
80+
val blocks = blocks()
81+
for (block in blocks) {
82+
if (stmt in jcBlockGraphImpl.instructions(block)) {
83+
return block
84+
}
85+
}
86+
throw IllegalStateException("block not found for $stmt in ${jcBlockGraphImpl.jcGraph.method}")
87+
}
88+
89+
override fun blocks(): Sequence<JcBasicBlock> {
90+
return getInitialStatement().location.method.flowGraph().blockGraph().asSequence()
91+
}
92+
93+
private val typedMethodsCache = ConcurrentHashMap<JcMethod, JcTypedMethod>()
94+
95+
val JcMethod.typed
96+
get() = typedMethodsCache.getOrPut(this) {
97+
enclosingClass.toType().declaredMethods.first { it.method == this }
98+
}
5499
}

0 commit comments

Comments
 (0)