diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt index f0a0e2bb4a..31cb8026b8 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt @@ -9,6 +9,7 @@ import org.jacodb.api.ext.toType import org.jacodb.impl.features.HierarchyExtensionImpl import org.jacodb.impl.features.SyncUsagesExtension import org.usvm.statistics.ApplicationGraph +import org.usvm.util.originalInst import java.util.concurrent.ConcurrentHashMap /** @@ -19,14 +20,17 @@ class JcApplicationGraph( ) : ApplicationGraph { private val jcApplicationGraph = JcApplicationGraphImpl(cp, SyncUsagesExtension(HierarchyExtensionImpl(cp), cp)) - override fun predecessors(node: JcInst): Sequence = - jcApplicationGraph.predecessors(node) + override fun predecessors(node: JcInst): Sequence { + return jcApplicationGraph.predecessors(node.originalInst()) + } - override fun successors(node: JcInst): Sequence = - jcApplicationGraph.successors(node) + override fun successors(node: JcInst): Sequence { + return jcApplicationGraph.successors(node.originalInst()) + } - override fun callees(node: JcInst): Sequence = - jcApplicationGraph.callees(node) + override fun callees(node: JcInst): Sequence { + return jcApplicationGraph.callees(node.originalInst()) + } override fun callers(method: JcMethod): Sequence = jcApplicationGraph.callers(method) @@ -37,8 +41,9 @@ class JcApplicationGraph( override fun exitPoints(method: JcMethod): Sequence = jcApplicationGraph.exitPoints(method) - override fun methodOf(node: JcInst): JcMethod = - jcApplicationGraph.methodOf(node) + override fun methodOf(node: JcInst): JcMethod { + return jcApplicationGraph.methodOf(node.originalInst()) + } private val typedMethodsCache = ConcurrentHashMap() diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt index e0dff78f9b..d429d3a25b 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt @@ -22,9 +22,11 @@ import org.usvm.statistics.TransitiveCoverageZoneObserver import org.usvm.statistics.UMachineObserver import org.usvm.statistics.collectors.CoveredNewStatesCollector import org.usvm.statistics.collectors.TargetsReachedStatesCollector +import org.usvm.statistics.distances.CfgStatistics import org.usvm.statistics.distances.CfgStatisticsImpl import org.usvm.statistics.distances.PlainCallGraphStatistics import org.usvm.stopstrategies.createStopStrategy +import org.usvm.util.originalInst val logger = object : KLogging() {}.logger @@ -72,12 +74,14 @@ class JcMachine( ) } + val transparentCfgStatistics = transparentCfgStatistics() + val pathSelector = createPathSelector( initialState, options, applicationGraph, { coverageStatistics }, - { cfgStatistics }, + { transparentCfgStatistics }, { callGraphStatistics } ) @@ -86,6 +90,7 @@ class JcMachine( StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { it.methodResult is JcMethodResult.JcException } + StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector() } @@ -122,6 +127,21 @@ class JcMachine( return statesCollector.collectedStates } + /** + * Returns a wrapper for the [cfgStatistics] that ignores [JcTransparentInstruction]s. + * Instead of calculating statistics for them, it just takes the statistics for + * their original instructions. + */ + private fun transparentCfgStatistics() = object : CfgStatistics { + override fun getShortestDistance(method: JcMethod, stmtFrom: JcInst, stmtTo: JcInst): UInt { + return cfgStatistics.getShortestDistance(method, stmtFrom.originalInst(), stmtTo.originalInst()) + } + + override fun getShortestDistanceToExit(method: JcMethod, stmtFrom: JcInst): UInt { + return cfgStatistics.getShortestDistanceToExit(method, stmtFrom.originalInst()) + } + } + private fun isStateTerminated(state: JcState): Boolean { return state.callStack.isEmpty() } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt index 13099df7de..c905a17a61 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt @@ -11,10 +11,17 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +/** + * An interface for instructions that replace or surround some [originalInst]. + */ +interface JcTransparentInstruction : JcInst { + val originalInst: JcInst +} + /** * Auxiliary instruction to handle method calls. * */ -sealed interface JcMethodCallBaseInst : JcInst { +sealed interface JcMethodCallBaseInst : JcTransparentInstruction { val method: JcMethod override val operands: List @@ -25,17 +32,20 @@ sealed interface JcMethodCallBaseInst : JcInst { } } + /** * Entrypoint method call instruction. * Can be used as initial instruction to start an analysis process. * */ data class JcMethodEntrypointInst( override val method: JcMethod, - val entrypointArguments: List> + val entrypointArguments: List>, ) : JcMethodCallBaseInst { // We don't care about the location of the entrypoint override val location: JcInstLocation get() = JcInstLocationImpl(method, -1, -1) + + override val originalInst: JcInst = method.instList.first() } sealed interface JcMethodCall { @@ -54,8 +64,10 @@ data class JcConcreteMethodCallInst( override val location: JcInstLocation, override val method: JcMethod, override val arguments: List>, - override val returnSite: JcInst -) : JcMethodCallBaseInst, JcMethodCall + override val returnSite: JcInst, +) : JcMethodCallBaseInst, JcMethodCall { + override val originalInst: JcInst = returnSite +} /** * Virtual method call instruction. @@ -67,8 +79,10 @@ data class JcVirtualMethodCallInst( override val location: JcInstLocation, override val method: JcMethod, override val arguments: List>, - override val returnSite: JcInst + override val returnSite: JcInst, ) : JcMethodCallBaseInst, JcMethodCall { fun toConcreteMethodCall(concreteMethod: JcMethod): JcConcreteMethodCallInst = JcConcreteMethodCallInst(location, concreteMethod, arguments, returnSite) + + override val originalInst: JcInst = returnSite } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt index c31085efd7..76c1c5723b 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt @@ -4,12 +4,14 @@ import org.jacodb.api.JcClassOrInterface import org.jacodb.api.JcRefType import org.jacodb.api.JcType import org.jacodb.api.JcTypedField +import org.jacodb.api.cfg.JcInst import org.jacodb.api.ext.findFieldOrNull import org.jacodb.api.ext.toType import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort import org.usvm.machine.JcContext +import org.usvm.machine.JcTransparentInstruction import org.usvm.memory.ULValue import org.usvm.memory.UWritableMemory import org.usvm.uctx @@ -29,3 +31,5 @@ fun UWritableMemory<*>.write(ref: ULValue<*, *>, value: UExpr<*>) { internal fun UWritableMemory.allocHeapRef(type: JcType, useStaticAddress: Boolean): UConcreteHeapRef = if (useStaticAddress) allocStatic(type) else allocConcrete(type) + +tailrec fun JcInst.originalInst(): JcInst = if (this is JcTransparentInstruction) originalInst.originalInst() else this \ No newline at end of file