mcm fix

csanadtelbisz · Jan 15, 2025 · 499ac17 · 499ac17
1 parent 35f2d5f
commit 499ac17
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 21 deletions.
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
@@ -79,9 +79,9 @@ class XcfaOcChecker(
   private val events = mutableMapOf<VarDecl<*>, MutableMap<Int, MutableList<E>>>()
   private val violations = mutableListOf<Violation>() // OR!
   private val branchingConditions = mutableListOf<Expr<BoolType>>()
-  private val pos = mutableListOf<R>()
-  private val rfs = mutableMapOf<VarDecl<*>, MutableSet<R>>()
-  private val wss = mutableMapOf<VarDecl<*>, MutableSet<R>>()
+  private var pos = mutableListOf<R>()
+  private var rfs = mutableMapOf<VarDecl<*>, MutableSet<R>>()
+  private var wss = mutableMapOf<VarDecl<*>, MutableSet<R>>()
 
   private val ocChecker: OcChecker<E> =
     if (conflictInput == null) decisionProcedure.checker()
@@ -102,12 +102,9 @@ class XcfaOcChecker(
         xcfa.initProcedures.forEach { ThreadProcessor(Thread(procedure = it.first)).process() }
         addCrossThreadRelations()
         memoryModel.filter(pos, rfs, wss).let { (filteredPos, filteredRfs, filteredWss) ->
-          pos.clear()
-          pos.addAll(filteredPos)
-          rfs.clear()
-          filteredRfs.forEach { (k, v) -> rfs[k] = v.toMutableSet() }
-          wss.clear()
-          filteredWss.forEach { (k, v) -> wss[k] = v.toMutableSet() }
+          pos = filteredPos
+          rfs = filteredRfs
+          wss = filteredWss
         }
         if (!addToSolver(ocChecker.solver)) return@let SafetyResult.safe(EmptyProof.getInstance())
 

diff --git a/...-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcMemoryConsistencyModel.kt b/...-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcMemoryConsistencyModel.kt
@@ -21,28 +21,36 @@ import hu.bme.mit.theta.core.decl.VarDecl
 
 internal fun interface MemoryConsistencyModelFilter {
   operator fun invoke(
-    pos: List<R>,
-    rfs: Map<VarDecl<*>, Set<R>>,
-    wss: Map<VarDecl<*>, Set<R>>,
-  ): Triple<List<R>, Map<VarDecl<*>, Set<R>>, Map<VarDecl<*>, Set<R>>>
+    pos: MutableList<R>,
+    rfs: MutableMap<VarDecl<*>, MutableSet<R>>,
+    wss: MutableMap<VarDecl<*>, MutableSet<R>>,
+  ): Triple<
+    MutableList<R>,
+    MutableMap<VarDecl<*>, MutableSet<R>>,
+    MutableMap<VarDecl<*>, MutableSet<R>>,
+  >
 }
 
 @Suppress("unused")
 enum class XcfaOcMemoryConsistencyModel(internal val filter: MemoryConsistencyModelFilter) {
   SC({ pos, rfs, wss -> Triple(pos, rfs, wss) }),
-  WSC({ pos, rfs, _ -> Triple(pos, rfs, mapOf()) }),
+  WSC({ pos, rfs, _ -> Triple(pos, rfs, mutableMapOf()) }),
   TSO({ pos, rfs, wss ->
     val newPos =
-      pos.filter {
-        !(it.from.const.varDecl != it.to.const.varDecl &&
-          it.from.type == WRITE &&
-          it.to.type == READ)
-      }
+      pos
+        .filter {
+          !(it.from.const.varDecl != it.to.const.varDecl &&
+            it.from.type == WRITE &&
+            it.to.type == READ)
+        }
+        .toMutableList()
     Triple(newPos, rfs, wss)
   }),
   PSO({ pos, rfs, wss ->
     val newPos =
-      pos.filter { !(it.from.const.varDecl != it.to.const.varDecl && it.from.type == WRITE) }
+      pos
+        .filter { !(it.from.const.varDecl != it.to.const.varDecl && it.from.type == WRITE) }
+        .toMutableList()
     Triple(newPos, rfs, wss)
   }),
 }
diff --git a/...jects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt b/...jects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.