Instead of keeping metadata, combine it with meaningful edges

ftsrg · Nov 6, 2024 · 8cad4c5 · 8cad4c5
1 parent c362fd6
commit 8cad4c5
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 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
@@ -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
@@ -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)
+    }
 }