From 89b72aa184cc09d26e7caca2566198b21dfac951 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Wed, 13 Nov 2024 14:21:56 +0100 Subject: [PATCH 1/8] xcfa oc checker optimization fix --- build.gradle.kts | 2 +- .../theta/xcfa/analysis/oc/XcfaOcChecker.kt | 18 +++++++++-- .../xcfa/cli/checkers/ConfigToOcChecker.kt | 1 + .../mit/theta/xcfa/cli/portfolio/complex25.kt | 13 +------- .../hu/bme/mit/theta/xcfa/gson/XcfaAdapter.kt | 2 +- .../hu/bme/mit/theta/xcfa/model/Builders.kt | 8 +++-- .../java/hu/bme/mit/theta/xcfa/model/XCFA.kt | 7 +++-- .../theta/xcfa/model/XcfaFurtherOptimizer.kt | 31 +++++++++---------- .../theta/xcfa/passes/ProcedurePassManager.kt | 14 +++++++-- 9 files changed, 56 insertions(+), 40 deletions(-) diff --git a/build.gradle.kts b/build.gradle.kts index 19d6102585..d097203cde 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.8.3" + version = "6.8.4" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt index cd6b33999f..7cbe0ca397 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt @@ -25,6 +25,7 @@ import hu.bme.mit.theta.analysis.algorithm.oc.OcChecker import hu.bme.mit.theta.analysis.algorithm.oc.Relation import hu.bme.mit.theta.analysis.algorithm.oc.RelationType import hu.bme.mit.theta.analysis.unit.UnitPrec +import hu.bme.mit.theta.common.exception.NotSolvableException import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.decl.ConstDecl import hu.bme.mit.theta.core.decl.Decls @@ -50,21 +51,25 @@ import hu.bme.mit.theta.solver.SolverStatus import hu.bme.mit.theta.xcfa.* import hu.bme.mit.theta.xcfa.analysis.XcfaPrec import hu.bme.mit.theta.xcfa.model.* +import hu.bme.mit.theta.xcfa.passes.* import kotlin.time.measureTime private val Expr<*>.vars get() = ExprUtils.getVars(this) class XcfaOcChecker( - private val xcfa: XCFA, + xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, private val logger: Logger, conflictInput: String?, private val outputConflictClauses: Boolean, nonPermissiveValidation: Boolean, private val autoConflictConfig: AutoConflictFinderConfig, + private val acceptUnreliableSafe: Boolean = false, ) : SafetyChecker> { + private val xcfa = xcfa.optimizeFurther(OcExtraPasses()) + private var indexing = VarIndexingFactory.indexing(0) private val localVars = mutableMapOf, MutableMap>>() private val memoryDecl = Decls.Var("__oc_checker_memory_declaration__", Int()) @@ -147,7 +152,16 @@ class XcfaOcChecker( else -> SafetyResult.unknown() } } - .also { logger.writeln(Logger.Level.MAINSTEP, "OC checker result: $it") } + .also { + logger.writeln(Logger.Level.MAINSTEP, "OC checker result: $it") + if (xcfa.unsafeUnrollUsed && !acceptUnreliableSafe) { + logger.writeln( + Logger.Level.MAINSTEP, + "Incomplete loop unroll used: safe result is unreliable.", + ) + throw NotSolvableException() + } + } private inner class ThreadProcessor(private val thread: Thread) { diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt index bef5ea5729..3e88eb043a 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt @@ -42,6 +42,7 @@ fun getOcChecker( ocConfig.outputConflictClauses, ocConfig.nonPermissiveValidation, ocConfig.autoConflict, + config.outputConfig.acceptUnreliableSafe ) return SafetyChecker { ocChecker.check() } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt index 7af6f13ee0..fb13f97b99 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt @@ -124,20 +124,9 @@ fun complexPortfolio25( debugConfig = portfolioConfig.debugConfig, ) - val forceUnrolledXcfa = - xcfa.optimizeFurther( - listOf( - AssumeFalseRemovalPass(), - MutexToVarPass(), - AtomicReadsOneWritePass(), - LoopUnrollPass(2), - ) - ) - val ocConfig = { inProcess: Boolean -> XcfaConfig( - inputConfig = - baseConfig.inputConfig.copy(xcfaWCtx = Triple(forceUnrolledXcfa, mcm, parseContext)), + inputConfig = baseConfig.inputConfig.copy(xcfaWCtx = Triple(xcfa, mcm, parseContext)), frontendConfig = baseConfig.frontendConfig, backendConfig = BackendConfig( diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/XcfaAdapter.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/XcfaAdapter.kt index 39d28e6f41..8c0d48b54b 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/XcfaAdapter.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/XcfaAdapter.kt @@ -98,7 +98,7 @@ class XcfaAdapter(val gsonSupplier: () -> Gson) : TypeAdapter() { lateinit var vars: Set lateinit var xcfaProcedures: Map lateinit var initProcedures: List>>> - var unsafeUnrollUsed: Boolean = false + var unsafeUnrollUsed = false val varsType = object : TypeToken>() {}.type diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt index d4e9fbfdc3..4cce1aa289 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt @@ -34,7 +34,6 @@ constructor( private val procedures: MutableSet = LinkedHashSet(), private val initProcedures: MutableList>>> = ArrayList(), val metaData: MutableMap = LinkedHashMap(), - var unsafeUnrollUsed: Boolean = false, ) { fun getVars(): Set = vars @@ -49,7 +48,6 @@ constructor( globalVars = vars, procedureBuilders = procedures, initProcedureBuilders = initProcedures, - unsafeUnrollUsed = unsafeUnrollUsed, ) } @@ -80,6 +78,7 @@ constructor( private val locs: MutableSet = LinkedHashSet(), private val edges: MutableSet = LinkedHashSet(), val metaData: MutableMap = LinkedHashMap(), + unsafeUnrollUsed: Boolean = false, ) { lateinit var initLoc: XcfaLocation @@ -91,6 +90,9 @@ constructor( var errorLoc: Optional = Optional.empty() private set + var unsafeUnrollUsed: Boolean = unsafeUnrollUsed + private set + lateinit var parent: XcfaBuilder private lateinit var built: XcfaProcedure private lateinit var optimized: XcfaProcedureBuilder @@ -322,6 +324,6 @@ constructor( } fun setUnsafeUnroll() { - parent.unsafeUnrollUsed = true + unsafeUnrollUsed = true } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt index f9500c5ddf..b23e1ee315 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt @@ -26,12 +26,12 @@ class XCFA( val globalVars: Set, // global variables val procedureBuilders: Set = emptySet(), val initProcedureBuilders: List>>> = emptyList(), - val unsafeUnrollUsed: Boolean = false, + var unsafeUnrollUsed: Boolean = false ) { - val pointsToGraph by this.lazyPointsToGraph + private var cachedHash: Int? = null - var cachedHash: Int? = null + val pointsToGraph by this.lazyPointsToGraph var procedures: Set // procedure definitions private set @@ -51,6 +51,7 @@ class XCFA( procedures = procedureBuilders.map { it.build(this) }.toSet() initProcedures = initProcedureBuilders.map { Pair(it.first.build(this), it.second) } + unsafeUnrollUsed = (procedureBuilders + initProcedureBuilders.map { it.first }).any { it.unsafeUnrollUsed } } /** Recreate an existing XCFA by substituting the procedures and initProcedures fields. */ diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaFurtherOptimizer.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaFurtherOptimizer.kt index 09000c6e2b..77652f6a59 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaFurtherOptimizer.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaFurtherOptimizer.kt @@ -15,22 +15,20 @@ */ package hu.bme.mit.theta.xcfa.model -import hu.bme.mit.theta.xcfa.passes.ProcedurePass import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager -fun XCFA.optimizeFurther(passes: List): XCFA { - if (passes.isEmpty()) return this - val passManager = ProcedurePassManager(passes) - val copy: XcfaProcedureBuilder.() -> XcfaProcedureBuilder = { - val newLocs = getLocs().associateWith { it.copy() } +fun XCFA.optimizeFurther(passManager: ProcedurePassManager): XCFA { + if (passManager.passes.isEmpty()) return this + val deepCopy: XcfaProcedure.() -> XcfaProcedureBuilder = { + val newLocs = locs.associateWith { it.copy() } XcfaProcedureBuilder( name = name, manager = passManager, - params = getParams().toMutableList(), - vars = getVars().toMutableSet(), - locs = getLocs().map { newLocs[it]!! }.toMutableSet(), + params = params.toMutableList(), + vars = vars.toMutableSet(), + locs = locs.map { newLocs[it]!! }.toMutableSet(), edges = - getEdges() + edges .map { val source = newLocs[it.source]!! val target = newLocs[it.target]!! @@ -40,10 +38,11 @@ fun XCFA.optimizeFurther(passes: List): XCFA { edge } .toMutableSet(), - metaData = metaData.toMutableMap(), + metaData = mutableMapOf(), + unsafeUnrollUsed = unsafeUnrollUsed, ) - .also { - it.copyMetaLocs( + .also { proc -> + proc.copyMetaLocs( newLocs[initLoc]!!, finalLoc.map { newLocs[it] }, errorLoc.map { newLocs[it] }, @@ -52,9 +51,9 @@ fun XCFA.optimizeFurther(passes: List): XCFA { } val builder = XcfaBuilder(name, globalVars.toMutableSet()) - procedureBuilders.forEach { builder.addProcedure(it.copy()) } - initProcedureBuilders.forEach { (proc, params) -> - val initProc = builder.getProcedures().find { it.name == proc.name } ?: proc.copy() + procedures.forEach { builder.addProcedure(it.deepCopy()) } + initProcedures.forEach { (proc, params) -> + val initProc = builder.getProcedures().find { it.name == proc.name } ?: proc.deepCopy() builder.addEntryPoint(initProc, params) } return builder.build() diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index f9979b3aae..77743c2767 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -18,9 +18,9 @@ package hu.bme.mit.theta.xcfa.passes import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.frontend.ParseContext -open class ProcedurePassManager(vararg passes: List) { +open class ProcedurePassManager(val passes: List>) { - val passes: List> = passes.toList() + constructor(vararg passes: List) : this(passes.toList()) } class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningLogger: Logger) : @@ -99,3 +99,13 @@ class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) : ) class LitmusPasses : ProcedurePassManager() + +class OcExtraPasses : + ProcedurePassManager( + listOf( + AssumeFalseRemovalPass(), + MutexToVarPass(), + AtomicReadsOneWritePass(), + LoopUnrollPass(2), // force loop unroll for BMC + ) + ) From ed702f80a6b262296823fcec8d1f043bb476f945 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Wed, 13 Nov 2024 14:24:27 +0100 Subject: [PATCH 2/8] format --- .../hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt | 2 +- .../java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt | 1 - .../xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt | 5 +++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt index 3e88eb043a..f71aab960e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt @@ -42,7 +42,7 @@ fun getOcChecker( ocConfig.outputConflictClauses, ocConfig.nonPermissiveValidation, ocConfig.autoConflict, - config.outputConfig.acceptUnreliableSafe + config.outputConfig.acceptUnreliableSafe, ) return SafetyChecker { ocChecker.check() } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt index fb13f97b99..53cce44448 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt @@ -46,7 +46,6 @@ import hu.bme.mit.theta.xcfa.cli.params.Refinement.SEQ_ITP import hu.bme.mit.theta.xcfa.cli.params.Search.* import hu.bme.mit.theta.xcfa.cli.runConfig import hu.bme.mit.theta.xcfa.model.XCFA -import hu.bme.mit.theta.xcfa.model.optimizeFurther import hu.bme.mit.theta.xcfa.passes.* import java.nio.file.Paths diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt index b23e1ee315..03126156ed 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt @@ -26,7 +26,7 @@ class XCFA( val globalVars: Set, // global variables val procedureBuilders: Set = emptySet(), val initProcedureBuilders: List>>> = emptyList(), - var unsafeUnrollUsed: Boolean = false + var unsafeUnrollUsed: Boolean = false, ) { private var cachedHash: Int? = null @@ -51,7 +51,8 @@ class XCFA( procedures = procedureBuilders.map { it.build(this) }.toSet() initProcedures = initProcedureBuilders.map { Pair(it.first.build(this), it.second) } - unsafeUnrollUsed = (procedureBuilders + initProcedureBuilders.map { it.first }).any { it.unsafeUnrollUsed } + unsafeUnrollUsed = + (procedureBuilders + initProcedureBuilders.map { it.first }).any { it.unsafeUnrollUsed } } /** Recreate an existing XCFA by substituting the procedures and initProcedures fields. */ From d2d50ba104e9996f35c7651e1966d2ccbd9a6720 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 13 Nov 2024 20:08:59 +0100 Subject: [PATCH 3/8] disable removedeadends because erroneous --- .../theta/xcfa/passes/ProcedurePassManager.kt | 4 +- .../mit/theta/xcfa/passes/RemoveDeadEnds.kt | 104 ++++++++++-------- 2 files changed, 59 insertions(+), 49 deletions(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index 77743c2767..0e624b12d3 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -52,7 +52,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL // trying to inline procedures InlineProceduresPass(parseContext), EmptyEdgeRemovalPass(), - RemoveDeadEnds(), + RemoveDeadEnds(parseContext), EliminateSelfLoops(), ), listOf(StaticCoiPass()), @@ -87,7 +87,7 @@ class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) : listOf( // trying to inline procedures InlineProceduresPass(parseContext), - RemoveDeadEnds(), + RemoveDeadEnds(parseContext), EliminateSelfLoops(), // handling remaining function calls LbePass(parseContext), diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveDeadEnds.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveDeadEnds.kt index 6f575f6c24..cd593d1772 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveDeadEnds.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveDeadEnds.kt @@ -15,64 +15,74 @@ */ package hu.bme.mit.theta.xcfa.passes +import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.xcfa.getFlatLabels import hu.bme.mit.theta.xcfa.model.* import java.util.stream.Collectors -class RemoveDeadEnds : ProcedurePass { +class RemoveDeadEnds(val parseContext: ParseContext) : ProcedurePass { - // TODO: thread start and procedure call should not be dead-end! Use-case: while(1) pthread_create(..); - override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { - val nonDeadEndEdges: MutableSet = LinkedHashSet() - val reachableEdges: MutableSet = LinkedHashSet() - val errorLoc = builder.errorLoc - errorLoc.ifPresent { xcfaLocation: XcfaLocation -> - collectNonDeadEndEdges(xcfaLocation, nonDeadEndEdges) - } - val finalLoc = builder.finalLoc - finalLoc.ifPresent { xcfaLocation: XcfaLocation -> - collectNonDeadEndEdges(xcfaLocation, nonDeadEndEdges) - } + // TODO: thread start and procedure call should not be dead-end! Use-case: while(1) + // pthread_create(..); + override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { + if (parseContext.multiThreading) return builder + val nonDeadEndEdges: MutableSet = LinkedHashSet() + val reachableEdges: MutableSet = LinkedHashSet() + val errorLoc = builder.errorLoc + errorLoc.ifPresent { xcfaLocation: XcfaLocation -> + collectNonDeadEndEdges(xcfaLocation, nonDeadEndEdges) + } + val finalLoc = builder.finalLoc + finalLoc.ifPresent { xcfaLocation: XcfaLocation -> + collectNonDeadEndEdges(xcfaLocation, nonDeadEndEdges) + } - builder.getEdges().filter { it.getFlatLabels().any { it is InvokeLabel || it is StartLabel } }.forEach { - nonDeadEndEdges.add(it) - collectNonDeadEndEdges(it.source, nonDeadEndEdges) - } + builder + .getEdges() + .filter { it.getFlatLabels().any { it is InvokeLabel || it is StartLabel } } + .forEach { + nonDeadEndEdges.add(it) + collectNonDeadEndEdges(it.source, nonDeadEndEdges) + } - filterReachableEdges(builder.initLoc, reachableEdges) - val collect = builder.getEdges().stream().filter { xcfaEdge: XcfaEdge -> - (!nonDeadEndEdges.contains(xcfaEdge) - || !reachableEdges.contains(xcfaEdge)) - }.collect(Collectors.toSet()) - for (edge in collect) { - builder.removeEdge(edge!!) + filterReachableEdges(builder.initLoc, reachableEdges) + val collect = + builder + .getEdges() + .stream() + .filter { xcfaEdge: XcfaEdge -> + (!nonDeadEndEdges.contains(xcfaEdge) || !reachableEdges.contains(xcfaEdge)) } - return builder + .collect(Collectors.toSet()) + for (edge in collect) { + builder.removeEdge(edge!!) } + return builder + } - private fun filterReachableEdges(loc: XcfaLocation, reachableEdges: MutableSet) { - val outgoingEdges: MutableSet = LinkedHashSet(loc.outgoingEdges) - while (outgoingEdges.isNotEmpty()) { - val any = outgoingEdges.stream().findAny() - val outgoingEdge = any.get() - outgoingEdges.remove(outgoingEdge) - if (!reachableEdges.contains(outgoingEdge)) { - reachableEdges.add(outgoingEdge) - outgoingEdges.addAll(outgoingEdge.target.outgoingEdges) - } - } + private fun filterReachableEdges(loc: XcfaLocation, reachableEdges: MutableSet) { + val outgoingEdges: MutableSet = LinkedHashSet(loc.outgoingEdges) + while (outgoingEdges.isNotEmpty()) { + val any = outgoingEdges.stream().findAny() + val outgoingEdge = any.get() + outgoingEdges.remove(outgoingEdge) + if (!reachableEdges.contains(outgoingEdge)) { + reachableEdges.add(outgoingEdge) + outgoingEdges.addAll(outgoingEdge.target.outgoingEdges) + } } + } - private fun collectNonDeadEndEdges(loc: XcfaLocation, nonDeadEndEdges: MutableSet) { - val incomingEdges: MutableSet = LinkedHashSet(loc.incomingEdges) - while (incomingEdges.isNotEmpty()) { - val any = incomingEdges.stream().findAny() - val incomingEdge = any.get() - incomingEdges.remove(incomingEdge) - if (!nonDeadEndEdges.contains(incomingEdge)) { - nonDeadEndEdges.add(incomingEdge) - incomingEdges.addAll(incomingEdge.source.incomingEdges) - } - } + private fun collectNonDeadEndEdges(loc: XcfaLocation, nonDeadEndEdges: MutableSet) { + val incomingEdges: MutableSet = LinkedHashSet(loc.incomingEdges) + while (incomingEdges.isNotEmpty()) { + val any = incomingEdges.stream().findAny() + val incomingEdge = any.get() + incomingEdges.remove(incomingEdge) + if (!nonDeadEndEdges.contains(incomingEdge)) { + nonDeadEndEdges.add(incomingEdge) + incomingEdges.addAll(incomingEdge.source.incomingEdges) + } } + } } From 2e797b9518082b0ce35ff505ba6c466a2101e3a7 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 00:27:56 +0100 Subject: [PATCH 4/8] Added back atomic_begin,_end, and a pass to remove them afterwards. --- .../grammar/expression/ExpressionVisitor.java | 8 ++- .../theta/xcfa/passes/ProcedurePassManager.kt | 1 + .../mit/theta/xcfa/passes/RemoveAtomics.kt | 51 +++++++++++++++++++ 3 files changed, 58 insertions(+), 2 deletions(-) create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index e02516a644..79b5e3ee7b 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -743,6 +743,10 @@ public Expr visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) { @Override public Expr visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) { final var variable = getVar(ctx.Identifier().getText()); + if (atomicVars.contains(variable)) { + preStatements.add(new CCall("__VERIFIER_atomic_begin", List.of(), parseContext)); + postStatements.add(new CCall("__VERIFIER_atomic_end", List.of(), parseContext)); + } return variable.getRef(); } @@ -983,7 +987,7 @@ public Function, Expr> visitPostfixExpressionIncrement( cexpr = new CExpr(expr, parseContext); // no need to truncate here, as left and right side types are the same CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext); - postStatements.add(cAssignment); + postStatements.add(0, cAssignment); functionVisitor.recordMetadata(ctx, cAssignment); functionVisitor.recordMetadata(ctx, cexpr); return primary; @@ -1004,7 +1008,7 @@ public Function, Expr> visitPostfixExpressionDecrement( cexpr = new CExpr(expr, parseContext); // no need to truncate here, as left and right side types are the same CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext); - postStatements.add(cAssignment); + postStatements.add(0, cAssignment); functionVisitor.recordMetadata(ctx, cAssignment); functionVisitor.recordMetadata(ctx, cexpr); return expr; diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index 0e624b12d3..89a0808921 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -70,6 +70,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL UnusedLocRemovalPass(), ), listOf(FetchExecuteWriteback(parseContext)), + listOf(RemoveAtomics()), ) class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) : diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt new file mode 100644 index 0000000000..58ca3bd7ba --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt @@ -0,0 +1,51 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xcfa.passes + +import hu.bme.mit.theta.xcfa.getFlatLabels +import hu.bme.mit.theta.xcfa.model.FenceLabel +import hu.bme.mit.theta.xcfa.model.SequenceLabel +import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder + +class RemoveAtomics : ProcedurePass { + + override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { + for (xcfaEdge in LinkedHashSet(builder.getEdges())) { + val labels = xcfaEdge.getFlatLabels() + val (beginIndex, beginLabel) = + labels + .mapIndexed { i1, i2 -> Pair(i1, i2) } + .firstOrNull { + it.second is FenceLabel && (it.second as FenceLabel).labels.contains("ATOMIC_BEGIN") + } ?: continue + val (endIndex, endLabel) = + labels + .mapIndexed { i1, i2 -> Pair(i1, i2) } + .lastOrNull { + it.second is FenceLabel && (it.second as FenceLabel).labels.contains("ATOMIC_END") + } ?: continue + val newLabels = + labels.subList(0, beginIndex) + + labels.subList(beginIndex + 1, endIndex).filter { + it !is FenceLabel || !it.labels.contains("ATOMIC_") + } + + labels.subList(endIndex + 1, labels.size) + builder.removeEdge(xcfaEdge) + builder.addEdge(xcfaEdge.withLabel(SequenceLabel(newLabels))) + } + return builder + } +} From d2a174f7fbdbbac890751b68625bfce6f77a21d7 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 00:28:14 +0100 Subject: [PATCH 5/8] Fix bug in cif --- .../main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index fe963cb479..d573eae8d0 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -768,7 +768,9 @@ class FrontendXcfaBuilder( xcfaEdge = XcfaEdge(elseEnd, endLoc, metadata = getMetadata(statement)) builder.addEdge(xcfaEdge) } else { - xcfaEdge = XcfaEdge(elseBranch, endLoc, metadata = getMetadata(statement)) + val elseAfterGuard = + buildPostStatement(guard, ParamPack(builder, elseBranch, breakLoc, continueLoc, returnLoc)) + xcfaEdge = XcfaEdge(elseAfterGuard, endLoc, metadata = getMetadata(statement)) builder.addEdge(xcfaEdge) } xcfaEdge = XcfaEdge(mainEnd, endLoc, metadata = getMetadata(statement)) From e02be8980cc10ceea71644f689b0275992559f77 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 00:30:45 +0100 Subject: [PATCH 6/8] Stupid typo fix --- .../src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt index 58ca3bd7ba..f36f8d5ae1 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt @@ -40,7 +40,7 @@ class RemoveAtomics : ProcedurePass { val newLabels = labels.subList(0, beginIndex) + labels.subList(beginIndex + 1, endIndex).filter { - it !is FenceLabel || !it.labels.contains("ATOMIC_") + it !is FenceLabel || !it.labels.any { it.contains("ATOMIC_") } } + labels.subList(endIndex + 1, labels.size) builder.removeEdge(xcfaEdge) From 615d2eee71147c8d18905eae7ae9a3d0b6902424 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 11:35:06 +0100 Subject: [PATCH 7/8] Not removing 'unnecessary' atomics --- .../theta/xcfa/passes/ProcedurePassManager.kt | 1 - .../mit/theta/xcfa/passes/RemoveAtomics.kt | 51 ------------------- 2 files changed, 52 deletions(-) delete mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt index 89a0808921..0e624b12d3 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt @@ -70,7 +70,6 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL UnusedLocRemovalPass(), ), listOf(FetchExecuteWriteback(parseContext)), - listOf(RemoveAtomics()), ) class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) : diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt deleted file mode 100644 index f36f8d5ae1..0000000000 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/RemoveAtomics.kt +++ /dev/null @@ -1,51 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.xcfa.passes - -import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.model.FenceLabel -import hu.bme.mit.theta.xcfa.model.SequenceLabel -import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder - -class RemoveAtomics : ProcedurePass { - - override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { - for (xcfaEdge in LinkedHashSet(builder.getEdges())) { - val labels = xcfaEdge.getFlatLabels() - val (beginIndex, beginLabel) = - labels - .mapIndexed { i1, i2 -> Pair(i1, i2) } - .firstOrNull { - it.second is FenceLabel && (it.second as FenceLabel).labels.contains("ATOMIC_BEGIN") - } ?: continue - val (endIndex, endLabel) = - labels - .mapIndexed { i1, i2 -> Pair(i1, i2) } - .lastOrNull { - it.second is FenceLabel && (it.second as FenceLabel).labels.contains("ATOMIC_END") - } ?: continue - val newLabels = - labels.subList(0, beginIndex) + - labels.subList(beginIndex + 1, endIndex).filter { - it !is FenceLabel || !it.labels.any { it.contains("ATOMIC_") } - } + - labels.subList(endIndex + 1, labels.size) - builder.removeEdge(xcfaEdge) - builder.addEdge(xcfaEdge.withLabel(SequenceLabel(newLabels))) - } - return builder - } -} From b13c1394f1d0aedbb1e4a20fb631ecdcb04761ea Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 14 Nov 2024 13:20:04 +0100 Subject: [PATCH 8/8] fix compile error in test --- .../test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt index d03c92478c..f7604eb9dd 100644 --- a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt +++ b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/passes/PassTests.kt @@ -287,7 +287,12 @@ class PassTests { PassTestData( global = { "x" type Int() init "0" }, passes = - listOf(NormalizePass(), DeterministicPass(), RemoveDeadEnds(), UnusedLocRemovalPass()), + listOf( + NormalizePass(), + DeterministicPass(), + RemoveDeadEnds(parseContext), + UnusedLocRemovalPass(), + ), input = { (init to "L1") { assume("1 == 1") } (init to "L2") { assume("1 == 1") }