From 858270409241a23ef5e673a0fe07187cfe3037cc Mon Sep 17 00:00:00 2001
From: Behzad Safaei <iwia103h@a0221.nhr.fau.de>
Date: Thu, 13 Feb 2025 22:20:21 +0100
Subject: [PATCH] Force write-after-read for AtomicInc nodes

---
 src/pairs/analysis/modules.py            |  8 ++++++++
 src/pairs/transformations/expressions.py | 12 ------------
 2 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/src/pairs/analysis/modules.py b/src/pairs/analysis/modules.py
index 24ab2be..d5311bc 100644
--- a/src/pairs/analysis/modules.py
+++ b/src/pairs/analysis/modules.py
@@ -39,8 +39,16 @@ class FetchModulesReferences(Visitor):
             self.visit(ast_node.capacity)
 
     def visit_AtomicInc(self, ast_node):
+        visit_once = self.visit_nodes_once
+        self.visit_nodes_once = False
+        # Force write after read for the same node (visited twice)
+        self.writing = False
+        self.visit(ast_node.elem)
         self.writing = True
         self.visit(ast_node.elem)
+        self.visit_nodes_once = visit_once
+
+
         self.writing = False
         self.visit(ast_node.value)
 
diff --git a/src/pairs/transformations/expressions.py b/src/pairs/transformations/expressions.py
index 1e1ab5e..750bce6 100644
--- a/src/pairs/transformations/expressions.py
+++ b/src/pairs/transformations/expressions.py
@@ -194,18 +194,6 @@ class AddExpressionDeclarations(Mutator):
 
         return ast_node
     
-    def mutate_AtomicInc(self, ast_node):
-        self.writing = True
-        ast_node.elem = self.mutate(ast_node.elem)
-        self.writing = False
-        ast_node.value = self.mutate(ast_node.value)
-        atomic_inc_id = id(ast_node)
-        if atomic_inc_id not in self.declared_exprs and atomic_inc_id not in self.params:
-            self.push_decl(Decl(ast_node.sim, ast_node))
-            self.declared_exprs.append(atomic_inc_id)
-
-        return ast_node
-
     def mutate_Block(self, ast_node):
         block_id = id(ast_node)
         self.decls[block_id] = []
-- 
GitLab