From 8f1e27e4877d3e0c1e31086e781a5eb2ff2c55e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Wed, 6 Sep 2023 12:01:47 +0200 Subject: [PATCH 01/22] COI v0 --- .../algorithm/cegar/CegarChecker.java | 30 +++ .../theta/xcfa/analysis/ConeOfInfluence.kt | 205 ++++++++++++++++++ .../bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 5 +- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 7 +- .../main/java/hu/bme/mit/theta/xcfa/Utils.kt | 15 +- .../hu/bme/mit/theta/xcfa/model/Builders.kt | 8 +- .../mit/theta/xcfa/passes/LoopUnrollPass.kt | 19 +- 7 files changed, 275 insertions(+), 14 deletions(-) create mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt 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..82a1b45a5a 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; @@ -86,6 +90,7 @@ public SafetyResult check(final P initPrec) { logger.write(Level.MAINSTEP, "Iteration %d%n", iteration); logger.write(Level.MAINSTEP, "| Checking abstraction...%n"); + System.err.println(prec); final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); abstractorResult = abstractor.check(arg, prec); abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime; @@ -96,6 +101,19 @@ public SafetyResult check(final P initPrec) { wdl.addIteration(iteration, argGraph, precString); + + + System.err.println("Printing ARG..." + System.lineSeparator()); + Graph g = ArgVisualizer.create(s -> s.toString().replace(" initialized=true", ""), Object::toString).visualize(arg); + try { + FileWriter myWriter = new FileWriter("/mnt/d/Theta/test/arg-latest.dot"); + myWriter.write(GraphvizWriter.getInstance().writeString(g)); + myWriter.close(); + } catch (IOException e) { + throw new RuntimeException(e); + } + System.err.println(arg.size() + System.lineSeparator()); + if (abstractorResult.isUnsafe()) { MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG"); @@ -136,6 +154,18 @@ 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("Printing ARG..." + System.lineSeparator()); + Graph g = ArgVisualizer.create(s -> s.toString().replace(" initialized=true", ""), Object::toString).visualize(arg); + try { + FileWriter myWriter = new FileWriter("/mnt/d/Theta/test/arg-latest.dot"); + myWriter.write(GraphvizWriter.getInstance().writeString(g)); + myWriter.close(); + } catch (IOException e) { + throw new RuntimeException(e); + } + System.err.println(arg.size() + System.lineSeparator()); + return cegarResult; } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt new file mode 100644 index 0000000000..061fba27a3 --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -0,0 +1,205 @@ +package hu.bme.mit.theta.xcfa.analysis + +import hu.bme.mit.theta.analysis.LTS +import hu.bme.mit.theta.analysis.Prec +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.model.* +import java.util.* +import kotlin.math.max +import kotlin.math.min + +lateinit var COI: ConeOfInfluence + +private typealias S = XcfaState +private typealias A = XcfaAction + +class ConeOfInfluence( + private val xcfa: XCFA, + var coreLts: LTS = getXcfaLts() +) { + + private var lastPrec: Prec? = null + + private val edgeToProcedure: MutableMap = mutableMapOf() + private val locToScc: MutableMap = mutableMapOf() + + private val directObservers: MutableMap> = mutableMapOf() + private val interProcessObservers: MutableMap> = mutableMapOf() + + val lts = object : LTS { + override fun getEnabledActionsFor(state: S): Collection { + val enabled = coreLts.getEnabledActionsFor(state) + return replaceIrrelevantActions(state, 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) + } + + private fun replaceIrrelevantActions(state: S, enabled: Collection): Collection { + if (lastPrec == null) return enabled + + val procedures = state.processes.map { (p, pState) -> + val loc = pState.locs.peek() + val procedure = edgeToProcedure[loc.incomingEdges.ifEmpty(loc::outgoingEdges).first()]!! + p to Pair(procedure, locToScc[loc]!!) + }.toMap() + return enabled.map { action -> + val otherProcedures = procedures.filter { it.key != action.pid }.values.fold( + mutableMapOf()) { acc, next -> + acc[next.first] = max(next.second, acc[next.first] ?: 0) + acc + } + if (!isObserved(action, otherProcedures)) { + replace(action) + } else { + action + } + } + } + + private fun isObserved(action: A, otherProcedures: Map): Boolean { + val toVisit = mutableListOf(action.edge) + while (toVisit.isNotEmpty()) { + val visiting = toVisit.removeFirst() + if (isRealObserver(visiting)) return true + + toVisit.addAll(directObservers[visiting] ?: emptySet()) + toVisit.addAll(interProcessObservers[visiting]?.filter { edge -> + otherProcedures[edgeToProcedure[edge]]!! > locToScc[edge.source]!! // the edge is still reachable + } ?: emptySet()) + } + return false + } + + private fun replace(action: A) = action.withLabel(action.label.replace().run { + if (this !is SequenceLabel) SequenceLabel(listOf(this)) else this + }) + + private fun XcfaLabel.replace(): XcfaLabel = when { + this is SequenceLabel -> SequenceLabel(labels.map { it.replace() }, metadata) + this is NondetLabel -> NondetLabel(labels.map { it.replace() }.toSet(), metadata) + this is StmtLabel && (this.stmt is AssignStmt<*> || this.stmt is HavocStmt<*>) -> NopLabel + else -> this + } + } + + init { + xcfa.procedures.forEach { tarjan(it.initLoc) } + } + + fun reinitialize(prec: Prec) { + directObservers.clear() + interProcessObservers.clear() + xcfa.procedures.forEach { procedure -> + procedure.edges.forEach { + edgeToProcedure[it] = procedure + findDirectObservers(it, prec) + findInterProcessObservers(it, prec) + } + } + lastPrec = prec + + System.err.println("Direct:") + directObservers.forEach { (k, v) -> System.err.println("${k.label} -> ${v.map { it.label }}") } + System.err.println("Indirect:") + interProcessObservers.forEach { (k, v) -> System.err.println("${k.label} -> ${v.map { it.label }}") } + } + + + 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) { + locToScc[stack.pop()] = scc + } + locToScc[stack.pop()] = scc // visiting + } + + toVisit.pop() + } + } + + + private fun isRealObserver(edge: XcfaEdge) = edge.label.collectAssumesVars().isNotEmpty() + + private 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, directObservers) + toVisit.addAll(visiting.target.outgoingEdges.filter { it !in visited }) + } + } + + 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, interProcessObservers) + } + } + } + + private 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 }) { + relation[source] = relation[source] ?: mutableSetOf() + relation[source]!!.add(target) + } + } + +} \ No newline at end of file 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..59b5407544 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,6 +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.COI import hu.bme.mit.theta.xcfa.analysis.ErrorDetection import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState @@ -109,7 +110,9 @@ data class XcfaCegarConfig( val ignoredVarRegistry = mutableMapOf, MutableSet>() - val lts = porLevel.getLts(xcfa, ignoredVarRegistry) + //val lts = porLevel.getLts(xcfa, ignoredVarRegistry) + COI.coreLts = porLevel.getLts(xcfa, ignoredVarRegistry) + val lts = COI.lts val waitlist = if (porLevel.isDynamic) { (lts as XcfaDporLts).waitlist } else { 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..47881915c9 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 @@ -39,12 +39,12 @@ import hu.bme.mit.theta.frontend.chc.ChcFrontend import hu.bme.mit.theta.llvm2xcfa.ArithmeticType import hu.bme.mit.theta.llvm2xcfa.XcfaUtils.fromFile 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.* import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts import hu.bme.mit.theta.xcfa.cli.utils.XcfaWitnessWriter import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer +import hu.bme.mit.theta.xcfa.analysis.COI +import hu.bme.mit.theta.xcfa.analysis.ConeOfInfluence import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.toDot import hu.bme.mit.theta.xcfa.passes.LbePass @@ -179,6 +179,7 @@ class XcfaCli(private val args: Array) { logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType") val parseContext = ParseContext() val xcfa = getXcfa(logger, explicitProperty, parseContext) + COI = ConeOfInfluence(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 ) From acba30dc7bb64662dcb74d113dcf53c81eeacc3f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Wed, 6 Sep 2023 12:26:03 +0200 Subject: [PATCH 02/22] COI interprocess observer edges filtered --- .../java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt index 061fba27a3..3fc1a78eb8 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -65,14 +65,17 @@ class ConeOfInfluence( } private fun isObserved(action: A, otherProcedures: Map): Boolean { - val toVisit = mutableListOf(action.edge) + val toVisit = edgeToProcedure.keys.filter { + it.source == action.edge.source && it.target == action.edge.target + }.toMutableList() while (toVisit.isNotEmpty()) { val visiting = toVisit.removeFirst() if (isRealObserver(visiting)) return true toVisit.addAll(directObservers[visiting] ?: emptySet()) toVisit.addAll(interProcessObservers[visiting]?.filter { edge -> - otherProcedures[edgeToProcedure[edge]]!! > locToScc[edge.source]!! // the edge is still reachable + otherProcedures.containsKey(edgeToProcedure[edge]) && + otherProcedures[edgeToProcedure[edge]]!! > locToScc[edge.source]!! // the edge is still reachable } ?: emptySet()) } return false From d042a1bf42d1a4af716c55197f8209673f959a79 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 7 Sep 2023 00:26:06 +0200 Subject: [PATCH 03/22] COI with transfer function --- .../theta/xcfa/analysis/ConeOfInfluence.kt | 77 ++++++++++++------- .../mit/theta/xcfa/analysis/XcfaAnalysis.kt | 7 +- .../bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 4 +- 3 files changed, 55 insertions(+), 33 deletions(-) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt index 3fc1a78eb8..8deb930012 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -1,7 +1,7 @@ package hu.bme.mit.theta.xcfa.analysis -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 @@ -19,48 +19,66 @@ private typealias A = XcfaAction class ConeOfInfluence( private val xcfa: XCFA, - var coreLts: LTS = getXcfaLts() ) { + lateinit var coreTransFunc: TransFunc> private var lastPrec: Prec? = null private val edgeToProcedure: MutableMap = mutableMapOf() + private val startThreads: MutableSet = mutableSetOf() private val locToScc: MutableMap = mutableMapOf() private val directObservers: MutableMap> = mutableMapOf() private val interProcessObservers: MutableMap> = mutableMapOf() - val lts = object : LTS { - override fun getEnabledActionsFor(state: S): Collection { - val enabled = coreLts.getEnabledActionsFor(state) - return replaceIrrelevantActions(state, enabled) - } + private data class ProcedureEntry( + val procedure: XcfaProcedure, + val scc: Int, + val pid: Int + ) - override fun

getEnabledActionsFor(state: S, explored: Collection, prec: P): Collection { + val transFunc = object : TransFunc> { + override fun getSuccStates(state: S, action: A, prec: XcfaPrec): Collection { if (lastPrec != prec) reinitialize(prec) - val enabled = coreLts.getEnabledActionsFor(state, explored, prec) - return replaceIrrelevantActions(state, enabled) + val effectiveAction = replaceIfIrrelevant(state, action) + return coreTransFunc.getSuccStates(state, effectiveAction, prec) } - private fun replaceIrrelevantActions(state: S, enabled: Collection): Collection { - if (lastPrec == null) return enabled + private fun replaceIfIrrelevant(state: S, action: A): A { + if (lastPrec == null) return action - val procedures = state.processes.map { (p, pState) -> + val procedures = state.processes.map { (pid, pState) -> val loc = pState.locs.peek() val procedure = edgeToProcedure[loc.incomingEdges.ifEmpty(loc::outgoingEdges).first()]!! - p to Pair(procedure, locToScc[loc]!!) - }.toMap() - return enabled.map { action -> - val otherProcedures = procedures.filter { it.key != action.pid }.values.fold( - mutableMapOf()) { acc, next -> - acc[next.first] = max(next.second, acc[next.first] ?: 0) - acc - } - if (!isObserved(action, otherProcedures)) { - replace(action) - } else { - action + ProcedureEntry(procedure, locToScc[loc]!!, pid) + }.toMutableSet() + + do { + var anyNew = false + startThreads.filter { edge -> + procedures.any { edgeToProcedure[edge] == it.procedure && it.scc >= locToScc[edge.source]!! } + }.forEach { edge -> + edge.getFlatLabels().filterIsInstance().forEach { startLabel -> + val procedure = xcfa.procedures.find { it.name == startLabel.name }!! + val procedureEntry = ProcedureEntry(procedure, locToScc[procedure.initLoc]!!, -1) + if (procedureEntry !in procedures) { + procedures.add(procedureEntry) + anyNew = true + } + } } + } while (anyNew) + + val otherProcedures = procedures.filter { it.pid != action.pid }.fold( + mutableMapOf()) { acc, next -> + acc[next.procedure] = max(next.scc, acc[next.procedure] ?: 0) + acc + } + + return if (!isObserved(action, otherProcedures)) { + replace(action) + } else { + action } } @@ -101,10 +119,11 @@ class ConeOfInfluence( directObservers.clear() interProcessObservers.clear() xcfa.procedures.forEach { procedure -> - procedure.edges.forEach { - edgeToProcedure[it] = procedure - findDirectObservers(it, prec) - findInterProcessObservers(it, prec) + procedure.edges.forEach { edge -> + edgeToProcedure[edge] = procedure + if (edge.getFlatLabels().any { it is StartLabel }) startThreads.add(edge) + findDirectObservers(edge, prec) + findInterProcessObservers(edge, prec) } } lastPrec = prec 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..74d36dfce6 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 @@ -50,9 +50,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 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 59b5407544..537fcd20aa 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 @@ -110,9 +110,7 @@ data class XcfaCegarConfig( val ignoredVarRegistry = mutableMapOf, MutableSet>() - //val lts = porLevel.getLts(xcfa, ignoredVarRegistry) - COI.coreLts = porLevel.getLts(xcfa, ignoredVarRegistry) - val lts = COI.lts + val lts = porLevel.getLts(xcfa, ignoredVarRegistry) val waitlist = if (porLevel.isDynamic) { (lts as XcfaDporLts).waitlist } else { From 587d2a8ea7e361243f8a2d45c5e00f4bc34bb218 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 7 Sep 2023 14:23:28 +0200 Subject: [PATCH 04/22] COI lts + transfunc --- .../theta/xcfa/analysis/ConeOfInfluence.kt | 104 +++++++++++++----- .../bme/mit/theta/xcfa/analysis/XcfaAction.kt | 6 +- .../bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 4 +- 3 files changed, 82 insertions(+), 32 deletions(-) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt index 8deb930012..05a6ee439c 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -1,5 +1,6 @@ package hu.bme.mit.theta.xcfa.analysis +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 @@ -7,6 +8,8 @@ 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.por.extension +import hu.bme.mit.theta.xcfa.analysis.por.nullableExtension import hu.bme.mit.theta.xcfa.model.* import java.util.* import kotlin.math.max @@ -17,9 +20,14 @@ lateinit var COI: ConeOfInfluence private typealias S = XcfaState private typealias A = XcfaAction +var XcfaAction.finalLabel: XcfaLabel by extension() +private var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() + class ConeOfInfluence( private val xcfa: XCFA, ) { + + var coreLts: LTS = getXcfaLts() lateinit var coreTransFunc: TransFunc> private var lastPrec: Prec? = null @@ -31,22 +39,30 @@ class ConeOfInfluence( private val directObservers: MutableMap> = mutableMapOf() private val interProcessObservers: MutableMap> = mutableMapOf() - private data class ProcedureEntry( + data class ProcedureEntry( val procedure: XcfaProcedure, val scc: Int, val pid: Int ) - val transFunc = object : TransFunc> { - override fun getSuccStates(state: S, action: A, prec: XcfaPrec): Collection { - if (lastPrec != prec) reinitialize(prec) - val effectiveAction = replaceIfIrrelevant(state, action) - return coreTransFunc.getSuccStates(state, effectiveAction, prec) + val transFunc = TransFunc> { state, action, prec -> + action.finalLabel = action.transFuncVersion?.label ?: action.label + coreTransFunc.getSuccStates(state, action.transFuncVersion ?: action, prec) + } + + val lts = object : LTS { + override fun getEnabledActionsFor(state: S): Collection { + val enabled = coreLts.getEnabledActionsFor(state) + return lastPrec?.let { replaceIrrelevantActions(state, enabled, it) } ?: enabled } - private fun replaceIfIrrelevant(state: S, action: A): A { - if (lastPrec == null) return action + 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 = edgeToProcedure[loc.incomingEdges.ifEmpty(loc::outgoingEdges).first()]!! @@ -69,16 +85,17 @@ class ConeOfInfluence( } } while (anyNew) - val otherProcedures = procedures.filter { it.pid != action.pid }.fold( - mutableMapOf()) { acc, next -> - acc[next.procedure] = max(next.scc, acc[next.procedure] ?: 0) - acc - } - - return if (!isObserved(action, otherProcedures)) { - replace(action) - } else { - action + return enabled.map { action -> + val otherProcedures = procedures.filter { it.pid != action.pid }.fold( + mutableMapOf()) { acc, next -> + acc[next.procedure] = max(next.scc, acc[next.procedure] ?: 0) + acc + } + if (!isObserved(action, otherProcedures)) { + replace(action, prec) + } else { + action + } } } @@ -99,16 +116,43 @@ class ConeOfInfluence( return false } - private fun replace(action: A) = action.withLabel(action.label.replace().run { - if (this !is SequenceLabel) SequenceLabel(listOf(this)) else this - }) + private fun replace(action: A, prec: Prec): XcfaAction { + val replacedLabel = action.label.replace(prec) + val newAction = action.withLabel(replacedLabel.first.wrapInSequenceLabel()) + newAction.transFuncVersion = action.withLabel(replacedLabel.second.wrapInSequenceLabel()) + return newAction + } + + private fun XcfaLabel.replace(prec: Prec): Pair = when (this) { + is SequenceLabel -> pairOf(labels.map { it.replace(prec) }) { SequenceLabel(it, metadata) } + is NondetLabel -> pairOf(labels.map { it.replace(prec) }) { NondetLabel(it.toSet(), metadata) } + is StmtLabel -> { + when (val stmt = this.stmt) { + is AssignStmt<*> -> if (stmt.varDecl in prec.usedVars) { + Pair(NopLabel, NopLabel) + } else { + Pair(this, NopLabel) + } + + is HavocStmt<*> -> if (stmt.varDecl in prec.usedVars) { + Pair(NopLabel, NopLabel) + } else { + Pair(this, NopLabel) + } + + else -> Pair(this, this) + } + } + + else -> Pair(this, this) + } - private fun XcfaLabel.replace(): XcfaLabel = when { - this is SequenceLabel -> SequenceLabel(labels.map { it.replace() }, metadata) - this is NondetLabel -> NondetLabel(labels.map { it.replace() }.toSet(), metadata) - this is StmtLabel && (this.stmt is AssignStmt<*> || this.stmt is HavocStmt<*>) -> NopLabel - else -> this + private inline fun pairOf(list: List>, builder: (List) -> T): Pair { + return Pair(builder(list.map { it.first }), builder(list.map { it.second })) } + + private fun XcfaLabel.wrapInSequenceLabel(): SequenceLabel = + if (this !is SequenceLabel) SequenceLabel(listOf(this)) else this } init { @@ -128,10 +172,10 @@ class ConeOfInfluence( } lastPrec = prec - System.err.println("Direct:") - directObservers.forEach { (k, v) -> System.err.println("${k.label} -> ${v.map { it.label }}") } - System.err.println("Indirect:") - interProcessObservers.forEach { (k, v) -> System.err.println("${k.label} -> ${v.map { it.label }}") } +// System.err.println("Direct:") +// directObservers.forEach { (k, v) -> System.err.println("${k.label} -> ${v.map { it.label }}") } +// System.err.println("Indirect:") +// interProcessObservers.forEach { (k, v) -> System.err.println("${k.label} -> ${v.map { it.label }}") } } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt index b323e180db..66a619503b 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt @@ -36,7 +36,11 @@ data class XcfaAction(val pid: Int, val edge: XcfaEdge) : StmtAction() { } override fun toString(): String { - return "$pid: $source -> $target [$label]" + try { + return "$pid: $source -> $target [$finalLabel]" + } catch (e: Exception) { + return "$pid: $source -> $target [$label]" + } } fun withLabel(sequenceLabel: SequenceLabel): XcfaAction { 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 537fcd20aa..5c6aac67a6 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 @@ -110,7 +110,9 @@ data class XcfaCegarConfig( val ignoredVarRegistry = mutableMapOf, MutableSet>() - val lts = porLevel.getLts(xcfa, ignoredVarRegistry) + COI.coreLts = porLevel.getLts(xcfa, ignoredVarRegistry) + val lts = COI.lts +// val lts = porLevel.getLts(xcfa, ignoredVarRegistry) val waitlist = if (porLevel.isDynamic) { (lts as XcfaDporLts).waitlist } else { From d660489d96451af6ca7e069f2b8346fe32189ceb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 7 Sep 2023 16:44:11 +0200 Subject: [PATCH 05/22] COI seems to be working version --- .../algorithm/cegar/CegarChecker.java | 14 ---- .../theta/xcfa/analysis/ConeOfInfluence.kt | 66 +++++++++---------- .../bme/mit/theta/xcfa/analysis/XcfaAction.kt | 6 +- .../theta/xcfa/analysis/por/XcfaSporLts.kt | 2 +- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 6 +- 5 files changed, 40 insertions(+), 54 deletions(-) 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 82a1b45a5a..8bb0f4309f 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 @@ -90,7 +90,6 @@ public SafetyResult check(final P initPrec) { logger.write(Level.MAINSTEP, "Iteration %d%n", iteration); logger.write(Level.MAINSTEP, "| Checking abstraction...%n"); - System.err.println(prec); final long abstractorStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS); abstractorResult = abstractor.check(arg, prec); abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime; @@ -101,19 +100,6 @@ public SafetyResult check(final P initPrec) { wdl.addIteration(iteration, argGraph, precString); - - - System.err.println("Printing ARG..." + System.lineSeparator()); - Graph g = ArgVisualizer.create(s -> s.toString().replace(" initialized=true", ""), Object::toString).visualize(arg); - try { - FileWriter myWriter = new FileWriter("/mnt/d/Theta/test/arg-latest.dot"); - myWriter.write(GraphvizWriter.getInstance().writeString(g)); - myWriter.close(); - } catch (IOException e) { - throw new RuntimeException(e); - } - System.err.println(arg.size() + System.lineSeparator()); - if (abstractorResult.isUnsafe()) { MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG"); diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt index 05a6ee439c..efbf77adc0 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -12,7 +12,6 @@ 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.max import kotlin.math.min lateinit var COI: ConeOfInfluence @@ -20,36 +19,33 @@ lateinit var COI: ConeOfInfluence private typealias S = XcfaState private typealias A = XcfaAction -var XcfaAction.finalLabel: XcfaLabel by extension() -private var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() - -class ConeOfInfluence( - private val xcfa: XCFA, -) { +class ConeOfInfluence(private val xcfa: XCFA) { var coreLts: LTS = getXcfaLts() lateinit var coreTransFunc: TransFunc> private var lastPrec: Prec? = null - private val edgeToProcedure: MutableMap = mutableMapOf() private val startThreads: MutableSet = mutableSetOf() - private val locToScc: MutableMap = mutableMapOf() + private val edgeToProcedure: MutableMap = mutableMapOf() + private var XcfaEdge.procedure: XcfaProcedure + get() = edgeToProcedure[this]!! + set(value) { + edgeToProcedure[this] = value + } + private var XcfaLocation.scc: Int by extension() private val directObservers: MutableMap> = mutableMapOf() private val interProcessObservers: MutableMap> = mutableMapOf() + private var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() + data class ProcedureEntry( val procedure: XcfaProcedure, val scc: Int, val pid: Int ) - val transFunc = TransFunc> { state, action, prec -> - action.finalLabel = action.transFuncVersion?.label ?: action.label - coreTransFunc.getSuccStates(state, action.transFuncVersion ?: action, prec) - } - val lts = object : LTS { override fun getEnabledActionsFor(state: S): Collection { val enabled = coreLts.getEnabledActionsFor(state) @@ -65,18 +61,18 @@ class ConeOfInfluence( private fun replaceIrrelevantActions(state: S, enabled: Collection, prec: Prec): Collection { val procedures = state.processes.map { (pid, pState) -> val loc = pState.locs.peek() - val procedure = edgeToProcedure[loc.incomingEdges.ifEmpty(loc::outgoingEdges).first()]!! - ProcedureEntry(procedure, locToScc[loc]!!, pid) + val procedure = loc.incomingEdges.ifEmpty(loc::outgoingEdges).first().procedure + ProcedureEntry(procedure, loc.scc, pid) }.toMutableSet() do { var anyNew = false startThreads.filter { edge -> - procedures.any { edgeToProcedure[edge] == it.procedure && it.scc >= locToScc[edge.source]!! } + 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, locToScc[procedure.initLoc]!!, -1) + val procedureEntry = ProcedureEntry(procedure, procedure.initLoc.scc, -1) if (procedureEntry !in procedures) { procedures.add(procedureEntry) anyNew = true @@ -86,12 +82,7 @@ class ConeOfInfluence( } while (anyNew) return enabled.map { action -> - val otherProcedures = procedures.filter { it.pid != action.pid }.fold( - mutableMapOf()) { acc, next -> - acc[next.procedure] = max(next.scc, acc[next.procedure] ?: 0) - acc - } - if (!isObserved(action, otherProcedures)) { + if (!isObserved(action, procedures)) { replace(action, prec) } else { action @@ -99,19 +90,24 @@ class ConeOfInfluence( } } - private fun isObserved(action: A, otherProcedures: Map): Boolean { + private fun isObserved(action: A, procedures: MutableSet): 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 - toVisit.addAll(directObservers[visiting] ?: emptySet()) - toVisit.addAll(interProcessObservers[visiting]?.filter { edge -> - otherProcedures.containsKey(edgeToProcedure[edge]) && - otherProcedures[edgeToProcedure[edge]]!! > locToScc[edge.source]!! // the edge is still reachable - } ?: emptySet()) + visited.add(visiting) + val toAdd = (directObservers[visiting] ?: emptySet()) union + (interProcessObservers[visiting]?.filter { edge -> + procedures.any { + it.procedure == edge.procedure && it.scc >= edge.source.scc + } // the edge is still reachable + } ?: emptySet()) + toVisit.addAll(toAdd.filter { it !in visited }) } return false } @@ -155,6 +151,10 @@ class ConeOfInfluence( if (this !is SequenceLabel) SequenceLabel(listOf(this)) else this } + val transFunc = TransFunc> { state, action, prec -> + coreTransFunc.getSuccStates(state, action.transFuncVersion ?: action, prec) + } + init { xcfa.procedures.forEach { tarjan(it.initLoc) } } @@ -164,7 +164,7 @@ class ConeOfInfluence( interProcessObservers.clear() xcfa.procedures.forEach { procedure -> procedure.edges.forEach { edge -> - edgeToProcedure[edge] = procedure + edge.procedure = procedure if (edge.getFlatLabels().any { it is StartLabel }) startThreads.add(edge) findDirectObservers(edge, prec) findInterProcessObservers(edge, prec) @@ -212,9 +212,9 @@ class ConeOfInfluence( if (lowest[visiting] == disc[visiting]) { val scc = sccCnt++ while (stack.peek() != visiting) { - locToScc[stack.pop()] = scc + stack.pop().scc = scc } - locToScc[stack.pop()] = scc // visiting + stack.pop().scc = scc // visiting } toVisit.pop() diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt index 66a619503b..b323e180db 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt @@ -36,11 +36,7 @@ data class XcfaAction(val pid: Int, val edge: XcfaEdge) : StmtAction() { } override fun toString(): String { - try { - return "$pid: $source -> $target [$finalLabel]" - } catch (e: Exception) { - return "$pid: $source -> $target [$label]" - } + return "$pid: $source -> $target [$label]" } fun withLabel(sequenceLabel: SequenceLabel): XcfaAction { 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..3129c2b283 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,7 +34,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : SporLts, XcfaAct companion object { - private val random: Random = Random.Default + var random: Random = Random.Default private val simpleXcfaLts = getXcfaLts() } 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 47881915c9..a828cdade1 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 @@ -45,6 +45,7 @@ import hu.bme.mit.theta.xcfa.cli.utils.XcfaWitnessWriter import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer import hu.bme.mit.theta.xcfa.analysis.COI import hu.bme.mit.theta.xcfa.analysis.ConeOfInfluence +import hu.bme.mit.theta.xcfa.analysis.por.XcfaSporLts import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.toDot import hu.bme.mit.theta.xcfa.passes.LbePass @@ -172,7 +173,10 @@ class XcfaCli(private val args: Array) { // propagating input variables LbePass.level = lbeLevel - if (randomSeed >= 0) XcfaDporLts.random = Random(randomSeed) + if (randomSeed >= 0){ + XcfaSporLts.random = Random(randomSeed) + XcfaDporLts.random = Random(randomSeed) + } LoopUnrollPass.UNROLL_LIMIT = loopUnroll WebDebuggerLogger.getInstance().setTitle(input?.name) From 0c8bc7c48fc89bce04ac1bdd331ad8af7dfc55ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 7 Sep 2023 17:15:30 +0200 Subject: [PATCH 06/22] COI handling multiple processes with the same procedure --- .../analysis/algorithm/cegar/CegarChecker.java | 12 ------------ .../mit/theta/xcfa/analysis/ConeOfInfluence.kt | 15 +++++++-------- .../hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 6 +++--- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 5 +++-- 4 files changed, 13 insertions(+), 25 deletions(-) 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 8bb0f4309f..3f8c74d35e 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 @@ -140,18 +140,6 @@ 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("Printing ARG..." + System.lineSeparator()); - Graph g = ArgVisualizer.create(s -> s.toString().replace(" initialized=true", ""), Object::toString).visualize(arg); - try { - FileWriter myWriter = new FileWriter("/mnt/d/Theta/test/arg-latest.dot"); - myWriter.write(GraphvizWriter.getInstance().writeString(g)); - myWriter.close(); - } catch (IOException e) { - throw new RuntimeException(e); - } - System.err.println(arg.size() + System.lineSeparator()); - return cegarResult; } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt index efbf77adc0..62a428ea53 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -80,17 +80,20 @@ class ConeOfInfluence(private val xcfa: XCFA) { } } } while (anyNew) + val multipleProcedures = procedures.groupingBy { it.procedure }.eachCount().filter { it.value > 1 }.keys return enabled.map { action -> - if (!isObserved(action, procedures)) { + if (!isObserved(action, procedures, multipleProcedures)) { replace(action, prec) } else { + action.transFuncVersion = null action } } } - private fun isObserved(action: A, procedures: MutableSet): Boolean { + private fun isObserved(action: A, procedures: MutableSet, + multipleProcedures: Set): Boolean { val toVisit = edgeToProcedure.keys.filter { it.source == action.edge.source && it.target == action.edge.target }.toMutableList() @@ -104,7 +107,8 @@ class ConeOfInfluence(private val xcfa: XCFA) { val toAdd = (directObservers[visiting] ?: emptySet()) union (interProcessObservers[visiting]?.filter { edge -> procedures.any { - it.procedure == edge.procedure && it.scc >= edge.source.scc + it.procedure == edge.procedure && it.scc >= edge.source.scc && + (it.procedure != visiting.procedure || it.procedure in multipleProcedures) } // the edge is still reachable } ?: emptySet()) toVisit.addAll(toAdd.filter { it !in visited }) @@ -171,11 +175,6 @@ class ConeOfInfluence(private val xcfa: XCFA) { } } lastPrec = prec - -// System.err.println("Direct:") -// directObservers.forEach { (k, v) -> System.err.println("${k.label} -> ${v.map { it.label }}") } -// System.err.println("Indirect:") -// interProcessObservers.forEach { (k, v) -> System.err.println("${k.label} -> ${v.map { it.label }}") } } 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 5c6aac67a6..2cdf69674b 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 @@ -110,11 +110,11 @@ data class XcfaCegarConfig( val ignoredVarRegistry = mutableMapOf, MutableSet>() - COI.coreLts = porLevel.getLts(xcfa, ignoredVarRegistry) + val porLts = porLevel.getLts(xcfa, ignoredVarRegistry) + COI.coreLts = porLts val lts = COI.lts -// val lts = porLevel.getLts(xcfa, ignoredVarRegistry) val waitlist = if (porLevel.isDynamic) { - (lts as XcfaDporLts).waitlist + (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 a828cdade1..2ec88287bc 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 @@ -174,8 +174,9 @@ class XcfaCli(private val args: Array) { // propagating input variables LbePass.level = lbeLevel if (randomSeed >= 0){ - XcfaSporLts.random = Random(randomSeed) - XcfaDporLts.random = Random(randomSeed) + val random = Random(randomSeed) + XcfaSporLts.random = random + XcfaDporLts.random = random } LoopUnrollPass.UNROLL_LIMIT = loopUnroll WebDebuggerLogger.getInstance().setTitle(input?.name) From 0385a7678bb753657bfa5f160a82cfc22f0aaedd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 7 Sep 2023 17:54:37 +0200 Subject: [PATCH 07/22] COI cli option --- .../main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 2cdf69674b..6021832842 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 @@ -78,6 +78,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 coiEnabled: Boolean = false, @Parameter(names = ["--refinement-solver"], description = "Refinement solver name") var refinementSolver: String = "Z3", @Parameter(names = ["--validate-refinement-solver"], @@ -112,7 +114,7 @@ data class XcfaCegarConfig( val porLts = porLevel.getLts(xcfa, ignoredVarRegistry) COI.coreLts = porLts - val lts = COI.lts + val lts = if(coiEnabled) COI.lts else porLts val waitlist = if (porLevel.isDynamic) { (porLts as XcfaDporLts).waitlist } else { From eeffc29657249c3d9cda130259dcd35377503189 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Tue, 12 Sep 2023 15:28:53 +0200 Subject: [PATCH 08/22] COI enhancements --- .../mit/theta/xcfa/analysis/ConeOfInfluence.kt | 17 ++++++++++++++--- .../bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt | 1 + 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt index 62a428ea53..656fb78cda 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -63,7 +63,7 @@ class ConeOfInfluence(private val xcfa: XCFA) { val loc = pState.locs.peek() val procedure = loc.incomingEdges.ifEmpty(loc::outgoingEdges).first().procedure ProcedureEntry(procedure, loc.scc, pid) - }.toMutableSet() + }.toMutableList() do { var anyNew = false @@ -80,7 +80,7 @@ class ConeOfInfluence(private val xcfa: XCFA) { } } } while (anyNew) - val multipleProcedures = procedures.groupingBy { it.procedure }.eachCount().filter { it.value > 1 }.keys + val multipleProcedures = findDuplicates(procedures.map { it.procedure }) return enabled.map { action -> if (!isObserved(action, procedures, multipleProcedures)) { @@ -92,7 +92,7 @@ class ConeOfInfluence(private val xcfa: XCFA) { } } - private fun isObserved(action: A, procedures: MutableSet, + 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 @@ -153,6 +153,17 @@ class ConeOfInfluence(private val xcfa: XCFA) { private fun XcfaLabel.wrapInSequenceLabel(): SequenceLabel = if (this !is SequenceLabel) SequenceLabel(listOf(this)) else this + + 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 + } } val transFunc = TransFunc> { state, action, prec -> 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 74d36dfce6..2737c59cbf 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 @@ -197,6 +197,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 From 4bb2ba2c88ac85a1d31bb9fd816b7a3a43fed032 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Wed, 13 Sep 2023 10:00:35 +0200 Subject: [PATCH 09/22] coi<->refiner fix --- .../hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt index 656fb78cda..d01c7c238b 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -129,13 +129,13 @@ class ConeOfInfluence(private val xcfa: XCFA) { is StmtLabel -> { when (val stmt = this.stmt) { is AssignStmt<*> -> if (stmt.varDecl in prec.usedVars) { - Pair(NopLabel, NopLabel) + Pair(this, StmtLabel(HavocStmt.of(stmt.varDecl), metadata = this.metadata)) } else { Pair(this, NopLabel) } is HavocStmt<*> -> if (stmt.varDecl in prec.usedVars) { - Pair(NopLabel, NopLabel) + Pair(this, this) } else { Pair(this, NopLabel) } @@ -155,10 +155,10 @@ class ConeOfInfluence(private val xcfa: XCFA) { if (this !is SequenceLabel) SequenceLabel(listOf(this)) else this fun findDuplicates(list: List): Set { - val seen = mutableSetOf() + val seen = mutableSetOf() val duplicates = mutableSetOf() for (item in list) { - if (!seen.add(item.name)) { + if (!seen.add(item)) { duplicates.add(item) } } From edab3a4eac0a20dbbc5a3d6450a0b4a633177b49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 14 Sep 2023 11:55:39 +0200 Subject: [PATCH 10/22] coi + por integration --- .../algorithm/cegar/CegarChecker.java | 8 +++--- .../theta/xcfa/analysis/ConeOfInfluence.kt | 4 +-- .../xcfa/analysis/por/XcfaAasporCoiLts.kt | 26 +++++++++++++++++++ .../theta/xcfa/analysis/por/XcfaAasporLts.kt | 2 +- .../theta/xcfa/analysis/por/XcfaDporLts.kt | 15 ++++++----- .../theta/xcfa/analysis/por/XcfaSporLts.kt | 3 ++- .../bme/mit/theta/xcfa/cli/ConfigOptions.kt | 23 ++++++++++++++++ .../bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 14 ++++------ 8 files changed, 71 insertions(+), 24 deletions(-) create mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt 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 3f8c74d35e..160ed4b8ef 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 @@ -84,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; @@ -95,10 +95,10 @@ 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); if (abstractorResult.isUnsafe()) { MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG"); diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt index d01c7c238b..ef5ec08bc7 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt @@ -19,6 +19,8 @@ lateinit var COI: ConeOfInfluence private typealias S = XcfaState private typealias A = XcfaAction +internal var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() + class ConeOfInfluence(private val xcfa: XCFA) { var coreLts: LTS = getXcfaLts() @@ -38,8 +40,6 @@ class ConeOfInfluence(private val xcfa: XCFA) { private val directObservers: MutableMap> = mutableMapOf() private val interProcessObservers: MutableMap> = mutableMapOf() - private var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() - data class ProcedureEntry( val procedure: XcfaProcedure, val scc: Int, 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..bf3c73d411 --- /dev/null +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt @@ -0,0 +1,26 @@ +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.transFuncVersion +import hu.bme.mit.theta.xcfa.model.XCFA + +class XcfaAasporCoiLts( + xcfa: XCFA, + ignoredVarRegistry: MutableMap, MutableSet>, + coiLTS: LTS, XcfaAction> +) : XcfaAasporLts(xcfa, ignoredVarRegistry) { + + init { + simpleXcfaLts = coiLTS + } + + override fun getPersistentSetFirstActions(allEnabledActions: Collection): List> { + val actions = super.getPersistentSetFirstActions(allEnabledActions) + return actions.map { a -> a.map { it.transFuncVersion ?: it } } + } +} \ 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..5d6f15d379 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) { 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 3129c2b283..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 @@ -35,9 +35,10 @@ open class XcfaSporLts(protected val xcfa: XCFA) : SporLts, XcfaAct companion object { var random: Random = Random.Default - private val simpleXcfaLts = getXcfaLts() } + 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..84f43eb448 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 @@ -311,6 +311,29 @@ enum class InitPrec( } +enum class ConeOfInfluenceMode( + val getLts: (XCFA, MutableMap, MutableSet>, POR) -> LTS, XcfaAction> +) { + + NONE({ xcfa, ivr, por -> + por.getLts(xcfa, ivr).also { NONE.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 6021832842..1ac60d3a6c 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,10 +42,8 @@ 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.COI -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.XcfaAasporCoiLts import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts import hu.bme.mit.theta.xcfa.model.XCFA import java.io.BufferedReader @@ -79,7 +77,7 @@ data class XcfaCegarConfig( @Parameter(names = ["--por-level"], description = "POR dependency level") var porLevel: POR = POR.NOPOR, @Parameter(names = ["--coi"]) - var coiEnabled: Boolean = false, + var coi: ConeOfInfluenceMode = ConeOfInfluenceMode.NONE, @Parameter(names = ["--refinement-solver"], description = "Refinement solver name") var refinementSolver: String = "Z3", @Parameter(names = ["--validate-refinement-solver"], @@ -112,11 +110,9 @@ data class XcfaCegarConfig( val ignoredVarRegistry = mutableMapOf, MutableSet>() - val porLts = porLevel.getLts(xcfa, ignoredVarRegistry) - COI.coreLts = porLts - val lts = if(coiEnabled) COI.lts else porLts + val lts = coi.getLts(xcfa, ignoredVarRegistry, porLevel) val waitlist = if (porLevel.isDynamic) { - (porLts as XcfaDporLts).waitlist + (coi.porLts as XcfaDporLts).waitlist } else { PriorityWaitlist.create, XcfaAction>>( search.getComp(xcfa)) From 07ee6dd0f7acfb6e4c744ea12eb6a105c53b2645 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sun, 17 Sep 2023 11:01:11 +0200 Subject: [PATCH 11/22] single thread coi --- .../theta/xcfa/analysis/ConeOfInfluence.kt | 281 ------------------ .../mit/theta/xcfa/analysis/XcfaAnalysis.kt | 1 + .../mit/theta/xcfa/analysis/coi/XcfaCoi.kt | 156 ++++++++++ .../xcfa/analysis/coi/XcfaCoiMultiThread.kt | 143 +++++++++ .../xcfa/analysis/coi/XcfaCoiSingleThread.kt | 68 +++++ .../xcfa/analysis/por/XcfaAasporCoiLts.kt | 2 +- .../bme/mit/theta/xcfa/cli/ConfigOptions.kt | 1 + .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 15 +- 8 files changed, 379 insertions(+), 288 deletions(-) delete mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt create mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt create mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt create mode 100644 subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt deleted file mode 100644 index ef5ec08bc7..0000000000 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/ConeOfInfluence.kt +++ /dev/null @@ -1,281 +0,0 @@ -package hu.bme.mit.theta.xcfa.analysis - -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.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: ConeOfInfluence - -private typealias S = XcfaState -private typealias A = XcfaAction - -internal var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() - -class ConeOfInfluence(private val xcfa: XCFA) { - - var coreLts: LTS = getXcfaLts() - lateinit var coreTransFunc: TransFunc> - - private var lastPrec: Prec? = null - - private val startThreads: MutableSet = mutableSetOf() - private val edgeToProcedure: MutableMap = mutableMapOf() - private var XcfaEdge.procedure: XcfaProcedure - get() = edgeToProcedure[this]!! - set(value) { - edgeToProcedure[this] = value - } - private var XcfaLocation.scc: Int by extension() - - private val directObservers: MutableMap> = mutableMapOf() - private val interProcessObservers: MutableMap> = mutableMapOf() - - data class ProcedureEntry( - val procedure: XcfaProcedure, - val scc: Int, - val pid: Int - ) - - 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 = (directObservers[visiting] ?: emptySet()) union - (interProcessObservers[visiting]?.filter { edge -> - procedures.any { - it.procedure == edge.procedure && it.scc >= edge.source.scc && - (it.procedure != visiting.procedure || it.procedure in multipleProcedures) - } // the edge is still reachable - } ?: emptySet()) - toVisit.addAll(toAdd.filter { it !in visited }) - } - return false - } - - private fun replace(action: A, prec: Prec): XcfaAction { - val replacedLabel = action.label.replace(prec) - val newAction = action.withLabel(replacedLabel.first.wrapInSequenceLabel()) - newAction.transFuncVersion = action.withLabel(replacedLabel.second.wrapInSequenceLabel()) - return newAction - } - - private fun XcfaLabel.replace(prec: Prec): Pair = when (this) { - is SequenceLabel -> pairOf(labels.map { it.replace(prec) }) { SequenceLabel(it, metadata) } - is NondetLabel -> pairOf(labels.map { it.replace(prec) }) { NondetLabel(it.toSet(), metadata) } - is StmtLabel -> { - when (val stmt = this.stmt) { - is AssignStmt<*> -> if (stmt.varDecl in prec.usedVars) { - Pair(this, StmtLabel(HavocStmt.of(stmt.varDecl), metadata = this.metadata)) - } else { - Pair(this, NopLabel) - } - - is HavocStmt<*> -> if (stmt.varDecl in prec.usedVars) { - Pair(this, this) - } else { - Pair(this, NopLabel) - } - - else -> Pair(this, this) - } - } - - else -> Pair(this, this) - } - - private inline fun pairOf(list: List>, builder: (List) -> T): Pair { - return Pair(builder(list.map { it.first }), builder(list.map { it.second })) - } - - private fun XcfaLabel.wrapInSequenceLabel(): SequenceLabel = - if (this !is SequenceLabel) SequenceLabel(listOf(this)) else this - - fun findDuplicates(list: List): Set { - val seen = mutableSetOf() - val duplicates = mutableSetOf() - for (item in list) { - if (!seen.add(item)) { - duplicates.add(item) - } - } - return duplicates - } - } - - val transFunc = TransFunc> { state, action, prec -> - coreTransFunc.getSuccStates(state, action.transFuncVersion ?: action, prec) - } - - init { - xcfa.procedures.forEach { tarjan(it.initLoc) } - } - - fun reinitialize(prec: Prec) { - directObservers.clear() - interProcessObservers.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 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() - } - } - - - private fun isRealObserver(edge: XcfaEdge) = edge.label.collectAssumesVars().isNotEmpty() - - private 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, directObservers) - toVisit.addAll(visiting.target.outgoingEdges.filter { it !in visited }) - } - } - - 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, interProcessObservers) - } - } - } - - private 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 }) { - 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/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt index 2737c59cbf..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 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..f984521fa9 --- /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 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 -> + 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..565170c4c3 --- /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 == edge.procedure && it.scc >= edge.source.scc && + (it.procedure != visiting.procedure || 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)) { + 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 index bf3c73d411..741dc93331 100644 --- 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 @@ -6,7 +6,7 @@ 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.transFuncVersion +import hu.bme.mit.theta.xcfa.analysis.coi.transFuncVersion import hu.bme.mit.theta.xcfa.model.XCFA class XcfaAasporCoiLts( 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 84f43eb448..5c58b7aa23 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 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 2ec88287bc..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 @@ -39,13 +39,16 @@ import hu.bme.mit.theta.frontend.chc.ChcFrontend import hu.bme.mit.theta.llvm2xcfa.ArithmeticType import hu.bme.mit.theta.llvm2xcfa.XcfaUtils.fromFile import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager -import hu.bme.mit.theta.xcfa.analysis.* +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.analysis.COI -import hu.bme.mit.theta.xcfa.analysis.ConeOfInfluence -import hu.bme.mit.theta.xcfa.analysis.por.XcfaSporLts import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.toDot import hu.bme.mit.theta.xcfa.passes.LbePass @@ -173,7 +176,7 @@ class XcfaCli(private val args: Array) { // propagating input variables LbePass.level = lbeLevel - if (randomSeed >= 0){ + if (randomSeed >= 0) { val random = Random(randomSeed) XcfaSporLts.random = random XcfaDporLts.random = random @@ -184,7 +187,7 @@ class XcfaCli(private val args: Array) { logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType") val parseContext = ParseContext() val xcfa = getXcfa(logger, explicitProperty, parseContext) - COI = ConeOfInfluence(xcfa) + 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") From fadeb4eb07014411efbccf94f94aafa8e4d60bac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sun, 17 Sep 2023 12:16:03 +0200 Subject: [PATCH 12/22] separate assume statements in LBE --- .../xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 c539affb06..23712bca7e 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 @@ -276,7 +276,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)) ) { From 7352c2df644636dc63e1e8d387cf5ba7716fd8ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Mon, 18 Sep 2023 14:17:49 +0200 Subject: [PATCH 13/22] maycover fix --- .../main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; } From 35ea8bbcbb6b9048e9a52574cb0c53386049786e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sat, 23 Sep 2023 11:23:05 +0200 Subject: [PATCH 14/22] edge wrapper optimization --- .../analysis/algorithm/cegar/COILogger.java | 72 +++++++++++++++++++ .../algorithm/cegar/CegarChecker.java | 7 ++ .../mit/theta/xcfa/analysis/coi/XcfaCoi.kt | 32 +++++++-- .../xcfa/analysis/coi/XcfaCoiMultiThread.kt | 55 ++++++++------ .../xcfa/analysis/coi/XcfaCoiSingleThread.kt | 16 +++-- 5 files changed, 149 insertions(+), 33 deletions(-) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java 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..90110e5cd7 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java @@ -0,0 +1,72 @@ +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 allTimer = 0; + static long nopTimer = 0; + static long originalTimer = 0; + static long ltsTimer = 0; + static long transFuncTimer = 0; + private static long startCoi = 0; + private static long startAll = 0; + private static long startNop = 0; + private static long startOriginal = 0; + private static long startLts = 0; + private static long startTransFunc = 0; + public static void startCoiTimer() { + startCoi = System.currentTimeMillis(); + } + public static void stopCoiTimer() { + coiTimer += System.currentTimeMillis() - startCoi; + } + public static void startAllTimer() { + startAll = System.currentTimeMillis(); + } + public static void stopAllTimer() { + allTimer += System.currentTimeMillis() - startAll; + } + public static void startNopTimer() { + startNop = System.currentTimeMillis(); + } + public static void stopNopTimer() { + nopTimer += System.currentTimeMillis() - startNop; + } + public static void startOriginalTimer() { + startOriginal = System.currentTimeMillis(); + } + public static void stopOriginalTimer() { + originalTimer += System.currentTimeMillis() - startOriginal; + } + public static void startLtsTimer() { + startLts = System.currentTimeMillis(); + } + public static void stopLtsTimer() { + ltsTimer += System.currentTimeMillis() - startLts; + } + public static void startTransFuncTimer() { + startTransFunc = System.currentTimeMillis(); + } + public static void stopTransFuncTimer() { + transFuncTimer += System.currentTimeMillis() - startTransFunc; + } + + static long nops = 0; + static List nopsList = new ArrayList<>(); + static long allLabels = 0; + static List allLabelsList = new ArrayList<>(); + public static void incNops() { + nops++; + } + public static void incAllLabels() { + allLabels++; + } + public static void newIteration() { + nopsList.add(nops); + allLabelsList.add(allLabels); + nops = 0; + allLabels = 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 160ed4b8ef..92ee5de5e7 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 @@ -99,6 +99,7 @@ public SafetyResult check(final P initPrec) { // String precString = prec.toString(); // wdl.addIteration(iteration, argGraph, precString); + COILogger.newIteration(); if (abstractorResult.isUnsafe()) { MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG"); @@ -140,6 +141,12 @@ 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 all labels: " + COILogger.allLabelsList); return cegarResult; } 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 index f984521fa9..8c21a68c72 100644 --- 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 @@ -3,6 +3,7 @@ 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 @@ -27,21 +28,44 @@ internal var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() abstract class XcfaCoi(protected val xcfa: XCFA) { + protected data class XcfaEdgeWrapper(val source: XcfaLocation, val target: XcfaLocation) { + + lateinit var edge: XcfaEdge + + constructor(edge: XcfaEdge) : this(edge.source, edge.target) { + this.edge = edge + } + } + + protected val XcfaEdge.wrapper: XcfaEdgeWrapper get() = XcfaEdgeWrapper(this) + 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() + protected val directObservation: MutableMap> = mutableMapOf() abstract val lts: LTS val transFunc = TransFunc> { state, action, prec -> - coreTransFunc.getSuccStates(state, action.transFuncVersion ?: action, prec) + val a = action.transFuncVersion ?: action + a.label.getFlatLabels().forEach { + COILogger.incAllLabels() + if (it is NopLabel) COILogger.incNops() + } + + 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) { @@ -103,7 +127,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { protected open fun addEdgeIfObserved( source: XcfaEdge, target: XcfaEdge, observableVars: Map, AccessType>, - precVars: Collection>, relation: MutableMap> + precVars: Collection>, relation: MutableMap> ) { val vars = target.getVars() var relevantAction = vars.any { it.value.isWritten && it.key in precVars } @@ -118,7 +142,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { } protected abstract fun addToRelation(source: XcfaEdge, target: XcfaEdge, - relation: MutableMap>) + relation: MutableMap>) protected fun isRealObserver(edge: XcfaEdge) = edge.label.collectAssumesVars().isNotEmpty() 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 index 565170c4c3..6e07139d93 100644 --- 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 @@ -2,6 +2,7 @@ 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 @@ -12,14 +13,14 @@ 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 val startThreads: MutableSet = mutableSetOf() + private val edgeToProcedure: MutableMap = mutableMapOf() private var XcfaEdge.procedure: XcfaProcedure - get() = edgeToProcedure[this]!! + get() = edgeToProcedure[this.wrapper]!! set(value) { - edgeToProcedure[this] = value + edgeToProcedure[this.wrapper] = value } - private val interProcessObservation: MutableMap> = mutableMapOf() + private val interProcessObservation: MutableMap> = mutableMapOf() data class ProcedureEntry( val procedure: XcfaProcedure, @@ -30,13 +31,21 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { override val lts = object : LTS { override fun getEnabledActionsFor(state: S): Collection { val enabled = coreLts.getEnabledActionsFor(state) - return lastPrec?.let { replaceIrrelevantActions(state, enabled, it) } ?: enabled + 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) - return replaceIrrelevantActions(state, enabled, prec) + COILogger.startCoiTimer() + val r = replaceIrrelevantActions(state, enabled, prec) + COILogger.stopCoiTimer() + return r } private fun replaceIrrelevantActions(state: S, enabled: Collection, prec: Prec): Collection { @@ -48,10 +57,10 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { 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 -> + startThreads.filter { edgeWrapper -> + procedures.any { edgeWrapper.edge.procedure == it.procedure && it.scc >= edgeWrapper.source.scc } + }.forEach { edgeWrapper -> + edgeWrapper.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) { @@ -78,18 +87,18 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { val toVisit = edgeToProcedure.keys.filter { it.source == action.edge.source && it.target == action.edge.target }.toMutableList() - val visited = mutableSetOf() + val visited = mutableSetOf() while (toVisit.isNotEmpty()) { val visiting = toVisit.removeFirst() - if (isRealObserver(visiting)) return true + if (isRealObserver(visiting.edge)) return true visited.add(visiting) val toAdd = (directObservation[visiting] ?: emptySet()) union - (interProcessObservation[visiting]?.filter { edge -> + (interProcessObservation[visiting]?.filter { edgeWrapper -> procedures.any { - it.procedure == edge.procedure && it.scc >= edge.source.scc && - (it.procedure != visiting.procedure || it.procedure in multipleProcedures) + it.procedure.name == edgeWrapper.edge.procedure.name && it.scc >= edgeWrapper.source.scc && + (it.procedure.name != visiting.edge.procedure.name || it.procedure in multipleProcedures) } // the edge is still reachable } ?: emptySet()) toVisit.addAll(toAdd.filter { it !in visited }) @@ -98,10 +107,10 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { } fun findDuplicates(list: List): Set { - val seen = mutableSetOf() + val seen = mutableSetOf() val duplicates = mutableSetOf() for (item in list) { - if (!seen.add(item)) { + if (!seen.add(item.name)) { duplicates.add(item) } } @@ -115,7 +124,7 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { xcfa.procedures.forEach { procedure -> procedure.edges.forEach { edge -> edge.procedure = procedure - if (edge.getFlatLabels().any { it is StartLabel }) startThreads.add(edge) + if (edge.getFlatLabels().any { it is StartLabel }) startThreads.add(edge.wrapper) findDirectObservers(edge, prec) findInterProcessObservers(edge, prec) } @@ -136,8 +145,10 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { } override fun addToRelation(source: XcfaEdge, target: XcfaEdge, - relation: MutableMap>) { - relation[source] = relation[source] ?: mutableSetOf() - relation[source]!!.add(target) + relation: MutableMap>) { + val sourceW = source.wrapper + val targetW = target.wrapper + relation[sourceW] = relation[sourceW] ?: mutableSetOf() + relation[sourceW]!!.add(targetW) } } \ 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 index e86648fd6d..cb8f264bfb 100644 --- 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 @@ -36,12 +36,12 @@ class XcfaCoiSingleThread(xcfa: XCFA) : XcfaCoi(xcfa) { fun reinitialize(prec: Prec) { lastPrec = prec directObservation.clear() - val realObservers = mutableSetOf() + val realObservers = mutableSetOf() xcfa.procedures.forEach { procedure -> procedure.edges.forEach { edge -> findDirectObservers(edge, prec) if (isRealObserver(edge)) { - realObservers.add(edge) + realObservers.add(edge.wrapper) } } } @@ -49,14 +49,16 @@ class XcfaCoiSingleThread(xcfa: XCFA) : XcfaCoi(xcfa) { } override fun addToRelation(source: XcfaEdge, target: XcfaEdge, - relation: MutableMap>) { - relation[target] = relation[target] ?: mutableSetOf() - relation[target]!!.add(source) + relation: MutableMap>) { + val sourceW = source.wrapper + val targetW = target.wrapper + relation[targetW] = relation[targetW] ?: mutableSetOf() + relation[targetW]!!.add(sourceW) } - private fun collectedObservedEdges(realObservers: Set) { + private fun collectedObservedEdges(realObservers: Set) { val toVisit = realObservers.toMutableList() - val visited = mutableSetOf() + val visited = mutableSetOf() while (toVisit.isNotEmpty()) { val visiting = toVisit.removeFirst() visited.add(visiting) From c833315bef32d1258947dd58e19dea1b047a103c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sat, 23 Sep 2023 11:32:01 +0200 Subject: [PATCH 15/22] no edge wrapper --- .../mit/theta/xcfa/analysis/coi/XcfaCoi.kt | 17 ++------- .../xcfa/analysis/coi/XcfaCoiMultiThread.kt | 38 +++++++++---------- .../xcfa/analysis/coi/XcfaCoiSingleThread.kt | 16 ++++---- 3 files changed, 28 insertions(+), 43 deletions(-) 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 index 8c21a68c72..252d00ece2 100644 --- 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 @@ -28,23 +28,12 @@ internal var XcfaAction.transFuncVersion: XcfaAction? by nullableExtension() abstract class XcfaCoi(protected val xcfa: XCFA) { - protected data class XcfaEdgeWrapper(val source: XcfaLocation, val target: XcfaLocation) { - - lateinit var edge: XcfaEdge - - constructor(edge: XcfaEdge) : this(edge.source, edge.target) { - this.edge = edge - } - } - - protected val XcfaEdge.wrapper: XcfaEdgeWrapper get() = XcfaEdgeWrapper(this) - 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() + protected val directObservation: MutableMap> = mutableMapOf() abstract val lts: LTS @@ -127,7 +116,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { protected open fun addEdgeIfObserved( source: XcfaEdge, target: XcfaEdge, observableVars: Map, AccessType>, - precVars: Collection>, relation: MutableMap> + precVars: Collection>, relation: MutableMap> ) { val vars = target.getVars() var relevantAction = vars.any { it.value.isWritten && it.key in precVars } @@ -142,7 +131,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { } protected abstract fun addToRelation(source: XcfaEdge, target: XcfaEdge, - relation: MutableMap>) + relation: MutableMap>) protected fun isRealObserver(edge: XcfaEdge) = edge.label.collectAssumesVars().isNotEmpty() 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 index 6e07139d93..6c3a96d95c 100644 --- 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 @@ -13,14 +13,14 @@ 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 val startThreads: MutableSet = mutableSetOf() + private val edgeToProcedure: MutableMap = mutableMapOf() private var XcfaEdge.procedure: XcfaProcedure - get() = edgeToProcedure[this.wrapper]!! + get() = edgeToProcedure[this]!! set(value) { - edgeToProcedure[this.wrapper] = value + edgeToProcedure[this] = value } - private val interProcessObservation: MutableMap> = mutableMapOf() + private val interProcessObservation: MutableMap> = mutableMapOf() data class ProcedureEntry( val procedure: XcfaProcedure, @@ -57,10 +57,10 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { do { var anyNew = false - startThreads.filter { edgeWrapper -> - procedures.any { edgeWrapper.edge.procedure == it.procedure && it.scc >= edgeWrapper.source.scc } - }.forEach { edgeWrapper -> - edgeWrapper.edge.getFlatLabels().filterIsInstance().forEach { startLabel -> + 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) { @@ -87,18 +87,18 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { val toVisit = edgeToProcedure.keys.filter { it.source == action.edge.source && it.target == action.edge.target }.toMutableList() - val visited = mutableSetOf() + val visited = mutableSetOf() while (toVisit.isNotEmpty()) { val visiting = toVisit.removeFirst() - if (isRealObserver(visiting.edge)) return true + if (isRealObserver(visiting)) return true visited.add(visiting) val toAdd = (directObservation[visiting] ?: emptySet()) union - (interProcessObservation[visiting]?.filter { edgeWrapper -> + (interProcessObservation[visiting]?.filter { edge -> procedures.any { - it.procedure.name == edgeWrapper.edge.procedure.name && it.scc >= edgeWrapper.source.scc && - (it.procedure.name != visiting.edge.procedure.name || it.procedure in multipleProcedures) + 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 }) @@ -124,7 +124,7 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { xcfa.procedures.forEach { procedure -> procedure.edges.forEach { edge -> edge.procedure = procedure - if (edge.getFlatLabels().any { it is StartLabel }) startThreads.add(edge.wrapper) + if (edge.getFlatLabels().any { it is StartLabel }) startThreads.add(edge) findDirectObservers(edge, prec) findInterProcessObservers(edge, prec) } @@ -145,10 +145,8 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { } override fun addToRelation(source: XcfaEdge, target: XcfaEdge, - relation: MutableMap>) { - val sourceW = source.wrapper - val targetW = target.wrapper - relation[sourceW] = relation[sourceW] ?: mutableSetOf() - relation[sourceW]!!.add(targetW) + 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 index cb8f264bfb..e86648fd6d 100644 --- 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 @@ -36,12 +36,12 @@ class XcfaCoiSingleThread(xcfa: XCFA) : XcfaCoi(xcfa) { fun reinitialize(prec: Prec) { lastPrec = prec directObservation.clear() - val realObservers = mutableSetOf() + val realObservers = mutableSetOf() xcfa.procedures.forEach { procedure -> procedure.edges.forEach { edge -> findDirectObservers(edge, prec) if (isRealObserver(edge)) { - realObservers.add(edge.wrapper) + realObservers.add(edge) } } } @@ -49,16 +49,14 @@ class XcfaCoiSingleThread(xcfa: XCFA) : XcfaCoi(xcfa) { } override fun addToRelation(source: XcfaEdge, target: XcfaEdge, - relation: MutableMap>) { - val sourceW = source.wrapper - val targetW = target.wrapper - relation[targetW] = relation[targetW] ?: mutableSetOf() - relation[targetW]!!.add(sourceW) + relation: MutableMap>) { + relation[target] = relation[target] ?: mutableSetOf() + relation[target]!!.add(source) } - private fun collectedObservedEdges(realObservers: Set) { + private fun collectedObservedEdges(realObservers: Set) { val toVisit = realObservers.toMutableList() - val visited = mutableSetOf() + val visited = mutableSetOf() while (toVisit.isNotEmpty()) { val visiting = toVisit.removeFirst() visited.add(visiting) From 85316d4b611a1273663a86eac491c3863cbb2903 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 28 Sep 2023 14:46:16 +0200 Subject: [PATCH 16/22] por-coi-por fix --- .../java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt | 2 +- .../src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt | 4 ++-- .../main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt | 3 +-- 3 files changed, 4 insertions(+), 5 deletions(-) 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 5d6f15d379..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 @@ -33,7 +33,7 @@ open 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-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 5c58b7aa23..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 @@ -316,8 +316,8 @@ enum class ConeOfInfluenceMode( val getLts: (XCFA, MutableMap, MutableSet>, POR) -> LTS, XcfaAction> ) { - NONE({ xcfa, ivr, por -> - por.getLts(xcfa, ivr).also { NONE.porLts = it } + 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 } 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 1ac60d3a6c..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 @@ -43,7 +43,6 @@ 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.* -import hu.bme.mit.theta.xcfa.analysis.por.XcfaAasporCoiLts import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts import hu.bme.mit.theta.xcfa.model.XCFA import java.io.BufferedReader @@ -77,7 +76,7 @@ data class XcfaCegarConfig( @Parameter(names = ["--por-level"], description = "POR dependency level") var porLevel: POR = POR.NOPOR, @Parameter(names = ["--coi"]) - var coi: ConeOfInfluenceMode = ConeOfInfluenceMode.NONE, + var coi: ConeOfInfluenceMode = ConeOfInfluenceMode.NO_COI, @Parameter(names = ["--refinement-solver"], description = "Refinement solver name") var refinementSolver: String = "Z3", @Parameter(names = ["--validate-refinement-solver"], From 3d55947b0fd22e1e9c563f36c153a78d7fd81f4a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sun, 1 Oct 2023 15:51:15 +0200 Subject: [PATCH 17/22] pred trans func optimization --- .../bme/mit/theta/analysis/pred/PredTransFunc.java | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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..fa69008e12 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 @@ -18,13 +18,16 @@ import hu.bme.mit.theta.analysis.TransFunc; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.pred.PredAbstractors.PredAbstractor; +import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import java.util.Collection; import java.util.Collections; +import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; public final class PredTransFunc implements TransFunc { @@ -48,6 +51,16 @@ public Collection getSuccStates(final PredState state, checkNotNull(action); checkNotNull(prec); + 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)); + } + final Collection succStates = predAbstractor.createStatesForExpr( And(state.toExpr(), action.toExpr()), VarIndexingFactory.indexing(0), prec, action.nextIndexing()); From b17c57ef3fedd17a7eef09c8984fb41944123703 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sun, 1 Oct 2023 23:50:04 +0200 Subject: [PATCH 18/22] pred abstractor opt --- .../theta/analysis/pred/PredAbstractors.java | 29 +++++++++++++++++++ .../theta/analysis/pred/PredTransFunc.java | 12 +------- 2 files changed, 30 insertions(+), 11 deletions(-) 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 fa69008e12..27bc732c16 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 @@ -51,19 +51,9 @@ public Collection getSuccStates(final PredState state, checkNotNull(action); checkNotNull(prec); - 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)); - } - 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; } From 6e223fe49eaae933ab55ce61651327e007648551 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Mon, 2 Oct 2023 09:31:29 +0200 Subject: [PATCH 19/22] import opt --- .../java/hu/bme/mit/theta/analysis/pred/PredTransFunc.java | 3 --- 1 file changed, 3 deletions(-) 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 27bc732c16..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 @@ -18,16 +18,13 @@ import hu.bme.mit.theta.analysis.TransFunc; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.pred.PredAbstractors.PredAbstractor; -import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import java.util.Collection; import java.util.Collections; -import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; public final class PredTransFunc implements TransFunc { From 19ea2625e5d7ccc2288f07eeacf1b1154b041397 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Wed, 4 Oct 2023 00:08:28 +0200 Subject: [PATCH 20/22] extended logging --- .../algorithm/cegar/BasicAbstractor.java | 1 + .../analysis/algorithm/cegar/COILogger.java | 31 +++++++++++++++++-- .../algorithm/cegar/CegarChecker.java | 3 ++ .../mit/theta/xcfa/analysis/coi/XcfaCoi.kt | 6 ++++ 4 files changed, 39 insertions(+), 2 deletions(-) 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 index 90110e5cd7..10f7ee739a 100644 --- 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 @@ -55,18 +55,45 @@ public static void stopTransFuncTimer() { static long nops = 0; static List nopsList = new ArrayList<>(); - static long allLabels = 0; - static List allLabelsList = 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 92ee5de5e7..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 @@ -146,7 +146,10 @@ public SafetyResult check(final P initPrec) { 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/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 index 252d00ece2..7b17de49b4 100644 --- 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 @@ -39,10 +39,16 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { 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) From 64e1160db682782a740e3abd5a353141300b11ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Wed, 4 Oct 2023 13:53:00 +0200 Subject: [PATCH 21/22] por coi fix --- .../analysis/algorithm/cegar/COILogger.java | 32 ------------------- .../xcfa/analysis/por/XcfaAasporCoiLts.kt | 10 +++--- 2 files changed, 6 insertions(+), 36 deletions(-) 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 index 10f7ee739a..1f93c7b300 100644 --- 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 @@ -5,16 +5,8 @@ public class COILogger { static long coiTimer = 0; - static long allTimer = 0; - static long nopTimer = 0; - static long originalTimer = 0; - static long ltsTimer = 0; static long transFuncTimer = 0; private static long startCoi = 0; - private static long startAll = 0; - private static long startNop = 0; - private static long startOriginal = 0; - private static long startLts = 0; private static long startTransFunc = 0; public static void startCoiTimer() { startCoi = System.currentTimeMillis(); @@ -22,30 +14,6 @@ public static void startCoiTimer() { public static void stopCoiTimer() { coiTimer += System.currentTimeMillis() - startCoi; } - public static void startAllTimer() { - startAll = System.currentTimeMillis(); - } - public static void stopAllTimer() { - allTimer += System.currentTimeMillis() - startAll; - } - public static void startNopTimer() { - startNop = System.currentTimeMillis(); - } - public static void stopNopTimer() { - nopTimer += System.currentTimeMillis() - startNop; - } - public static void startOriginalTimer() { - startOriginal = System.currentTimeMillis(); - } - public static void stopOriginalTimer() { - originalTimer += System.currentTimeMillis() - startOriginal; - } - public static void startLtsTimer() { - startLts = System.currentTimeMillis(); - } - public static void stopLtsTimer() { - ltsTimer += System.currentTimeMillis() - startLts; - } public static void startTransFuncTimer() { startTransFunc = System.currentTimeMillis(); } 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 index 741dc93331..38cd7085da 100644 --- 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 @@ -8,6 +8,7 @@ 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, @@ -19,8 +20,9 @@ class XcfaAasporCoiLts( simpleXcfaLts = coiLTS } - override fun getPersistentSetFirstActions(allEnabledActions: Collection): List> { - val actions = super.getPersistentSetFirstActions(allEnabledActions) - return actions.map { a -> a.map { it.transFuncVersion ?: it } } - } + 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 From e712a35ee740ba578ae643ccf668e5a9d04e4290 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 18 Jan 2024 09:25:46 +0100 Subject: [PATCH 22/22] LBE fix --- .../xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 23712bca7e..c539affb06 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 @@ -276,7 +276,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 || (it is StmtLabel && it.stmt is AssumeStmt) } } + location.incomingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } } || location.outgoingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } } || (level == LbeLevel.LBE_LOCAL && !atomicPhase && isNotLocal(outEdge)) ) {