-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
COI (abstract data-flow-based statement simplification)
- Loading branch information
Showing
17 changed files
with
506 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
156 changes: 156 additions & 0 deletions
156
subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,156 @@ | ||
| package hu.bme.mit.theta.xcfa.analysis.coi | ||
|
|
||
| import hu.bme.mit.theta.analysis.LTS | ||
| import hu.bme.mit.theta.analysis.Prec | ||
| import hu.bme.mit.theta.analysis.TransFunc | ||
| import hu.bme.mit.theta.analysis.expr.ExprState | ||
| import hu.bme.mit.theta.core.decl.VarDecl | ||
| import hu.bme.mit.theta.core.stmt.AssignStmt | ||
| import hu.bme.mit.theta.core.stmt.HavocStmt | ||
| 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.analysis.getXcfaLts | ||
| import hu.bme.mit.theta.xcfa.analysis.por.extension | ||
| import hu.bme.mit.theta.xcfa.analysis.por.nullableExtension | ||
| import hu.bme.mit.theta.xcfa.model.* | ||
| import java.util.* | ||
| import kotlin.math.min | ||
|
|
||
| lateinit var ConeOfInfluence: XcfaCoi | ||
|
|
||
| internal typealias S = XcfaState<out ExprState> | ||
| internal typealias A = XcfaAction | ||
|
|
||
| internal var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() | ||
|
|
||
| abstract class XcfaCoi(protected val xcfa: XCFA) { | ||
|
|
||
| var coreLts: LTS<S, A> = getXcfaLts() | ||
| lateinit var coreTransFunc: TransFunc<S, A, XcfaPrec<out Prec>> | ||
|
|
||
| protected var lastPrec: Prec? = null | ||
| protected var XcfaLocation.scc: Int by extension() | ||
| protected val directObservation: MutableMap<XcfaEdge, MutableSet<XcfaEdge>> = mutableMapOf() | ||
|
|
||
| abstract val lts: LTS<S, A> | ||
|
|
||
| val transFunc = TransFunc<S, A, XcfaPrec<out Prec>> { state, action, prec -> | ||
| coreTransFunc.getSuccStates(state, action.transFuncVersion ?: action, prec) | ||
| } | ||
|
|
||
| init { | ||
| xcfa.procedures.forEach { tarjan(it.initLoc) } | ||
| } | ||
|
|
||
| private fun tarjan(initLoc: XcfaLocation) { | ||
| var sccCnt = 0 | ||
| var discCnt = 0 | ||
| val disc = mutableMapOf<XcfaLocation, Int>() | ||
| val lowest = mutableMapOf<XcfaLocation, Int>() | ||
| val visited = mutableSetOf<XcfaLocation>() | ||
| val stack = Stack<XcfaLocation>() | ||
| val toVisit = Stack<XcfaLocation>() | ||
| toVisit.push(initLoc) | ||
|
|
||
| while (toVisit.isNotEmpty()) { | ||
| val visiting = toVisit.peek() | ||
| if (visiting !in visited) { | ||
| disc[visiting] = discCnt++ | ||
| lowest[visiting] = disc[visiting]!! | ||
| stack.push(visiting) | ||
| visited.add(visiting) | ||
| } | ||
|
|
||
| for (edge in visiting.outgoingEdges) { | ||
| if (edge.target in stack) { | ||
| lowest[visiting] = min(lowest[visiting]!!, lowest[edge.target]!!) | ||
| } else if (edge.target !in visited) { | ||
| toVisit.push(edge.target) | ||
| break | ||
| } | ||
| } | ||
|
|
||
| if (toVisit.peek() != visiting) continue | ||
|
|
||
| if (lowest[visiting] == disc[visiting]) { | ||
| val scc = sccCnt++ | ||
| while (stack.peek() != visiting) { | ||
| stack.pop().scc = scc | ||
| } | ||
| stack.pop().scc = scc // visiting | ||
| } | ||
|
|
||
| toVisit.pop() | ||
| } | ||
| } | ||
|
|
||
| protected fun findDirectObservers(edge: XcfaEdge, prec: Prec) { | ||
| val precVars = prec.usedVars | ||
| val writtenVars = edge.getVars().filter { it.value.isWritten && it.key in precVars } | ||
| if (writtenVars.isEmpty()) return | ||
|
|
||
| val toVisit = mutableListOf(edge) | ||
| val visited = mutableSetOf<XcfaEdge>() | ||
| while (toVisit.isNotEmpty()) { | ||
| val visiting = toVisit.removeFirst() | ||
| visited.add(visiting) | ||
| addEdgeIfObserved(edge, visiting, writtenVars, precVars, directObservation) | ||
| toVisit.addAll(visiting.target.outgoingEdges.filter { it !in visited }) | ||
| } | ||
| } | ||
|
|
||
| protected open fun addEdgeIfObserved( | ||
| source: XcfaEdge, target: XcfaEdge, observableVars: Map<VarDecl<*>, AccessType>, | ||
| precVars: Collection<VarDecl<*>>, relation: MutableMap<XcfaEdge, MutableSet<XcfaEdge>> | ||
| ) { | ||
| val vars = target.getVars() | ||
| var relevantAction = vars.any { it.value.isWritten && it.key in precVars } | ||
| if (!relevantAction) { | ||
| val assumeVars = target.label.collectAssumesVars() | ||
| relevantAction = assumeVars.any { it in precVars } | ||
| } | ||
|
|
||
| if (relevantAction && vars.any { it.key in observableVars && it.value.isRead }) { | ||
| addToRelation(source, target, relation) | ||
| } | ||
| } | ||
|
|
||
| protected abstract fun addToRelation(source: XcfaEdge, target: XcfaEdge, | ||
| relation: MutableMap<XcfaEdge, MutableSet<XcfaEdge>>) | ||
|
|
||
| protected fun isRealObserver(edge: XcfaEdge) = edge.label.collectAssumesVars().isNotEmpty() | ||
|
|
||
| protected fun replace(action: A, prec: Prec): XcfaAction { | ||
| val replacedLabel = action.label.replace(prec) | ||
| action.transFuncVersion = action.withLabel(replacedLabel.run { | ||
| if (this !is SequenceLabel) SequenceLabel(listOf(this)) else this | ||
| }) | ||
| return action | ||
| } | ||
|
|
||
| private fun XcfaLabel.replace(prec: Prec): XcfaLabel = when (this) { | ||
| is SequenceLabel -> SequenceLabel(labels.map { it.replace(prec) }, metadata) | ||
| is NondetLabel -> NondetLabel(labels.map { it.replace(prec) }.toSet(), metadata) | ||
| is StmtLabel -> { | ||
| when (val stmt = this.stmt) { | ||
| is AssignStmt<*> -> if (stmt.varDecl in prec.usedVars) { | ||
| StmtLabel(HavocStmt.of(stmt.varDecl), metadata = this.metadata) | ||
| } else { | ||
| NopLabel | ||
| } | ||
|
|
||
| is HavocStmt<*> -> if (stmt.varDecl in prec.usedVars) { | ||
| this | ||
| } else { | ||
| NopLabel | ||
| } | ||
|
|
||
| else -> this | ||
| } | ||
| } | ||
|
|
||
| else -> this | ||
| } | ||
| } |
143 changes: 143 additions & 0 deletions
143
...xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,143 @@ | ||
| package hu.bme.mit.theta.xcfa.analysis.coi | ||
|
|
||
| import hu.bme.mit.theta.analysis.LTS | ||
| import hu.bme.mit.theta.analysis.Prec | ||
| import hu.bme.mit.theta.xcfa.getFlatLabels | ||
| import hu.bme.mit.theta.xcfa.getVars | ||
| import hu.bme.mit.theta.xcfa.isWritten | ||
| import hu.bme.mit.theta.xcfa.model.StartLabel | ||
| import hu.bme.mit.theta.xcfa.model.XCFA | ||
| import hu.bme.mit.theta.xcfa.model.XcfaEdge | ||
| import hu.bme.mit.theta.xcfa.model.XcfaProcedure | ||
|
|
||
| class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { | ||
|
|
||
| private val startThreads: MutableSet<XcfaEdge> = mutableSetOf() | ||
| private val edgeToProcedure: MutableMap<XcfaEdge, XcfaProcedure> = mutableMapOf() | ||
| private var XcfaEdge.procedure: XcfaProcedure | ||
| get() = edgeToProcedure[this]!! | ||
| set(value) { | ||
| edgeToProcedure[this] = value | ||
| } | ||
| private val interProcessObservation: MutableMap<XcfaEdge, MutableSet<XcfaEdge>> = mutableMapOf() | ||
|
|
||
| data class ProcedureEntry( | ||
| val procedure: XcfaProcedure, | ||
| val scc: Int, | ||
| val pid: Int | ||
| ) | ||
|
|
||
| override val lts = object : LTS<S, A> { | ||
| override fun getEnabledActionsFor(state: S): Collection<A> { | ||
| val enabled = coreLts.getEnabledActionsFor(state) | ||
| return lastPrec?.let { replaceIrrelevantActions(state, enabled, it) } ?: enabled | ||
| } | ||
|
|
||
| override fun <P : Prec> getEnabledActionsFor(state: S, explored: Collection<A>, prec: P): Collection<A> { | ||
| if (lastPrec != prec) reinitialize(prec) | ||
| val enabled = coreLts.getEnabledActionsFor(state, explored, prec) | ||
| return replaceIrrelevantActions(state, enabled, prec) | ||
| } | ||
|
|
||
| private fun replaceIrrelevantActions(state: S, enabled: Collection<A>, prec: Prec): Collection<A> { | ||
| val procedures = state.processes.map { (pid, pState) -> | ||
| val loc = pState.locs.peek() | ||
| val procedure = loc.incomingEdges.ifEmpty(loc::outgoingEdges).first().procedure | ||
| ProcedureEntry(procedure, loc.scc, pid) | ||
| }.toMutableList() | ||
|
|
||
| do { | ||
| var anyNew = false | ||
| startThreads.filter { edge -> | ||
| procedures.any { edge.procedure == it.procedure && it.scc >= edge.source.scc } | ||
| }.forEach { edge -> | ||
| edge.getFlatLabels().filterIsInstance<StartLabel>().forEach { startLabel -> | ||
| val procedure = xcfa.procedures.find { it.name == startLabel.name }!! | ||
| val procedureEntry = ProcedureEntry(procedure, procedure.initLoc.scc, -1) | ||
| if (procedureEntry !in procedures) { | ||
| procedures.add(procedureEntry) | ||
| anyNew = true | ||
| } | ||
| } | ||
| } | ||
| } while (anyNew) | ||
| val multipleProcedures = findDuplicates(procedures.map { it.procedure }) | ||
|
|
||
| return enabled.map { action -> | ||
| if (!isObserved(action, procedures, multipleProcedures)) { | ||
| replace(action, prec) | ||
| } else { | ||
| action.transFuncVersion = null | ||
| action | ||
| } | ||
| } | ||
| } | ||
|
|
||
| private fun isObserved(action: A, procedures: MutableList<ProcedureEntry>, | ||
| multipleProcedures: Set<XcfaProcedure>): Boolean { | ||
| val toVisit = edgeToProcedure.keys.filter { | ||
| it.source == action.edge.source && it.target == action.edge.target | ||
| }.toMutableList() | ||
| val visited = mutableSetOf<XcfaEdge>() | ||
|
|
||
| while (toVisit.isNotEmpty()) { | ||
| val visiting = toVisit.removeFirst() | ||
| if (isRealObserver(visiting)) return true | ||
|
|
||
| visited.add(visiting) | ||
| val toAdd = (directObservation[visiting] ?: emptySet()) union | ||
| (interProcessObservation[visiting]?.filter { edge -> | ||
| procedures.any { | ||
| it.procedure.name == edge.procedure.name && it.scc >= edge.source.scc && | ||
| (it.procedure.name != visiting.procedure.name || it.procedure in multipleProcedures) | ||
| } // the edge is still reachable | ||
| } ?: emptySet()) | ||
| toVisit.addAll(toAdd.filter { it !in visited }) | ||
| } | ||
| return false | ||
| } | ||
|
|
||
| fun findDuplicates(list: List<XcfaProcedure>): Set<XcfaProcedure> { | ||
| val seen = mutableSetOf<String>() | ||
| val duplicates = mutableSetOf<XcfaProcedure>() | ||
| for (item in list) { | ||
| if (!seen.add(item.name)) { | ||
| duplicates.add(item) | ||
| } | ||
| } | ||
| return duplicates | ||
| } | ||
| } | ||
|
|
||
| fun reinitialize(prec: Prec) { | ||
| directObservation.clear() | ||
| interProcessObservation.clear() | ||
| xcfa.procedures.forEach { procedure -> | ||
| procedure.edges.forEach { edge -> | ||
| edge.procedure = procedure | ||
| if (edge.getFlatLabels().any { it is StartLabel }) startThreads.add(edge) | ||
| findDirectObservers(edge, prec) | ||
| findInterProcessObservers(edge, prec) | ||
| } | ||
| } | ||
| lastPrec = prec | ||
| } | ||
|
|
||
| private fun findInterProcessObservers(edge: XcfaEdge, prec: Prec) { | ||
| val precVars = prec.usedVars | ||
| val writtenVars = edge.getVars().filter { it.value.isWritten && it.key in precVars } | ||
| if (writtenVars.isEmpty()) return | ||
|
|
||
| xcfa.procedures.forEach { procedure -> | ||
| procedure.edges.forEach { | ||
| addEdgeIfObserved(edge, it, writtenVars, precVars, interProcessObservation) | ||
| } | ||
| } | ||
| } | ||
|
|
||
| override fun addToRelation(source: XcfaEdge, target: XcfaEdge, | ||
| relation: MutableMap<XcfaEdge, MutableSet<XcfaEdge>>) { | ||
| relation[source] = relation[source] ?: mutableSetOf() | ||
| relation[source]!!.add(target) | ||
| } | ||
| } |
Oops, something went wrong.