From ef55998b778813ddc8a9d6e0b89acadd745d3f2e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Mon, 6 Nov 2023 15:54:07 +0100 Subject: [PATCH] get vars assignstmt fix --- .../xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt index 799d6bfd1b..468b8a5c6c 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt @@ -111,6 +111,9 @@ private fun List.mergeAndCollect(): VarAccessMap = this.fold(mapOf (acc.keys + next.keys).associateWith { acc[it].merge(next[it]) } } +private operator fun VarAccessMap?.plus(other: VarAccessMap?): VarAccessMap = + listOfNotNull(this, other).mergeAndCollect() + /** * The list of mutexes acquired by the label. */ @@ -150,7 +153,7 @@ fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { is StmtLabel -> { when (stmt) { is HavocStmt<*> -> mapOf(stmt.varDecl to WRITE) - is AssignStmt<*> -> StmtUtils.getVars(stmt).associateWith { READ } + mapOf(stmt.varDecl to WRITE) + is AssignStmt<*> -> ExprUtils.getVars(stmt.expr).associateWith { READ } + mapOf(stmt.varDecl to WRITE) else -> StmtUtils.getVars(stmt).associateWith { READ } } } @@ -158,9 +161,9 @@ fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { is NondetLabel -> labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() is SequenceLabel -> labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() is InvokeLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } + is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } + mapOf(pidVar to READ) is JoinLabel -> mapOf(pidVar to READ) is ReadLabel -> mapOf(global to READ, local to READ) - is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } + mapOf(pidVar to READ) is WriteLabel -> mapOf(global to WRITE, local to WRITE) else -> emptyMap() }