diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java index a8506c0182..9ff64bff3b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java @@ -86,7 +86,7 @@ public void setState(final S state) { public boolean mayCover(final ArgNode node) { if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) { - return ancestors().noneMatch(n -> n.equals(node) || n.isSubsumed()); + return !(this.equals(node) || this.isSubsumed()); } else { return false; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java index b4785eeb81..e9811ba8fb 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java @@ -129,6 +129,7 @@ private void close(final ArgNode node, final Collection> can for (final ArgNode candidate : candidates) { if (candidate.mayCover(node)) { node.cover(candidate); + COILogger.incCovers(); return; } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java new file mode 100644 index 0000000000..1f93c7b300 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java @@ -0,0 +1,67 @@ +package hu.bme.mit.theta.analysis.algorithm.cegar; + +import java.util.ArrayList; +import java.util.List; + +public class COILogger { + static long coiTimer = 0; + static long transFuncTimer = 0; + private static long startCoi = 0; + private static long startTransFunc = 0; + public static void startCoiTimer() { + startCoi = System.currentTimeMillis(); + } + public static void stopCoiTimer() { + coiTimer += System.currentTimeMillis() - startCoi; + } + public static void startTransFuncTimer() { + startTransFunc = System.currentTimeMillis(); + } + public static void stopTransFuncTimer() { + transFuncTimer += System.currentTimeMillis() - startTransFunc; + } + + static long nops = 0; + static List nopsList = new ArrayList<>(); + public static void incNops() { + nops++; + } + public static void decNops() { + nops--; + } + static long havocs = 0; + static List havocsList = new ArrayList<>(); + public static void incHavocs() { + havocs++; + } + public static void decHavocs() { + havocs--; + } + static long allLabels = 0; + static List allLabelsList = new ArrayList<>(); + public static void incAllLabels() { + allLabels++; + } + static long exploredActions = 0; + static List exploredActionsList = new ArrayList<>(); + public static void incExploredActions() { + exploredActions++; + } + static long covers = 0; + static List coversList = new ArrayList<>(); + public static void incCovers() { + covers++; + } + public static void newIteration() { + nopsList.add(nops); + havocsList.add(havocs); + allLabelsList.add(allLabels); + exploredActionsList.add(exploredActions); + coversList.add(covers); + nops = 0; + havocs = 0; + allLabels = 0; + exploredActions = 0; + covers = 0; + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java index 677ab071be..81ab702a4c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java @@ -29,9 +29,13 @@ import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.common.logging.NullLogger; +import hu.bme.mit.theta.common.visualization.Graph; +import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; import hu.bme.mit.theta.common.visualization.writer.JSONWriter; import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger; +import java.io.FileWriter; +import java.io.IOException; import java.util.concurrent.TimeUnit; import static com.google.common.base.Preconditions.checkNotNull; @@ -80,7 +84,7 @@ public SafetyResult check(final P initPrec) { AbstractorResult abstractorResult = null; P prec = initPrec; int iteration = 0; - WebDebuggerLogger wdl = WebDebuggerLogger.getInstance(); +// WebDebuggerLogger wdl = WebDebuggerLogger.getInstance(); do { ++iteration; @@ -91,10 +95,11 @@ public SafetyResult check(final P initPrec) { abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime; logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult); - String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg)); - String precString = prec.toString(); +// String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg)); +// String precString = prec.toString(); - wdl.addIteration(iteration, argGraph, precString); +// wdl.addIteration(iteration, argGraph, precString); + COILogger.newIteration(); if (abstractorResult.isUnsafe()) { MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG"); @@ -136,6 +141,15 @@ public SafetyResult check(final P initPrec) { assert cegarResult != null; logger.write(Level.RESULT, "%s%n", cegarResult); logger.write(Level.INFO, "%s%n", stats); + System.err.println("Abstractor time: " + stats.getAbstractorTimeMs()); + System.err.println("Refiner time: " + stats.getRefinerTimeMs()); + System.err.println("COI time: " + COILogger.coiTimer); + System.err.println("TransFunc time: " + COILogger.transFuncTimer); + System.err.println("COI NOP labels: " + COILogger.nopsList); + System.err.println("COI havoc labels: " + COILogger.havocsList); + System.err.println("COI all labels: " + COILogger.allLabelsList); + System.err.println("Covers: " + COILogger.coversList); + System.err.println("Explored actions: " + COILogger.exploredActionsList); return cegarResult; } 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 6e6121c3ae..460e07248e 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.COI 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 { + COI.coreTransFunc = transFunc as TransFunc, XcfaAction, XcfaPrec> + coreTransFunc = COI.transFunc as TransFunc, XcfaAction, XcfaPrec

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

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

> = coreTransFunc @@ -192,6 +198,7 @@ fun , P : XcfaPrec> getXcfaAbstractor( BasicAbstractor.builder(getXcfaArgBuilder(analysis, lts, errorDetection)) .waitlist(waitlist as Waitlist>) // TODO: can we do this nicely? .stopCriterion(stopCriterion as StopCriterion).logger(logger) + .projection { it.processes } .build() // TODO: can we do this nicely? /// EXPL 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..7b17de49b4 --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt @@ -0,0 +1,175 @@ +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.algorithm.cegar.COILogger +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 COI: 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 -> + val a = action.transFuncVersion ?: action + action.label.getFlatLabels().forEach { + if (it is NopLabel) COILogger.decNops() + if (it is StmtLabel && it.stmt is HavocStmt<*>) COILogger.decHavocs() + } + a.label.getFlatLabels().forEach { + COILogger.incAllLabels() + if (it is NopLabel) COILogger.incNops() + if (it is StmtLabel && it.stmt is HavocStmt<*>) COILogger.incHavocs() + } + COILogger.incExploredActions() + + COILogger.startTransFuncTimer() + val r = coreTransFunc.getSuccStates(state, a, prec) + COILogger.stopTransFuncTimer() + + r + } + + init { + COILogger.startCoiTimer() + xcfa.procedures.forEach { tarjan(it.initLoc) } + COILogger.stopCoiTimer() + } + + 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..6c3a96d95c --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt @@ -0,0 +1,152 @@ +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.algorithm.cegar.COILogger +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) + COILogger.startCoiTimer() + val r = lastPrec?.let { replaceIrrelevantActions(state, enabled, it) } ?: enabled + COILogger.stopCoiTimer() + return r + } + + override fun

getEnabledActionsFor(state: S, explored: Collection, prec: P): Collection { + COILogger.startCoiTimer() + if (lastPrec != prec) reinitialize(prec) + COILogger.stopCoiTimer() + val enabled = coreLts.getEnabledActionsFor(state, explored, prec) + COILogger.startCoiTimer() + val r = replaceIrrelevantActions(state, enabled, prec) + COILogger.stopCoiTimer() + return r + } + + 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..38cd7085da --- /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 getTransitionOf(action: XcfaAction): XcfaEdge = + super.getTransitionOf(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 f5ba5b18fc..54043acd80 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,7 +23,7 @@ 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, +open class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap, MutableSet>) : XcfaSporLts(xcfa) { @@ -33,7 +33,7 @@ class XcfaAasporLts(xcfa: XCFA, prec: P ): Set { // Collecting enabled actions - val allEnabledActions = getAllEnabledActionsFor(state) + val allEnabledActions = simpleXcfaLts.getEnabledActionsFor(state, exploredActions, prec) // Calculating the persistent set starting from every (or some of the) enabled transition or from exploredActions if it is not empty // The minimal persistent 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 81ddf8de8d..a3b7ba7cf9 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 @@ -198,7 +198,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { if (stack.size >= 2) { val lastButOne = stack[stack.size - 2] val mutexNeverReleased = - last.mutexLocks.containsKey("") && (last.state.mutexes.keys subtract lastButOne.state.mutexes.keys).contains( + last.mutexLocks.containsKey( + "") && (last.state.mutexes.keys subtract lastButOne.state.mutexes.keys).contains( "" ) if (last.node.explored.isEmpty() || mutexNeverReleased) { @@ -413,10 +414,10 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { private fun notdep(start: Int, action: A): List { val e = stack[start].action return stack.slice(start + 1 until stack.size).filterIndexed { index, item -> - item.node.parent.get() == stack[start + 1 + index - 1].node && !dependent( - e, item.action - ) - }.map { it.action }.toMutableList().apply { add(action) } + item.node.parent.get() == stack[start + 1 + index - 1].node && !dependent( + e, item.action + ) + }.map { it.action }.toMutableList().apply { add(action) } } /** @@ -468,7 +469,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. @@ -484,9 +485,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 cbaba22ba1..86b4843173 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 @@ -34,10 +34,11 @@ open class XcfaSporLts(protected val xcfa: XCFA) : SporLts, XcfaAct companion object { - private val random: Random = Random.Default - private val simpleXcfaLts = getXcfaLts() + var random: Random = Random.Default } + protected var simpleXcfaLts = getXcfaLts() + init { collectBackwardTransitions() } 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..e3215fc235 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.COI 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_POR({ xcfa, ivr, por -> + COI.coreLts = por.getLts(xcfa, ivr).also { COI_POR.porLts = it } + COI.lts + }), + POR_COI({ xcfa, ivr, _ -> + COI.coreLts = getXcfaLts() + XcfaAasporCoiLts(xcfa, ivr, COI.lts) + }), + POR_COI_POR({ xcfa, ivr, por -> + COI.coreLts = por.getLts(xcfa, ivr).also { POR_COI_POR.porLts = it } + XcfaAasporCoiLts(xcfa, ivr, COI.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 fc9e1363f2..34aad89a80 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"], @@ -109,9 +109,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 e0c908663e..beca64d107 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,7 +42,11 @@ 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.COI +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 import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer import hu.bme.mit.theta.xcfa.model.XCFA @@ -172,13 +176,18 @@ class XcfaCli(private val args: Array) { // propagating input variables LbePass.level = lbeLevel - if (randomSeed >= 0) XcfaDporLts.random = Random(randomSeed) + if (randomSeed >= 0) { + val random = Random(randomSeed) + XcfaSporLts.random = random + XcfaDporLts.random = random + } LoopUnrollPass.UNROLL_LIMIT = loopUnroll WebDebuggerLogger.getInstance().setTitle(input?.name) logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType") val parseContext = ParseContext() val xcfa = getXcfa(logger, explicitProperty, parseContext) + COI = 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/LoopUnrollPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt index 9613ba5b98..fc4aaa8a0a 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 @@ -40,6 +40,7 @@ import java.util.* class LoopUnrollPass : ProcedurePass { companion object { + var UNROLL_LIMIT = 50 private val solver: Solver = SolverManager.resolveSolverFactory("Z3").createSolver() @@ -48,8 +49,11 @@ class LoopUnrollPass : ProcedurePass { private val testedLoops = mutableSetOf() private data class Loop( - val loopVar: VarDecl<*>, val loopVarModifiers: List, val loopVarInit: XcfaEdge, val loopCondEdge: XcfaEdge, val exitCondEdge: XcfaEdge, val loopStart: XcfaLocation, val loopLocs: List, val loopEdges: List + val loopVar: VarDecl<*>, val loopVarModifiers: List, val loopVarInit: XcfaEdge, + val loopCondEdge: XcfaEdge, val exitCondEdge: XcfaEdge, val loopStart: XcfaLocation, + val loopLocs: List, val loopEdges: List ) { + private class BasicStmtAction(private val stmt: Stmt) : StmtAction() { constructor(edge: XcfaEdge) : this(edge.label.toStmt()) constructor(edges: List) : this(SequenceLabel(edges.map { it.label }).toStmt()) @@ -63,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 )