Merge pull request #316 from csanadtelbisz/xcfa-oc

Minor Xcfa pass & oc checker fixes
ftsrg · Nov 8, 2024 · c85c711 · c85c711
2 parents e1a443a + ec3b08e
commit c85c711
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 8 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.7.0"
+    version = "6.7.1"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt
@@ -303,7 +303,9 @@ class XcfaOcChecker(
                     val condWithConsts = stmt.cond.with(consts)
                     val asAssign =
                       consts.size == 1 &&
-                        consts.keys.first().let { it is VarDecl<*> && it !in lastWrites }
+                        consts.keys.first().let {
+                          it is VarDecl<*> && it.threadVar(pid) !in lastWrites
+                        }
                     if (edge.source.outgoingEdges.size > 1 || !asAssign) {
                       guard = guard + condWithConsts
                       if (firstLabel) {
@@ -320,6 +322,7 @@ class XcfaOcChecker(
 
                   is HavocStmt<*> -> {
                     last = event(stmt.varDecl, EventType.WRITE)
+                    last.first().assignment = True()
                   }
 
                   is MemoryAssignStmt<*, *, *> -> {

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
@@ -16,6 +16,7 @@
 package hu.bme.mit.theta.xcfa.passes
 
 import hu.bme.mit.theta.core.stmt.Stmts.Assume
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.False
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
 import hu.bme.mit.theta.xcfa.model.*
 
@@ -24,37 +25,54 @@ class EmptyEdgeRemovalPass : ProcedurePass {
 
   override fun run(builder: XcfaProcedureBuilder): XcfaProcedureBuilder {
     while (true) {
+      builder.getEdges().filter { it.label.isSureStuck() }.forEach { builder.removeEdge(it) }
+
       val edge =
         builder.getEdges().find {
           it.label.isNop() &&
             !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)
       }
     }
   }
 
+  private fun XcfaLabel.isSureStuck(): Boolean =
+    when (this) {
+      is SequenceLabel -> labels.any { it.isSureStuck() }
+      is NondetLabel -> labels.all { it.isSureStuck() }
+      is StmtLabel -> stmt == Assume(False())
+      else -> false
+    }
+
   private fun XcfaLabel.isNop(): Boolean =
     when (this) {
       is NondetLabel -> labels.all { it.isNop() }
       is SequenceLabel -> labels.all { it.isNop() }
       is NopLabel -> true
       is StmtLabel -> stmt == Assume(True())
       else -> false
-    }.and(metadata is EmptyMetaData)
+    }
 }
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/UnusedVarPass.kt
@@ -61,7 +61,10 @@ class UnusedVarPass(private val uniqueWarningLogger: Logger) : ProcedurePass {
     } while (lastEdges != edges)
 
     val allVars =
-      Sets.union(builder.getVars(), builder.parent.getVars().map { it.wrappedVar }.toSet())
+      Sets.union(
+        builder.parent.getProcedures().flatMap { it.getVars() }.toSet(),
+        builder.parent.getVars().map { it.wrappedVar }.toSet(),
+      )
     val varsAndParams = Sets.union(allVars, builder.getParams().map { it.first }.toSet())
     if (!varsAndParams.containsAll(usedVars)) {
       uniqueWarningLogger.writeln(