copyright + code formatting

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() {

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,7 +93,10 @@ 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)
         }
     }
 
@@ -161,7 +165,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,12 +193,15 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS<S, A> {
                 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<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
@@ -266,7 +276,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS<S, A> {
                         }
 
                         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<S, A> {
             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<S, A> {
                 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<S, A> {
          * 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<Int, Int>, map2: Map<Int, Int>) =
-            (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<S, 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)
+                    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<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) && 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
+                }
             }
-        }
     }
 
     /**

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

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