diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcTypes.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcTypes.kt index 93f6039780..f39dbdc99c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcTypes.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcTypes.kt @@ -41,12 +41,12 @@ enum class EventType { WRITE, READ } abstract class Event( val const: IndexedConstDecl<*>, val type: EventType, - val guard: List>, + var guard: Set>, val pid: Int, val clkId: Int ) { - val guardExpr: Expr = guard.toAnd() + val guardExpr: Expr get() = guard.toAnd() var assignment: Expr? = null var enabled: Boolean? = null @@ -77,7 +77,9 @@ data class Relation( val declRef: RefExpr = RefExpr.of(decl) var enabled: Boolean? = null - override fun toString() = "Relation($type, ${from.const.name}[${from.type.toString()[0]}], ${to.const.name}[${to.type.toString()[0]}])" + override fun toString() = + "Relation($type, ${from.const.name}[${from.type.toString()[0]}], ${to.const.name}[${to.type.toString()[0]}])" + fun enabled(valuation: Map, LitExpr<*>>): Boolean? { enabled = if (type == RelationType.PO) true else valuation[decl]?.let { (it as BoolLitExpr).value } return enabled diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt index f0507b0f73..f10dd7889d 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt @@ -18,7 +18,10 @@ package hu.bme.mit.theta.xcfa.analysis.oc import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.oc.* +import hu.bme.mit.theta.analysis.algorithm.oc.EventType +import hu.bme.mit.theta.analysis.algorithm.oc.OcChecker +import hu.bme.mit.theta.analysis.algorithm.oc.Relation +import hu.bme.mit.theta.analysis.algorithm.oc.RelationType import hu.bme.mit.theta.analysis.unit.UnitPrec import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.decl.* @@ -35,12 +38,10 @@ import hu.bme.mit.theta.core.type.inttype.IntExprs.Int import hu.bme.mit.theta.core.utils.ExprUtils import hu.bme.mit.theta.core.utils.TypeUtils.cast import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory +import hu.bme.mit.theta.xcfa.* import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaPrec import hu.bme.mit.theta.xcfa.analysis.XcfaState -import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.isAtomicBegin -import hu.bme.mit.theta.xcfa.isAtomicEnd import hu.bme.mit.theta.xcfa.model.* import hu.bme.mit.theta.xcfa.passes.AssumeFalseRemovalPass import hu.bme.mit.theta.xcfa.passes.AtomicReadsOneWritePass @@ -68,10 +69,12 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv private val rfs = mutableMapOf, MutableList>() override fun check(prec: XcfaPrec?): SafetyResult, XcfaAction> = let { - if (xcfa.initProcedures.size > 1) error("Multiple entry points are not supported by this checker.") + if (xcfa.initProcedures.size > 1) error("Multiple entry points are not supported by OC checker.") logger.write(Logger.Level.MAINSTEP, "Adding constraints...\n") - if (!addConstraints()) return@let SafetyResult.safe() // no violations + xcfa.initProcedures.forEach { processThread(Thread(it.first)) } + addCrossThreadRelations() + if (!addToSolver()) return@let SafetyResult.safe() // no violations in the model logger.write(Logger.Level.MAINSTEP, "Start checking...\n") val status = ocChecker.check(events, pos, rfs) @@ -85,25 +88,11 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv } }.also { logger.write(Logger.Level.MAINSTEP, "OC checker result: $it\n") } - private fun addConstraints(): Boolean { - val threads = xcfa.initProcedures.map { Thread(it.first) }.toMutableSet() - this.threads.addAll(threads) - while (threads.isNotEmpty()) { - val thread = threads.first() - threads.remove(thread) - val newThreads = processThread(thread) - threads.addAll(newThreads) - this.threads.addAll(newThreads) - } - - addCrossThreadRelations() - return addToSolver() - } - private fun processThread(thread: Thread): List { + threads.add(thread) val pid = thread.pid var last = listOf() - var guard = listOf>() + var guard = setOf>() lateinit var lastWrites: MutableMap, Set> lateinit var edge: XcfaEdge var inEdge = false @@ -142,7 +131,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv check(current.incoming == current.loc.incomingEdges.size) check(current.incoming == current.guards.size || current.loc.initial) check(current.incoming == current.lastWrites.size) // lastEvents intentionally skipped - check(current.incoming == current.pidLookups.size) + check(current.incoming == current.threadLookups.size) check(current.incoming == current.atomics.size) check(current.atomics.all { it == current.atomics.first() }) // bad pattern otherwise @@ -153,12 +142,10 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv } if (current.loc.final) { - current.lastEvents.forEach { final -> - thread.joinEvents.forEach { join -> po(final, join) } - } + thread.finalEvents.addAll(current.lastEvents) } - val mergedGuard = current.guards.toOrInList() + val mergedGuard = current.guards.toOrInSet() val assumeConsts = mutableMapOf, MutableList>>() for (e in current.loc.outgoingEdges) { @@ -168,13 +155,16 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv // intersection of guards of incoming edges: guard = mergedGuard lastWrites = current.lastWrites.merge().toMutableMap() - val pidLookup = current.pidLookups.merge { s1, s2 -> + val threadLookup = current.threadLookups.merge { s1, s2 -> s1 + s2.filter { (guard2, _) -> s1.none { (guard1, _) -> guard1 == guard2 } } }.toMutableMap() var firstLabel = true atomicEntered = current.atomics.firstOrNull() edge.getFlatLabels().forEach { label -> + if (label.references.isNotEmpty() || label.dereferences.isNotEmpty()) { + error("References not supported by OC checker.") + } when (label) { is StmtLabel -> { when (val stmt = label.stmt) { @@ -217,28 +207,35 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv is StartLabel -> { // TODO StartLabel params + if (label.name in thread.startHistory) { + error("Recursive thread start not supported by OC checker.") + } val procedure = xcfa.procedures.find { it.name == label.name } ?: error("Procedure not found: ${label.name}") last = newEvent(label.pidVar, EventType.WRITE) val pidVar = label.pidVar.threadVar(pid) if (this.threads.any { it.pidVar == pidVar }) { - error("Multi-thread use of pthread_t variables are not supported by this checker.") + error("Using a pthread_t variable in multiple threads is not supported by OC checker.") } - val newThread = Thread(procedure, guard, pidVar, last.first()) + val newHistory = thread.startHistory + thread.procedure.name + val newThread = Thread(procedure, guard, pidVar, last.first(), newHistory) last.first().assignment = Eq(last.first().const.ref, Int(newThread.pid)) - pidLookup[pidVar] = setOf(Pair(guard, newThread.pid)) - threads.add(newThread) + threadLookup[pidVar] = setOf(Pair(guard, newThread)) + processThread(newThread) } is JoinLabel -> { - val guardTemp = guard + val incomingGuard = guard val lastEvents = mutableListOf() - pidLookup[label.pidVar.threadVar(pid)]?.forEach { (g, pid) -> - guard = g - lastEvents.addAll(newEvent(label.pidVar, EventType.READ)) - threads.find { it.pid == pid }?.joinEvents?.add(lastEvents.last()) - } ?: error("Thread started in a different thread: not supported by this checker.") - guard = guardTemp + val joinGuards = mutableListOf>>() + threadLookup[label.pidVar.threadVar(pid)]?.forEach { (g, thread) -> + guard = incomingGuard + g + thread.finalEvents.map { it.guard }.toOrInSet() + val joinEvent = newEvent(label.pidVar, EventType.READ).first() + thread.finalEvents.forEach { final -> po(final, joinEvent) } + lastEvents.add(joinEvent) + joinGuards.add(guard) + } ?: error("Thread started in a different thread: not supported by OC checker.") + guard = joinGuards.toOrInSet() last = lastEvents } @@ -251,7 +248,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv } is NopLabel -> {} - else -> error("Unsupported label type by this checker: $label") + else -> error("Unsupported label type by OC checker: $label") } firstLabel = false } @@ -261,7 +258,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv searchItem.guards.add(guard) searchItem.lastEvents.addAll(last) searchItem.lastWrites.add(lastWrites) - searchItem.pidLookups.add(pidLookup) + searchItem.threadLookups.add(threadLookup) searchItem.atomics.add(atomicEntered) searchItem.incoming++ if (searchItem.incoming == searchItem.loc.incomingEdges.size) { @@ -274,7 +271,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv for (e in current.loc.outgoingEdges) { val first = e.getFlatLabels().first() if (first !is StmtLabel || first.stmt !is AssumeStmt) { - error("Branching with non-assume labels not supported by this checker.") + error("Branching with non-assume labels not supported by OC checker.") } } assumeConsts.forEach { (_, set) -> @@ -287,7 +284,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv } } - if (waitList.isNotEmpty()) error("Loops and dangling edges not supported by this checker.") + if (waitList.isNotEmpty()) error("Loops and dangling edges not supported by OC checker.") return threads } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcTypes.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcTypes.kt index 04b19f8246..ec28aaa278 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcTypes.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcTypes.kt @@ -49,16 +49,16 @@ internal fun Collection>.toAnd(): Expr = when (size) { /** * Takes the OR of the contained lists mapped to an AND expression. Simplifications are made based on the list sizes. */ -internal fun Collection>>.toOrInList(): List> = when (size) { - 0 -> listOf() +internal fun Collection>>.toOrInSet(): Set> = when (size) { + 0 -> setOf() 1 -> first() - else -> listOf(Or(map { it.toAnd() })) + else -> setOf(Or(map { it.toAnd() })) } internal class XcfaEvent( const: IndexedConstDecl<*>, type: EventType, - guard: List>, + guard: Set>, pid: Int, val edge: XcfaEdge, clkId: Int = uniqueId() @@ -80,10 +80,11 @@ internal data class Violation( internal data class Thread( val procedure: XcfaProcedure, - val guard: List> = listOf(), + val guard: Set> = setOf(), val pidVar: VarDecl<*>? = null, val startEvent: XcfaEvent? = null, - val joinEvents: MutableSet = mutableSetOf(), + val startHistory: List = listOf(), + val finalEvents: MutableSet = mutableSetOf(), val pid: Int = uniqueId(), ) { @@ -96,10 +97,10 @@ internal data class Thread( internal data class SearchItem(val loc: XcfaLocation) { - val guards: MutableList>> = mutableListOf() + val guards: MutableList>> = mutableListOf() val lastEvents: MutableList = mutableListOf() val lastWrites: MutableList, Set>> = mutableListOf() - val pidLookups: MutableList, Set>, Int>>>> = mutableListOf() + val threadLookups: MutableList, Set>, Thread>>>> = mutableListOf() val atomics: MutableList = mutableListOf() var incoming: Int = 0 }