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 b47afc462f..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 @@ -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,8 +93,9 @@ 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) } } @@ -162,7 +164,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,15 +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() @@ -238,12 +242,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 @@ -253,8 +257,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 <= checkNotNull(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 +275,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { } newLastDependents[action.pid] = index - newLastDependents = max(newLastDependents, - checkNotNull(stack[index].lastDependents[action.pid])) + newLastDependents = + max(newLastDependents, stack[index].lastDependents[action.pid]!!) relevantProcesses.remove(action.pid) } } @@ -289,13 +292,14 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { if (!item.state.isBottom) { releasedMutexes.forEach { m -> last.mutexLocks[m]?.let { - stack[it].mutexLocks.remove(m) + 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 +331,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 { @@ -360,7 +362,9 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { if (node != visiting) { if (!push(visiting, startStackSize) || noInfluenceOnRealExploration( - realStackSize)) continue + realStackSize + ) + ) continue } // visiting is not on the stack: no cycle && further virtual exploration can influence real exploration @@ -398,7 +402,9 @@ 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) + max( + map1[key] ?: -1, map2[key] ?: -1 + ) }.toMutableMap() /** @@ -406,13 +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 -> - item.node.parent.get() == stack[start + 1 + index - 1].node && !dependent(e, - item.action) - } - .map { it.action } - .toMutableList().apply { add(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) } } /** @@ -435,13 +439,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) && checkNotNull(last.lastDependents[process]).all { (otherProcess, index) -> - index >= realStackSize || index >= checkNotNull(last.processLastAction[otherProcess]) + private fun noInfluenceOnRealExploration(realStackSize: Int) = + last.processLastAction.keys.all { process -> + last.lastDependents.containsKey(process) && last.lastDependents[process]!!.all { (_, index) -> + index >= realStackSize + } } - } } /** @@ -453,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 } } } @@ -471,8 +473,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 da6dec34eb..e0c908663e 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 @@ -48,6 +48,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 @@ -76,6 +77,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 @@ -164,13 +168,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) @@ -187,7 +192,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 b3db63ef51..c0f7c69d35 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 @@ -94,7 +94,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 65e5496ee5..077a589ad1 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 fd3b3d68f9..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 @@ -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..9613ba5b98 --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt @@ -0,0 +1,237 @@ +/* + * 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 +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 65370c72e6..ab2faf0fe3 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() + } +}