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