Skip to content

Commit a4123e6

Browse files
authored
Fix absence of JcMethodCall in the CFG (#70)
1 parent 8c4290c commit a4123e6

File tree

4 files changed

+57
-14
lines changed

4 files changed

+57
-14
lines changed

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

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ import org.jacodb.api.ext.toType
99
import org.jacodb.impl.features.HierarchyExtensionImpl
1010
import org.jacodb.impl.features.SyncUsagesExtension
1111
import org.usvm.statistics.ApplicationGraph
12+
import org.usvm.util.originalInst
1213
import java.util.concurrent.ConcurrentHashMap
1314

1415
/**
@@ -19,14 +20,17 @@ class JcApplicationGraph(
1920
) : ApplicationGraph<JcMethod, JcInst> {
2021
private val jcApplicationGraph = JcApplicationGraphImpl(cp, SyncUsagesExtension(HierarchyExtensionImpl(cp), cp))
2122

22-
override fun predecessors(node: JcInst): Sequence<JcInst> =
23-
jcApplicationGraph.predecessors(node)
23+
override fun predecessors(node: JcInst): Sequence<JcInst> {
24+
return jcApplicationGraph.predecessors(node.originalInst())
25+
}
2426

25-
override fun successors(node: JcInst): Sequence<JcInst> =
26-
jcApplicationGraph.successors(node)
27+
override fun successors(node: JcInst): Sequence<JcInst> {
28+
return jcApplicationGraph.successors(node.originalInst())
29+
}
2730

28-
override fun callees(node: JcInst): Sequence<JcMethod> =
29-
jcApplicationGraph.callees(node)
31+
override fun callees(node: JcInst): Sequence<JcMethod> {
32+
return jcApplicationGraph.callees(node.originalInst())
33+
}
3034

3135
override fun callers(method: JcMethod): Sequence<JcInst> =
3236
jcApplicationGraph.callers(method)
@@ -37,8 +41,9 @@ class JcApplicationGraph(
3741
override fun exitPoints(method: JcMethod): Sequence<JcInst> =
3842
jcApplicationGraph.exitPoints(method)
3943

40-
override fun methodOf(node: JcInst): JcMethod =
41-
jcApplicationGraph.methodOf(node)
44+
override fun methodOf(node: JcInst): JcMethod {
45+
return jcApplicationGraph.methodOf(node.originalInst())
46+
}
4247

4348
private val typedMethodsCache = ConcurrentHashMap<JcMethod, JcTypedMethod>()
4449

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

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,11 @@ import org.usvm.statistics.TransitiveCoverageZoneObserver
2222
import org.usvm.statistics.UMachineObserver
2323
import org.usvm.statistics.collectors.CoveredNewStatesCollector
2424
import org.usvm.statistics.collectors.TargetsReachedStatesCollector
25+
import org.usvm.statistics.distances.CfgStatistics
2526
import org.usvm.statistics.distances.CfgStatisticsImpl
2627
import org.usvm.statistics.distances.PlainCallGraphStatistics
2728
import org.usvm.stopstrategies.createStopStrategy
29+
import org.usvm.util.originalInst
2830

2931
val logger = object : KLogging() {}.logger
3032

@@ -72,12 +74,14 @@ class JcMachine(
7274
)
7375
}
7476

77+
val transparentCfgStatistics = transparentCfgStatistics()
78+
7579
val pathSelector = createPathSelector(
7680
initialState,
7781
options,
7882
applicationGraph,
7983
{ coverageStatistics },
80-
{ cfgStatistics },
84+
{ transparentCfgStatistics },
8185
{ callGraphStatistics }
8286
)
8387

@@ -86,6 +90,7 @@ class JcMachine(
8690
StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<JcState>(coverageStatistics) {
8791
it.methodResult is JcMethodResult.JcException
8892
}
93+
8994
StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector()
9095
}
9196

@@ -122,6 +127,21 @@ class JcMachine(
122127
return statesCollector.collectedStates
123128
}
124129

130+
/**
131+
* Returns a wrapper for the [cfgStatistics] that ignores [JcTransparentInstruction]s.
132+
* Instead of calculating statistics for them, it just takes the statistics for
133+
* their original instructions.
134+
*/
135+
private fun transparentCfgStatistics() = object : CfgStatistics<JcMethod, JcInst> {
136+
override fun getShortestDistance(method: JcMethod, stmtFrom: JcInst, stmtTo: JcInst): UInt {
137+
return cfgStatistics.getShortestDistance(method, stmtFrom.originalInst(), stmtTo.originalInst())
138+
}
139+
140+
override fun getShortestDistanceToExit(method: JcMethod, stmtFrom: JcInst): UInt {
141+
return cfgStatistics.getShortestDistanceToExit(method, stmtFrom.originalInst())
142+
}
143+
}
144+
125145
private fun isStateTerminated(state: JcState): Boolean {
126146
return state.callStack.isEmpty()
127147
}

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

Lines changed: 19 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,17 @@ import org.usvm.UExpr
1111
import org.usvm.UHeapRef
1212
import org.usvm.USort
1313

14+
/**
15+
* An interface for instructions that replace or surround some [originalInst].
16+
*/
17+
interface JcTransparentInstruction : JcInst {
18+
val originalInst: JcInst
19+
}
20+
1421
/**
1522
* Auxiliary instruction to handle method calls.
1623
* */
17-
sealed interface JcMethodCallBaseInst : JcInst {
24+
sealed interface JcMethodCallBaseInst : JcTransparentInstruction {
1825
val method: JcMethod
1926

2027
override val operands: List<JcExpr>
@@ -25,17 +32,20 @@ sealed interface JcMethodCallBaseInst : JcInst {
2532
}
2633
}
2734

35+
2836
/**
2937
* Entrypoint method call instruction.
3038
* Can be used as initial instruction to start an analysis process.
3139
* */
3240
data class JcMethodEntrypointInst(
3341
override val method: JcMethod,
34-
val entrypointArguments: List<Pair<JcRefType, UHeapRef>>
42+
val entrypointArguments: List<Pair<JcRefType, UHeapRef>>,
3543
) : JcMethodCallBaseInst {
3644
// We don't care about the location of the entrypoint
3745
override val location: JcInstLocation
3846
get() = JcInstLocationImpl(method, -1, -1)
47+
48+
override val originalInst: JcInst = method.instList.first()
3949
}
4050

4151
sealed interface JcMethodCall {
@@ -54,8 +64,10 @@ data class JcConcreteMethodCallInst(
5464
override val location: JcInstLocation,
5565
override val method: JcMethod,
5666
override val arguments: List<UExpr<out USort>>,
57-
override val returnSite: JcInst
58-
) : JcMethodCallBaseInst, JcMethodCall
67+
override val returnSite: JcInst,
68+
) : JcMethodCallBaseInst, JcMethodCall {
69+
override val originalInst: JcInst = returnSite
70+
}
5971

6072
/**
6173
* Virtual method call instruction.
@@ -67,8 +79,10 @@ data class JcVirtualMethodCallInst(
6779
override val location: JcInstLocation,
6880
override val method: JcMethod,
6981
override val arguments: List<UExpr<out USort>>,
70-
override val returnSite: JcInst
82+
override val returnSite: JcInst,
7183
) : JcMethodCallBaseInst, JcMethodCall {
7284
fun toConcreteMethodCall(concreteMethod: JcMethod): JcConcreteMethodCallInst =
7385
JcConcreteMethodCallInst(location, concreteMethod, arguments, returnSite)
86+
87+
override val originalInst: JcInst = returnSite
7488
}

usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,14 @@ import org.jacodb.api.JcClassOrInterface
44
import org.jacodb.api.JcRefType
55
import org.jacodb.api.JcType
66
import org.jacodb.api.JcTypedField
7+
import org.jacodb.api.cfg.JcInst
78
import org.jacodb.api.ext.findFieldOrNull
89
import org.jacodb.api.ext.toType
910
import org.usvm.UConcreteHeapRef
1011
import org.usvm.UExpr
1112
import org.usvm.USort
1213
import org.usvm.machine.JcContext
14+
import org.usvm.machine.JcTransparentInstruction
1315
import org.usvm.memory.ULValue
1416
import org.usvm.memory.UWritableMemory
1517
import org.usvm.uctx
@@ -29,3 +31,5 @@ fun UWritableMemory<*>.write(ref: ULValue<*, *>, value: UExpr<*>) {
2931

3032
internal fun UWritableMemory<JcType>.allocHeapRef(type: JcType, useStaticAddress: Boolean): UConcreteHeapRef =
3133
if (useStaticAddress) allocStatic(type) else allocConcrete(type)
34+
35+
tailrec fun JcInst.originalInst(): JcInst = if (this is JcTransparentInstruction) originalInst.originalInst() else this

0 commit comments

Comments
 (0)