Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 13 additions & 8 deletions usvm-jvm/src/main/kotlin/org/usvm/machine/JcApplicationGraph.kt
Original file line number Diff line number Diff line change
Expand Up @@ -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

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

override fun predecessors(node: JcInst): Sequence<JcInst> =
jcApplicationGraph.predecessors(node)
override fun predecessors(node: JcInst): Sequence<JcInst> {
return jcApplicationGraph.predecessors(node.originalInst())
}

override fun successors(node: JcInst): Sequence<JcInst> =
jcApplicationGraph.successors(node)
override fun successors(node: JcInst): Sequence<JcInst> {
return jcApplicationGraph.successors(node.originalInst())
}

override fun callees(node: JcInst): Sequence<JcMethod> =
jcApplicationGraph.callees(node)
override fun callees(node: JcInst): Sequence<JcMethod> {
return jcApplicationGraph.callees(node.originalInst())
}

override fun callers(method: JcMethod): Sequence<JcInst> =
jcApplicationGraph.callers(method)
Expand All @@ -37,8 +41,9 @@ class JcApplicationGraph(
override fun exitPoints(method: JcMethod): Sequence<JcInst> =
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<JcMethod, JcTypedMethod>()

Expand Down
22 changes: 21 additions & 1 deletion usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -72,12 +74,14 @@ class JcMachine(
)
}

val transparentCfgStatistics = transparentCfgStatistics()

val pathSelector = createPathSelector(
initialState,
options,
applicationGraph,
{ coverageStatistics },
{ cfgStatistics },
{ transparentCfgStatistics },
{ callGraphStatistics }
)

Expand All @@ -86,6 +90,7 @@ class JcMachine(
StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<JcState>(coverageStatistics) {
it.methodResult is JcMethodResult.JcException
}

StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector()
}

Expand Down Expand Up @@ -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<JcMethod, JcInst> {
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()
}
Expand Down
24 changes: 19 additions & 5 deletions usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt
Original file line number Diff line number Diff line change
Expand Up @@ -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<JcExpr>
Expand All @@ -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<Pair<JcRefType, UHeapRef>>
val entrypointArguments: List<Pair<JcRefType, UHeapRef>>,
) : 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 {
Expand All @@ -54,8 +64,10 @@ data class JcConcreteMethodCallInst(
override val location: JcInstLocation,
override val method: JcMethod,
override val arguments: List<UExpr<out USort>>,
override val returnSite: JcInst
) : JcMethodCallBaseInst, JcMethodCall
override val returnSite: JcInst,
) : JcMethodCallBaseInst, JcMethodCall {
override val originalInst: JcInst = returnSite
}

/**
* Virtual method call instruction.
Expand All @@ -67,8 +79,10 @@ data class JcVirtualMethodCallInst(
override val location: JcInstLocation,
override val method: JcMethod,
override val arguments: List<UExpr<out USort>>,
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
}
4 changes: 4 additions & 0 deletions usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -29,3 +31,5 @@ fun UWritableMemory<*>.write(ref: ULValue<*, *>, value: UExpr<*>) {

internal fun UWritableMemory<JcType>.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