From c6860e6df916a0f282710bd936d6bcf13504b759 Mon Sep 17 00:00:00 2001 From: s0mark Date: Mon, 20 Nov 2023 22:25:46 +0100 Subject: [PATCH] formatting stack abstraction files --- .../algorithm/cegar/BasicAbstractor.java | 2 +- .../refinement/SingleExprTraceRefiner.java | 10 +++++----- .../hu/bme/mit/theta/xcfa/analysis/Utils.kt | 14 +++++++++---- .../mit/theta/xcfa/analysis/XcfaAbstractor.kt | 8 +++++--- .../mit/theta/xcfa/analysis/XcfaAnalysis.kt | 20 ++++++++++--------- .../analysis/XcfaSingeExprTraceRefiner.kt | 19 ++++++++++-------- 6 files changed, 43 insertions(+), 30 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java index 43bf8d074c..f731a7cd70 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java @@ -50,7 +50,7 @@ public class BasicAbstractor protected final Logger logger; protected BasicAbstractor(final ArgBuilder argBuilder, final Function projection, - final Waitlist> waitlist, final StopCriterion stopCriterion, final Logger logger) { + final Waitlist> waitlist, final StopCriterion stopCriterion, final Logger logger) { this.argBuilder = checkNotNull(argBuilder); this.projection = checkNotNull(projection); this.waitlist = checkNotNull(waitlist); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java index d1b406ff1e..8594753d9f 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java @@ -45,8 +45,8 @@ public class SingleExprTraceRefiner exprTraceChecker, - final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger) { + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, final Logger logger) { this.exprTraceChecker = checkNotNull(exprTraceChecker); this.precRefiner = checkNotNull(precRefiner); this.pruneStrategy = checkNotNull(pruneStrategy); @@ -55,9 +55,9 @@ protected SingleExprTraceRefiner(final ExprTraceChecker exprTraceChecker, } protected SingleExprTraceRefiner(final ExprTraceChecker exprTraceChecker, - final PrecRefiner precRefiner, - final PruneStrategy pruneStrategy, final Logger logger, - final NodePruner nodePruner) { + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, final Logger logger, + final NodePruner nodePruner) { this.exprTraceChecker = checkNotNull(exprTraceChecker); this.precRefiner = checkNotNull(precRefiner); this.pruneStrategy = checkNotNull(pruneStrategy); diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt index ffdfce0922..cf112f301d 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt @@ -44,11 +44,13 @@ internal fun XcfaState.withGeneralizedVars(): S { return when (sGlobal) { is ExplState -> ExplState.of(sGlobal.getVal().changeVars(varLookup)) is PredState -> PredState.of(sGlobal.preds.map { p -> p.changeVars(varLookup) }) - else -> throw NotImplementedError("Generalizing variable instances is not implemented for data states that are not explicit or predicate.") + else -> throw NotImplementedError( + "Generalizing variable instances is not implemented for data states that are not explicit or predicate.") } as S } class LazyDelegate(val getProperty: T.() -> P) { + private var calculated = false private lateinit var property: P @@ -62,7 +64,11 @@ class LazyDelegate(val getProperty: T.() -> P) { } val XCFA.isInlined: Boolean by LazyDelegate { - !this.procedures.any { p -> p.edges.any { e -> e.getFlatLabels().any { l -> - l is InvokeLabel && this.procedures.any { it.name == l.name } - } } } + !this.procedures.any { p -> + p.edges.any { e -> + e.getFlatLabels().any { l -> + l is InvokeLabel && this.procedures.any { it.name == l.name } + } + } + } } \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt index 72ce3a9026..3d0f25823b 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAbstractor.kt @@ -90,7 +90,6 @@ class XcfaAbstractor( waitlist.clear() // Optimization - return if (arg.isSafe) { Preconditions.checkState(arg.isComplete, "Returning incomplete ARG as safe") AbstractorResult.safe() @@ -120,14 +119,17 @@ class XcfaAbstractor( } } - companion object{ - fun builder(argBuilder: ArgBuilder): BasicAbstractor.Builder { + companion object { + + fun builder( + argBuilder: ArgBuilder): BasicAbstractor.Builder { return Builder(argBuilder) } } class Builder(argBuilder: ArgBuilder) : BasicAbstractor.Builder(argBuilder) { + override fun build(): BasicAbstractor { return XcfaAbstractor(argBuilder, projection, waitlist, stopCriterion, logger) } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt index b8e04eb29a..a662316543 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt @@ -169,10 +169,11 @@ fun getXcfaErrorPredicate( fun getPartialOrder(partialOrd: PartialOrd) = PartialOrd> { s1, s2 -> - s1.processes == s2.processes && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes && partialOrd.isLeq(s1.sGlobal, s2.sGlobal) + s1.processes == s2.processes && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes && partialOrd.isLeq( + s1.sGlobal, s2.sGlobal) } -private fun stackIsLeq(s1: XcfaState, s2: XcfaState) = s2.processes.keys.all { pid -> +private fun stackIsLeq(s1: XcfaState, s2: XcfaState) = s2.processes.keys.all { pid -> s1.processes[pid]?.let { ps1 -> val ps2 = s2.processes.getValue(pid) ps1.locs.peek() == ps2.locs.peek() && ps1.paramsInitialized && ps2.paramsInitialized @@ -181,7 +182,8 @@ private fun stackIsLeq(s1: XcfaState, s2: XcfaState) = s2.p fun getStackPartialOrder(partialOrd: PartialOrd) = PartialOrd> { s1, s2 -> - s1.processes.size == s2.processes.size && stackIsLeq(s1, s2) && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes + s1.processes.size == s2.processes.size && stackIsLeq(s1, + s2) && s1.bottom == s2.bottom && s1.mutexes == s2.mutexes && partialOrd.isLeq(s1.withGeneralizedVars(), s2.withGeneralizedVars()) } @@ -189,7 +191,7 @@ private fun , P : XcfaPrec> getXcfaArgBui analysis: Analysis, lts: LTS, XcfaAction>, errorDetection: ErrorDetection) - : ArgBuilder = + : ArgBuilder = ArgBuilder.create( lts, analysis, @@ -216,7 +218,7 @@ fun , P : XcfaPrec> getXcfaAbstractor( /// EXPL private fun getExplXcfaInitFunc(xcfa: XCFA, - solver: Solver): (XcfaPrec) -> List> { + solver: Solver): (XcfaPrec) -> List> { val processInitState = xcfa.initProcedures.mapIndexed { i, it -> val initLocStack: LinkedList = LinkedList() initLocStack.add(it.first.initLoc) @@ -230,7 +232,7 @@ private fun getExplXcfaInitFunc(xcfa: XCFA, } private fun getExplXcfaTransFunc(solver: Solver, - maxEnum: Int): (XcfaState, XcfaAction, XcfaPrec) -> List> { + maxEnum: Int): (XcfaState, XcfaAction, XcfaPrec) -> List> { val explTransFunc = ExplStmtTransFunc.create(solver, maxEnum) return { s, a, p -> val (newSt, newAct) = s.apply(a) @@ -241,7 +243,7 @@ private fun getExplXcfaTransFunc(solver: Solver, } class ExplXcfaAnalysis(xcfa: XCFA, solver: Solver, maxEnum: Int, - partialOrd: PartialOrd>) : XcfaAnalysis( + partialOrd: PartialOrd>) : XcfaAnalysis( corePartialOrd = partialOrd, coreInitFunc = getExplXcfaInitFunc(xcfa, solver), coreTransFunc = getExplXcfaTransFunc(solver, maxEnum) @@ -250,7 +252,7 @@ class ExplXcfaAnalysis(xcfa: XCFA, solver: Solver, maxEnum: Int, /// PRED private fun getPredXcfaInitFunc(xcfa: XCFA, - predAbstractor: PredAbstractor): (XcfaPrec) -> List> { + predAbstractor: PredAbstractor): (XcfaPrec) -> List> { val processInitState = xcfa.initProcedures.mapIndexed { i, it -> val initLocStack: LinkedList = LinkedList() initLocStack.add(it.first.initLoc) @@ -275,7 +277,7 @@ private fun getPredXcfaTransFunc( } class PredXcfaAnalysis(xcfa: XCFA, solver: Solver, predAbstractor: PredAbstractor, - partialOrd: PartialOrd>) : XcfaAnalysis( + partialOrd: PartialOrd>) : XcfaAnalysis( corePartialOrd = partialOrd, coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor), coreTransFunc = getPredXcfaTransFunc(predAbstractor) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt index ac696bc1f0..432e88a0e9 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingeExprTraceRefiner.kt @@ -29,6 +29,7 @@ import java.util.LinkedList class XcfaSingleExprTraceRefiner : SingleExprTraceRefiner { + private constructor( exprTraceChecker: ExprTraceChecker, precRefiner: PrecRefiner, @@ -47,14 +48,15 @@ class XcfaSingleExprTraceRefiner): Pair>? { trace.states.forEachIndexed { i, s -> val state = s as XcfaState - state.processes.entries.find { (_, processState) -> processState.popped != null }?.let { (pid, processState) -> - val stackBeforePop = LinkedList(processState.locs) - stackBeforePop.push(processState.popped) - val processesBeforePop = state.processes.toMutableMap() - processesBeforePop[pid] = processState.copy(locs = stackBeforePop) - val stateBeforePop = state.copy(processes = processesBeforePop) - return Pair(i, stateBeforePop) - } + state.processes.entries.find { (_, processState) -> processState.popped != null } + ?.let { (pid, processState) -> + val stackBeforePop = LinkedList(processState.locs) + stackBeforePop.push(processState.popped) + val processesBeforePop = state.processes.toMutableMap() + processesBeforePop[pid] = processState.copy(locs = stackBeforePop) + val stateBeforePop = state.copy(processes = processesBeforePop) + return Pair(i, stateBeforePop) + } } return null } @@ -94,6 +96,7 @@ class XcfaSingleExprTraceRefiner create( exprTraceChecker: ExprTraceChecker, precRefiner: PrecRefiner, pruneStrategy: PruneStrategy, logger: Logger