Skip to content

Commit

Permalink
Fixed bugs from Sonar
Browse files Browse the repository at this point in the history
  • Loading branch information
leventeBajczi committed Jul 23, 2023
1 parent e2be852 commit 48308e9
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 14 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ class FiniteStateChecker<S : ExplState, A : StmtAction, T>(
initStates.forEach { lastIds[it] = initId }
while (initStates.isNotEmpty()) {
val state = initStates.pop()
val lastId = lastIds[state]!!
val lastId = checkNotNull(lastIds[state])
val actions = actionFunc.getEnabledActionsFor(state)

val nextStates = actions.map { a ->
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,7 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
val opCompiled = pattern.op.accept(this)
return events.map { a ->
events.map { b ->
Pair(Tuple2.of(a, b), if (a == b) True() else opCompiled[Tuple2.of(a, b)]!!)
Pair(Tuple2.of(a, b), if (a == b) True() else checkNotNull(opCompiled[Tuple2.of(a, b)]))
}
}.flatten().toMap()
}
Expand All @@ -181,7 +181,8 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp

override fun compile(pattern: Inverse): Map<Tuple, Expr<BoolType>> {
val opCompiled = pattern.op.accept(this)
return events.map { a -> events.map { b -> Pair(Tuple2.of(a, b), opCompiled[Tuple2.of(b, a)]!!) } }.flatten()
return events.map { a -> events.map { b -> Pair(Tuple2.of(a, b), checkNotNull(opCompiled[Tuple2.of(b, a)])) } }
.flatten()
.toMap()
}

Expand Down Expand Up @@ -213,16 +214,16 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
events.map { b ->
Iff(Or(opCompiled[Tuple2.of(a, b)], Or(events.map { c ->
Or(
And(opCompiled[Tuple2.of(a, c)], consts[Tuple2.of(c, b)]!!.ref),
And(consts[Tuple2.of(a, c)]!!.ref, opCompiled[Tuple2.of(c, b)])
And(opCompiled[Tuple2.of(a, c)], checkNotNull(consts[Tuple2.of(c, b)]).ref),
And(checkNotNull(consts[Tuple2.of(a, c)]).ref, opCompiled[Tuple2.of(c, b)])
)
})), consts[Tuple2.of(a, b)]!!.ref)
})), checkNotNull(consts[Tuple2.of(a, b)]).ref)
}
}.flatten())
transitiveConstraints.add(constraints)
val ret = events.map { a ->
events.map { b ->
Pair(Tuple2.of(a, b), if (a == b) True() else consts[Tuple2.of(a, b)]!!.ref)
Pair(Tuple2.of(a, b), if (a == b) True() else checkNotNull(consts[Tuple2.of(a, b)]).ref)
}
}
return ret.flatten().toMap()
Expand All @@ -249,7 +250,7 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
val opCompiled = pattern.op.accept(this)
val ret = events.map { a ->
events.map { b ->
Pair(Tuple2.of(a, b), if (a == b) opCompiled[Tuple1.of(a)]!! else False())
Pair(Tuple2.of(a, b), if (a == b) checkNotNull(opCompiled[Tuple1.of(a)]) else False())
}
}
return ret.flatten().toMap()
Expand All @@ -276,14 +277,18 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
events.map { b ->
Iff(Or(opCompiled[Tuple2.of(a, b)], Or(events.filter { c -> a != c && b != c }.map { c ->
Or(
And(opCompiled[Tuple2.of(a, c)], consts[Tuple2.of(c, b)]!!.ref),
And(consts[Tuple2.of(a, c)]!!.ref, opCompiled[Tuple2.of(c, b)])
And(opCompiled[Tuple2.of(a, c)], checkNotNull(consts[Tuple2.of(c, b)]).ref),
And(checkNotNull(consts[Tuple2.of(a, c)]).ref, opCompiled[Tuple2.of(c, b)])
)
})), consts[Tuple2.of(a, b)]!!.ref)
})), checkNotNull(consts[Tuple2.of(a, b)]).ref)
}
}.flatten())
transitiveConstraints.add(constraints)
val ret = events.map { a -> events.map { b -> Pair(Tuple2.of(a, b), consts[Tuple2.of(a, b)]!!.ref) } }
val ret = events.map { a ->
events.map { b ->
Pair(Tuple2.of(a, b), checkNotNull(consts[Tuple2.of(a, b)]).ref)
}
}
return ret.flatten().toMap()
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -241,10 +241,10 @@ private fun getAtomicBlockInnerLocations(initialLocation: XcfaLocation): List<Xc
isAtomic[initialLocation] = false
while (!locationsToVisit.isEmpty()) {
val visiting = locationsToVisit.removeAt(0)
if (isAtomic[visiting]!!) atomicLocations.add(visiting)
if (checkNotNull(isAtomic[visiting])) atomicLocations.add(visiting)
visitedLocations.add(visiting)
for (outEdge in visiting.outgoingEdges) {
var isNextAtomic = isAtomic[visiting]!!
var isNextAtomic = checkNotNull(isAtomic[visiting])
if (outEdge.getFlatLabels().stream().anyMatch { label ->
label is FenceLabel && label.labels.contains("ATOMIC_BEGIN")
}) {
Expand Down

0 comments on commit 48308e9

Please sign in to comment.