disable removedeadends because erroneous

ftsrg · Nov 13, 2024 · d2d50ba · d2d50ba
1 parent ed702f8
commit d2d50ba
Show file tree

Hide file tree

Showing 2 changed files with 59 additions and 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
@@ -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
@@ -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<XcfaEdge> = LinkedHashSet()
-        val reachableEdges: MutableSet<XcfaEdge> = 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<XcfaEdge> = LinkedHashSet()
+    val reachableEdges: MutableSet<XcfaEdge> = 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<XcfaEdge>) {
-        val outgoingEdges: MutableSet<XcfaEdge> = 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<XcfaEdge>) {
+    val outgoingEdges: MutableSet<XcfaEdge> = 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<XcfaEdge>) {
-        val incomingEdges: MutableSet<XcfaEdge> = 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<XcfaEdge>) {
+    val incomingEdges: MutableSet<XcfaEdge> = 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)
+      }
     }
+  }
 }