From a97d7458c632e850c3fc7ff36513626f689fae55 Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 18 Apr 2024 11:01:22 +0200
Subject: [PATCH] Fixed error in SyntacticContextAnalysis when loop iterations
 are empty (cherry-picked from alias branch).

---
 .../analysis/SyntacticContextAnalysis.java    | 45 +++++++++----------
 1 file changed, 20 insertions(+), 25 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java
index 4e5393c52f..ae38affaa3 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java
@@ -10,7 +10,6 @@
 import com.google.common.collect.Iterables;
 
 import java.util.HashMap;
-import java.util.List;
 import java.util.Map;
 import java.util.Stack;
 import java.util.function.Predicate;
@@ -100,9 +99,6 @@ public String toString() {
         }
     }
 
-    // We use this enum to track loop nesting
-    private enum LoopMarkerTypes {START, INC, END}
-
     // ============================================================================
 
     private final Map<Event, Info> infoMap = new HashMap<>();
@@ -138,7 +134,7 @@ private void run(Program program) {
     }
 
     private void run(Thread thread, LoopAnalysis loops) {
-        final Map<Event, LoopMarkerTypes> loopMarkerTypesMap = getLoopMarkerTypesMap(thread, loops);
+        final Map<Event, LoopAnalysis.LoopIterationInfo> loopMarkerTypesMap = getLoopMarkerTypesMap(thread, loops);
 
         Stack<Context> curContextStack = new Stack<>();
         curContextStack.push(new ThreadContext(thread));
@@ -161,32 +157,31 @@ private void run(Thread thread, LoopAnalysis loops) {
                 } while (!topCallCtx.funCallMarker.getFunctionName().equals(retMarker.getFunctionName()));
             }
 
-            if (loopMarkerTypesMap.containsKey(ev)) {
-                switch (loopMarkerTypesMap.get(ev)) {
-                    case START -> curContextStack.push(new LoopContext(ev, 1));
-                    case INC -> {
-                        assert curContextStack.peek() instanceof LoopContext;
-                        int iterNum = ((LoopContext) curContextStack.pop()).iterationNumber;
-                        curContextStack.push(new LoopContext(ev, iterNum + 1));
-                    }
-                    case END -> {
-                        assert curContextStack.peek() instanceof LoopContext;
-                        curContextStack.pop();
-                    }
+            final LoopAnalysis.LoopIterationInfo iteration = loopMarkerTypesMap.get(ev);
+            if (iteration != null) {
+                final boolean start = ev == iteration.getIterationStart();
+                final boolean end = ev == iteration.getIterationEnd();
+                assert start || end;
+                if (start) {
+                    curContextStack.push(new LoopContext(ev, iteration.getIterationNumber()));
+                }
+                if (end) {
+                    assert curContextStack.peek() instanceof LoopContext c &&
+                            c.loopMarker == iteration.getIterationStart() &&
+                            c.iterationNumber == iteration.getIterationNumber();
+                    curContextStack.pop();
                 }
             }
         }
     }
 
-    private Map<Event, LoopMarkerTypes> getLoopMarkerTypesMap(Thread thread, LoopAnalysis loopAnalysis) {
-        final Map<Event, LoopMarkerTypes> loopMarkerTypesMap = new HashMap<>();
+    private Map<Event, LoopAnalysis.LoopIterationInfo> getLoopMarkerTypesMap(Thread thread, LoopAnalysis loopAnalysis) {
+        final Map<Event, LoopAnalysis.LoopIterationInfo> loopMarkerTypesMap = new HashMap<>();
         for (LoopAnalysis.LoopInfo loop : loopAnalysis.getLoopsOfFunction(thread)) {
-            final List<LoopAnalysis.LoopIterationInfo> iterations = loop.iterations();
-
-            loopMarkerTypesMap.put(iterations.get(0).getIterationStart(), LoopMarkerTypes.START);
-            iterations.subList(1, iterations.size())
-                    .forEach(iter -> loopMarkerTypesMap.put(iter.getIterationStart(), LoopMarkerTypes.INC));
-            loopMarkerTypesMap.put(iterations.get(iterations.size() - 1).getIterationEnd(), LoopMarkerTypes.END);
+            for (LoopAnalysis.LoopIterationInfo iteration : loop.iterations()) {
+                loopMarkerTypesMap.put(iteration.getIterationStart(), iteration);
+                loopMarkerTypesMap.put(iteration.getIterationEnd(), iteration);
+            }
         }
         return loopMarkerTypesMap;
     }