Skip to content

Commit

Permalink
sync fixes + toStrings
Browse files Browse the repository at this point in the history
  • Loading branch information
@szdan97
szdan97 committed Dec 2, 2024
1 parent 6ad63b3 commit 1bf5fdd
Show file tree
Hide file tree
Showing 6 changed files with 210 additions and 78 deletions.
2 changes: 2 additions & 0 deletions subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAction.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,8 @@ constructor(
get() = stmts

override fun toString(): String {
// TODO: change back
return "$pid: $source -> $target"
return "$pid: $source -> $target [${getStmts()}]"
}

Expand Down
5 changes: 3 additions & 2 deletions subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,7 @@ fun getCoreXcfaLts() =
.toSet()
.filter { action ->
s.syncingOn?.let { key ->
action.label.getFlatLabels().first().let { it is SyncRecvLabel && it.key == key }
action.label.getFlatLabels().firstOrNull()?.let { it is SyncRecvLabel && it.key == key } ?: false
} ?: true
}
}
Expand Down Expand Up @@ -262,7 +262,8 @@ fun <S : ExprState> getPartialOrder(partialOrd: PartialOrd<PtrState<S>>) =
s1.processes == s2.processes &&
s1.bottom == s2.bottom &&
s1.mutexes == s2.mutexes &&
partialOrd.isLeq(s1.sGlobal, s2.sGlobal)
partialOrd.isLeq(s1.sGlobal, s2.sGlobal) &&
s1.syncingOn == s2.syncingOn
}

private fun <S : ExprState> stackIsLeq(s1: XcfaState<PtrState<S>>, s2: XcfaState<PtrState<S>>) =
Expand Down
2 changes: 2 additions & 0 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 @@ -320,6 +320,8 @@ constructor(
}

override fun toString(): String {
// TODO: change back
return "${processes.toString().replace(",", ",\\n")} \\n{$sGlobal, ${if (bottom) ", bottom" else ""}}\\n $syncingOn"
return "$processes {$sGlobal, mutex=$mutexes${if (bottom) ", bottom" else ""}}"
}
}
Expand Down
241 changes: 174 additions & 67 deletions subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/ThyssenXcfaDslTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,12 @@
*/
package hu.bme.mit.theta.xcfa.cli

import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder
import hu.bme.mit.theta.analysis.algorithm.cegar.BasicArgAbstractor
import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker
import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy.FULL
import hu.bme.mit.theta.common.logging.ConsoleLogger
import hu.bme.mit.theta.common.logging.Logger
import hu.bme.mit.theta.core.decl.VarDecl
import hu.bme.mit.theta.core.stmt.AssumeStmt
import hu.bme.mit.theta.core.stmt.Stmts
Expand All @@ -30,13 +36,32 @@ import hu.bme.mit.theta.core.type.booltype.BoolType
import hu.bme.mit.theta.core.type.inttype.IntExprs
import hu.bme.mit.theta.core.type.inttype.IntExprs.*
import hu.bme.mit.theta.core.type.inttype.IntType
import hu.bme.mit.theta.frontend.ParseContext
import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.ArithmeticType.efficient
import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM
import hu.bme.mit.theta.xcfa.AssignStmtLabel
import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
import hu.bme.mit.theta.xcfa.analysis.XcfaAnalysis
import hu.bme.mit.theta.xcfa.analysis.getCoreXcfaLts
import hu.bme.mit.theta.xcfa.cli.params.*
import hu.bme.mit.theta.xcfa.cli.params.Backend.CEGAR
import hu.bme.mit.theta.xcfa.cli.params.CexMonitorOptions.CHECK
import hu.bme.mit.theta.xcfa.cli.params.CexMonitorOptions.DISABLE
import hu.bme.mit.theta.xcfa.cli.params.ConeOfInfluenceMode.NO_COI
import hu.bme.mit.theta.xcfa.cli.params.Domain.EXPL
import hu.bme.mit.theta.xcfa.cli.params.ExprSplitterOptions.WHOLE
import hu.bme.mit.theta.xcfa.cli.params.InitPrec.ALLVARS
import hu.bme.mit.theta.xcfa.cli.params.InitPrec.EMPTY
import hu.bme.mit.theta.xcfa.cli.params.POR.NOPOR
import hu.bme.mit.theta.xcfa.cli.params.Refinement.SEQ_ITP
import hu.bme.mit.theta.xcfa.cli.params.Search.DFS
import hu.bme.mit.theta.xcfa.cli.params.Search.ERR
import hu.bme.mit.theta.xcfa.model.ParamDirection.*
import hu.bme.mit.theta.xcfa.model.global
import hu.bme.mit.theta.xcfa.model.*
import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager
import hu.bme.mit.theta.xcfa.passes.UnusedLocRemovalPass
import hu.bme.mit.theta.xcfa.passes.*
import org.junit.Test
import java.io.File

