From be488035173cc8146913c4d70ae02a7e1a157a63 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 7 Nov 2024 01:02:01 +0100 Subject: [PATCH 1/2] single assume fix --- .../theta/xcfa/analysis/oc/XcfaOcChecker.kt | 3 +- .../java/hu/bme/mit/theta/xcfa/model/XCFA.kt | 2 ++ .../theta/xcfa/passes/EmptyEdgeRemovalPass.kt | 28 +++++++++++++++---- .../mit/theta/xcfa/passes/UnusedVarPass.kt | 5 +++- 4 files changed, 31 insertions(+), 7 deletions(-) diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt index c9cb77d55d..4645720aae 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt @@ -303,7 +303,7 @@ 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 +320,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 index 9e90b22d57..107af4e127 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 43c29685ee..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 @@ -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,31 +25,48 @@ 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() } @@ -56,5 +74,5 @@ class EmptyEdgeRemovalPass : ProcedurePass { 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 index 13e3e6d808..c8c36903f3 100644 --- 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( From ec3b08e4d3857ca4afd40d94b1a596981c6d4ba7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Thu, 7 Nov 2024 01:32:11 +0100 Subject: [PATCH 2/2] single assume fix --- build.gradle.kts | 2 +- .../java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/build.gradle.kts b/build.gradle.kts index e5be05ea9b..90e1684143 100644 --- 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/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt index 4645720aae..884fa69d17 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt +++ b/subprojects/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.threadVar(pid) !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) {