From 1acb884b60136f4312a68cc5336f1901e823914c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sat, 24 Jun 2023 18:48:11 +0200 Subject: [PATCH 01/10] remove unnecessary changes --- .../main/java/hu/bme/mit/theta/analysis/expl/ExplPrec.java | 1 - .../src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 5 ----- 2 files changed, 6 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplPrec.java index 6330ca41d3..7d813a2cee 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplPrec.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplPrec.java @@ -27,7 +27,6 @@ import java.util.Collections; import java.util.Optional; import java.util.Set; -import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkNotNull; 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 90c7cff4a8..c67e1bc4fa 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 @@ -118,9 +118,6 @@ class XcfaCli(private val args: Array) { @Parameter var remainingFlags: MutableList = ArrayList() - @Parameter(names = ["--seed"], description = "Random seed") - var randomSeed: Int = -1 - private fun run() { /// Checking flags try { @@ -169,8 +166,6 @@ class XcfaCli(private val args: Array) { val swFrontend = Stopwatch.createStarted() LbePass.level = lbeLevel - if(randomSeed >= 0) XcfaDporLts.random = Random(randomSeed) - val xcfa = try { val stream = FileInputStream(input!!) val xcfaFromC = getXcfaFromC(stream, explicitProperty == ErrorDetection.OVERFLOW) From 3ed48a006e83f715f7302f1b0a024d1feb8f0291 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Fri, 1 Sep 2023 11:02:52 +0200 Subject: [PATCH 02/10] merging devs from por/benchmarking --- .../mit/theta/analysis/algorithm/ArgNode.java | 18 +- .../analysis/expl/ExplStmtOptimizer.java | 2 +- .../analysis/pred/PredStmtOptimizer.java | 2 +- .../mit/theta/core/utils}/StmtSimplifier.java | 3 +- .../theta/core}/utils/StmtSimplifierTest.java | 4 +- .../theta/xcfa/analysis/por/XcfaDporLts.kt | 61 ++--- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 8 +- subprojects/xcfa/xcfa/build.gradle.kts | 2 + .../main/java/hu/bme/mit/theta/xcfa/Utils.kt | 2 +- .../hu/bme/mit/theta/xcfa/model/Builders.kt | 2 +- .../hu/bme/mit/theta/xcfa/passes/LbePass.kt | 6 +- .../mit/theta/xcfa/passes/LoopUnrollPass.kt | 223 ++++++++++++++++++ .../theta/xcfa/passes/ProcedurePassManager.kt | 1 + .../theta/xcfa/passes/SimplifyExprsPass.kt | 78 +++++- 14 files changed, 341 insertions(+), 71 deletions(-) rename subprojects/common/{analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer => core/src/main/java/hu/bme/mit/theta/core/utils}/StmtSimplifier.java (99%) rename subprojects/common/{analysis/src/test/java/hu/bme/mit/theta/analysis => core/src/test/java/hu/bme/mit/theta/core}/utils/StmtSimplifierTest.java (98%) create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt 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 06b453911d..ad7b1f96ca 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 @@ -273,17 +273,13 @@ public int hashCode() { return result; } - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - ArgNode argNode = (ArgNode) o; - return depth == argNode.depth && - state.equals(argNode.state) && - coveringNode.equals(argNode.coveringNode) && - Set.copyOf(outEdges).equals(Set.copyOf(argNode.outEdges)) && - target == argNode.target; - } + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + ArgNode argNode = (ArgNode) o; + return id == argNode.id; + } @Override public String toString() { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtOptimizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtOptimizer.java index 91835e6db7..625f446dd3 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtOptimizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtOptimizer.java @@ -16,7 +16,7 @@ package hu.bme.mit.theta.analysis.expl; import hu.bme.mit.theta.analysis.stmtoptimizer.StmtOptimizer; -import hu.bme.mit.theta.analysis.stmtoptimizer.StmtSimplifier; +import hu.bme.mit.theta.core.utils.StmtSimplifier; import hu.bme.mit.theta.core.stmt.Stmt; public class ExplStmtOptimizer implements StmtOptimizer { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStmtOptimizer.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStmtOptimizer.java index b5f9687b69..548a6f39a7 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStmtOptimizer.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/pred/PredStmtOptimizer.java @@ -16,7 +16,7 @@ package hu.bme.mit.theta.analysis.pred; import hu.bme.mit.theta.analysis.stmtoptimizer.StmtOptimizer; -import hu.bme.mit.theta.analysis.stmtoptimizer.StmtSimplifier; +import hu.bme.mit.theta.core.utils.StmtSimplifier; import hu.bme.mit.theta.core.model.ImmutableValuation; import hu.bme.mit.theta.core.stmt.Stmt; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtSimplifier.java similarity index 99% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtSimplifier.java rename to subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtSimplifier.java index c9a9563337..53d87cdd2d 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtSimplifier.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtSimplifier.java @@ -14,7 +14,7 @@ * limitations under the License. */ -package hu.bme.mit.theta.analysis.stmtoptimizer; +package hu.bme.mit.theta.core.utils; import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.core.decl.Decl; @@ -38,7 +38,6 @@ import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.inttype.IntLitExpr; -import hu.bme.mit.theta.core.utils.ExprUtils; import java.math.BigInteger; import java.util.ArrayList; diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/utils/StmtSimplifierTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/StmtSimplifierTest.java similarity index 98% rename from subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/utils/StmtSimplifierTest.java rename to subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/StmtSimplifierTest.java index a9382a5908..f4d0aeb353 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/utils/StmtSimplifierTest.java +++ b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/StmtSimplifierTest.java @@ -13,7 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.utils; +package hu.bme.mit.theta.core.utils; import static com.google.common.collect.ImmutableSet.of; import static hu.bme.mit.theta.core.decl.Decls.Var; @@ -31,7 +31,7 @@ import java.util.Set; import com.google.common.collect.ImmutableList; -import hu.bme.mit.theta.analysis.stmtoptimizer.StmtSimplifier; +import hu.bme.mit.theta.core.utils.StmtSimplifier; import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.core.stmt.SequenceStmt; import org.junit.Test; 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 e41d572896..57d73c7bac 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 @@ -92,8 +92,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { * Partial order of states considering sleep sets (unexplored behavior). */ fun getPartialOrder(partialOrd: PartialOrd) = PartialOrd { s1, s2 -> - partialOrd.isLeq(s1, s2) && s2.reExplored == true && s1.sleep.containsAll( - s2.sleep - s2.explored) + partialOrd.isLeq(s1, s2) && s2.reExplored == true && s1.sleep.containsAll(s2.sleep - s2.explored) } } @@ -189,14 +188,12 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { exploreLazily() } while (stack.isNotEmpty() && - (last.node.isSubsumed || (last.node.isExpanded && last.backtrack.subtract( - last.sleep).isEmpty())) + (last.node.isSubsumed || (last.node.isExpanded && last.backtrack.subtract(last.sleep).isEmpty())) ) { // until we need to pop (the last is covered or not feasible, or it has no more actions that need to be explored 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.state.mutexes.keys subtract lastButOne.state.mutexes.keys).contains("") if (last.node.explored.isEmpty() || mutexNeverReleased) { // if a mutex is never released another action (practically all the others) have to be explored lastButOne.backtrack = lastButOne.state.enabled.toMutableSet() @@ -238,10 +235,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { val newaction = item.inEdge.get().action val process = newaction.pid - val newProcessLastAction = last.processLastAction.toMutableMap() - .apply { this[process] = stack.size } - var newLastDependents = (last.lastDependents[process]?.toMutableMap() - ?: mutableMapOf()).apply { + val newProcessLastAction = last.processLastAction.toMutableMap().apply { this[process] = stack.size } + var newLastDependents = (last.lastDependents[process]?.toMutableMap() ?: mutableMapOf()).apply { this[process] = stack.size } val relevantProcesses = (newProcessLastAction.keys - setOf(process)).toMutableSet() @@ -253,8 +248,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { val action = node.inEdge.get().action if (relevantProcesses.contains(action.pid)) { - if (newLastDependents.containsKey( - action.pid) && index <= newLastDependents[action.pid]!!) { + if (newLastDependents.containsKey(action.pid) && index <= newLastDependents[action.pid]!!) { // there is an action a' such that action -> a' -> newaction (->: happens-before) relevantProcesses.remove(action.pid) } else if (dependent(newaction, action)) { @@ -272,8 +266,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { } newLastDependents[action.pid] = index - newLastDependents = max(newLastDependents, - stack[index].lastDependents[action.pid]!!) + newLastDependents = max(newLastDependents, stack[index].lastDependents[action.pid]!!) relevantProcesses.remove(action.pid) } } @@ -287,15 +280,10 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { val lockedMutexes = newMutexes - oldMutexes val releasedMutexes = oldMutexes - newMutexes if (!item.state.isBottom) { - releasedMutexes.forEach { m -> - last.mutexLocks[m]?.let { - stack[it].mutexLocks.remove(m) - } - } + releasedMutexes.forEach { m -> last.mutexLocks[m]?.let { stack[it].mutexLocks.remove(m) } } } - val isCoveringNode = item.parent.get() != last.node - val isVirtualExploration = virtualLimit < stack.size || isCoveringNode + val isVirtualExploration = virtualLimit < stack.size || item.parent.get() != last.node val newSleep = if (isVirtualExploration) { item.state.sleep } else { @@ -327,13 +315,11 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { stack.push( StackItem( node = item, - processLastAction = if (!isCoveringNode) newProcessLastAction else last.processLastAction.toMutableMap(), + processLastAction = newProcessLastAction, lastDependents = last.lastDependents.toMutableMap().apply { - if (!isCoveringNode) { - this[process] = newLastDependents - newProcesses.forEach { - this[it] = max(this[it] ?: mutableMapOf(), newLastDependents) - } + this[process] = newLastDependents + newProcesses.forEach { + this[it] = max(this[it] ?: mutableMapOf(), newLastDependents) } }, mutexLocks = last.mutexLocks.toMutableMap().apply { @@ -359,8 +345,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { while (stack.size > startStackSize && stack.peek().node != visiting.parent.get()) stack.pop() if (node != visiting) { - if (!push(visiting, startStackSize) || noInfluenceOnRealExploration( - realStackSize)) continue + if (!push(visiting, startStackSize) || noInfluenceOnRealExploration(realStackSize)) continue } // visiting is not on the stack: no cycle && further virtual exploration can influence real exploration @@ -397,9 +382,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { * Returns a map with the keys of the original maps and the maximum of the reference numbers associated to each key. */ private fun max(map1: Map, map2: Map) = - (map1.keys union map2.keys).associateWith { key -> - max(map1[key] ?: -1, map2[key] ?: -1) - }.toMutableMap() + (map1.keys union map2.keys).associateWith { key -> max(map1[key] ?: -1, map2[key] ?: -1) }.toMutableMap() /** * See the article for the definition of notdep. @@ -408,8 +391,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { 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) + item.node.parent.get() == stack[start + 1 + index - 1].node && !dependent(e, item.action) } .map { it.action } .toMutableList().apply { add(action) } @@ -435,11 +417,9 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { /** * Returns true when the virtual exploration cannot detect any more races relevant in the "real" exploration (the part of the search stack before the first covering node). */ - private fun noInfluenceOnRealExploration( - realStackSize: Int) = last.processLastAction.keys.all { process -> - last.lastDependents.containsKey( - process) && last.lastDependents[process]!!.all { (otherProcess, index) -> - index >= realStackSize || index >= last.processLastAction[otherProcess]!! + private fun noInfluenceOnRealExploration(realStackSize: Int) = last.processLastAction.keys.all { process -> + last.lastDependents.containsKey(process) && last.lastDependents[process]!!.all { (_, index) -> + index >= realStackSize } } } @@ -471,8 +451,7 @@ class XcfaAadporLts(private val xcfa: XCFA) : XcfaDporLts(xcfa) { /** * Returns actions to be explored from the given state considering the given precision. */ - override fun

getEnabledActionsFor(state: S, exploredActions: Collection, - prec: P): Set { + override fun

getEnabledActionsFor(state: S, exploredActions: Collection, prec: P): Set { this.prec = prec return getEnabledActionsFor(state) } 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 27fe74f7d7..0f479b8d0c 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 @@ -46,6 +46,7 @@ import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer import hu.bme.mit.theta.xcfa.model.XCFA import hu.bme.mit.theta.xcfa.model.toDot import hu.bme.mit.theta.xcfa.passes.LbePass +import hu.bme.mit.theta.xcfa.passes.LoopUnrollPass import org.antlr.v4.runtime.CharStreams import java.io.File import java.io.FileInputStream @@ -74,6 +75,9 @@ class XcfaCli(private val args: Array) { description = "Level of LBE (NO_LBE, LBE_LOCAL, LBE_SEQ, LBE_FULL)") var lbeLevel: LbePass.LbeLevel = LbePass.LbeLevel.LBE_SEQ + @Parameter(names = ["--unroll"], description = "Max number of loop iterations to unroll") + var loopUnroll: Int = 50 + @Parameter(names = ["--input-type"], description = "Format of the input") var inputType: InputType = InputType.C @@ -162,13 +166,14 @@ class XcfaCli(private val args: Array) { val gsonForOutput = getGson() val logger = ConsoleLogger(logLevel) val explicitProperty: ErrorDetection = getExplicitProperty() + registerAllSolverManagers(solverHome, logger) // propagating input variables LbePass.level = lbeLevel if (randomSeed >= 0) XcfaDporLts.random = Random(randomSeed) + LoopUnrollPass.UNROLL_LIMIT = loopUnroll WebDebuggerLogger.getInstance().setTitle(input?.name) - logger.write(Logger.Level.INFO, "Parsing the input $input as $inputType") val parseContext = ParseContext() val xcfa = getXcfa(logger, explicitProperty, parseContext) @@ -185,7 +190,6 @@ class XcfaCli(private val args: Array) { // verification stopwatch.reset().start() logger.write(Logger.Level.INFO, "Starting verification of ${xcfa.name} using $backend") - registerAllSolverManagers(solverHome, logger) val config = parseConfigFromCli() if (strategy != Strategy.PORTFOLIO && printConfigFile != null) { printConfigFile!!.writeText(gsonForOutput.toJson(config)) diff --git a/subprojects/xcfa/xcfa/build.gradle.kts b/subprojects/xcfa/xcfa/build.gradle.kts index 322fe35b0e..cad8a876f0 100644 --- a/subprojects/xcfa/xcfa/build.gradle.kts +++ b/subprojects/xcfa/xcfa/build.gradle.kts @@ -22,4 +22,6 @@ dependencies { implementation(project(":theta-core")) implementation(project(":theta-grammar")) implementation(project(":theta-c-frontend")) + implementation(project(":theta-analysis")) + implementation(project(":theta-solver")) } 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 d2227ad288..b2c6876b71 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 @@ -83,7 +83,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. */ -private fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { +internal fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { is StmtLabel -> { when (stmt) { is HavocStmt<*> -> mapOf(stmt.varDecl to WRITE) 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 16c83f636a..12a817f73f 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 @@ -55,7 +55,7 @@ class XcfaBuilder @JvmOverloads constructor( } fun addEntryPoint(toAdd: XcfaProcedureBuilder, params: List>) { - procedures.add(toAdd) + addProcedure(toAdd) initProcedures.add(Pair(toAdd, params)) } } 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 d51fcacca8..6bd2fff5f0 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 @@ -16,6 +16,8 @@ package hu.bme.mit.theta.xcfa.passes import com.google.common.base.Preconditions +import hu.bme.mit.theta.core.stmt.AssumeStmt +import hu.bme.mit.theta.core.type.booltype.FalseExpr import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.xcfa.collectVars import hu.bme.mit.theta.xcfa.getAtomicBlockInnerLocations @@ -303,8 +305,8 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { */ private fun isNotLocal(edge: XcfaEdge): Boolean { return !edge.getFlatLabels().all { label -> - !(label is StartLabel || label is JoinLabel) && label.collectVars() - .all(builder.getVars()::contains) + !(label is StartLabel || label is JoinLabel) && label.collectVars().all(builder.getVars()::contains) && + !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) } } } \ No newline at end of file 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 new file mode 100644 index 0000000000..f337d2cf5f --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt @@ -0,0 +1,223 @@ +package hu.bme.mit.theta.xcfa.passes + +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expl.ExplStmtTransFunc +import hu.bme.mit.theta.analysis.expr.StmtAction +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.model.ImmutableValuation +import hu.bme.mit.theta.core.stmt.AssumeStmt +import hu.bme.mit.theta.core.stmt.Stmt +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.xcfa.collectVars +import hu.bme.mit.theta.xcfa.collectVarsWithAccessType +import hu.bme.mit.theta.xcfa.getFlatLabels +import hu.bme.mit.theta.xcfa.isWritten +import hu.bme.mit.theta.xcfa.model.* +import java.util.* + +/** + * Unrolls loops where the number of loop executions can be determined statically. + * The UNROLL_LIMIT refers to the number of loop executions: loops that are executed more times than this limit + * are not unrolled. + */ +class LoopUnrollPass : ProcedurePass { + + companion object { + var UNROLL_LIMIT = 50 + + private val solver: Solver = SolverManager.resolveSolverFactory("Z3").createSolver() + } + + 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 + ) { + 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()) + + override fun getStmts() = listOf(stmt) + } + + private fun count(transFunc: ExplStmtTransFunc): Int { + val prec = ExplPrec.of(listOf(loopVar)) + var state = ExplState.of(ImmutableValuation.empty()) + state = transFunc.getSuccStates(state, BasicStmtAction(loopVarInit), prec).first() + + var cnt = 0 + while (!transFunc.getSuccStates(state, BasicStmtAction(loopCondEdge), prec).first().isBottom) { + cnt++ + if (cnt > UNROLL_LIMIT) return -1 + 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() } + return when { + this == stmtToRemove -> NopLabel + this is SequenceLabel -> SequenceLabel(labels.map { it.removeCondition() }, metadata) + else -> this + } + } + + private fun copyBody(builder: XcfaProcedureBuilder, startLocation: XcfaLocation, index: Int): XcfaLocation { + val locs = loopLocs.associateWith { + val loc = XcfaLocation("loop${index}_${it.name}") + builder.addLoc(loc) + loc + } + + loopEdges.forEach { + val newSource = if (it.source == loopStart) startLocation else locs[it.source]!! + val newLabel = if (it.source == loopStart) it.label.removeCondition() else it.label + val edge = XcfaEdge(newSource, locs[it.target]!!, newLabel, it.metadata) + builder.addEdge(edge) + } + + return locs[loopStart]!! + } + + fun unroll(builder: XcfaProcedureBuilder, transFunc: ExplStmtTransFunc) { + val count = count(transFunc) + if (count == -1) return + + (loopLocs - loopStart).forEach(builder::removeLoc) + loopEdges.forEach(builder::removeEdge) + builder.removeEdge(exitCondEdge) + + var startLocation = loopStart + for (i in 0 until count) { + startLocation = copyBody(builder, startLocation, i) + } + + builder.addEdge( + XcfaEdge( + source = startLocation, + target = exitCondEdge.target, + label = exitCondEdge.label.removeCondition(), + metadata = exitCondEdge.metadata + ) + ) + } + } + + override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { + val transFunc = ExplStmtTransFunc.create(solver, 1) + while (true) { + val loop = findLoop(builder.initLoc) ?: break + loop.unroll(builder, transFunc) + testedLoops.add(loop) + } + return builder + } + + private fun findLoop(initLoc: XcfaLocation): Loop? { // DFS + val stack = Stack() + val explored = mutableSetOf() + stack.push(initLoc) + while (stack.isNotEmpty()) { + val current = stack.peek() + val edgesToExplore = current.outgoingEdges subtract explored + if (edgesToExplore.isEmpty()) { + stack.pop() + } else { + val edge = edgesToExplore.random() + if (edge.target in stack) { // loop found + isUnrollable(edge.target, stack)?.let { return it } + } else { + stack.push(edge.target) + } + explored.add(edge) + } + } + return null + } + + private fun isUnrollable(loopStart: XcfaLocation, stack: Stack): Loop? { + if (loopStart.outgoingEdges.size != 2) return null + val loopLocations = stack.slice(stack.lastIndexOf(loopStart) until stack.size) + val loopEdges = loopLocations.flatMap { loc -> + if (loc == loopStart) { + val loopEdge = loc.outgoingEdges.filter { it.target in loopLocations } + if (loopEdge.size != 1) return null + loopEdge + } else { + if (!loopLocations.containsAll(loc.outgoingEdges.map { it.target })) { + return null + } + loc.outgoingEdges + } + } + + val loopVar = loopStart.outgoingEdges.map { + val vars = it.label.collectVarsWithAccessType() + if (vars.size != 1) return null + vars.keys.first() + }.reduce { v1, v2 -> if (v1 != v2) return null else v1 } + + var edge = loopStart.outgoingEdges.find { it.target in loopLocations }!! + val necessaryLoopEdges = mutableSetOf(edge) + while (edge.target.outgoingEdges.size == 1) { + edge = edge.target.outgoingEdges.first() + necessaryLoopEdges.add(edge) + } + val finalEdges = loopStart.incomingEdges.filter { it.source in loopLocations } + if (finalEdges.size == 1) { + edge = finalEdges.first() + necessaryLoopEdges.add(edge) + while (edge.source.incomingEdges.size == 1) { + edge = edge.source.incomingEdges.first() + necessaryLoopEdges.add(edge) + } + } + + val loopVarModifiers = loopEdges.filter { + val vars = it.label.collectVarsWithAccessType() + if (vars[loopVar].isWritten) { + if (it !in necessaryLoopEdges || vars.size > 1) return null + true + } else { + false + } + } + + lateinit var loopVarInit: XcfaEdge + var loc = loopStart + while (true) { + val inEdges = loc.incomingEdges.filter { it.source !in loopLocations } + if (inEdges.size != 1) return null + val inEdge = inEdges.first() + val vars = inEdge.label.collectVarsWithAccessType() + if (vars[loopVar].isWritten) { + if (vars.size > 1) return null + loopVarInit = inEdge + break + } + loc = inEdge.source + } + + return Loop( + loopVar = loopVar, + loopVarModifiers = loopVarModifiers, + loopVarInit = loopVarInit, + loopCondEdge = loopStart.outgoingEdges.find { it.target in loopLocations }!!, + exitCondEdge = loopStart.outgoingEdges.find { it.target !in loopLocations }!!, + loopStart = loopStart, + loopLocs = loopLocations, + loopEdges = loopEdges + ).also { if (it in testedLoops) return null } + } +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index ac9d3e8d41..0915ccf9f8 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -35,6 +35,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext) : ProcedurePas SvCompIntrinsicsPass(parseContext), FpFunctionsToExprsPass(parseContext), PthreadFunctionsPass(parseContext), + LoopUnrollPass(), // trying to inline procedures InlineProceduresPass(parseContext), RemoveDeadEnds(parseContext), diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt index bf7b59d555..7a6f23df8a 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt @@ -16,21 +16,28 @@ package hu.bme.mit.theta.xcfa.passes +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.model.ImmutableValuation +import hu.bme.mit.theta.core.model.MutableValuation +import hu.bme.mit.theta.core.model.Valuation import hu.bme.mit.theta.core.stmt.AssignStmt import hu.bme.mit.theta.core.stmt.AssumeStmt import hu.bme.mit.theta.core.stmt.Stmts.Assign import hu.bme.mit.theta.core.stmt.Stmts.Assume +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type import hu.bme.mit.theta.core.type.abstracttype.NeqExpr +import hu.bme.mit.theta.core.utils.ExprUtils import hu.bme.mit.theta.core.utils.ExprUtils.simplify +import hu.bme.mit.theta.core.utils.StmtUtils import hu.bme.mit.theta.core.utils.TypeUtils.cast import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType -import hu.bme.mit.theta.xcfa.model.SequenceLabel -import hu.bme.mit.theta.xcfa.model.StmtLabel -import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder +import hu.bme.mit.theta.xcfa.model.* /** - * This pass simplifies the expressions inside statements. + * This pass simplifies the expressions inside statements and substitutes the values of constant variables + * (that is, variables assigned only once). * Requires the ProcedureBuilder to be `deterministic` (@see DeterministicPass) * Sets the `simplifiedExprs` flag on the ProcedureBuilder */ @@ -39,12 +46,13 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass { override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { checkNotNull(builder.metaData["deterministic"]) + val valuation = findConstVariables(builder) val edges = LinkedHashSet(builder.getEdges()) for (edge in edges) { val newLabels = (edge.label as SequenceLabel).labels.map { if (it is StmtLabel) when (it.stmt) { is AssignStmt<*> -> { - val simplified = simplify(it.stmt.expr) + val simplified = simplify(it.stmt.expr, valuation) if (parseContext.metadata.getMetadataValue(it.stmt.expr, "cType").isPresent) parseContext.metadata.create(simplified, "cType", CComplexType.getType(it.stmt.expr, parseContext)) @@ -53,7 +61,7 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass { } is AssumeStmt -> { - val simplified = simplify(it.stmt.cond) + val simplified = simplify(it.stmt.cond, valuation) if (parseContext.metadata.getMetadataValue(it.stmt.cond, "cType").isPresent) { parseContext.metadata.create(simplified, "cType", CComplexType.getType(it.stmt.cond, parseContext)) @@ -73,4 +81,60 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass { builder.metaData["simplifiedExprs"] = Unit return builder } -} \ No newline at end of file + + private fun findConstVariables(builder: XcfaProcedureBuilder): Valuation { + val valuation = MutableValuation() + builder.parent.getProcedures() + .flatMap { it.getEdges() } + .map { it.label.collectVarsWithLabels() } + .filter { it.isNotEmpty() }.merge() + .map { + val writes = it.value.filter { label -> label.isWrite(it.key) } + if (writes.size == 1 && writes.first() is StmtLabel) { + val label = writes.first() as StmtLabel + if (label.stmt is AssignStmt<*> && label.stmt.expr.isConst()) { + return@map label.stmt + } + } + null + } + .filterNotNull() + .forEach { assignment -> + valuation.put(assignment.varDecl, assignment.expr.eval(ImmutableValuation.empty())) + } + return valuation + } + + private fun List, List>>.merge(): Map, List> = + this.fold(mapOf()) { acc, next -> + (acc.keys + next.keys).associateWith { + mutableListOf().apply { + acc[it]?.let { addAll(it) } + next[it]?.let { addAll(it) } + } + } + } + + private fun XcfaLabel.collectVarsWithLabels(): Map, List> = when (this) { + is StmtLabel -> StmtUtils.getVars(stmt).associateWith { listOf(this) } + is NondetLabel -> labels.map { it.collectVarsWithLabels() }.merge() + is SequenceLabel -> labels.map { it.collectVarsWithLabels() }.merge() + is InvokeLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { listOf(this) } + is JoinLabel -> mapOf(pidVar to listOf(this)) + is ReadLabel -> mapOf(global to listOf(this), local to listOf(this)) + is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten() + .associateWith { listOf(this) } + mapOf(pidVar to listOf(this)) + + is WriteLabel -> mapOf(global to listOf(this), local to listOf(this)) + else -> emptyMap() + } + + private fun XcfaLabel.isWrite(v: VarDecl<*>) = + this is StmtLabel && this.stmt is AssignStmt<*> && this.stmt.varDecl == v + + private fun Expr.isConst(): Boolean { + val vars = mutableListOf>() + ExprUtils.collectVars(this, vars) + return vars.isEmpty() + } +} From 996494ab129022f6f559c81cb82297e03f7e2be1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Fri, 1 Sep 2023 11:49:39 +0200 Subject: [PATCH 03/10] copyright + code formatting --- .../mit/theta/analysis/algorithm/ArgNode.java | 14 ++-- .../theta/xcfa/analysis/por/XcfaDporLts.kt | 65 ++++++++++++++----- .../hu/bme/mit/theta/xcfa/passes/LbePass.kt | 4 +- .../mit/theta/xcfa/passes/LoopUnrollPass.kt | 28 +++++++- 4 files changed, 81 insertions(+), 30 deletions(-) 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 ad7b1f96ca..a8506c0182 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 @@ -273,13 +273,13 @@ public int hashCode() { return result; } - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - ArgNode argNode = (ArgNode) o; - return id == argNode.id; - } + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + ArgNode argNode = (ArgNode) o; + return id == argNode.id; + } @Override public String toString() { 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 57d73c7bac..4585e87b90 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 @@ -75,7 +75,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { companion object { - var random: Random = Random.Default // use Random(seed) with a seed or Random.Default without seed + var random: Random = + Random.Default // use Random(seed) with a seed or Random.Default without seed /** * Simple LTS that returns the enabled actions in a state. @@ -92,7 +93,10 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { * Partial order of states considering sleep sets (unexplored behavior). */ fun getPartialOrder(partialOrd: PartialOrd) = PartialOrd { s1, s2 -> - partialOrd.isLeq(s1, s2) && s2.reExplored == true && s1.sleep.containsAll(s2.sleep - s2.explored) + partialOrd.isLeq( + s1, + s2 + ) && s2.reExplored == true && s1.sleep.containsAll(s2.sleep - s2.explored) } } @@ -161,7 +165,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { // lazy pruning: goes to the root when the stack is empty while (stack.isEmpty() && node.parent.isPresent) node = node.parent.get() - node.state.reExplored = true // lazy pruning: indicates that the state is explored in the current iteration + node.state.reExplored = + true // lazy pruning: indicates that the state is explored in the current iteration push(node, stack.size) } @@ -188,12 +193,15 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { exploreLazily() } while (stack.isNotEmpty() && - (last.node.isSubsumed || (last.node.isExpanded && last.backtrack.subtract(last.sleep).isEmpty())) + (last.node.isSubsumed || (last.node.isExpanded && last.backtrack.subtract(last.sleep) + .isEmpty())) ) { // until we need to pop (the last is covered or not feasible, or it has no more actions that need to be explored 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.state.mutexes.keys subtract lastButOne.state.mutexes.keys).contains( + "" + ) if (last.node.explored.isEmpty() || mutexNeverReleased) { // if a mutex is never released another action (practically all the others) have to be explored lastButOne.backtrack = lastButOne.state.enabled.toMutableSet() @@ -235,10 +243,12 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { val newaction = item.inEdge.get().action val process = newaction.pid - val newProcessLastAction = last.processLastAction.toMutableMap().apply { this[process] = stack.size } - var newLastDependents = (last.lastDependents[process]?.toMutableMap() ?: mutableMapOf()).apply { - this[process] = stack.size - } + val newProcessLastAction = + last.processLastAction.toMutableMap().apply { this[process] = stack.size } + var newLastDependents = + (last.lastDependents[process]?.toMutableMap() ?: mutableMapOf()).apply { + this[process] = stack.size + } val relevantProcesses = (newProcessLastAction.keys - setOf(process)).toMutableSet() // Race detection @@ -266,7 +276,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { } newLastDependents[action.pid] = index - newLastDependents = max(newLastDependents, stack[index].lastDependents[action.pid]!!) + newLastDependents = + max(newLastDependents, stack[index].lastDependents[action.pid]!!) relevantProcesses.remove(action.pid) } } @@ -280,7 +291,13 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { val lockedMutexes = newMutexes - oldMutexes val releasedMutexes = oldMutexes - newMutexes if (!item.state.isBottom) { - releasedMutexes.forEach { m -> last.mutexLocks[m]?.let { stack[it].mutexLocks.remove(m) } } + releasedMutexes.forEach { m -> + last.mutexLocks[m]?.let { + stack[it].mutexLocks.remove( + m + ) + } + } } val isVirtualExploration = virtualLimit < stack.size || item.parent.get() != last.node @@ -345,7 +362,10 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { while (stack.size > startStackSize && stack.peek().node != visiting.parent.get()) stack.pop() if (node != visiting) { - if (!push(visiting, startStackSize) || noInfluenceOnRealExploration(realStackSize)) continue + if (!push(visiting, startStackSize) || noInfluenceOnRealExploration( + realStackSize + ) + ) continue } // visiting is not on the stack: no cycle && further virtual exploration can influence real exploration @@ -382,7 +402,12 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { * Returns a map with the keys of the original maps and the maximum of the reference numbers associated to each key. */ private fun max(map1: Map, map2: Map) = - (map1.keys union map2.keys).associateWith { key -> max(map1[key] ?: -1, map2[key] ?: -1) }.toMutableMap() + (map1.keys union map2.keys).associateWith { key -> + max( + map1[key] ?: -1, + map2[key] ?: -1 + ) + }.toMutableMap() /** * See the article for the definition of notdep. @@ -391,7 +416,10 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { 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) + item.node.parent.get() == stack[start + 1 + index - 1].node && !dependent( + e, + item.action + ) } .map { it.action } .toMutableList().apply { add(action) } @@ -417,11 +445,12 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { /** * Returns true when the virtual exploration cannot detect any more races relevant in the "real" exploration (the part of the search stack before the first covering node). */ - private fun noInfluenceOnRealExploration(realStackSize: Int) = last.processLastAction.keys.all { process -> - last.lastDependents.containsKey(process) && last.lastDependents[process]!!.all { (_, index) -> - index >= realStackSize + private fun noInfluenceOnRealExploration(realStackSize: Int) = + last.processLastAction.keys.all { process -> + last.lastDependents.containsKey(process) && last.lastDependents[process]!!.all { (_, index) -> + index >= realStackSize + } } - } } /** 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..080a866925 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 @@ -36,7 +36,7 @@ import kotlin.collections.set * * Middle location: a location whose incoming degree is 1 * */ -class LbePass(val parseContext: ParseContext) : ProcedurePass { +class aLbePass(val parseContext: ParseContext) : ProcedurePass { companion object { @@ -306,7 +306,7 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { private fun isNotLocal(edge: XcfaEdge): Boolean { return !edge.getFlatLabels().all { label -> !(label is StartLabel || label is JoinLabel) && label.collectVars().all(builder.getVars()::contains) && - !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) + !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) } } } \ No newline at end of file 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 f337d2cf5f..704aafebfe 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 @@ -1,3 +1,18 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ package hu.bme.mit.theta.xcfa.passes import hu.bme.mit.theta.analysis.expl.ExplPrec @@ -55,10 +70,13 @@ 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 } @@ -68,7 +86,11 @@ class LoopUnrollPass : ProcedurePass { .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) + this is SequenceLabel -> SequenceLabel( + labels.map { it.removeCondition() }, + metadata + ) + else -> this } } From 2c863d7c8d0dd0b991cbeda6f1186f3b8a5fee7e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Fri, 1 Sep 2023 11:55:27 +0200 Subject: [PATCH 04/10] code formatting --- .../theta/xcfa/analysis/por/XcfaDporLts.kt | 33 ++++++++----------- .../hu/bme/mit/theta/xcfa/passes/LbePass.kt | 4 +-- .../mit/theta/xcfa/passes/LoopUnrollPass.kt | 16 +++------ 3 files changed, 19 insertions(+), 34 deletions(-) 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 4585e87b90..81ddf8de8d 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 @@ -94,8 +94,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { */ fun getPartialOrder(partialOrd: PartialOrd) = PartialOrd { s1, s2 -> partialOrd.isLeq( - s1, - s2 + s1, s2 ) && s2.reExplored == true && s1.sleep.containsAll(s2.sleep - s2.explored) } } @@ -192,16 +191,16 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { // when lazy pruning is used the explored parts from previous iterations are reexplored to detect possible races exploreLazily() } - while (stack.isNotEmpty() && - (last.node.isSubsumed || (last.node.isExpanded && last.backtrack.subtract(last.sleep) - .isEmpty())) + while (stack.isNotEmpty() && (last.node.isSubsumed || (last.node.isExpanded && last.backtrack.subtract( + last.sleep + ).isEmpty())) ) { // until we need to pop (the last is covered or not feasible, or it has no more actions that need to be explored 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( - "" - ) + val mutexNeverReleased = + last.mutexLocks.containsKey("") && (last.state.mutexes.keys subtract lastButOne.state.mutexes.keys).contains( + "" + ) if (last.node.explored.isEmpty() || mutexNeverReleased) { // if a mutex is never released another action (practically all the others) have to be explored lastButOne.backtrack = lastButOne.state.enabled.toMutableSet() @@ -404,8 +403,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { private fun max(map1: Map, map2: Map) = (map1.keys union map2.keys).associateWith { key -> max( - map1[key] ?: -1, - map2[key] ?: -1 + map1[key] ?: -1, map2[key] ?: -1 ) }.toMutableMap() @@ -414,15 +412,11 @@ 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 -> + 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 + e, item.action ) - } - .map { it.action } - .toMutableList().apply { add(action) } + }.map { it.action }.toMutableList().apply { add(action) } } /** @@ -462,8 +456,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { val aGlobalVars = a.edge.getGlobalVars(xcfa) val bGlobalVars = b.edge.getGlobalVars(xcfa) // dependent if they access the same variable (at least one write) - return (aGlobalVars.keys intersect bGlobalVars.keys) - .any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten } + return (aGlobalVars.keys intersect bGlobalVars.keys).any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten } } } 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 080a866925..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 @@ -36,7 +36,7 @@ import kotlin.collections.set * * Middle location: a location whose incoming degree is 1 * */ -class aLbePass(val parseContext: ParseContext) : ProcedurePass { +class LbePass(val parseContext: ParseContext) : ProcedurePass { companion object { @@ -306,7 +306,7 @@ class aLbePass(val parseContext: ParseContext) : ProcedurePass { private fun isNotLocal(edge: XcfaEdge): Boolean { return !edge.getFlatLabels().all { label -> !(label is StartLabel || label is JoinLabel) && label.collectVars().all(builder.getVars()::contains) && - !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) + !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) } } } \ No newline at end of file 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 704aafebfe..9613ba5b98 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 @@ -48,14 +48,7 @@ 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()) @@ -82,13 +75,12 @@ class LoopUnrollPass : ProcedurePass { } 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 + labels.map { it.removeCondition() }, metadata ) else -> this From 4556bc8c9e46e25dc16e4df788e65ab1eaaa75a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sun, 10 Sep 2023 14:30:09 +0200 Subject: [PATCH 05/10] removed ArgNode comparison simplification --- .../java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java | 6 +++++- 1 file changed, 5 insertions(+), 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..06b453911d 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 @@ -278,7 +278,11 @@ public boolean equals(Object o) { if (this == o) return true; if (o == null || getClass() != o.getClass()) return false; ArgNode argNode = (ArgNode) o; - return id == argNode.id; + return depth == argNode.depth && + state.equals(argNode.state) && + coveringNode.equals(argNode.coveringNode) && + Set.copyOf(outEdges).equals(Set.copyOf(argNode.outEdges)) && + target == argNode.target; } @Override From d1f33e6cd1de382436a41ac1e99470c191d5c2d2 Mon Sep 17 00:00:00 2001 From: "thetabotmaintainer[bot]" <139346997+thetabotmaintainer[bot]@users.noreply.github.com> Date: Sun, 10 Sep 2023 15:07:55 +0200 Subject: [PATCH 06/10] Reformatted code (#204) Co-authored-by: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> --- .../hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt | 11 ++++++----- .../main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt | 2 +- .../hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt | 6 +++++- 3 files changed, 12 insertions(+), 7 deletions(-) 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..8a0749a941 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) } } /** 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..96cbd7832a 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 @@ -306,7 +306,7 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { private fun isNotLocal(edge: XcfaEdge): Boolean { return !edge.getFlatLabels().all { label -> !(label is StartLabel || label is JoinLabel) && label.collectVars().all(builder.getVars()::contains) && - !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) + !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) } } } \ No newline at end of file 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..c3d421bc79 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()) From 9b4a0ef6817728a0ee14331cdd256cf64d960a41 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= <56129746+csanadtelbisz@users.noreply.github.com> Date: Sun, 10 Sep 2023 17:47:40 +0200 Subject: [PATCH 07/10] replaced LoopUnrollPass solver initialization (no solver home registration required) --- .../xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 2 +- subprojects/xcfa/xcfa/build.gradle.kts | 1 + .../main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) 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..7d73f4ace1 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 @@ -168,7 +168,6 @@ class XcfaCli(private val args: Array) { val gsonForOutput = getGson() val logger = ConsoleLogger(logLevel) val explicitProperty: ErrorDetection = getExplicitProperty() - registerAllSolverManagers(solverHome, logger) // propagating input variables LbePass.level = lbeLevel @@ -192,6 +191,7 @@ class XcfaCli(private val args: Array) { // verification stopwatch.reset().start() logger.write(Logger.Level.INFO, "Starting verification of ${xcfa.name} using $backend") + registerAllSolverManagers(solverHome, logger) val config = parseConfigFromCli() if (strategy != Strategy.PORTFOLIO && printConfigFile != null) { printConfigFile!!.writeText(gsonForOutput.toJson(config)) diff --git a/subprojects/xcfa/xcfa/build.gradle.kts b/subprojects/xcfa/xcfa/build.gradle.kts index cad8a876f0..1094a17c91 100644 --- a/subprojects/xcfa/xcfa/build.gradle.kts +++ b/subprojects/xcfa/xcfa/build.gradle.kts @@ -24,4 +24,5 @@ dependencies { implementation(project(":theta-c-frontend")) implementation(project(":theta-analysis")) implementation(project(":theta-solver")) + implementation(project(mapOf("path" to ":theta-solver-z3"))) } 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 c3d421bc79..2d461f42b0 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 @@ -43,7 +43,7 @@ class LoopUnrollPass : ProcedurePass { var UNROLL_LIMIT = 50 - private val solver: Solver = SolverManager.resolveSolverFactory("Z3").createSolver() + private val solver: Solver = Z3SolverFactory.getInstance().createSolver() } private val testedLoops = mutableSetOf() From be9444c2c575775def9a453c3cee20f5e46f02ef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= <56129746+csanadtelbisz@users.noreply.github.com> Date: Sun, 10 Sep 2023 18:33:57 +0200 Subject: [PATCH 08/10] Fixed z3 dependency --- .../main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 2d461f42b0..2c0c0a03a8 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 @@ -24,7 +24,7 @@ import hu.bme.mit.theta.core.model.ImmutableValuation import hu.bme.mit.theta.core.stmt.AssumeStmt import hu.bme.mit.theta.core.stmt.Stmt import hu.bme.mit.theta.solver.Solver -import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.solver.z3.Z3SolverFactory import hu.bme.mit.theta.xcfa.collectVars import hu.bme.mit.theta.xcfa.collectVarsWithAccessType import hu.bme.mit.theta.xcfa.getFlatLabels From c43d0a148d0d19bcf2e01ef2547336364a1e5d71 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= <56129746+csanadtelbisz@users.noreply.github.com> Date: Sun, 10 Sep 2023 23:18:14 +0200 Subject: [PATCH 09/10] resolve sonarcloud bugs --- .../bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt | 12 +++++++----- .../hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt | 6 +++--- 2 files changed, 10 insertions(+), 8 deletions(-) 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 8a0749a941..63f7a47d8b 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 @@ -258,7 +258,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { val action = node.inEdge.get().action if (relevantProcesses.contains(action.pid)) { - if (newLastDependents.containsKey(action.pid) && index <= newLastDependents[action.pid]!!) { + if (newLastDependents.containsKey(action.pid) && index <= checkNotNull( + newLastDependents[action.pid])) { // there is an action a' such that action -> a' -> newaction (->: happens-before) relevantProcesses.remove(action.pid) } else if (dependent(newaction, action)) { @@ -277,7 +278,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { newLastDependents[action.pid] = index newLastDependents = - max(newLastDependents, stack[index].lastDependents[action.pid]!!) + max(newLastDependents, checkNotNull(stack[index].lastDependents[action.pid])) relevantProcesses.remove(action.pid) } } @@ -442,9 +443,10 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { */ private fun noInfluenceOnRealExploration(realStackSize: Int) = last.processLastAction.keys.all { process -> - last.lastDependents.containsKey(process) && last.lastDependents[process]!!.all { (_, index) -> - index >= realStackSize - } + last.lastDependents.containsKey(process) && + checkNotNull(last.lastDependents[process]).all { (_, index) -> + index >= realStackSize + } } } 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 2c0c0a03a8..f8281e686a 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 @@ -99,13 +99,13 @@ class LoopUnrollPass : ProcedurePass { } loopEdges.forEach { - val newSource = if (it.source == loopStart) startLocation else locs[it.source]!! + val newSource = if (it.source == loopStart) startLocation else checkNotNull(locs[it.source]) val newLabel = if (it.source == loopStart) it.label.removeCondition() else it.label - val edge = XcfaEdge(newSource, locs[it.target]!!, newLabel, it.metadata) + val edge = XcfaEdge(newSource, checkNotNull(locs[it.target]!!), newLabel, it.metadata) builder.addEdge(edge) } - return locs[loopStart]!! + return checkNotNull(locs[loopStart]) } fun unroll(builder: XcfaProcedureBuilder, transFunc: ExplStmtTransFunc) { From 53a611af6b9baa36b9b3194b91e554929150d0ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= <56129746+csanadtelbisz@users.noreply.github.com> Date: Wed, 20 Sep 2023 17:36:20 +0200 Subject: [PATCH 10/10] xcfa projection + separate mayCover versions for CEGAR and other algorithms (impact) --- .../hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java | 9 --------- .../hu/bme/mit/theta/analysis/algorithm/ArgNode.java | 8 ++++++++ .../theta/analysis/algorithm/cegar/BasicAbstractor.java | 2 +- .../java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt | 1 + 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java index f94ecce888..3b322ed01a 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java @@ -109,13 +109,4 @@ public Collection> expand(final ArgNode node, final P prec) return newSuccNodes; } - public void close(final ArgNode node) { - checkNotNull(node); - if (!node.isSubsumed()) { - final ARG arg = node.arg; - final Optional> nodeToCoverWith = arg.getNodes().filter(n -> n.mayCover(node)).findFirst(); - nodeToCoverWith.ifPresent(node::cover); - } - } - } 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 06b453911d..81f5a5270a 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 @@ -92,6 +92,14 @@ public boolean mayCover(final ArgNode node) { } } + public boolean mayCoverStandard(final ArgNode node) { + if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) { + return !(this.equals(node) || this.isSubsumed()); // no need to check ancestors in CEGAR + } else { + return false; + } + } + public void setCoveringNode(final ArgNode node) { if (!node.canCover) return; checkNotNull(node); 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..6c55d2ff79 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 @@ -127,7 +127,7 @@ private void close(final ArgNode node, final Collection> can return; } for (final ArgNode candidate : candidates) { - if (candidate.mayCover(node)) { + if (candidate.mayCoverStandard(node)) { node.cover(candidate); return; } 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..1f66ff86b6 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 @@ -192,6 +192,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