diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt index 4527e608b7..5cf15eda39 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt @@ -71,14 +71,31 @@ data class XcfaState @JvmOverloads constructor( "ATOMIC_BEGIN" -> changes.add { it.enterMutex("", a.pid) } "ATOMIC_END" -> changes.add { it.exitMutex("", a.pid) } in Regex("mutex_lock\\((.*)\\)") -> changes.add { state -> - state.enterMutex( - label.substring("mutex_lock".length + 1, label.length - 1), a.pid) + state.enterMutex(label.substring("mutex_lock".length + 1, label.length - 1), a.pid) } in Regex("mutex_unlock\\((.*)\\)") -> changes.add { state -> - state.exitMutex( - label.substring("mutex_unlock".length + 1, label.length - 1), a.pid) + state.exitMutex(label.substring("mutex_unlock".length + 1, label.length - 1), a.pid) } + + in Regex("start_cond_wait\\((.*)\\)") -> { + val args = label.substring("start_cond_wait".length + 1, label.length - 1).split(",") + changes.add { state -> state.enterMutex(args[0], -1) } + changes.add { state -> state.exitMutex(args[1], a.pid) } + } + + in Regex("cond_wait\\((.*)\\)") -> { + val args = label.substring("cond_wait".length + 1, label.length - 1).split(",") + changes.add { state -> state.enterMutex(args[0], a.pid) } + changes.add { state -> state.exitMutex(args[0], a.pid) } + changes.add { state -> state.enterMutex(args[1], a.pid) } + } + + in Regex("cond_signal\\((.*)\\)") -> changes.add { state -> + state.exitMutex(label.substring("cond_signal".length + 1, label.length - 1), -1) + } + + else -> error("Unknown fence label $label") } }.let { false } @@ -86,23 +103,18 @@ data class XcfaState @JvmOverloads constructor( val proc = xcfa?.procedures?.find { proc -> proc.name == it.name } ?: error( "No such method ${it.name}.") val returnStmt = SequenceLabel( - proc.params.withIndex().filter { it.value.second != ParamDirection.IN } - .map { iVal -> - StmtLabel(Assign( - cast((it.params[iVal.index] as RefExpr<*>).decl as VarDecl<*>, - iVal.value.first.type), - cast(iVal.value.first.ref, iVal.value.first.type)), - metadata = it.metadata) - }) + proc.params.withIndex().filter { it.value.second != ParamDirection.IN }.map { iVal -> + StmtLabel(Assign(cast((it.params[iVal.index] as RefExpr<*>).decl as VarDecl<*>, + iVal.value.first.type), cast(iVal.value.first.ref, iVal.value.first.type)), + metadata = it.metadata) + }) changes.add { state -> - state.invokeFunction(a.pid, proc, returnStmt, proc.params.toMap(), - it.tempLookup) + state.invokeFunction(a.pid, proc, returnStmt, proc.params.toMap(), it.tempLookup) } false } - is ReturnLabel -> changes.add { state -> state.returnFromFunction(a.pid) } - .let { true } + is ReturnLabel -> changes.add { state -> state.returnFromFunction(a.pid) }.let { true } is JoinLabel -> { changes.add { state -> state.enterMutex("${threadLookup[it.pidVar]}", a.pid) } @@ -121,12 +133,10 @@ data class XcfaState @JvmOverloads constructor( } changes.add { state -> - if (checkNotNull(state.processes[a.pid]).locs.isEmpty()) state.endProcess( - a.pid) else state + if (checkNotNull(state.processes[a.pid]).locs.isEmpty()) state.endProcess(a.pid) else state } - return Pair(changes.fold(this) { current, change -> change(current) }, - a.withLabel(SequenceLabel(newLabels))) + return Pair(changes.fold(this) { current, change -> change(current) }, a.withLabel(SequenceLabel(newLabels))) } private fun start(startLabel: StartLabel): XcfaState { @@ -151,17 +161,13 @@ data class XcfaState @JvmOverloads constructor( val pid = pidCnt++ val lookup = XcfaProcessState.createLookup(procedure, "T$pid", "") newThreadLookup[startLabel.pidVar] = pid - newProcesses[pid] = XcfaProcessState( - LinkedList(listOf(procedure.initLoc)), - prefix = "T$pid", - varLookup = LinkedList(listOf(lookup)), - returnStmts = LinkedList(listOf(returnStmt)), + newProcesses[pid] = XcfaProcessState(LinkedList(listOf(procedure.initLoc)), prefix = "T$pid", + varLookup = LinkedList(listOf(lookup)), returnStmts = LinkedList(listOf(returnStmt)), paramStmts = LinkedList(listOf(Pair( /* init */ SequenceLabel(paramList.filter { it.value != ParamDirection.OUT }.map { StmtLabel(Assign(cast(it.key.changeVars(lookup), it.key.type), - cast(it.key.changeVars(tempLookup).ref, it.key.type)), - metadata = EmptyMetaData) + cast(it.key.changeVars(tempLookup).ref, it.key.type)), metadata = EmptyMetaData) }), /* deinit */ SequenceLabel(paramList.filter { it.value != ParamDirection.IN }.map { @@ -184,11 +190,9 @@ data class XcfaState @JvmOverloads constructor( } private fun invokeFunction(pid: Int, proc: XcfaProcedure, returnStmt: XcfaLabel, - paramList: Map, ParamDirection>, - tempLookup: Map, VarDecl<*>>): XcfaState { + paramList: Map, ParamDirection>, tempLookup: Map, VarDecl<*>>): XcfaState { val newProcesses: MutableMap = LinkedHashMap(processes) - newProcesses[pid] = checkNotNull( - processes[pid]?.enterFunction(proc, returnStmt, paramList, tempLookup)) + newProcesses[pid] = checkNotNull(processes[pid]?.enterFunction(proc, returnStmt, paramList, tempLookup)) return copy(processes = newProcesses) } @@ -226,15 +230,10 @@ data class XcfaState @JvmOverloads constructor( } } -data class XcfaProcessState( - val locs: LinkedList, - val varLookup: LinkedList, VarDecl<*>>>, +data class XcfaProcessState(val locs: LinkedList, val varLookup: LinkedList, VarDecl<*>>>, val returnStmts: LinkedList = LinkedList(listOf(NopLabel)), - val paramStmts: LinkedList> = LinkedList( - listOf(Pair(NopLabel, NopLabel))), - val paramsInitialized: Boolean = false, - val prefix: String = "" -) { + val paramStmts: LinkedList> = LinkedList(listOf(Pair(NopLabel, NopLabel))), + val paramsInitialized: Boolean = false, val prefix: String = "") { fun withNewLoc(l: XcfaLocation): XcfaProcessState { val deque: LinkedList = LinkedList(locs) @@ -249,8 +248,7 @@ data class XcfaProcessState( else -> "${locs.peek()!!} [${locs.size}], initilized=$paramsInitialized" } - fun enterFunction(xcfaProcedure: XcfaProcedure, returnStmt: XcfaLabel, - paramList: Map, ParamDirection>, + fun enterFunction(xcfaProcedure: XcfaProcedure, returnStmt: XcfaLabel, paramList: Map, ParamDirection>, tempLookup: Map, VarDecl<*>>): XcfaProcessState { val deque: LinkedList = LinkedList(locs) val varLookup: LinkedList, VarDecl<*>>> = LinkedList(varLookup) @@ -272,8 +270,8 @@ data class XcfaProcessState( cast(it.key.changeVars(lookup).ref, it.key.type)), metadata = EmptyMetaData) }), )) - return copy(locs = deque, varLookup = varLookup, returnStmts = returnStmts, - paramStmts = paramStmts, paramsInitialized = false) + return copy(locs = deque, varLookup = varLookup, returnStmts = returnStmts, paramStmts = paramStmts, + paramsInitialized = false) } fun exitFunction(): XcfaProcessState { @@ -285,8 +283,7 @@ data class XcfaProcessState( varLookup.pop() returnStmts.pop() paramStmts.pop() - return copy(locs = deque, varLookup = varLookup, returnStmts = returnStmts, - paramStmts = paramStmts) + return copy(locs = deque, varLookup = varLookup, returnStmts = returnStmts, paramStmts = paramStmts) } override fun equals(other: Any?): Boolean { @@ -310,8 +307,8 @@ data class XcfaProcessState( companion object { fun createLookup(proc: XcfaProcedure, threadPrefix: String, - procPrefix: String): Map, VarDecl<*>> = - listOf(proc.params.map { it.first }, proc.vars).flatten().associateWith { + procPrefix: String): Map, VarDecl<*>> = listOf(proc.params.map { it.first }, proc.vars).flatten() + .associateWith { val sj = StringJoiner("::") if (threadPrefix != "") sj.add(threadPrefix) else sj.add("_") diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt index 64ed3d15e3..38b140cbe4 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt @@ -31,24 +31,23 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap() - val persistentSetFirstActions = if (exploredActions.isEmpty()) { - getPersistentSetFirstActions(allEnabledActions) + // Calculating the source set starting from every (or some of the) enabled transition or from exploredActions if it is not empty + // The minimal source set is stored + var minimalSourceSet = mutableSetOf() + val sourceSetFirstActions = if (exploredActions.isEmpty()) { + getSourceSetFirstActions(state, allEnabledActions) } else { setOf(exploredActions) } var finalIgnoredVars = setOf>() - // Calculate persistent sets from all possible starting action set - for (firstActions in persistentSetFirstActions) { - // Variables that have been ignored (if they would be in the precision, more actions have had to be added to the persistent set) + // Calculate source sets from all possible starting action set + for (firstActions in sourceSetFirstActions) { + // Variables that have been ignored (if they would be in the precision, more actions have had to be added to the source set) val ignoredVars = mutableSetOf>() - val persistentSet = calculatePersistentSet(allEnabledActions, firstActions, prec, - ignoredVars) - if (minimalPersistentSet.isEmpty() || persistentSet.size < minimalPersistentSet.size) { - minimalPersistentSet = persistentSet.toMutableSet() + val sourceSet = calculateSourceSet(allEnabledActions, firstActions, prec, ignoredVars) + if (minimalSourceSet.isEmpty() || sourceSet.size < minimalSourceSet.size) { + minimalSourceSet = sourceSet.toMutableSet() finalIgnoredVars = ignoredVars } } @@ -58,28 +57,27 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap, - firstActions: Collection, prec: Prec, - ignoredVars: MutableSet>): Set { + private fun calculateSourceSet(enabledActions: Collection, firstActions: Collection, + prec: Prec, ignoredVars: MutableSet>): Set { if (firstActions.any(this::isBackwardAction)) { return enabledActions.toSet() } - val persistentSet = firstActions.toMutableSet() - val otherActions = enabledActions.toMutableSet() // actions not in the persistent set + val sourceSet = firstActions.toMutableSet() + val otherActions = enabledActions.toMutableSet() // actions not in the source set firstActions.forEach(otherActions::remove) val ignoredVarsByAction = otherActions.associateWith { mutableSetOf>() } @@ -88,39 +86,36 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap() for (action in otherActions) { - // for every action that is not in the persistent set it is checked whether it should be added to the persistent set - // (because it is dependent with an action already in the persistent set) + // for every action that is not in the source set it is checked whether it should be added to the source set + // (because it is dependent with an action already in the source set) val potentialIgnoredVars = mutableSetOf>() - if (persistentSet.any { persistentSetAction -> - areDependents(persistentSetAction, action, prec, potentialIgnoredVars) - }) { + if (sourceSet.any { areDependents(it, action, prec, potentialIgnoredVars) }) { if (isBackwardAction(action)) { return enabledActions.toSet() // see POR algorithm for the reason of removing backward transitions } - persistentSet.add(action) + sourceSet.add(action) actionsToRemove.add(action) addedNewAction = true } else { - checkNotNull(ignoredVarsByAction[action]).addAll( - potentialIgnoredVars) // the action is not added to the persistent set because we ignore variables in potentialIgnoredVars + // the action is not added to the source set because we ignore variables in potentialIgnoredVars + checkNotNull(ignoredVarsByAction[action]).addAll(potentialIgnoredVars) } } actionsToRemove.forEach(otherActions::remove) } otherActions.forEach { action -> ignoredVars.addAll(checkNotNull(ignoredVarsByAction[action])) } - return persistentSet + return sourceSet } - private fun areDependents(persistentSetAction: XcfaAction, action: XcfaAction, prec: Prec, + private fun areDependents(sourceSetAction: XcfaAction, action: XcfaAction, prec: Prec, ignoredVariables: MutableSet>): Boolean { - if (isSameProcess(persistentSetAction, action)) { + if (isSameProcess(sourceSetAction, action)) { return true } - val usedByPersistentSetAction = getCachedUsedSharedObjects( - getEdgeOf(persistentSetAction)) + val usedBySourceSetAction = getCachedUsedSharedObjects(getEdgeOf(sourceSetAction)) val influencedSharedObjects = getInfluencedSharedObjects(getEdgeOf(action)) for (varDecl in influencedSharedObjects) { - if (usedByPersistentSetAction.contains(varDecl)) { + if (usedBySourceSetAction.contains(varDecl)) { if (varDecl !in prec.usedVars) { // the actions would be dependent, but we may have a chance to ignore it in the current abstraction ignoredVariables.add(varDecl) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt index cf73181dc8..3fa838fc90 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt @@ -33,6 +33,9 @@ import kotlin.random.Random /** * LTS with a POR (Partial Order Reduction) algorithm applied as a filter when returning enabled actions. + * The algorithm is similar to the static source-set based POR algorithm described in the following paper: + * Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K. (2017): + * Comparing source sets and persistent sets for partial order reduction * * @param xcfa the XCFA of the verified program */ @@ -40,7 +43,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> companion object { - private val random: Random = Random.Default + var random: Random = Random.Default private val simpleXcfaLts = getXcfaLts() } @@ -76,16 +79,16 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> // Collecting enabled actions val allEnabledActions = getAllEnabledActionsFor(state) - // Calculating the persistent set starting from every (or some of the) enabled transition; the minimal persistent set is stored - var minimalPersistentSet = setOf() - val persistentSetFirstActions = getPersistentSetFirstActions(allEnabledActions) - for (firstActions in persistentSetFirstActions) { - val persistentSet = calculatePersistentSet(allEnabledActions, firstActions) - if (minimalPersistentSet.isEmpty() || persistentSet.size < minimalPersistentSet.size) { - minimalPersistentSet = persistentSet + // Calculating the source set starting from every (or some of the) enabled transition; the minimal source set is stored + var minimalSourceSet = setOf() + val sourceSetFirstActions = getSourceSetFirstActions(state, allEnabledActions) + for (firstActions in sourceSetFirstActions) { + val sourceSet = calculateSourceSet(allEnabledActions, firstActions) + if (minimalSourceSet.isEmpty() || sourceSet.size < minimalSourceSet.size) { + minimalSourceSet = sourceSet } } - return minimalPersistentSet + return minimalSourceSet } /** @@ -98,65 +101,101 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> simpleXcfaLts.getEnabledActionsFor(state) /** - * Returns the possible starting actions of a persistent set. + * Returns the possible starting actions of a source set. * * @param allEnabledActions the enabled actions in the present state - * @return the possible starting actions of a persistent set + * @return the possible starting actions of a source set */ - protected fun getPersistentSetFirstActions( + protected fun getSourceSetFirstActions(state: XcfaState<*>, allEnabledActions: Collection): Collection> { val enabledActionsByProcess = allEnabledActions.groupBy(XcfaAction::pid) val enabledProcesses = enabledActionsByProcess.keys.toList().shuffled(random) - return enabledProcesses.map { checkNotNull(enabledActionsByProcess[it]) } + return enabledProcesses.map { pid -> + val firstProcesses = mutableSetOf(pid) + checkMutexBlocks(state, pid, firstProcesses, enabledActionsByProcess) + firstProcesses.flatMap { enabledActionsByProcess[it] ?: emptyList() } + } } /** - * Calculates a persistent set of enabled actions starting from a particular action. + * Checks whether a process is blocked by a mutex and if it is, it adds the process that blocks it to the set of + * first processes. + * + * @param state the current state + * @param pid the process whose blocking is to be checked + * @param firstProcesses the set of first processes + * @param enabledActionsByProcess the enabled actions grouped by processes + * @return the set of first processes + */ + private fun checkMutexBlocks(state: XcfaState<*>, pid: Int, firstProcesses: MutableSet, + enabledActionsByProcess: Map>) { + val processState = checkNotNull(state.processes[pid]) + if (!processState.paramsInitialized) return + val disabledOutEdges = processState.locs.peek().outgoingEdges.filter { edge -> + enabledActionsByProcess[pid]?.none { action -> action.target == edge.target } ?: true + } + disabledOutEdges.forEach { edge -> + edge.getFlatLabels().filterIsInstance().forEach { fence -> + fence.labels.filter { it.startsWith("mutex_lock") }.forEach { lock -> + val mutex = lock.substringAfter('(').substringBefore(')') + state.mutexes[mutex]?.let { pid2 -> + if (pid2 !in firstProcesses) { + firstProcesses.add(pid2) + checkMutexBlocks(state, pid2, firstProcesses, enabledActionsByProcess) + } + } + } + } + } + } + + /** + * Calculates a source set of enabled actions starting from a particular action. * * @param enabledActions the enabled actions in the present state - * @param firstActions the actions that will be added to the persistent set as the first actions - * @return a persistent set of enabled actions + * @param firstActions the actions that will be added to the source set as the first actions + * @return a source set of enabled actions */ - private fun calculatePersistentSet(enabledActions: Collection, + private fun calculateSourceSet(enabledActions: Collection, firstActions: Collection): Set { if (firstActions.any(::isBackwardAction)) { return enabledActions.toSet() } - val persistentSet = firstActions.toMutableSet() - val otherActions = (enabledActions.toMutableSet() subtract persistentSet).toMutableSet() // actions not in the persistent set + val sourceSet = firstActions.toMutableSet() + val otherActions = (enabledActions.toMutableSet() subtract sourceSet).toMutableSet() // actions not in the source set var addedNewAction = true while (addedNewAction) { addedNewAction = false val actionsToRemove = mutableSetOf() for (action in otherActions) { - // for every action that is not in the persistent set it is checked whether it should be added to the persistent set - // (because it is dependent with an action already in the persistent set) - if (persistentSet.any { persistentSetAction -> areDependents(persistentSetAction, action) }) { + // for every action that is not in the source set it is checked whether it should be added to the source set + // (because it is dependent with an action already in the source set) + if (sourceSet.any { areDependents(it, action) }) { if (isBackwardAction(action)) { return enabledActions.toSet() // see POR algorithm for the reason of removing backward transitions } - persistentSet.add(action) + sourceSet.add(action) actionsToRemove.add(action) addedNewAction = true } } actionsToRemove.forEach(otherActions::remove) } - return persistentSet + return sourceSet } /** * Determines whether an action is dependent with another one (based on the notions introduced for the POR - * algorithm) already in the persistent set. + * algorithm) already in the source set. * - * @param persistentSetAction the action in the persistent set - * @param action the other action (not in the persistent set) - * @return true, if the two actions are dependent in the context of persistent sets + * @param sourceSetAction the action in the source set + * @param action the other action (not in the source set) + * @return true, if the two actions are dependent in the context of source sets */ - private fun areDependents(persistentSetAction: XcfaAction, action: XcfaAction): Boolean { - val usedByPersistentSetAction = getCachedUsedSharedObjects(getEdgeOf(persistentSetAction)) - return isSameProcess(persistentSetAction, action) || - getInfluencedSharedObjects(getEdgeOf(action)).any { it in usedByPersistentSetAction } + private fun areDependents(sourceSetAction: XcfaAction, action: XcfaAction): Boolean { + val usedBySourceSetAction = getCachedUsedSharedObjects(getEdgeOf(sourceSetAction)) + return isSameProcess(sourceSetAction, action) || + getInfluencedSharedObjects(getEdgeOf(action)).any { it in usedBySourceSetAction } } /** @@ -188,14 +227,25 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> * @param edge whose global variables are to be returned * @return the set of directly or indirectly used global variables */ - private fun getUsedSharedObjects(edge: XcfaEdge): Set> = - if (edge.getFlatLabels().any(XcfaLabel::isAtomicBegin)) { - getSharedObjectsWithBFS(edge) { - it.getFlatLabels().none(XcfaLabel::isAtomicEnd) - }.toSet() + private fun getUsedSharedObjects(edge: XcfaEdge): Set> { + val flatLabels = edge.getFlatLabels() + return if (flatLabels.any(XcfaLabel::isAtomicBegin)) { + getSharedObjectsWithBFS(edge) { it.getFlatLabels().none(XcfaLabel::isAtomicEnd) }.toSet() } else { - getDirectlyUsedSharedObjects(edge) + val lock = flatLabels.firstOrNull { + it is FenceLabel && it.labels.any { l -> l.startsWith("mutex_lock") } + } as FenceLabel? + if (lock != null) { + val mutex = lock.labels.first { l -> l.startsWith("mutex_lock") } + .substringAfter('(').substringBefore(')') + getSharedObjectsWithBFS(edge) { + it.getFlatLabels().none { fl -> fl is FenceLabel && "mutex_unlock(${mutex})" in fl.labels } + }.toSet() + } else { + getDirectlyUsedSharedObjects(edge) + } } + } /** * Same as [getUsedSharedObjects] with an additional cache layer. diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt index 244e1e5548..e4ff9e4b8d 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt @@ -43,6 +43,7 @@ import hu.bme.mit.theta.xcfa.analysis.ErrorDetection import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts +import hu.bme.mit.theta.xcfa.analysis.por.XcfaSporLts import hu.bme.mit.theta.xcfa.cli.utils.XcfaWitnessWriter import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer import hu.bme.mit.theta.xcfa.model.XCFA @@ -174,7 +175,10 @@ class XcfaCli(private val args: Array) { // propagating input variables LbePass.level = lbeLevel - if (randomSeed >= 0) XcfaDporLts.random = Random(randomSeed) + if (randomSeed >= 0){ + XcfaSporLts.random = Random(randomSeed) + XcfaDporLts.random = Random(randomSeed) + } if (argToFile) { WebDebuggerLogger.enableWebDebuggerLogger() WebDebuggerLogger.getInstance().setTitle(input?.name) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/PthreadFunctionsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/PthreadFunctionsPass.kt index bfe9f56947..eae9425e8d 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/PthreadFunctionsPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/PthreadFunctionsPass.kt @@ -36,70 +36,86 @@ class PthreadFunctionsPass(val parseContext: ParseContext) : ProcedurePass { checkNotNull(builder.metaData["deterministic"]) for (edge in ArrayList(builder.getEdges())) { val edges = edge.splitIf(this::predicate) - if (edges.size > 1 || (edges.size == 1 && predicate( - (edges[0].label as SequenceLabel).labels[0]))) { + if (edges.size > 1 || (edges.size == 1 && predicate((edges[0].label as SequenceLabel).labels[0]))) { builder.removeEdge(edge) - val labels: MutableList = ArrayList() edges.forEach { if (predicate((it.label as SequenceLabel).labels[0])) { val invokeLabel = it.label.labels[0] as InvokeLabel - val fence = when (invokeLabel.name) { + val metadata = invokeLabel.metadata + val fences: List = when (invokeLabel.name) { "pthread_join" -> { var handle = invokeLabel.params[1] while (handle is Reference<*, *>) handle = handle.op - check( - handle is RefExpr && (handle as RefExpr).decl is VarDecl) + check(handle is RefExpr && (handle as RefExpr).decl is VarDecl) - JoinLabel((handle as RefExpr).decl as VarDecl<*>, - metadata = invokeLabel.metadata) + listOf(JoinLabel((handle as RefExpr).decl as VarDecl<*>, metadata)) } "pthread_create" -> { var handle = invokeLabel.params[1] while (handle is Reference<*, *>) handle = handle.op - check( - handle is RefExpr && (handle as RefExpr).decl is VarDecl) + check(handle is RefExpr && (handle as RefExpr).decl is VarDecl) val funcptr = invokeLabel.params[3] - check( - funcptr is RefExpr && (funcptr as RefExpr).decl is VarDecl) + check(funcptr is RefExpr && (funcptr as RefExpr).decl is VarDecl) val param = invokeLabel.params[4] - StartLabel((funcptr as RefExpr).decl.name, + listOf(StartLabel((funcptr as RefExpr).decl.name, listOf(Int(0), param), // int(0) to solve StartLabel not handling return params - (handle as RefExpr).decl as VarDecl<*>, - metadata = invokeLabel.metadata) + (handle as RefExpr).decl as VarDecl<*>, metadata)) } "pthread_mutex_lock" -> { var handle = invokeLabel.params[1] while (handle is Reference<*, *>) handle = handle.op - check( - handle is RefExpr && (handle as RefExpr).decl is VarDecl) + check(handle is RefExpr && (handle as RefExpr).decl is VarDecl) - FenceLabel(setOf("mutex_lock(${handle.decl.name})"), - metadata = invokeLabel.metadata) + listOf(FenceLabel(setOf("mutex_lock(${handle.decl.name})"), metadata)) } "pthread_mutex_unlock" -> { var handle = invokeLabel.params[1] while (handle is Reference<*, *>) handle = handle.op - check( - handle is RefExpr && (handle as RefExpr).decl is VarDecl) + check(handle is RefExpr && (handle as RefExpr).decl is VarDecl) - FenceLabel(setOf("mutex_unlock(${handle.decl.name})"), - metadata = invokeLabel.metadata) + listOf(FenceLabel(setOf("mutex_unlock(${handle.decl.name})"), metadata)) } + "pthread_cond_wait" -> { + var cond = invokeLabel.params[1] + while (cond is Reference<*, *>) cond = cond.op + var handle = invokeLabel.params[2] + while (handle is Reference<*, *>) handle = handle.op + check(cond is RefExpr && (cond as RefExpr).decl is VarDecl) + check(handle is RefExpr && (handle as RefExpr).decl is VarDecl) + + listOf( + FenceLabel(setOf("start_cond_wait(${cond.decl.name},${handle.decl.name})"), + metadata), + FenceLabel(setOf("cond_wait(${cond.decl.name},${handle.decl.name})"), metadata) + ) + } + + "pthread_cond_signal" -> { + var cond = invokeLabel.params[1] + while (cond is Reference<*, *>) cond = cond.op + check(cond is RefExpr && (cond as RefExpr).decl is VarDecl) + + listOf(FenceLabel(setOf("cond_signal(${cond.decl.name})"), metadata)) + } + + "pthread_mutex_init", "pthread_cond_init" -> listOf(NopLabel) + else -> error("Unknown pthread function ${invokeLabel.name}") } - labels.add(fence) + edge.withLabel(SequenceLabel(fences)).splitIf { fence -> + fence is FenceLabel && fence.labels.any { l -> l.startsWith("start_cond_wait") } + }.forEach(builder::addEdge) } else { - labels.addAll(it.label.labels) + builder.addEdge(edge.withLabel(SequenceLabel(it.label.labels))) } } - builder.addEdge(edge.withLabel(SequenceLabel(labels))) } } return builder