Skip to content

Commit

Permalink
code formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
@csanadtelbisz
csanadtelbisz committed Sep 1, 2023
1 parent 996494a commit 2c863d7
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 34 deletions.
33 changes: 13 additions & 20 deletions ...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,8 +94,7 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS<S, A> {
*/
fun <E : ExprState> getPartialOrder(partialOrd: PartialOrd<E>) = PartialOrd<E> { s1, s2 ->
partialOrd.isLeq(
s1,
s2
s1, s2
) && s2.reExplored == true && s1.sleep.containsAll(s2.sleep - s2.explored)
}
}
Expand Down Expand Up @@ -192,16 +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()
Expand Down Expand Up @@ -404,8 +403,7 @@ 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
map1[key] ?: -1, map2[key] ?: -1
)
}.toMutableMap()

Expand All @@ -414,15 +412,11 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS<S, A> {
*/
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 ->
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) }
}

/**
Expand Down Expand Up @@ -462,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 }
}
}

Expand Down
4 changes: 2 additions & 2 deletions subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

Expand Down Expand Up @@ -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)
}
}
}
16 changes: 4 additions & 12 deletions subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,14 +48,7 @@ class LoopUnrollPass : ProcedurePass {
private val testedLoops = mutableSetOf<Loop>()

private data class Loop(
val loopVar: VarDecl<*>,
val loopVarModifiers: List<XcfaEdge>,
val loopVarInit: XcfaEdge,
val loopCondEdge: XcfaEdge,
val exitCondEdge: XcfaEdge,
val loopStart: XcfaLocation,
val loopLocs: List<XcfaLocation>,
val loopEdges: List<XcfaEdge>
val loopVar: VarDecl<*>, val loopVarModifiers: List<XcfaEdge>, val loopVarInit: XcfaEdge, val loopCondEdge: XcfaEdge, val exitCondEdge: XcfaEdge, val loopStart: XcfaLocation, val loopLocs: List<XcfaLocation>, val loopEdges: List<XcfaEdge>
) {
private class BasicStmtAction(private val stmt: Stmt) : StmtAction() {
constructor(edge: XcfaEdge) : this(edge.label.toStmt())
Expand All @@ -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
Expand Down

0 comments on commit 2c863d7

Please sign in to comment.