Merge pull request #202 from csanadtelbisz/por/dpor

Constant variable substitution, loop unroll pass + dpor code cleanup

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<ExplState> {

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;
 

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/stmtoptimizer/StmtSimplifier.java → 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;

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/utils/StmtSimplifierTest.java → 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;

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<S, A> {
 
     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<S, A> {
          * Partial order of states considering sleep sets (unexplored behavior).
          */
         fun <E : ExprState> getPartialOrder(partialOrd: PartialOrd<E>) = PartialOrd<E> { 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<S, A> {
             // 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<S, A> {
                 // 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<S, A> {
             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<S, A> {
 
                 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<S, A> {
                         }
 
                         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<S, A> {
             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<S, A> {
             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<S, A> {
 
                 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,21 +402,21 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS<S, A> {
          */
         private fun max(map1: Map<Int, Int>, map2: Map<Int, Int>) =
             (map1.keys union map2.keys).associateWith { key ->
-                max(map1[key] ?: -1, map2[key] ?: -1)
+                max(
+                    map1[key] ?: -1, map2[key] ?: -1
+                )
             }.toMutableMap()
 
         /**
          * See the article for the definition of notdep.
          */
         private fun notdep(start: Int, action: A): List<A> {
             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<S, A> {
         /**
          * 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<S, A> {
         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 <P : Prec> getEnabledActionsFor(state: S, exploredActions: Collection<A>,
-        prec: P): Set<A> {
+    override fun <P : Prec> getEnabledActionsFor(state: S, exploredActions: Collection<A>, prec: P): Set<A> {
         this.prec = prec
         return getEnabledActionsFor(state)
     }

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<String>) {
         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<String>) {
         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<String>) {
         // 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))

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"))
 }

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt

@@ -94,7 +94,7 @@ private fun List<VarAccessMap>.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)

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<Expr<*>>) {
-        procedures.add(toAdd)
+        addProcedure(toAdd)
         initProcedures.add(Pair(toAdd, params))
     }
 }

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)
         }
     }
 }