diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaFurtherOptimizer.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaFurtherOptimizer.kt index 9a70626567..ba88ef04f6 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaFurtherOptimizer.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaFurtherOptimizer.kt @@ -25,16 +25,33 @@ 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() } XcfaProcedureBuilder( name = name, manager = passManager, params = getParams().toMutableList(), vars = getVars().toMutableSet(), - locs = getLocs().toMutableSet(), - edges = getEdges().toMutableSet(), + locs = getLocs().map { newLocs[it]!! }.toMutableSet(), + edges = + getEdges() + .map { + val source = newLocs[it.source]!! + val target = newLocs[it.target]!! + val edge = it.withSource(source).withTarget(target) + source.outgoingEdges.add(edge) + target.incomingEdges.add(edge) + edge + } + .toMutableSet(), metaData = metaData.toMutableMap(), ) - .also { it.copyMetaLocs(this) } + .also { + it.copyMetaLocs( + newLocs[initLoc]!!, + finalLoc.map { newLocs[it] }, + errorLoc.map { newLocs[it] }, + ) + } } val builder = XcfaBuilder(name, globalVars.toMutableSet()) 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 7969e42f50..d4e9fbfdc3 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 @@ -241,13 +241,17 @@ constructor( } } - fun copyMetaLocs(from: XcfaProcedureBuilder) { + fun copyMetaLocs( + initLoc: XcfaLocation, + finalLoc: Optional, + errorLoc: Optional, + ) { check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - initLoc = from.initLoc - finalLoc = from.finalLoc - errorLoc = from.errorLoc + this.initLoc = initLoc + this.finalLoc = finalLoc + this.errorLoc = errorLoc } fun addEdge(toAdd: XcfaEdge) {