From 8cad4c575db7fe6a3228adf7d3d05cdde002322d Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Wed, 6 Nov 2024 23:20:04 +0100
Subject: [PATCH] Instead of keeping metadata, combine it with meaningful edges

---
 .../java/hu/bme/mit/theta/xcfa/model/XCFA.kt    |  2 ++
 .../theta/xcfa/passes/EmptyEdgeRemovalPass.kt   | 17 ++++++++++++-----
 2 files changed, 14 insertions(+), 5 deletions(-)

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 37340afece..8873df6632 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
@@ -144,6 +144,8 @@ data class XcfaEdge(
   fun withTarget(target: XcfaLocation): XcfaEdge = XcfaEdge(source, target, label, metadata)
 
   fun withSource(source: XcfaLocation): XcfaEdge = XcfaEdge(source, target, label, metadata)
+
+  fun withMetadata(metadata: MetaData): XcfaEdge = XcfaEdge(source, target, label, metadata)
 }
 
 data class XcfaGlobalVar
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EmptyEdgeRemovalPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EmptyEdgeRemovalPass.kt
index 4dffafd1f0..dd9adf3563 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EmptyEdgeRemovalPass.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/EmptyEdgeRemovalPass.kt
@@ -33,20 +33,27 @@ class EmptyEdgeRemovalPass : ProcedurePass {
             !it.target.error &&
             !it.target.final &&
             !it.source.initial &&
-            (it.source.outgoingEdges.size == 1 || it.target.incomingEdges.size == 1) &&
-            it.metadata is EmptyMetaData
+            (it.source.outgoingEdges.size == 1 || it.target.incomingEdges.size == 1)
         } ?: return builder
       val collapseBefore = edge.source.outgoingEdges.size == 1
       builder.removeEdge(edge)
       if (collapseBefore) {
         val incomingEdges = edge.source.incomingEdges.toList()
         incomingEdges.forEach { builder.removeEdge(it) }
-        incomingEdges.forEach { builder.addEdge(it.withTarget(edge.target)) }
+        incomingEdges.forEach {
+          builder.addEdge(
+            it.withTarget(edge.target).withMetadata(it.metadata.combine(edge.metadata))
+          )
+        }
         builder.removeLoc(edge.source)
       } else {
         val outgoingEdges = edge.target.outgoingEdges.toList()
         outgoingEdges.forEach { builder.removeEdge(it) }
-        outgoingEdges.forEach { builder.addEdge(it.withSource(edge.source)) }
+        outgoingEdges.forEach {
+          builder.addEdge(
+            it.withSource(edge.source).withMetadata(edge.metadata.combine(it.metadata))
+          )
+        }
         builder.removeLoc(edge.target)
       }
     }
@@ -67,5 +74,5 @@ class EmptyEdgeRemovalPass : ProcedurePass {
       is NopLabel -> true
       is StmtLabel -> stmt == Assume(True())
       else -> false
-    }.and(metadata is EmptyMetaData)
+    }
 }