xcfa pass phases

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<XcfaGlobalVar> = LinkedHashSet(),
     private val procedures: MutableSet<XcfaProcedureBuilder> = LinkedHashSet(),
     private val initProcedures: MutableList<Pair<XcfaProcedureBuilder, List<Expr<*>>>> = ArrayList(),
-    val metaData: MutableMap<String, Any> = LinkedHashMap()) {
+    val metaData: MutableMap<String, Any> = LinkedHashMap()
+) {
 
     fun getVars(): Set<XcfaGlobalVar> = vars
     fun getProcedures(): Set<XcfaProcedureBuilder> = 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<Pair<VarDecl<*>, ParamDirection>> = ArrayList(),
     private val vars: MutableSet<VarDecl<*>> = LinkedHashSet(),
     private val locs: MutableSet<XcfaLocation> = LinkedHashSet(),
@@ -78,8 +79,10 @@ class XcfaProcedureBuilder @JvmOverloads constructor(
     var errorLoc: Optional<XcfaLocation> = 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<Pair<VarDecl<*>, ParamDirection>> = if (this::optimized.isInitialized) optimized.params else params
     fun getVars(): Set<VarDecl<*>> = if (this::optimized.isInitialized) optimized.vars else vars
     fun getLocs(): Set<XcfaLocation> = 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()

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<XcfaProcedure> =                                // procedure definitions
-        procedureBuilders.map { it.build(this) }.toSet()
+    var procedures: Set<XcfaProcedure>                                // procedure definitions
         private set
-    var initProcedures: List<Pair<XcfaProcedure, List<Expr<*>>>> =      // procedure names and parameter assignments
-        initProcedureBuilders.map { Pair(it.first.build(this), it.second) }
+
+    var initProcedures: List<Pair<XcfaProcedure, List<Expr<*>>>>      // 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<XcfaProcedure>,
-        initProcedures: List<Pair<XcfaProcedure, List<Expr<*>>>>
-    ): XCFA {
+    fun recreate(procedures: Set<XcfaProcedure>, initProcedures: List<Pair<XcfaProcedure, List<Expr<*>>>>): XCFA {
         this.procedures = procedures
         this.initProcedures = initProcedures
         return this

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/InlineProceduresPass.kt

@@ -34,30 +34,29 @@ 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])) {
                             foundOne = true
                             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<XcfaLocation, XcfaLocation> = 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)
     }
 }

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<ProcedurePass>)
+open class ProcedurePassManager(vararg passes: List<ProcedurePass>) {
 
-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<List<ProcedurePass>> = 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

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)