Skip to content

Commit

Permalink
Fixed problem with PIDs
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Jul 21, 2023
1 parent bf54d4d commit 4703e57
Show file tree
Hide file tree
Showing 4 changed files with 21 additions and 147 deletions.
6 changes: 3 additions & 3 deletions subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,9 @@ import hu.bme.mit.theta.xcfa.model.*
import hu.bme.mit.theta.xcfa.passes.changeVars
import java.util.*

private var pidCnt = 1
private var procCnt = 1

data class XcfaState<S : ExprState> @JvmOverloads constructor(
val xcfa: XCFA?,
val processes: Map<Int, XcfaProcessState>,
Expand All @@ -38,7 +41,6 @@ data class XcfaState<S : ExprState> @JvmOverloads constructor(
val bottom: Boolean = false,
) : ExprState {

private var pidCnt = 1

override fun isBottom(): Boolean {
return bottom || sGlobal.isBottom
Expand Down Expand Up @@ -234,8 +236,6 @@ data class XcfaProcessState(
val prefix: String = ""
) {

private var procCnt = 1

fun withNewLoc(l: XcfaLocation): XcfaProcessState {
val deque: LinkedList<XcfaLocation> = LinkedList(locs)
deque.pop()
Expand Down
3 changes: 1 addition & 2 deletions ...jects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysisTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ class XcfaAnalysisTest {
arrayOf("/01function.c", SafetyResult<*, *>::isUnsafe),
arrayOf("/02functionparam.c", SafetyResult<*, *>::isSafe),
arrayOf("/03nondetfunction.c", SafetyResult<*, *>::isUnsafe),
arrayOf("/04multithread.c", SafetyResult<*, *>::isSafe),
arrayOf("/04multithread.c", SafetyResult<*, *>::isUnsafe),
)
}
}
Expand Down Expand Up @@ -143,7 +143,6 @@ class XcfaAnalysisTest {
@ParameterizedTest
@MethodSource("data")
fun testDporExpl(filepath: String, verdict: (SafetyResult<*, *>) -> Boolean) {
if (filepath.contains("multithread")) return // TODO: why does it fail to verify?
val stream = javaClass.getResourceAsStream(filepath)
val xcfa = getXcfaFromC(stream!!, ParseContext(), false)

Expand Down
130 changes: 0 additions & 130 deletions subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaCegarTest.kt
View file

This file was deleted.

29 changes: 17 additions & 12 deletions ...jects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaStateLtsTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ class XcfaStateLtsTest {

@Test
fun testApply() {
val actionOrder: MutableList<XcfaAction> = ArrayList()
val actionOrder: MutableList<(XcfaState<ExplState>) -> XcfaAction> = ArrayList()
val expectations: MutableList<Predicate<XcfaState<ExplState>>> = ArrayList()
val lts = getXcfaLts()
lateinit var initState: XcfaState<ExplState>
Expand Down Expand Up @@ -78,59 +78,61 @@ class XcfaStateLtsTest {
val sporLts = XcfaSporLts(xcfa)
val aasporLts = XcfaAasporLts(xcfa, LinkedHashMap())

actionOrder.add(XcfaAction(0, edges[1]))
actionOrder.add { XcfaAction(0, edges[1]) }
expectations.add {
it.processes[0]!!.locs.size == 2 && it.processes[0]!!.locs.peek() == edges[0].source &&
lts.getEnabledActionsFor(it).size == 1 &&
sporLts.getEnabledActionsFor(it).size == 1 &&
aasporLts.getEnabledActionsFor(it, emptyList(), ExplPrec.empty()).size == 1
}

actionOrder.add(XcfaAction(0, edges[0]))
actionOrder.add { XcfaAction(0, edges[0]) }
expectations.add {
it.processes[0]!!.locs.size == 2 && it.processes[0]!!.locs.peek() == edges[0].target &&
lts.getEnabledActionsFor(it).size == 1 &&
sporLts.getEnabledActionsFor(it).size == 1 &&
aasporLts.getEnabledActionsFor(it, emptyList(), ExplPrec.empty()).size == 1
}

actionOrder.add(XcfaAction(0, XcfaEdge(edges[0].target, edges[0].target, ReturnLabel(NopLabel))))
actionOrder.add { XcfaAction(0, XcfaEdge(edges[0].target, edges[0].target, ReturnLabel(NopLabel))) }
expectations.add {
it.processes[0]!!.locs.size == 1 && it.processes[0]!!.locs.peek() == edges[1].target &&
lts.getEnabledActionsFor(it).size == 1 &&
sporLts.getEnabledActionsFor(it).size == 1 &&
aasporLts.getEnabledActionsFor(it, emptyList(), ExplPrec.empty()).size == 1
}

actionOrder.add(XcfaAction(0, edges[2]))
actionOrder.add { XcfaAction(0, edges[2]) }
expectations.add {
it.processes.size == 2 &&
it.processes[0]!!.locs.size == 1 && it.processes[0]!!.locs.peek() == edges[2].target &&
it.processes[1]!!.locs.size == 1 && it.processes[1]!!.locs.peek() == edges[0].source &&
it.processes[it.foreignKey()!!]!!.locs.size == 1 && it.processes[it.foreignKey()!!]!!.locs.peek() == edges[0].source &&
lts.getEnabledActionsFor(it).size == 2 &&
sporLts.getEnabledActionsFor(it).size == 1 &&
aasporLts.getEnabledActionsFor(it, emptyList(), ExplPrec.empty()).size == 1
}

actionOrder.add(XcfaAction(1, edges[0]))
actionOrder.add { s -> XcfaAction(s.foreignKey()!!, edges[0]) }
expectations.add {
it.processes.size == 2 &&
it.processes[0]!!.locs.size == 1 && it.processes[0]!!.locs.peek() == edges[2].target &&
it.processes[1]!!.locs.size == 1 && it.processes[1]!!.locs.peek() == edges[0].target &&
it.processes[it.foreignKey()!!]!!.locs.size == 1 && it.processes[it.foreignKey()!!]!!.locs.peek() == edges[0].target &&
lts.getEnabledActionsFor(it).size == 2 &&
sporLts.getEnabledActionsFor(it).size == 1 &&
aasporLts.getEnabledActionsFor(it, emptyList(), ExplPrec.empty()).size == 1
}

actionOrder.add(XcfaAction(1, XcfaEdge(edges[0].target, edges[0].target, ReturnLabel(NopLabel))))
actionOrder.add { s ->
XcfaAction(s.foreignKey()!!, XcfaEdge(edges[0].target, edges[0].target, ReturnLabel(NopLabel)))
}
expectations.add {
it.processes.size == 1 && it.processes[0]!!.locs.size == 1 && it.processes[0]!!.locs.peek() == edges[2].target &&
lts.getEnabledActionsFor(it).size == 1 &&
sporLts.getEnabledActionsFor(it).size == 1 &&
aasporLts.getEnabledActionsFor(it, emptyList(), ExplPrec.empty()).size == 1
}

actionOrder.add(XcfaAction(0, edges[3]))
actionOrder.add { XcfaAction(0, edges[3]) }
expectations.add {
it.processes[0]!!.locs.size == 1 && it.processes[0]!!.locs.peek() == edges[3].target &&
lts.getEnabledActionsFor(it).size == 1 &&
Expand All @@ -141,10 +143,13 @@ class XcfaStateLtsTest {
var state = initState
for ((index, xcfaAction) in actionOrder.withIndex()) {
println("Test $index: $xcfaAction")
val newState = state.apply(xcfaAction)
val newState = state.apply(xcfaAction(state))
assertTrue(expectations[index].test(newState.first))
state = newState.first
println("Test $index OK")
}
}
}
}

private fun XcfaState<*>.foreignKey(): Int? =
processes.keys.firstOrNull { key -> key != 0 }

0 comments on commit 4703e57

Please sign in to comment.