diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java index 863a8802ad..2fbaf2b9e1 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredAbstractors.java @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.analysis.pred; +import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.ConstDecl; import hu.bme.mit.theta.core.decl.Decls; @@ -23,6 +24,7 @@ import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.PathUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexing; import hu.bme.mit.theta.solver.Solver; @@ -69,6 +71,15 @@ public interface PredAbstractor { Collection createStatesForExpr(final Expr expr, final VarIndexing exprIndexing, final PredPrec prec, final VarIndexing precIndexing); + + default Collection createStatesForExpr(final Expr expr, + final VarIndexing exprIndexing, + final PredPrec prec, + final VarIndexing precIndexing, + final PredState state, + final ExprAction action) { + return createStatesForExpr(expr, exprIndexing, prec, precIndexing); + } } /** @@ -225,5 +236,23 @@ public Collection createStatesForExpr(final Expr expr, return Collections.singleton(PredState.of(newStatePreds)); } + @Override + public Collection createStatesForExpr(final Expr expr, + final VarIndexing exprIndexing, + final PredPrec prec, + final VarIndexing precIndexing, + final PredState state, + final ExprAction action) { + var actionExpr = action.toExpr(); + if (actionExpr.equals(True())) { + var filteredPreds = state.getPreds().stream().filter(p -> { + var vars = ExprUtils.getVars(p); + var indexing = action.nextIndexing(); + return vars.stream().allMatch(v -> indexing.get(v) == 0); + }).collect(Collectors.toList()); + return Collections.singleton(PredState.of(filteredPreds)); + } + return createStatesForExpr(expr, exprIndexing, prec, precIndexing); + } } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredTransFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredTransFunc.java index fa243f4fcb..b5ac6c5e2e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredTransFunc.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredTransFunc.java @@ -50,7 +50,7 @@ public Collection getSuccStates(final PredState state, final Collection succStates = predAbstractor.createStatesForExpr( And(state.toExpr(), action.toExpr()), VarIndexingFactory.indexing(0), prec, - action.nextIndexing()); + action.nextIndexing(), state, action); return succStates.isEmpty() ? Collections.singleton(PredState.bottom()) : succStates; } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt index 1f66ff86b6..29f55d2bdb 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt @@ -38,6 +38,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.core.utils.TypeUtils import hu.bme.mit.theta.solver.Solver import hu.bme.mit.theta.xcfa.analysis.XcfaProcessState.Companion.createLookup +import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.getGlobalVars import hu.bme.mit.theta.xcfa.isWritten @@ -50,9 +51,14 @@ import java.util.function.Predicate open class XcfaAnalysis( private val corePartialOrd: PartialOrd>, private val coreInitFunc: InitFunc, XcfaPrec

>, - private val coreTransFunc: TransFunc, XcfaAction, XcfaPrec

>, + private var coreTransFunc: TransFunc, XcfaAction, XcfaPrec

>, ) : Analysis, XcfaAction, XcfaPrec

> { + init { + ConeOfInfluence.coreTransFunc = transFunc as TransFunc, XcfaAction, XcfaPrec> + coreTransFunc = ConeOfInfluence.transFunc as TransFunc, XcfaAction, XcfaPrec

> + } + override fun getPartialOrd(): PartialOrd> = corePartialOrd override fun getInitFunc(): InitFunc, XcfaPrec

> = coreInitFunc override fun getTransFunc(): TransFunc, XcfaAction, XcfaPrec

> = coreTransFunc diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt new file mode 100644 index 0000000000..fc38995493 --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt @@ -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 +internal typealias A = XcfaAction + +internal var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() + +abstract class XcfaCoi(protected val xcfa: XCFA) { + + var coreLts: LTS = getXcfaLts() + lateinit var coreTransFunc: TransFunc> + + protected var lastPrec: Prec? = null + protected var XcfaLocation.scc: Int by extension() + protected val directObservation: MutableMap> = mutableMapOf() + + abstract val lts: LTS + + val transFunc = TransFunc> { 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() + val lowest = mutableMapOf() + val visited = mutableSetOf() + val stack = Stack() + val toVisit = Stack() + 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() + 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, AccessType>, + precVars: Collection>, relation: MutableMap> + ) { + 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>) + + 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 + } +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt new file mode 100644 index 0000000000..14802dc422 --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt @@ -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 = mutableSetOf() + private val edgeToProcedure: MutableMap = mutableMapOf() + private var XcfaEdge.procedure: XcfaProcedure + get() = edgeToProcedure[this]!! + set(value) { + edgeToProcedure[this] = value + } + private val interProcessObservation: MutableMap> = mutableMapOf() + + data class ProcedureEntry( + val procedure: XcfaProcedure, + val scc: Int, + val pid: Int + ) + + override val lts = object : LTS { + override fun getEnabledActionsFor(state: S): Collection { + val enabled = coreLts.getEnabledActionsFor(state) + return lastPrec?.let { replaceIrrelevantActions(state, enabled, it) } ?: enabled + } + + override fun

getEnabledActionsFor(state: S, explored: Collection, prec: P): Collection { + if (lastPrec != prec) reinitialize(prec) + val enabled = coreLts.getEnabledActionsFor(state, explored, prec) + return replaceIrrelevantActions(state, enabled, prec) + } + + private fun replaceIrrelevantActions(state: S, enabled: Collection, prec: Prec): Collection { + 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().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, + multipleProcedures: Set): Boolean { + val toVisit = edgeToProcedure.keys.filter { + it.source == action.edge.source && it.target == action.edge.target + }.toMutableList() + val visited = mutableSetOf() + + 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): Set { + val seen = mutableSetOf() + val duplicates = mutableSetOf() + 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>) { + relation[source] = relation[source] ?: mutableSetOf() + relation[source]!!.add(target) + } +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt new file mode 100644 index 0000000000..e86648fd6d --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt @@ -0,0 +1,68 @@ +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.model.XCFA +import hu.bme.mit.theta.xcfa.model.XcfaEdge +import hu.bme.mit.theta.xcfa.model.XcfaLocation + +class XcfaCoiSingleThread(xcfa: XCFA) : XcfaCoi(xcfa) { + + private var observed: Set> = setOf() + + override val lts = object : LTS { + override fun getEnabledActionsFor(state: S): Collection { + val enabled = coreLts.getEnabledActionsFor(state) + return lastPrec?.let { replaceIrrelevantActions(enabled, it) } ?: enabled + } + + override fun

getEnabledActionsFor(state: S, explored: Collection, prec: P): Collection { + if (lastPrec != prec) reinitialize(prec) + val enabled = coreLts.getEnabledActionsFor(state, explored, prec) + return replaceIrrelevantActions(enabled, prec) + } + + private fun replaceIrrelevantActions(enabled: Collection, prec: Prec): Collection = + enabled.map { action -> + if (Pair(action.source, action.target) !in observed) { + replace(action, prec) + } else { + action.transFuncVersion = null + action + } + } + } + + fun reinitialize(prec: Prec) { + lastPrec = prec + directObservation.clear() + val realObservers = mutableSetOf() + xcfa.procedures.forEach { procedure -> + procedure.edges.forEach { edge -> + findDirectObservers(edge, prec) + if (isRealObserver(edge)) { + realObservers.add(edge) + } + } + } + collectedObservedEdges(realObservers) + } + + override fun addToRelation(source: XcfaEdge, target: XcfaEdge, + relation: MutableMap>) { + relation[target] = relation[target] ?: mutableSetOf() + relation[target]!!.add(source) + } + + private fun collectedObservedEdges(realObservers: Set) { + val toVisit = realObservers.toMutableList() + val visited = mutableSetOf() + while (toVisit.isNotEmpty()) { + val visiting = toVisit.removeFirst() + visited.add(visiting) + val toAdd = directObservation[visiting] ?: emptySet() + toVisit.addAll(toAdd.filter { it !in visited }) + } + observed = visited.map { it.source to it.target }.toSet() + } +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt new file mode 100644 index 0000000000..562dd1e800 --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt @@ -0,0 +1,28 @@ +package hu.bme.mit.theta.xcfa.analysis.por + +import hu.bme.mit.theta.analysis.LTS +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.core.decl.Decl +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.xcfa.analysis.XcfaAction +import hu.bme.mit.theta.xcfa.analysis.XcfaState +import hu.bme.mit.theta.xcfa.analysis.coi.transFuncVersion +import hu.bme.mit.theta.xcfa.model.XCFA +import hu.bme.mit.theta.xcfa.model.XcfaEdge + +class XcfaAasporCoiLts( + xcfa: XCFA, + ignoredVarRegistry: MutableMap, MutableSet>, + coiLTS: LTS, XcfaAction> +) : XcfaAasporLts(xcfa, ignoredVarRegistry) { + + init { + simpleXcfaLts = coiLTS + } + + override fun getEdgeOf(action: XcfaAction): XcfaEdge = + super.getEdgeOf(action.transFuncVersion ?: action) + + override fun isBackwardAction(action: XcfaAction): Boolean = + backwardTransitions.any { it.source == action.edge.source && it.target == action.edge.target } +} \ No newline at end of file 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 38b140cbe4..ee5bcc5e21 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 @@ -23,13 +23,13 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.model.XCFA -class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap, MutableSet>) : +open class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap, MutableSet>) : XcfaSporLts(xcfa) { override fun

getEnabledActionsFor(state: XcfaState<*>, exploredActions: Collection, prec: P): Set { // Collecting enabled actions - val allEnabledActions = getAllEnabledActionsFor(state) + val allEnabledActions = simpleXcfaLts.getEnabledActionsFor(state, exploredActions, prec) // 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 diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt index 63f7a47d8b..6a60b9a5ae 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt @@ -471,7 +471,7 @@ class XcfaAadporLts(private val xcfa: XCFA) : XcfaDporLts(xcfa) { /** * The current precision of the abstraction. */ - private lateinit var prec: Prec + private var prec: Prec? = null /** * Returns actions to be explored from the given state considering the given precision. @@ -487,9 +487,9 @@ class XcfaAadporLts(private val xcfa: XCFA) : XcfaDporLts(xcfa) { override fun dependent(a: A, b: A): Boolean { if (a.pid == b.pid) return true + val precVars = prec?.usedVars?.toSet() ?: return super.dependent(a, b) val aGlobalVars = a.edge.getGlobalVars(xcfa) val bGlobalVars = b.edge.getGlobalVars(xcfa) - val precVars = prec.usedVars.toSet() // dependent if they access the same variable in the precision (at least one write) return (aGlobalVars.keys intersect bGlobalVars.keys intersect precVars).any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten } } 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 3fa838fc90..b384f1bc25 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 @@ -44,9 +44,10 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> companion object { var random: Random = Random.Default - private val simpleXcfaLts = getXcfaLts() } + protected var simpleXcfaLts = getXcfaLts() + /* CACHE COLLECTIONS */ /** @@ -63,7 +64,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> /** * Backward transitions in the transition system (a transition of a loop). */ - private val backwardTransitions: MutableSet = mutableSetOf() + protected val backwardTransitions: MutableSet = mutableSetOf() init { collectBackwardTransitions() @@ -311,7 +312,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> * @param action the action whose edge is to be returned * @return the edge of the action */ - protected fun getEdgeOf(action: XcfaAction) = action.edge + protected open fun getEdgeOf(action: XcfaAction) = action.edge /** * Returns the outgoing edges of the target of the given edge. @@ -337,7 +338,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> * @param action the action to be classified as backward action or non-backward action * @return true, if the action is a backward action */ - protected fun isBackwardAction(action: XcfaAction): Boolean = backwardTransitions.contains(getEdgeOf(action)) + protected open fun isBackwardAction(action: XcfaAction): Boolean = backwardTransitions.contains(getEdgeOf(action)) /** * Collects backward edges of the given XCFA. diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt index 506ad1d44b..3f73d66666 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt @@ -41,6 +41,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs import hu.bme.mit.theta.solver.Solver import hu.bme.mit.theta.solver.SolverFactory import hu.bme.mit.theta.xcfa.analysis.* +import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence import hu.bme.mit.theta.xcfa.analysis.por.* import hu.bme.mit.theta.xcfa.cli.utils.XcfaDistToErrComparator import hu.bme.mit.theta.xcfa.collectAssumes @@ -311,6 +312,29 @@ enum class InitPrec( } +enum class ConeOfInfluenceMode( + val getLts: (XCFA, MutableMap, MutableSet>, POR) -> LTS, XcfaAction> +) { + + NO_COI({ xcfa, ivr, por -> + por.getLts(xcfa, ivr).also { NO_COI.porLts = it } + }), + COI({ xcfa, ivr, por -> + ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { COI.porLts = it } + ConeOfInfluence.lts + }), + POR_COI({ xcfa, ivr, _ -> + ConeOfInfluence.coreLts = getXcfaLts() + XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts) + }), + POR_COI_POR({ xcfa, ivr, por -> + ConeOfInfluence.coreLts = por.getLts(xcfa, ivr).also { POR_COI_POR.porLts = it } + XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts) + }) + ; + var porLts: LTS, XcfaAction>? = null +} + // TODO CexMonitor: disable for multi_seq? enum class CexMonitorOptions { diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt index e68e5e8d30..2532911a10 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt @@ -42,9 +42,7 @@ import hu.bme.mit.theta.core.decl.Decl import hu.bme.mit.theta.core.type.Type import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.solver.SolverFactory -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.* import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts import hu.bme.mit.theta.xcfa.model.XCFA import java.io.BufferedReader @@ -77,6 +75,8 @@ data class XcfaCegarConfig( var initPrec: InitPrec = InitPrec.EMPTY, @Parameter(names = ["--por-level"], description = "POR dependency level") var porLevel: POR = POR.NOPOR, + @Parameter(names = ["--coi"]) + var coi: ConeOfInfluenceMode = ConeOfInfluenceMode.NO_COI, @Parameter(names = ["--refinement-solver"], description = "Refinement solver name") var refinementSolver: String = "Z3", @Parameter(names = ["--validate-refinement-solver"], @@ -107,9 +107,9 @@ data class XcfaCegarConfig( val ignoredVarRegistry = mutableMapOf, MutableSet>() - val lts = porLevel.getLts(xcfa, ignoredVarRegistry) + val lts = coi.getLts(xcfa, ignoredVarRegistry, porLevel) val waitlist = if (porLevel.isDynamic) { - (lts as XcfaDporLts).waitlist + (coi.porLts as XcfaDporLts).waitlist } else { PriorityWaitlist.create, XcfaAction>>( search.getComp(xcfa)) 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 e4ff9e4b8d..19cd03eb05 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 @@ -42,6 +42,9 @@ import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager 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.coi.ConeOfInfluence +import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread +import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiSingleThread 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 @@ -175,9 +178,10 @@ class XcfaCli(private val args: Array) { // propagating input variables LbePass.level = lbeLevel - if (randomSeed >= 0){ - XcfaSporLts.random = Random(randomSeed) - XcfaDporLts.random = Random(randomSeed) + if (randomSeed >= 0) { + val random = Random(randomSeed) + XcfaSporLts.random = random + XcfaDporLts.random = random } if (argToFile) { WebDebuggerLogger.enableWebDebuggerLogger() @@ -185,10 +189,10 @@ class XcfaCli(private val args: Array) { } LoopUnrollPass.UNROLL_LIMIT = loopUnroll - logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType") val parseContext = ParseContext() val xcfa = getXcfa(logger, explicitProperty, parseContext) + ConeOfInfluence = if (parseContext.multiThreading) XcfaCoiMultiThread(xcfa) else XcfaCoiSingleThread(xcfa) logger.write(Logger.Level.INFO, "Frontend finished: ${xcfa.name} (in ${ stopwatch.elapsed(TimeUnit.MILLISECONDS) } ms)\n") diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt index c0f7c69d35..1d59429472 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt @@ -49,6 +49,14 @@ fun XcfaLabel.collectAssumes(): Iterable> = when (this) { else -> setOf() } +fun XcfaLabel.collectAssumesVars(): Set> { + return collectAssumes().flatMap { + val v = mutableSetOf>() + ExprUtils.collectVars(it, v) + v + }.toSet() +} + fun XcfaLabel.collectHavocs(): Set> = when (this) { is StmtLabel -> when (stmt) { is HavocStmt<*> -> setOf(stmt) @@ -92,7 +100,7 @@ private fun List.mergeAndCollect(): VarAccessMap = this.fold(mapOf /** * Returns the list of accessed variables by the label. - * The variable is associated with true if the variable is written and false otherwise. + * The variable is associated with an AccessType object based on whether the variable is read/written by the label. */ internal fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { is StmtLabel -> { @@ -164,6 +172,11 @@ fun XcfaEdge.getGlobalVars(xcfa: XCFA): Map, AccessType> { } } +/** + * Returns the list of accessed variables by the edge associated with an AccessType object. + */ +fun XcfaEdge.getVars(): Map, AccessType> = label.collectVarsWithAccessType() + /** * Returns true if the edge starts an atomic block. */ diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt index 077a589ad1..5590f2f048 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt @@ -198,7 +198,13 @@ class XcfaProcedureBuilder @JvmOverloads constructor( !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } while (locs.any(pred)) { locs.removeIf(pred) - edges.removeIf { pred(it.source) } + edges.removeIf { + pred(it.source).also { removing -> + if (removing) { + it.target.incomingEdges.remove(it) + } + } + } } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt index 4f7e8b8f68..4889fc3a18 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt @@ -278,7 +278,7 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { if (location.outgoingEdges.size != 1) return false val outEdge = location.outgoingEdges.first() if ( - location.incomingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } } + location.incomingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel || (it is StmtLabel && it.stmt is AssumeStmt) } } || location.outgoingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } } || (level == LbeLevel.LBE_LOCAL && !atomicPhase && isNotLocal(outEdge)) ) { diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt index f8281e686a..9b7a4ac9d5 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt @@ -67,22 +67,21 @@ class LoopUnrollPass : ProcedurePass { state = transFunc.getSuccStates(state, BasicStmtAction(loopVarInit), prec).first() var cnt = 0 - while (!transFunc.getSuccStates(state, BasicStmtAction(loopCondEdge), prec) - .first().isBottom - ) { + while (!transFunc.getSuccStates(state, BasicStmtAction(loopCondEdge), prec).first().isBottom) { cnt++ if (cnt > UNROLL_LIMIT) return -1 - state = - transFunc.getSuccStates(state, BasicStmtAction(loopVarModifiers), prec).first() + state = transFunc.getSuccStates(state, BasicStmtAction(loopVarModifiers), prec).first() } return cnt } private fun XcfaLabel.removeCondition(): XcfaLabel { - val stmtToRemove = - getFlatLabels().find { it is StmtLabel && it.stmt is AssumeStmt && (it.collectVars() - loopVar).isEmpty() } + val stmtToRemove = getFlatLabels().find { + it is StmtLabel && it.stmt is AssumeStmt && (it.collectVars() - loopVar).isEmpty() + } return when { this == stmtToRemove -> NopLabel + this is SequenceLabel -> SequenceLabel( labels.map { it.removeCondition() }, metadata )