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 a092ef61a9..4c9d1d3e15 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 @@ -30,7 +30,8 @@ class XcfaBuilder @JvmOverloads constructor( private val vars: MutableSet = LinkedHashSet(), private val procedures: MutableSet = LinkedHashSet(), private val initProcedures: MutableList>>> = ArrayList(), - val metaData: MutableMap = LinkedHashMap()) { + val metaData: MutableMap = LinkedHashMap() +) { fun getVars(): Set = vars fun getProcedures(): Set = procedures @@ -63,7 +64,7 @@ class XcfaBuilder @JvmOverloads constructor( @XcfaDsl class XcfaProcedureBuilder @JvmOverloads constructor( var name: String, - private val manager: ProcedurePassManager, + val manager: ProcedurePassManager, private val params: MutableList, ParamDirection>> = ArrayList(), private val vars: MutableSet> = LinkedHashSet(), private val locs: MutableSet = LinkedHashSet(), @@ -78,8 +79,10 @@ class XcfaProcedureBuilder @JvmOverloads constructor( var errorLoc: Optional = Optional.empty() private set lateinit var parent: XcfaBuilder - private lateinit var optimized: XcfaProcedureBuilder private lateinit var built: XcfaProcedure + private lateinit var optimized: XcfaProcedureBuilder + private lateinit var partlyOptimized: XcfaProcedureBuilder + private var lastOptimized: Int = -1 fun getParams(): List, ParamDirection>> = if (this::optimized.isInitialized) optimized.params else params fun getVars(): Set> = if (this::optimized.isInitialized) optimized.vars else vars fun getLocs(): Set = if (this::optimized.isInitialized) optimized.locs else locs @@ -88,13 +91,29 @@ class XcfaProcedureBuilder @JvmOverloads constructor( fun optimize() { if (!this::optimized.isInitialized) { var that = this - for (pass in manager.passes) { + for (pass in manager.passes.flatten()) { that = pass.run(that) } optimized = that } } + fun optimize(phase: Int): Boolean { // true, if optimization is finished (no more phases to execute) + if (this::optimized.isInitialized || phase >= manager.passes.size) return true + if (phase <= lastOptimized) return lastOptimized >= manager.passes.size - 1 + check(phase == lastOptimized + 1) { "Wrong optimization phase!" } + + var that = if (this::partlyOptimized.isInitialized) partlyOptimized else this + for (pass in manager.passes[phase]) { + that = pass.run(that) + } + + partlyOptimized = that + lastOptimized = phase + if (phase >= manager.passes.size - 1) optimized = that + return phase >= manager.passes.size - 1 + } + fun build(parent: XCFA): XcfaProcedure { if (this::built.isInitialized) return built; if (!this::optimized.isInitialized) optimize() 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 2f3f367246..0916e1e5ca 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 @@ -30,19 +30,29 @@ class XCFA( var cachedHash: Int? = null - var procedures: Set = // procedure definitions - procedureBuilders.map { it.build(this) }.toSet() + var procedures: Set // procedure definitions private set - var initProcedures: List>>> = // procedure names and parameter assignments - initProcedureBuilders.map { Pair(it.first.build(this), it.second) } + + var initProcedures: List>>> // procedure names and parameter assignments private set + init { + var phase = 0 + do { + var ready = true + procedureBuilders.forEach { ready = it.optimize(phase) && ready } + initProcedureBuilders.forEach { ready = it.first.optimize(phase) && ready } + phase++ + } while (!ready) + + procedures = procedureBuilders.map { it.build(this) }.toSet() + initProcedures = initProcedureBuilders.map { Pair(it.first.build(this), it.second) } + } + /** * Recreate an existing XCFA by substituting the procedures and initProcedures fields. */ - fun recreate(procedures: Set, - initProcedures: List>>> - ): XCFA { + fun recreate(procedures: Set, initProcedures: List>>>): XCFA { this.procedures = procedures this.initProcedures = initProcedures return this diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt index 3a42d18c37..5cfbfa728c 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt @@ -34,19 +34,16 @@ class InlineProceduresPass(val parseContext: ParseContext) : ProcedurePass { override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { if (!builder.canInline()) return builder checkNotNull(builder.metaData["deterministic"]) - check( - builder.metaData["inlined"] == null) { "Recursive programs are not supported by inlining." } + check(builder.metaData["inlined"] == null) { "Recursive programs are not supported by inlining." } builder.metaData["inlined"] = Unit while (true) { var foundOne = false for (edge in ArrayList(builder.getEdges())) { val pred: (XcfaLabel) -> Boolean = { it -> - it is InvokeLabel && builder.parent.getProcedures() - .any { p -> p.name == it.name } + it is InvokeLabel && builder.parent.getProcedures().any { p -> p.name == it.name } } val edges = edge.splitIf(pred) - if (edges.size > 1 || (edges.size == 1 && pred( - (edges[0].label as SequenceLabel).labels[0]))) { + if (edges.size > 1 || (edges.size == 1 && pred((edges[0].label as SequenceLabel).labels[0]))) { builder.removeEdge(edge) edges.forEach { if (pred((it.label as SequenceLabel).labels[0])) { @@ -54,10 +51,12 @@ class InlineProceduresPass(val parseContext: ParseContext) : ProcedurePass { val source = it.source val target = it.target val invokeLabel: InvokeLabel = it.label.labels[0] as InvokeLabel - val procedure = builder.parent.getProcedures() - .find { p -> p.name == invokeLabel.name } + val procedure = builder.parent.getProcedures().find { p -> p.name == invokeLabel.name } checkNotNull(procedure) - procedure.optimize() + val inlineIndex = builder.manager.passes.indexOfFirst { phase -> + phase.any { pass -> pass is InlineProceduresPass } + } + procedure.optimize(inlineIndex) val newLocs: MutableMap = LinkedHashMap() procedure.getLocs().forEach { newLocs.put(it, it.inlinedCopy()) } @@ -91,8 +90,7 @@ class InlineProceduresPass(val parseContext: ParseContext) : ProcedurePass { val finalLoc = procedure.finalLoc val errorLoc = procedure.errorLoc - builder.addEdge( - XcfaEdge(source, checkNotNull(newLocs[initLoc]), SequenceLabel(inStmts))) + builder.addEdge(XcfaEdge(source, checkNotNull(newLocs[initLoc]), SequenceLabel(inStmts))) if (finalLoc.isPresent) builder.addEdge(XcfaEdge(checkNotNull(newLocs[finalLoc.get()]), target, SequenceLabel(outStmts))) @@ -116,7 +114,6 @@ class InlineProceduresPass(val parseContext: ParseContext) : ProcedurePass { } private fun XcfaLocation.inlinedCopy(): XcfaLocation { - return copy(name + XcfaLocation.uniqueCounter(), initial = false, final = false, - error = false) + return copy(name + XcfaLocation.uniqueCounter(), initial = false, final = false, error = false) } } \ No newline at end of file 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 b1ba9c758d..dc457d87cd 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,38 +18,48 @@ package hu.bme.mit.theta.xcfa.passes import hu.bme.mit.theta.frontend.ParseContext -open class ProcedurePassManager(val passes: List) +open class ProcedurePassManager(vararg passes: List) { -class CPasses(checkOverflow: Boolean, parseContext: ParseContext) : ProcedurePassManager(listOf( - // formatting - NormalizePass(parseContext), - DeterministicPass(parseContext), - // removing redundant elements - EmptyEdgeRemovalPass(parseContext), - UnusedLocRemovalPass(parseContext), - // handling intrinsics - ErrorLocationPass(checkOverflow, parseContext), - FinalLocationPass(checkOverflow, parseContext), - SvCompIntrinsicsPass(parseContext), - FpFunctionsToExprsPass(parseContext), - CLibraryFunctionsPass(parseContext), - // optimizing -// UnusedWriteRemovalPass(), - SimplifyExprsPass(parseContext), - LoopUnrollPass(), - // trying to inline procedures - InlineProceduresPass(parseContext), - RemoveDeadEnds(parseContext), - EliminateSelfLoops(parseContext), - // handling remaining function calls - NondetFunctionPass(parseContext), - LbePass(parseContext), - NormalizePass(parseContext), // needed after lbe, TODO - DeterministicPass(parseContext), // needed after lbe, TODO - HavocPromotionAndRange(parseContext), - // Final cleanup - UnusedVarPass(parseContext), -)) + val passes: List> = passes.toList() +} + +class CPasses(checkOverflow: Boolean, parseContext: ParseContext) : ProcedurePassManager( + listOf( + // formatting + NormalizePass(parseContext), + DeterministicPass(parseContext), + // removing redundant elements + EmptyEdgeRemovalPass(parseContext), + UnusedLocRemovalPass(parseContext), + // handling intrinsics + ErrorLocationPass(checkOverflow, parseContext), + FinalLocationPass(checkOverflow, parseContext), + SvCompIntrinsicsPass(parseContext), + FpFunctionsToExprsPass(parseContext), + CLibraryFunctionsPass(parseContext), + ), + listOf( + // optimizing + SimplifyExprsPass(parseContext), + LoopUnrollPass(), + ), + listOf( + // trying to inline procedures + InlineProceduresPass(parseContext), + RemoveDeadEnds(parseContext), + EliminateSelfLoops(parseContext), + ), + listOf( + // handling remaining function calls + NondetFunctionPass(parseContext), + LbePass(parseContext), + NormalizePass(parseContext), // needed after lbe, TODO + DeterministicPass(parseContext), // needed after lbe, TODO + HavocPromotionAndRange(parseContext), + // Final cleanup + UnusedVarPass(parseContext), + ) +) class ChcPasses : ProcedurePassManager(listOf(/* // formatting diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt index a53a57b815..2f1d5c3540 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt @@ -96,7 +96,6 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass { } val unusedVars = xcfaBuilder.getVars().map { it.wrappedVar } union builder.getVars() subtract usedVars subtract builder.getParams().map { it.first }.toSet() - System.err.println("Unused vars: $unusedVars") xcfaBuilder.getProcedures().forEach { b -> b.getEdges().toList().forEach { edge -> val newLabel = edge.label.removeUnusedWrites(unusedVars) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedWriteRemovalPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedWriteRemovalPass.kt deleted file mode 100644 index f9a134aed2..0000000000 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedWriteRemovalPass.kt +++ /dev/null @@ -1,51 +0,0 @@ -/* - * Copyright 2023 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.core.decl.VarDecl -import hu.bme.mit.theta.core.stmt.AssignStmt -import hu.bme.mit.theta.core.stmt.HavocStmt -import hu.bme.mit.theta.xcfa.collectVarsWithAccessType -import hu.bme.mit.theta.xcfa.isRead -import hu.bme.mit.theta.xcfa.model.* - -/** - * Remove unused writes from the program. - * Requires the ProcedureBuilder to be `deterministic` (@see DeterministicPass) - */ -class UnusedWriteRemovalPass : ProcedurePass { - - override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder { - checkNotNull(builder.metaData["deterministic"]) - - val usedVars = mutableSetOf>() - builder.getEdges().forEach { - it.label.collectVarsWithAccessType().forEach { (varDecl, access) -> - if (access.isRead) usedVars.add(varDecl) - } - } - val unusedVars = builder.getVars() subtract usedVars subtract builder.getParams().map { it.first }.toSet() - - builder.getEdges().toList().forEach { edge -> - val newLabel = edge.label.removeUnusedWrites(unusedVars) - builder.removeEdge(edge) - builder.addEdge(edge.withLabel(newLabel)) - } - - return builder - } -} \ No newline at end of file