class ThyssenXcfaDslTest {

Expand Down Expand Up @@ -111,13 +136,13 @@ class ThyssenXcfaDslTest {
val schedulerProc = procedure("GlobalScheduler") {
(init to "Stable") { nop() }

("Stable" to "L1") { sendChan(runDiag, runDiagAck, listOf()) }
("Stable" to "L1") { syncSend(runDiag) }

("L1" to "L2a") { sendChan(runA, runAAck, listOf()) }
("L1" to "L2b") { sendChan(runB, runBAck, listOf()) }
("L1" to "L2a") { syncSend(runA) }
("L1" to "L2b") { syncSend(runB) }

("L2a" to "L3a") { sendChan(runB, runBAck, listOf()) }
("L2b" to "L3b") { sendChan(runA, runAAck, listOf()) }
("L2a" to "L3a") { syncSend(runB) }
("L2b" to "L3b") { syncSend(runA) }

("L3a" to "Stable") { nop() }
("L3b" to "Stable") { nop() }
Expand All @@ -139,88 +164,104 @@ class ThyssenXcfaDslTest {
"(or (not newPermanentCommA) (not newPermanentCommB)))"

("L0" to "L0") {
receiveChan(runDiag, runDiagAck, listOf(
havoc(newFailureA),
havoc(newFailureB),
assume(Not(And(newFailureA.ref, newFailureB.ref))),
okA assign And(okA.ref, Not(newFailureA.ref)),
okB assign And(okB.ref, Not(newFailureB.ref)),

havoc(newTransientCommA),
havoc(newTransientCommB),
havoc(newPermanentCommA),
havoc(newPermanentCommB),
assume(commFailureAssumptions),
AtoBCommPermFailed assign newPermanentCommA.ref,
BtoACommPermFailed assign newPermanentCommB.ref,
AtoBCommOk assign And(Not(AtoBCommPermFailed.ref), Not(newTransientCommA.ref)),
BtoACommOk assign And(Not(BtoACommPermFailed.ref), Not(newTransientCommB.ref)),

okAforB assign Ite<BoolType>(AtoBCommOk.ref, okA.ref, okAforB.ref),
okBforA assign Ite<BoolType>(BtoACommOk.ref, okB.ref, okBforA.ref)
)
)
syncRecv(runDiag)
havoc(newFailureA)
havoc(newFailureB)
assume(Not(And(newFailureA.ref, newFailureB.ref)))
okA assign And(okA.ref, Not(newFailureA.ref))
okB assign And(okB.ref, Not(newFailureB.ref))

havoc(newTransientCommA)
havoc(newTransientCommB)
havoc(newPermanentCommA)
havoc(newPermanentCommB)
assume(commFailureAssumptions)
AtoBCommPermFailed assign newPermanentCommA.ref
BtoACommPermFailed assign newPermanentCommB.ref
AtoBCommOk assign And(Not(AtoBCommPermFailed.ref), Not(newTransientCommA.ref))
BtoACommOk assign And(Not(BtoACommPermFailed.ref), Not(newTransientCommB.ref))

okAforB assign Ite<BoolType>(AtoBCommOk.ref, okA.ref, okAforB.ref)
okBforA assign Ite<BoolType>(BtoACommOk.ref, okB.ref, okBforA.ref)
}
}
val RWA_A = procedure("RWA_A") {
(init to "Master") { nop() }
("Master" to "Master") { receiveChan(runA, runAAck, listOf(
("Master" to "Master") {
syncRecv(runA)
assume("okA and okBforA")
)) }
("Master" to "Standalone") { receiveChan(runA, runAAck, listOf(
}
("Master" to "Standalone") {
syncRecv(runA)
assume("okA and not okBforA")
)) }
("Standalone" to "Standalone") { receiveChan(runA, runAAck, listOf(
}
("Standalone" to "Standalone") {
syncRecv(runA)
assume("okA")
)) }
("Standalone" to "Error") { receiveChan(runA, runAAck, listOf(
}
("Standalone" to "Error") {
syncRecv(runA)
assume("(not okA)")
)) }
("Error" to "Error") { receiveChan(runA, runAAck, listOf(
}
("Error" to "Error") {
syncRecv(runA)
nop()
)) }
("Master" to "Passive") { receiveChan(runA, runAAck, listOf(
}
("Master" to "Passive") {
syncRecv(runA)
assume("(and (not okA) okBforA)")
)) }
("Master" to "Error") { receiveChan(runA, runAAck, listOf(
}
("Master" to "Error") {
syncRecv(runA)
assume("(and (not okA) (not okBforA))")
)) }
("Passive" to "Error") { receiveChan(runA, runAAck, listOf(
}
("Passive" to "Error") {
syncRecv(runA)
assume("(not okBforA)")
)) }
("Passive" to "Passive") { receiveChan(runA, runAAck, listOf(
}
("Passive" to "Passive") {
syncRecv(runA)
assume("okBforA")
)) }
}
}
val RWA_B = procedure("RWA_A") {
val RWA_B = procedure("RWA_B") {
(init to "Silent") { nop() }
("Silent" to "Silent") { receiveChan(runA, runAAck, listOf(
("Silent" to "Silent") {
syncRecv(runB)
assume("(and okB okAforB)")
)) }
("Silent" to "Standalone") { receiveChan(runA, runAAck, listOf(
}
("Silent" to "Standalone") {
syncRecv(runB)
assume("(and okB (not okAforB))")
)) }
("Standalone" to "Standalone") { receiveChan(runA, runAAck, listOf(
}
("Standalone" to "Standalone") {
syncRecv(runB)
assume("okB")
)) }
("Standalone" to "Error") { receiveChan(runA, runAAck, listOf(
}
("Standalone" to "Error") {
syncRecv(runB)
assume("(not okB)")
)) }
("Error" to "Error") { receiveChan(runA, runAAck, listOf(
}
("Error" to "Error") {
syncRecv(runB)
nop()
)) }
("Silent" to "Passive") { receiveChan(runA, runAAck, listOf(
}
("Silent" to "Passive") {
syncRecv(runB)
assume("(and (not okB) okAforB)")
)) }
("Silent" to "Error") { receiveChan(runA, runAAck, listOf(
}
("Silent" to "Error") {
syncRecv(runB)
assume("(and (not okB) (not okAforB))")
)) }
("Passive" to "Error") { receiveChan(runA, runAAck, listOf(
}
("Passive" to "Error") {
syncRecv(runB)
assume("(not okAforB)")
)) }
("Passive" to "Passive") { receiveChan(runA, runAAck, listOf(
}
("Passive" to "Passive") {
syncRecv(runB)
assume("okAforB")
)) }
}
}

val main = procedure("main") {
Expand All @@ -247,8 +288,74 @@ class ThyssenXcfaDslTest {

@Test
fun defineXcfa() {
val xcfa = getXcfa()
println(xcfa.toDot())
LbePass.level = LbePass.LbeLevel.LBE_LOCAL
val origXcfa = getXcfa()
val passedXcfa = origXcfa.optimizeFurther(
ProcedurePassManager(
listOf(
NormalizePass(),
DeterministicPass(),
EliminateSelfLoops(),
SBEPass(),
LbePass(ParseContext())
)
)
)
println(origXcfa.toDot())

val inputConfig = InputConfig(
xcfaWCtx = Triple(origXcfa, listOf(), ParseContext()),
property = ErrorDetection.NO_ERROR
)
val frontendConfig = FrontendConfig(
lbeLevel = LbePass.level,
loopUnroll = LoopUnrollPass.UNROLL_LIMIT,
inputType = InputType.C,
specConfig = CFrontendConfig(arithmetic = efficient),
)
val backendConfig = BackendConfig(
backend = CEGAR,
timeoutMs = 0,
specConfig =
CegarConfig(
initPrec = ALLVARS,
porLevel = NOPOR,
porRandomSeed = -1,
coi = NO_COI,
cexMonitor = DISABLE,
abstractorConfig =
CegarAbstractorConfig(
abstractionSolver = "Z3",
validateAbstractionSolver = false,
domain = EXPL,
maxEnum = 1,
search = DFS,
),
refinerConfig = CegarRefinerConfig(
refinementSolver = "Z3",
validateRefinementSolver = false,
refinement = SEQ_ITP,
exprSplitter = WHOLE,
pruneStrategy = FULL,
),
),
)
val outputConfig = OutputConfig(
enableOutput = true,
resultFolder = File("F:\\egyetem\\thesta\\theta\\subprojects\\xcfa\\xcfa\\src\\test\\temp")
)
runConfig(
XcfaConfig(
inputConfig,
frontendConfig,
backendConfig,
outputConfig,
DebugConfig()
),
ConsoleLogger(Logger.Level.SUBSTEP),
ConsoleLogger(Logger.Level.SUBSTEP),
true
)
}

}
24 changes: 17 additions & 7 deletions subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Dsl.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs
import hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool
import hu.bme.mit.theta.core.type.booltype.BoolLitExpr
import hu.bme.mit.theta.core.type.booltype.BoolType
import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs
import hu.bme.mit.theta.core.type.inttype.IntExprs
import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
import hu.bme.mit.theta.core.type.inttype.IntLitExpr
Expand Down Expand Up @@ -182,6 +183,18 @@ class XcfaProcedureBuilderContext(val builder: XcfaProcedureBuilder) {
return SequenceLabel(labelList)
}

fun syncSend(channel: VarDecl<*>): SequenceLabel {
val label = SyncSendLabel(channel)
labelList.add(label)
return SequenceLabel(labelList)
}

fun syncRecv(channel: VarDecl<*>): SequenceLabel {
val label = SyncRecvLabel(channel)
labelList.add(label)
return SequenceLabel(labelList)
}

fun havoc(value: String): SequenceLabel {
val varDecl = this@XcfaProcedureBuilderContext.builder.lookup(value)
val label = StmtLabel(Havoc(varDecl))
Expand Down Expand Up @@ -314,13 +327,10 @@ class XcfaProcedureBuilderContext(val builder: XcfaProcedureBuilder) {
}

infix fun String.to(to: String): (lambda: SequenceLabelContext.() -> SequenceLabel) -> XcfaEdge {
val startName = this@XcfaProcedureBuilderContext.builder.name + this
val to = this@XcfaProcedureBuilderContext.builder.name + to
val loc1 = locationLut.getOrElse(startName) { XcfaLocation(this, metadata = EmptyMetaData) }
locationLut.putIfAbsent(startName, loc1)
val startName = this
val loc1 = locationLut.getOrPut(startName) { XcfaLocation( this@XcfaProcedureBuilderContext.builder.name+"_"+this, metadata = EmptyMetaData) }
builder.addLoc(loc1)
val loc2 = locationLut.getOrElse(to) { XcfaLocation(to, metadata = EmptyMetaData) }
locationLut.putIfAbsent(to, loc2)
val loc2 = locationLut.getOrPut(to) { XcfaLocation(this@XcfaProcedureBuilderContext.builder.name+"_"+to, metadata = EmptyMetaData) }
builder.addLoc(loc2)
return { lambda ->
val edge = XcfaEdge(loc1, loc2, lambda(SequenceLabelContext()), EmptyMetaData)
Expand Down Expand Up @@ -357,4 +367,4 @@ fun XcfaBuilder.procedure(
lambda: XcfaProcedureBuilderContext.() -> Unit,
): XcfaProcedureBuilderContext {
return procedure(name, ProcedurePassManager(), lambda)
}
}
Loading

0 comments on commit 1bf5fdd

Please sign in to comment.